Home > Research > Publications & Outputs > Guessing Winning Policies in LTL Synthesis by S...

Links

Text available via DOI:

View graph of relations

Guessing Winning Policies in LTL Synthesis by Semantic Learning.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Published
Close
Publication date17/07/2023
Host publicationComputer Aided Verification - 35th International Conference, CAV 2023, Proceedings
EditorsConstantin Enea, Akash Lal
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Pages390-414
Number of pages25
ISBN (print)9783031377051
<mark>Original language</mark>English

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13964 LNCS
ISSN (Print)0302-9743
ISSN (electronic)1611-3349

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’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.