## Sasha Rubin - "Formula synthesis in propositional dynamic logic with shuffle"

*I will introduce a new type of problem in logic called the "formula synthesis problem": for a logic L, given a set of formulas represented by a context-free grammar G, and a structure M, find a formula F (or say none exists) generated by G that is true in M. This problem generalises the model-checking problem (in case the grammar generates just a single formula). I will instantiate this problem taking L to be propositional dynamic logic (PDL) extended with program shuffle. In this setting, the formula synthesis problem is undecidable, but I will consider some natural restrictions that are decidable using classic tools of tree automata theory. For instance, the problem is EXPTIME-complete if the logic is restricted to PDL. The choice of this logic was also motivated by rephrasing a hierarchical synthesis problem in AI known as Hierarchical Task Network Planning. This talk is based on joint work with Sophie Pinchinat and François Schwarzentruber, published in AAAI22.*

13/06/2022