Technical Report: DCC-2014-07

Kleene Algebra Completeness

Sabine Broda, Sílvia Cavadas, Nelma Moreira

Centro de Matemática da Universidade do Porto
R. Campo Alegre 687, 4169-007 Porto, Portugal
July 2014


This paper gives a new presentation of Kozen's proof of Kleene algebra completeness featured in his article "A completeness theorem for Kleene algebras and the algebra of regular events". A few new variants are introduced, shortening the proof. Specifically, we directly construct an epsilon-free automaton to prove an equivalent to Kleene's representation theorem (implementing Glushkov's instead of Thompson's construction), and we bypass the use of minimal automata by directly implementing a Myhill-Nerode equivalence relation on the union of equivalent deterministic automata.