Guessing Winning Policies in LTL Synthesis by Semantic Learning

D 2023

Guessing Winning Policies in LTL Synthesis by Semantic Learning

KŘETÍNSKÝ, Jan, Tobias MEGGENDORFER, Maximilian PROKOP a Sabine RIEDER

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

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

DOI

http://dx.doi.org/10.1007/978-3-031-37706-8_20

Klíčová slova anglicky

verification; synthesis; temporal logic; machine learning

Štítky

core_A, firank_1

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 7. 4. 2024 23:28, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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 MU

Ná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 MU

Ná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

Citovat

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.

@inproceedings{2321221,
   author = {Křetínský, Jan and Meggendorfer, Tobias and Prokop, Maximilian and Rieder, Sabine},
   address = {Cham},
   booktitle = {Computer Aided Verification - 35th International Conference, CAV 2023, Proceedings, Part I},
   doi = {http://dx.doi.org/10.1007/978-3-031-37706-8_20},
   editor = {Constantin Enea and Akash Lal},
   keywords = {verification; synthesis; temporal logic; machine learning},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-031-37705-1},
   pages = {390-414},
   publisher = {Springer},
   title = {Guessing Winning Policies in LTL Synthesis by Semantic Learning},
   year = {2023}
}

TY  - JOUR
ID  - 2321221
AU  - Křetínský, Jan - Meggendorfer, Tobias - Prokop, Maximilian - Rieder, Sabine
PY  - 2023
TI  - Guessing Winning Policies in LTL Synthesis by Semantic Learning
PB  - Springer
CY  - Cham
SN  - 9783031377051
KW  - verification
KW  - synthesis
KW  - temporal logic
KW  - machine learning
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.
ER  -

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. \textit{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.

Podrobný výpis o publikaci