Completeness for identity-free Kleene lattices

Carte non disponible

Date(s) - 05/04/2018
11 h 00 min - 12 h 30 min


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.

Posts created 14

Articles similaires

Commencez à saisir votre recherche ci-dessus et pressez Entrée pour rechercher. ESC pour annuler.

Retour en haut
Secured By miniOrange