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