The Complexity of Kleene Algebra with Tests

Kleene algebras with tests provide a natural framework for equational specification and verification. Kleene algebras with tests and related systems have been used successfully in basic safety analysis, source-to-source program transformation, and concurrency control. The equational theory of Kleene algebras with tests has been shown to be decidable in at most exponential time by an efficient reduction to Propositional Dynamic Logic. In this paper we prove that the theory is PSPACE-complete. 1 Introduction Kleene algebra with tests (KAT) [15] is an algebraic system intermediate to Kleene algebra (KA) and Propositional Dynamic Logic (PDL) in expressive power. One can use KAT for a range of common verification tasks without resorting to the full power of PDL. KAT and related systems have been applied successfully to real problems in basic safety analysis, source-to-source 1 Bell Communications Research Inc., 445 South St., Morristown, NJ 07960, USA 2 Computer Science Department, Cor...