The Complexity of PDL with Interleaving
BROWN UNIV PROVIDENCE RI DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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 cnlog n for some positive constant c. Moreover, this lower bound holds even when restricted to formulas, 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 2cnlog n.
- Computer Programming and Software