The Complexity of Kleene Algebra with Tests
Permanent Link(s)
Collections
Author
Cohen, Ernie
Kozen, Dexter
Smith, Frederick
Abstract
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.
Date Issued
1996-07
Publisher
Cornell University
Keywords
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR96-1598
Type
technical report