Göller, Stefan ;
Lohrey, Markus ;
Lutz, Carsten
PDL with Intersection and Converse is 2EXPcomplete
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 ICPDLsatisfiability in $2$EXP, which improves the
previously known nonelementary upper bound and implies
$2$EXPcompleteness 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 twoway 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{gller_et_al:DSP:2008:1409,
author = {Stefan G{\"o}ller and Markus Lohrey and Carsten Lutz},
title = {PDL with Intersection and Converse is 2EXPcomplete},
booktitle = {AlgorithmicLogical Theory of Infinite Structures},
year = {2008},
editor = {Rod Downey and Bakhadyr Khoussainov and Dietrich Kuske and Markus Lohrey and Moshe Y. Vardi},
number = {07441},
series = {Dagstuhl Seminar Proceedings},
ISSN = {18624405},
publisher = {Internationales Begegnungs und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2008/1409},
annote = {Keywords: Satisfiability, Propositional Dynamic Logic, Computational Complexity}
}
2008
Keywords: 

Satisfiability, Propositional Dynamic Logic, Computational Complexity 
Seminar: 

07441  AlgorithmicLogical Theory of Infinite Structures

Related Scholarly Article: 


Issue date: 

2008 
Date of publication: 

2008 