KŘETÍNSKÝ, Jan, Tobias MEGGENDORFER, Maximilian PROKOP a Sabine RIEDER. Guessing Winning Policies in LTL Synthesis by Semantic Learning. In Constantin Enea and Akash Lal. Computer Aided Verification - 35th International Conference, CAV 2023, Proceedings, Part I. Cham: Springer, 2023, s. 390-414. ISBN 978-3-031-37705-1. Dostupné z: https://dx.doi.org/10.1007/978-3-031-37706-8_20.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Guessing Winning Policies in LTL Synthesis by Semantic Learning
Autoři KŘETÍNSKÝ, Jan (203 Česká republika, garant, domácí), Tobias MEGGENDORFER (276 Německo), Maximilian PROKOP (276 Německo, domácí) a Sabine RIEDER (276 Německo).
Vydání Cham, Computer Aided Verification - 35th International Conference, CAV 2023, Proceedings, Part I, od s. 390-414, 25 s. 2023.
Nakladatel Springer
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
Forma vydání tištěná verze "print"
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/23:00131847
Organizační jednotka Fakulta informatiky
ISBN 978-3-031-37705-1
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-031-37706-8_20
Klíčová slova anglicky verification; synthesis; temporal logic; machine learning
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 7. 4. 2024 23:28.
Anotace
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.
Návaznosti
MUNI/A/1081/2022, interní kód MUNázev: Modelování, analýza a verifikace (2023)
Investor: Masarykova univerzita, Modelování, analýza a verifikace (2023)
MUNI/A/1433/2022, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 23
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 23
VytisknoutZobrazeno: 28. 4. 2024 08:22