Completeness for identity-free Kleene lattices
Amina Doumane
IRIF, Université de Paris
http://perso.ens-lyon.fr/amina.doumane/
Date(s) : 05/04/2018 iCal
11h00 - 12h30
We provide a finite set of axioms for identity-free Kleene lattices, which we prove sound and complete 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.
Catégories
