The complexity of PDL with interleaving

Abstract

To provide a logic for reasoning about concurrently executing programs, Abrahamson has defined an extension of propositional dynamic logic (PDL) by allowing interleaving as an operator for combining programs, in addition to the regular PDL operators union, concatenation, and star. We show that the satisfiability problem for interleaving PDL is complete for deterministic double-exponential time, and that this problem requires time double-exponential in cn/log n for some positive constant c. Moreover, this lower bound holds even when restricted to formulas where each program appearing in the formula has the form a1|a2|...|ak where denotes the interleaving operator and where a1,...,ak are regular programs, i.e., programs built from atomic programs using only the regular operators. Another consequence of the method used to prove this result is that the equivalence problem for regular expressions with interleaving requires space 2cn/log n and that this lower bound holds even to decide whether (E1|E2\...|Ek)∪F ≡ Σ* where E1,..., Ek, F are ordinary regular expressions; this improves a previous result of the authors. Moreover, the same lower bound holds for the containment problem for expressions of the form E1|E2|...|Ek.