conference paper published yes Jan Kretinsky author 44CEF464-F248-11E8-B48F-1D18A9856A870000-0002-8122-2881 Tobias Meggendorfer author b21b0c15-30a2-11eb-80dc-f13ca25802e10000-0002-1712-2165 Maximilian Prokop author Sabine Rieder author KrCh department CAV: Computer Aided Verification We provide a learning-based technique for guessing a winning strategy in a parity game originating from an LTL synthesis problem. A cheaply obtained guess can be useful in several applications. Not only can the guessed strategy be applied as best-effort in cases where the game’s huge size prohibits rigorous approaches, but it can also increase the scalability of rigorous LTL synthesis in several ways. Firstly, checking whether a guessed strategy is winning is easier than constructing one. Secondly, even if the guess is wrong in some places, it can be fixed by strategy iteration faster than constructing one from scratch. Thirdly, the guess can be used in on-the-fly approaches to prioritize exploration in the most fruitful directions. In contrast to previous works, we (i) reflect the highly structured logical information in game’s states, the so-called semantic labelling, coming from the recent LTL-to-automata translations, and (ii) learn to reflect it properly by learning from previously solved games, bringing the solving process closer to human-like reasoning. https://research-explorer.ista.ac.at/download/14259/14276/2023_LNCS_CAV_Kretinsky.pdf application/pdfno https://creativecommons.org/licenses/by/4.0/ Springer Nature2023Paris, France eng 0302-9743 1611-3349 9783031377051 00131078650002010.1007/978-3-031-37706-8_20 13964390-414 Kretinsky, Jan, Tobias Meggendorfer, Maximilian Prokop, and Sabine Rieder. “Guessing Winning Policies in LTL Synthesis by Semantic Learning.” In <i>35th International Conference on Computer Aided Verification</i>, 13964:390–414. Springer Nature, 2023. <a href="https://doi.org/10.1007/978-3-031-37706-8_20">https://doi.org/10.1007/978-3-031-37706-8_20</a>. Kretinsky, Jan, et al. “Guessing Winning Policies in LTL Synthesis by Semantic Learning.” <i>35th International Conference on Computer Aided Verification</i>, vol. 13964, Springer Nature, 2023, pp. 390–414, doi:<a href="https://doi.org/10.1007/978-3-031-37706-8_20">10.1007/978-3-031-37706-8_20</a>. Kretinsky J, Meggendorfer T, Prokop M, Rieder S. Guessing winning policies in LTL synthesis by semantic learning. In: <i>35th International Conference on Computer Aided Verification</i>. Vol 13964. Springer Nature; 2023:390-414. doi:<a href="https://doi.org/10.1007/978-3-031-37706-8_20">10.1007/978-3-031-37706-8_20</a> Kretinsky, J., Meggendorfer, T., Prokop, M., &#38; Rieder, S. (2023). Guessing winning policies in LTL synthesis by semantic learning. In <i>35th International Conference on Computer Aided Verification</i> (Vol. 13964, pp. 390–414). Paris, France: Springer Nature. <a href="https://doi.org/10.1007/978-3-031-37706-8_20">https://doi.org/10.1007/978-3-031-37706-8_20</a> Kretinsky J, Meggendorfer T, Prokop M, Rieder S. 2023. Guessing winning policies in LTL synthesis by semantic learning. 35th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13964, 390–414. J. Kretinsky, T. Meggendorfer, M. Prokop, and S. Rieder, “Guessing winning policies in LTL synthesis by semantic learning,” in <i>35th International Conference on Computer Aided Verification</i>, Paris, France, 2023, vol. 13964, pp. 390–414. J. Kretinsky, T. Meggendorfer, M. Prokop, S. Rieder, in:, 35th International Conference on Computer Aided Verification, Springer Nature, 2023, pp. 390–414. 142592023-09-03T22:01:16Z2026-07-07T13:39:23Z