License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.07441.5
URN: urn:nbn:de:0030-drops-14093
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2008/1409/
Go to the corresponding Portal

Göller, Stefan ; Lohrey, Markus ; Lutz, Carsten

PDL with Intersection and Converse is 2EXP-complete

pdf-format:
07441.GoellerStefan.ExtAbstract.1409.pdf (0.2 MB)

Abstract

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$.


BibTeX - Entry

@InProceedings{goller_et_al:DagSemProc.07441.5,
  author =	{G\"{o}ller, Stefan and Lohrey, Markus and Lutz, Carsten},
  title =	{{PDL with Intersection and Converse is 2EXP-complete}},
  booktitle =	{Algorithmic-Logical Theory of Infinite Structures},
  pages =	{1--17},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7441},
  editor =	{Rod Downey and Bakhadyr Khoussainov and Dietrich Kuske and Markus Lohrey and Moshe Y. Vardi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2008/1409},
  URN =		{urn:nbn:de:0030-drops-14093},
  doi =		{10.4230/DagSemProc.07441.5},
  annote =	{Keywords: Satisfiability, Propositional Dynamic Logic, Computational Complexity}
}

Keywords: Satisfiability, Propositional Dynamic Logic, Computational Complexity
Collection: 07441 - Algorithmic-Logical Theory of Infinite Structures
Issue Date: 2008
Date of publication: 09.04.2008

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI