On the Coalgebraic Theory of Kleene Algebra with Tests

We develop a coalgebraic theory of Kleene algebra with tests (KAT) along the lines of Rutten (1998) for Kleene algebra and Chen and Pucella (2003) for a limited version of KAT, resolving two open problems of Chen and Pucella. Our treatment includes a simple definition of the Brzozowski derivative for KAT expressions and an automata-theoretic interpretation involving automata on guarded strings. We also give a complexity analysis, showing that an efficient implementation of coinductive equivalence proofs in this setting is essentially equivalent to standard automata-theoretic constructions. It follows that coinductive equivalence proofs can be generated automatically in PSPACE. This matches the bound of Worthington (2008) for the automatic generation of equational proofs in KAT.