
Kleene Algebra Completeness
Sabine Broda, Sílvia Cavadas, Nelma Moreira
Centro de Matemática da Universidade do Porto
R. Campo Alegre 687, 4169007 Porto, Portugal
email: sbb@dcc.fc.up.pt,silviacavadas@gmail.com, nam@dcc.fc.up.pt
July 2014
Abstract
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 epsilonfree 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 MyhillNerode equivalence relation on the union of equivalent deterministic automata.
