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, 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 2(cn/log n).
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 30, 1994
- Accession Number
- ADA281044
Entities
People
- Alain J. Mayer
- Larry J. Stockmeyer
Organizations
- Brown University