Relational Kleene Lattices
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 which are natural in binary relation models: intersection and converse. While regular languages are closed under those operations, the above characterisation breaks. Instead, we give a characterisation in terms of languages of directed and labelled graphs. We then design a finite automata model allowing to recognise such graphs, by taking inspiration from Petri nets. This model allows us to obtain decidability of identityfree 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. The decidability of graphlanguage equivalence is not addressed in our work, but was solved later on by Y. Nakamura (see this paper).
Test equations
How to use this :
Write down equations in the lefthand side fields of the applet, and see their validity just to their right (a green tick meaning yes and a red cross meaning no). The rightmost button allow you to see more details, and to hide them afterwards.
Write an equation in the input field of the applet, and see its validity just to the right (a green tick meaning yes and a red cross meaning no).
Equations should be entered like this:
<expr1> <cmp> <expr2>
An expression can use strings as variables/letters, and the operations:
<expr1>  <expr2>
: the set union<expr1> & <expr2>
: the set intersection<expr1> . <expr2>
: the composition of relations<expr1>+
: the transitive closure of a relation<expr1>{<int>}
: the fixed iteration. For instance,(a.b){3}
is a shorthand for(a.b).(a.b).(a.b)
You can also use brackets (...)
.
The valid comparaisons <cmp>
are:
<=
: loose inclusion>=
: converse of the loose inclusion<
: strict inclusion>
: converse of the strict inclusion=
: equality=/=
: negation of the equality<>
: means that the two expressions are incomparable, i.e. neither one of them is included in the other.
For instance, (ab)^+ . C & d < d & a.b.C & (da)
is an acceptable equation.
The tester
Automaton visualizer
Detailled equation checking
Related documents
Equation checker  
Main page (hosted by github)  
Documentation  
Related papers  
Petri automata
(in LMCS 2017)
with Damien Pous. 
More  
Algebras of relations: from algorithms to formal proofs (in Université de Lyon 2016)  More  
Petri automata for Kleene allegories
(in LICS 2015)
with Damien Pous. 
More  
Decidability of identityfree relational Kleene lattices
(in JFLA 2015)
with Damien Pous. 
More  
Related talks  
The Equational Theory of Positive Relation Algebra
MOVE
in Marseille,
March 2017
.

More  
The Equational Theory of Positive Relation Algebra
PACE
in Shanghai,
November 2016
.

More  
A Kleene Theorem for Petri automata
Highlights
in Brussels,
September 2016
.

More  
Petri automata for Kleene Allegories
LiCS
in Kyoto,
July 2015
.

More  
Petri automata for Kleene allegories
Rapido
in Paris,
June 2015
.

More  
Petri automata for Kleene allegories
Midlands Graduate School
in Sheffield,
April 2015
.

More  
Décidabilité des Treillis de Kleene sans identité
JFLA
in Val d'Ajol,
January 2015
(in French)
.

More  
Decidability of Identityfree Kleene Lattices
LAC
in Chambéry,
November 2014
.

More 