Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition

摘要

PPDL~(det) extends propositional dynamic logic (PDL) with parallel composition of programs. This new construct has separation semantics: to execute the parallel program (α || β) the initial state is separated into two substates and the programs α and β are executed on these substates. By adapting the elimination of Hintikka sets procedure, we provide a decision procedure for the satisfiability problem of PPDL~(det). We prove that this decision procedure can be executed in deterministic exponential time, hence that the satisfiability problem of PPDL~(det) is EXPTIME-complete.