PDL with Intersection and Converse is 2EXP-complete

Authors Stefan Göller, Markus Lohrey, Carsten Lutz

Thumbnail PDF


  • Filesize: 200 kB
  • 17 pages

Document Identifiers

Author Details

Stefan Göller
Markus Lohrey
Carsten Lutz

Cite AsGet BibTex

Stefan Göller, Markus Lohrey, and Carsten Lutz. PDL with Intersection and Converse is 2EXP-complete. In Algorithmic-Logical Theory of Infinite Structures. Dagstuhl Seminar Proceedings, Volume 7441, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)


The logic ICPDL is the expressive extension of Propositional Dynamic Logic (PDL), which admits intersection and converse as program operators. The result of this paper is containment of ICPDL-satisfiability in $2$EXP, which improves the previously known non-elementary upper bound and implies $2$EXP-completeness due to an existing lower bound for PDL with intersection (IPDL). The proof proceeds showing that every satisfiable ICPDL formula has model of tree width at most two. Next, we reduce satisfiability in ICPDL to $omega$-regular tree satisfiability in ICPDL. In the latter problem the set of possible models is restricted to trees of an $omega$-regular tree language. In the final step,$omega$-regular tree satisfiability is reduced the emptiness problem for alternating two-way automata on infinite trees. In this way, a more elegant proof is obtained for Danecki's difficult result that satisfiability in IPDL is in $2EXP$.
  • Satisfiability
  • Propositional Dynamic Logic
  • Computational Complexity


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail