Invited Speaker: Suguman Bansal
TBA
Invited Speaker: Augusto B. Corrêa
Augusto B. Corrêa is a postdoctoral researcher at the University of Basel, Switzerland, working in the group of Prof. Malte Helmert. He works in classical planning, focusing on how different representations impact the performance of planners. Other topics of his research include generalized planning, computational complexity, and interactive models for planning. Augusto is the creator of the Powerlifted planners and one of the developers of the Levitron and Scorpion Maidu planners, which won the satisficing track of the last International Planning Competition.
Lifted Planning: Recent Advances in Planning Using First-Order Representations
Lifted planning is usually defined as planning directly over a first-order representation. From the mid-1990s until the late 2010s, lifted planning was sidelined, as most of the state-of-the-art planners first ground the task and then solve it using a propositional representation. Moreover, it was unclear whether lifted planners could scale. But as planning problems become harder, they also become infeasible to ground. Recently, lifted planners came back into play, aiming at problems where grounding is a bottleneck. In this talk, we survey recent advances in lifted planning, including lifted state-space search and satisfiability. We draw some direct connections between recent lifted planners and other areas of computer science, such as constraint satisfaction problems, databases, and logic programming.
Invited Speaker: Jan Křetínský
After PhD from Technical University of Munich in 2013 and from Masaryk University Brno in 2014, Jan 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, in particular in reactive synthesis.
Learning and Guessing Winning Policies in LTL Synthesis via Semantics
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.