Accession Number:

ADA281044

Title:

The Complexity of PDL with Interleaving

Descriptive Note:

Corporate Author:

BROWN UNIV PROVIDENCE RI DEPT OF COMPUTER SCIENCE

Report Date:

1994-06-30

Pagination or Media Count:

13.0

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 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.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE