Formula Synthesis in Propositional Dynamic Logic with Shuffle

Authors

  • Sophie Pinchinat IRISA/Univ Rennes
  • Sasha Rubin The University of Sydney
  • François Schwarzentruber IRISA/Univ Rennes

DOI:

https://doi.org/10.1609/aaai.v36i9.21227

Keywords:

Planning, Routing, And Scheduling (PRS)

Abstract

We introduce the formula-synthesis problem for Propositional Dynamic Logic with Shuffle (PDL || ). This problem, which generalises the model-checking problem againsts PDL || is the following: given a finite transition system and a regular term-grammar that generates (possibly infinitely many) PDL || formulas, find a formula generated by the grammar that is true in the structure (or return that there is none). We prove that the problem is undecidable in general, but add certain restrictions on the input structure or on the input grammar to yield decidability. In particular, we prove that (1) if the grammar only generates formulas in PDL (without shuffle), then the problem is EXPTIME-complete, and a further restriction to linear grammars is PSPACE-complete, and a further restriction to non-recursive grammars is NP-complete, and (2) if one restricts the input structure to have only simple paths then the problem is in 2-EXPTIME. This work is motivated by and opens up connections to other forms of synthesis from hierarchical descriptions, including HTN problems in Planning and Attack-tree Synthesis problems in Security.

Downloads

Published

2022-06-28

How to Cite

Pinchinat, S., Rubin, S., & Schwarzentruber, F. (2022). Formula Synthesis in Propositional Dynamic Logic with Shuffle. Proceedings of the AAAI Conference on Artificial Intelligence, 36(9), 9902-9909. https://doi.org/10.1609/aaai.v36i9.21227

Issue

Section

AAAI Technical Track on Planning, Routing, and Scheduling