A Kleene Theorem for Petri automata

Highlights in Brussels, September 2016

Petri Automata are automata based on Petri nets, whose operational semantics is designed to recognise sets of graphs. We introduced them in a recent paper [1] with Pous to study Kleene Allegory (KAl) expressions: terms built from a finite alphabet of variables, with the constants 0 and 1, the unary operators converse and Kleene star, and the binary operators union, composition and intersection. To any such expression, one can associate a set of graphs such that two expressions are universally equivalent when interpreted as binary relations if and only if their associated sets of graphs are equal. In [1] we gave a method to build from any Kleene Allegory expression a Petri automaton recognising the appropriate set of series parallel graphs. It is then natural to wonder what is the class of graph languages recognised by Petri automata. For the usual notion of finite state automata, the well known Kleene Theorem states that the languages recognisable by automata are exactly those specifiable by regular expressions. This year we provided a similar theorem for Petri automata and Kleene Allegory expressions [2]. Indeed the graph languages specified by Petri automata are precisely the languages denoted by KAl. Moreover, this entails that decidability of the equational theory of Kleene Allegories is equivalent to that of language equivalence for Petri automata. This decidability problem is still open. It is worth mentioning that the technical part of the proof in [2] actually uses a smaller syntax than Kleene Allegories, without converse nor identity. In this fragment the considered graphs are series-parallel, so that the key technical result is actually a Kleene theorem for series-parallel regular expressions and languages. References: [1] Paul Brunet and Damien Pous. Petri automata for Kleene allegories. In Logic in Computer Science (LICS), 2015 30th Annual ACM/IEEE Symposium on, pages 68–79, July 2015. [2] Paul Brunet. Algebras of relations: from algorithms to formal proofs. PhD Thesis, October 2016.

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
	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