KAC : Kleene Algebras with Converse
The equational theory generated by all algebras of binary relations with operations of union, composition, converse and reflexive transitive closure was studied by Bernátsky, Bloom, Ésik and Stefanescu in 1995. In particular, they obtained its decidability by using a particular automata construction. In this project, we showed that deciding this equational theory is PSpacecomplete, by providing a PSpace algorithm (the problem is easily shown to be PSpacehard). We obtained other algorithms that are timeefficient in practice, despite not being PSpace. Our results use an alternative automata construction, inspired by the one from Bloom, Ésik and Stefanescu. Those two constructions may be related by exhibiting a bisimulation between the resulting deterministic automata, and by showing how our construction results in more sharing between states, thus producing smaller automata.
Equation checker
How to use this :
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:
0
: the empty relation1
: the identity relation<expr1>  <expr2>
: the set union<expr1> . <expr2>
: the composition of relations<expr1>~
: the converse of a relation<expr1>*
: the reflexive transitive closure of a relation.<expr1>+
: the transitive closure of a relation.<expr1>{<int>}
: the iteration of a relation. For instance,(a.b){3}
is a shorthand for(a.b).(a.b).(a.b)
You can also use brackets (...)
. For letters/variables, you may use a'
instead of a~
.
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, ((1a'b)+C)~.a =/= 0
is an acceptable equation.
The checker
Automata builder
How to use this :
Simply input an automaton in the text box, choose from one of the constructions on the left scroll box, and click “Build” to generate the automaton and its closure.
An automaton is specified through the following syntax:
initial : <list of initial states separated by spaces>
final : <list of final states separated by spaces>
<source>  <label> > <target>
<source>  <label> > <target>
...
See below for an example.
The builder
Related documents
Publications  
Kleene algebra with converse
(in RAMICS 2014)
with Damien Pous. 
More  
Kleene Algebra with Converse
RAMiCS
in Marienstatt,
April 2014
.

More  
Algorithms for Kleene algebra with converse
(in JLAMP 2016)
with Damien Pous. 
More  
Internship  
Algèbres de Relations, Étude des algèbres de Kleene avec converse
Internship defence
in Paris,
September 2013
(Internship defence, in French)
.

More  
Internship report  
Coq proof  
with bounds  
with generalized converse  
``pen and paper'' proof  
Equation checker  
Sources  
Documentation  
Other presentations  
Equivalence of regular expressions with converse on relations
PiCoq
in Lyon,
June 2013
.

More  
Deciding Kleene Algebra with converse is PSpacecomplete
PACE
in Lyon,
February 2014
.

More  
Deciding Kleene Algebra with converse is PSpacecomplete
GeoCal
in Bordeaux,
March 2014
.

More 