The Equational Theory of Positive Relation Algebra

PACE in Shanghai, November 2016
Algebras of relations appear naturally in many contexts, in computer science as well as in mathematics. They constitute a framework well suited to the semantics of imperative programs. Kleene algebras are a starting point: these algebras enjoy very strong decidability properties, and a complete axiomatisation. The goal of this talk was to export known results from Kleene algebra to some of its extensions. We first consider a known extension: Kleene algebras with converse. Decidability of these algebras is already known, but the algorithm witnessing this result was too complicated to be practical. We propose a simpler algorithm, which is more efficient, and whose correctness is easier to establish. It allows us to prove that this problem lies in the complexity class PSpace-complete. Then we study Kleene allegories. Few results were known about this extension. Following results about closely related algebras, we establish the equivalence between equality in Kleene allegories and the equality of certain sets of graphs. We then develop a new automaton model (so-called Petri automata), based on Petri nets. We prove the equivalence between the original problem and comparing these automata. In the restricted setting of identity-free Kleene lattices, we also provide an algorithm performing this comparison. This algorithm uses exponential space. However, we prove that the problem of comparing Petri automata lies in the class ExpSpace- complete.

Related talks

The Equational Theory of Positive Relation Algebra
MOVE in Marseille, March 2017
.
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
Cardinalities of finite relations in Coq (in ITP 2016)
with Insa Stucke and Damien Pous.
More
Algorithms for Kleene algebra with converse (in JLAMP 2016)
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 identity-free relational Kleene lattices (in JFLA 2015)
with Damien Pous.
More
Kleene algebra with converse (in RAMICS 2014)
with Damien Pous.
More

Updated: