| Summary: | Kleene algebra axioms are complete with respect to both language models and
binary relation models. In particular, two regular expressions recognise the
same language if and only if they are universally equivalent in the model of
binary relations. We consider Kleene allegories, i.e., Kleene algebras with two
additional operations and a constant which are natural in binary relation
models: intersection, converse, and the full relation. While regular languages
are closed under those operations, the above characterisation breaks. Putting
together a few results from the literature, we give a characterisation in terms
of languages of directed and labelled graphs. By taking inspiration from Petri
nets, we design a finite automata model, Petri automata, allowing to recognise
such graphs. We prove a Kleene theorem for this automata model: the sets of
graphs recognisable by Petri automata are precisely the sets of graphs
definable through the extended regular expressions we consider. Petri automata
allow us to obtain decidability of identity-free relational Kleene lattices,
i.e., the equational theory generated by binary relations on the signature of
regular expressions with intersection, but where one forbids unit. This
restriction is used to ensure that the corresponding graphs are acyclic. We
actually show that this decision problem is EXPSPACE-complete.
|
|---|