Algorithms for Kleene algebra 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. We show that deciding this equational theory is PSpace-complete, by providing a PSpace algorithm (the problem is easily shown to be PSpace-hard). We obtain 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. We relate those two constructions 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.
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 | |
|
Une introduction aux algèbres de Kleene
Inter'Actions
in Lyon,
May 2016
(in French)
.
|
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 Identity-free Kleene Lattices
LAC
in Chambéry,
November 2014
.
|
More | |
|
Kleene Algebra with Converse
RAMiCS
in Marienstatt,
April 2014
.
|
More | |
|
Deciding Kleene Algebra with converse is PSpace-complete
GeoCal
in Bordeaux,
March 2014
.
|
More | |
|
Deciding Kleene Algebra with converse is PSpace-complete
PACE
in Lyon,
February 2014
.
|
More | |
|
Algèbres de Relations, Étude des algèbres de Kleene avec converse
Internship defence
in Paris,
September 2013
(Internship defence, in French)
.
|
More | |
|
Equivalence of regular expressions with converse on relations
PiCoq
in Lyon,
June 2013
.
|
More | |
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 | |
|
Cardinalities of finite relations in Coq
(in ITP 2016)
with Insa Stucke and Damien Pous. |
More | |
|
Petri automata for Kleene allegories
(in LICS 2015)
with Damien Pous. |
More | |
|
Decidability of identity-free relational Kleene lattices
(in JFLA 2015)
with Damien Pous. |
More | |
|
Kleene algebra with converse
(in RAMICS 2014)
with Damien Pous. |
More | |