Algorithms for Kleene algebra with converse

with Damien Pous .

journal paper, in JLAMP 2016

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.

@article{bp16jlamp,
    title = "Algorithms for Kleene algebra with converse",
    author = "{Paul Brunet}, {Damien Pous}",
    year = 2016,
    journal = "JLAMP",
    doi = "10.1016/j.jlamp.2015.07.005"
}

Links

	Permanent link
	Paper on Science Direct

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