Kleene Algebra with Tests: Completeness and Decidability

Abstract

Kleene algebras with tests provide a rigorous framework for equational specification and verification. They have been used successfully in basic safety analysis, source-to-source program transformation, and concurrency control. We prove the completeness of the equational theory of Kleene algebra with tests and *-continuous Kleene algebra with tests over language-theoretic and relational models. We also show decidability. Cohen's reduction of Kleene algebra with hypotheses of the form $r=0$ to Kleene algebra without hypotheses is simplified and extended to handle Kleene algebras with tests.