Title: Learning and Guessing Winning Policies in LTL Synthesis via Semantics

Speaker: Jan Křetínský    (bio) (bio)

After PhD from Technical University of Munich in 2013 and from Masaryk University Brno in 2014, Jan Křetínský was a research fellow at IST Austria and since 2015 a professor at TU Munich, getting tenure there. While still affiliated, he has recently moved to MU Brno. His main focus is basic research in verification, control and explainability of complex systems. Since 2013 he has been advocating and pioneering the use of AI and ML in verification.

When: Tuesday, 15 October 2024 at 1900 hrs (IST)       

Abstract:
We discuss a learning-based framework for guessing a winning strategy in a parity game originating from a reactive synthesis problem for LTL. Its applications range from cases where the game's huge size prohibits rigorous approaches, over increasing scalability of rigorous synthesis, to explainability of synthesized controllers. We discuss the advantages and caveats of these new avenues in synthesis. On the technical level, we describe (i) how to 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) to do so by learning from previously solved games, bringing the solution process closer to human-like reasoning.