Equational axioms of test algebra

Abstract

We present a complete axiomatization of test algebra ([24,18,29]), the two-sorted algebraic variant of Propositional Dynamic Logic (PDL,[21,7]). The axiomatization consists of adding a finite number of equations to any axiomatization of Kleene algebra ([15,26,17,4]) and algebraic translations of the Segerberg ([27]) axioms for PDL. Kleene algebras are not finitely axiomatizable ([25,6]), so our result does not give us a finite axiomatization of test algebra: in fact, no finite equational axiomatization exists. We also present a single-sorted version of test algebra, using the notion of dynamic negation ([9,2,11]), to which the previous results carry over.