Standard
Guessing Winning Policies in LTL Synthesis by Semantic Learning. / Kretínský, Jan
; Meggendorfer, Tobias; Prokop, Maximilian et al.
Computer Aided Verification - 35th International Conference, CAV 2023, Proceedings. ed. / Constantin Enea; Akash Lal. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. p. 390-414 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13964 LNCS).
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Harvard
Kretínský, J
, Meggendorfer, T, Prokop, M & Rieder, S 2023,
Guessing Winning Policies in LTL Synthesis by Semantic Learning. in C Enea & A Lal (eds),
Computer Aided Verification - 35th International Conference, CAV 2023, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13964 LNCS, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 390-414.
https://doi.org/10.1007/978-3-031-37706-8_20APA
Kretínský, J.
, Meggendorfer, T., Prokop, M., & Rieder, S. (2023).
Guessing Winning Policies in LTL Synthesis by Semantic Learning. In C. Enea, & A. Lal (Eds.),
Computer Aided Verification - 35th International Conference, CAV 2023, Proceedings (pp. 390-414). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13964 LNCS). Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.1007/978-3-031-37706-8_20Vancouver
Kretínský J
, Meggendorfer T, Prokop M, Rieder S.
Guessing Winning Policies in LTL Synthesis by Semantic Learning. In Enea C, Lal A, editors, Computer Aided Verification - 35th International Conference, CAV 2023, Proceedings. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. 2023. p. 390-414. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-37706-8_20
Author
Kretínský, Jan
; Meggendorfer, Tobias ; Prokop, Maximilian et al. /
Guessing Winning Policies in LTL Synthesis by Semantic Learning. Computer Aided Verification - 35th International Conference, CAV 2023, Proceedings. editor / Constantin Enea ; Akash Lal. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. pp. 390-414 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Bibtex
@inproceedings{745dd0c1601747378df6715601f859b0,
title = "Guessing Winning Policies in LTL Synthesis by Semantic Learning.",
abstract = "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{\textquoteright}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{\textquoteright}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.",
author = "Jan Kret{\'i}nsk{\'y} and Tobias Meggendorfer and Maximilian Prokop and Sabine Rieder",
year = "2023",
month = jul,
day = "17",
doi = "10.1007/978-3-031-37706-8_20",
language = "English",
isbn = "9783031377051",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",
pages = "390--414",
editor = "Constantin Enea and Akash Lal",
booktitle = "Computer Aided Verification - 35th International Conference, CAV 2023, Proceedings",
}
RIS
TY - GEN
T1 - Guessing Winning Policies in LTL Synthesis by Semantic Learning.
AU - Kretínský, Jan
AU - Meggendorfer, Tobias
AU - Prokop, Maximilian
AU - Rieder, Sabine
PY - 2023/7/17
Y1 - 2023/7/17
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-031-37706-8_20
DO - 10.1007/978-3-031-37706-8_20
M3 - Conference contribution/Paper
SN - 9783031377051
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 390
EP - 414
BT - Computer Aided Verification - 35th International Conference, CAV 2023, Proceedings
A2 - Enea, Constantin
A2 - Lal, Akash
PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik
ER -
