Formula Synthesis in Propositional Dynamic Logic with Shuffle

This talk is based on joint work with Sasha Rubin and François Schwarzentruber, published in AAAI22. 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 ϕ (or say none exists) generated by G that is true in M. This problem generalizes 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. This is a very interesting case because PDL formulas contain programs. 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.

Authors

• Sophie Pinchinat

Keywords

No keywords are indexed for this paper.