### 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.