Previous work refining complexity measures for PDL with interleaving is extended in this paper. PDL is the propositional dynamic logic introduced by Fisher and Ladner in 1979. It uses the operator of union to express nondeterminacy. PDL has been augmented with the operator of interleaving to express asynchronous concurrency; the augmented PDL is called IPDL. The authors refine earlier results on the complexity of IPDL. In particular, they show that the satisfiability problem for IPDL is complete for deterministic double-exponential time, and establish a lower bound of 2 ^{c n &slash;} log n.

The authors establish a correspondence between Turing machines and IPDL expressions encoding the complement of their accepting computations. They use this correspondence to derive the main results. The proofs are well motivated and well documented, and thus are worth reading for anyone interested in complexity in general.