Completeness for Identity-free Kleene Lattices

March 25, 2019

Amina Doumane (Université de Varsovie)

We provide a finite set of axioms for identity-free Kleene lattices, which we prove sound and com-
plete for the equational theory of their relational models. This equational theory was previously
proved to coincide with that of language models and to be ExpSpace-complete; expressions of
the corresponding syntax moreover make it possible to denote precisely those languages of graphs
that can be accepted by Petri automata. Finite axiomatisability was missing to obtain the same
picture as for Kleene algebra, regular expressions, and (word) automata.
Our proof builds on the completeness theorem for Kleene algebra, and on a novel automata
construction that makes it possible to extract axiomatic proofs using a Kleene-like algorithm.