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 PSpace-complete, by providing a PSpace algorithm (the problem is easily shown to be PSpace-hard). We obtained other algorithms that are time-efficient 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 relation
  • 1: 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, ((1|a'|b)+|C)~.a =/= 0 is an acceptable equation.

The checker

Wrong

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

OK
Initial automaton
Closure automaton

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 PSpace-complete
PACE in Lyon, February 2014
.
More
Deciding Kleene Algebra with converse is PSpace-complete
GeoCal in Bordeaux, March 2014
.
More