Nominal techniques have received a lot of attention in recent years, as they describe in a simple yet precise manner phenomena related to variable renaming, like alpha-equivalence, scopes, locality... However, they seem to suffer from two shortcomings: they are not yet able to handle interleaved scopes, and do not apply well to relational semantics of programs. In this talk I will describe an ongoing project to provide an algebraic treatment of the semantics of programming languages which contain explicitly allocation and de-allocation binders, inspired by previous work of Gabbay, Ghica and Petrişan. I will present the initial setup, defining a notion of alpha-equivalence of traces, and briefly describe how this may be extended to regular languages. I will present some decidability results we obtained, and hint at future investigations. Most of these developments have been formalised in Coq. This is joint work with Alexandra Silva and Daniela Petrisan.

Concurrent Kleene algebras (CKA) and bi-Kleene algebras support equational reasoning about computing systems with concurrent behaviours. Their natural semantics is given by series(-parallel) rational pomset languages, a standard true concurrency semantics, which is often associated with processes of Petri nets.

In the first part of the talk, I will present a recent proof of completeness, showing that two series-rational expressions are equivalent according to the laws of CKA exactly when their pomset semantics are equal.

In a second part, I will use Petri nets to reduce the problem of containment of languages of pomsets to the equivalence of finite state automata. In doing so, we prove decidability as well as provide tight complexity bounds.

Joint work with Damien Pous, Georg Struth, Tobias Kappé, Alexandra Silva, and Fabio Zanasi

Concurrent Kleene algebras (CKA) and bi-Kleene algebras support equational reasoning about computing systems with concurrent behaviours. Their natural semantics is given by series(-parallel) rational pomset languages, a standard true concurrency semantics, which is often associated with processes of Petri nets.

In the first part of the talk, I will present an automaton model designed to describe such languages of pomset, which satisfies a Kleene-like theorem. The main difference with previous constructions is that from expressions to automata, we use Brzozowski derivatives.

In a second part, I will use Petri nets to reduce the problem of containment of languages of pomsets to the equivalence of finite state automata. In doing so, we prove decidabilty as well as provide tight complexity bounds.

I will finish the presentation by briefly presenting a recent proof of completeness, showing that two series-rational expressions are equivalent according to the laws of CKA exactly when their pomset semantics are equal.

Joint work with Damien Pous, Georg Struth, Tobias Kappé, Bas Luttik, Alexandra Silva, and Fabio Zanasi.

Concurrent Kleene algebras support equational reasoning about computing systems with concurrent behaviours. Their natural semantics is given by series(-parallel) rational pomset languages, a standard true concurrency semantics, which is often associated with processes of Petri nets. We use constructions on Petri nets to provide two decision procedures for such pomset languages motivated by the equational and the refinement theory of concurrent Kleene algebra. The contribution to the first problem lies in a much simpler algorithm and an ExpSpace complexity bound. Decidability of the second, more interesting problem is new and, in fact, ExpSpace-complete.

We investigate the equational theory of algebras of formal languages with the constants empty language and unit language, the unary mirror image and Kleene star operators, and the binary operations of union, intersection and concatenation. We start by reducing the problem of deciding the validity of an equation over this signature to the equality of certain graph languages. This allows us to derive decidability, and to show that this problem is in fact ExpSpace-complete. Using this graph characterisation, and removing the Kleene star from our signature, we then propose a complete finite axiomatisation of this theory. This development was obtained using the proof assistant Coq.

We investigate the equational theory of algebras of formal languages with the constants empty language and unit language, the unary mirror image and Kleene star operators, and the binary operations of union, intersection and concatenation. We start by reducing the problem of deciding the validity of an equation over this signature to the equality of certain graph languages. This allows us to derive decidability, and to show that this problem is in fact ExpSpace-complete. Using this graph characterisation, and removing the Kleene star from our signature, we then propose a complete finite axiomatisation of this theory. This development was obtained using the proof assistant Coq.

RAMiCS, Lyon, May 2017 (Special session on mechanised reasoning)

We investigate the equational theory of algebras of formal languages with the constants empty language and unit language, the unary mirror image and Kleene star operators, and the binary operations of union, intersection and concatenation. We start by reducing the problem of deciding the validity of an equation over this signature to the equality of certain graph languages. This allows us to derive decidability, and to show that this problem is in fact ExpSpace-complete. Using this graph characterisation, and removing the Kleene star from our signature, we then propose a complete finite axiomatisation of this theory. This development was obtained using the proof assistant Coq.

We investigate the equational theory of algebras of formal languages with the constants empty language and unit language, the unary mirror image and Kleene star operators, and the binary operations of union, intersection and concatenation. We start by reducing the problem of deciding the validity of an equation over this signature to the equality of certain graph languages. This allows us to derive decidability, and to show that this problem is in fact ExpSpace-complete. Using this graph characterisation, and removing the Kleene star from our signature, we then propose a complete finite axiomatisation of this theory. This development was obtained using the proof assistant Coq.

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.

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.

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.

An axiomatisation of Nominal Kleene Algebra has been proposed by Gabbay and Ciancia, and then shown to be complete and decidable by Kozen et al. However, one can think of at least four different formulations for a Kleene Algebra with names: using freshness conditions or a presheaf structure (types), and with explicit permutations or not. We formally show that these variations are all equivalent. Then we introduce an extension of Nominal Kleene Algebra, motivated by relational models of programming languages. The idea is to let letters (i.e., atomic programs) carry a set of names, rather than being reduced to a single name. We formally show that this extension is at least as expressive as the original one, and that it may be presented with or without a presheaf structure, and with or without syntactic permutations. Whether this extension is strictly more expressive remains open. All our results were formally checked using the Coq proof assistant.

Une algèbre de Kleene est une structure algébrique munie des opérations de expressions régulières: zéro, un, somme, produit et étoile. Les relations binaires forment une telle algèbre, ainsi que les langages. Cette théorie est décidable, c'est à dire qu'il existe un algorithme permettant de décider si une équation utilisant uniquement ces opérations est une loi universelle des algèbres de Kleene. Ceci a plusieurs applications. 1) Il est assez naturel de modéliser une instruction d'un programme par une relation entre états mémoire. Cette abstraction permet de plonger les programmes dans une algèbre de Kleene relationnelle. Ainsi, on peut tester dans certains cas si deux programmes sont équivalents en utilisant cette théorie. 2) Dans une preuve mathématique manipulant des relations binaires, on peut faire appel à cet algorithme pour automatiser certaines étapes de preuve. Diverses extensions de ces algèbres existent, certaines étant mieux comprises que d'autres.

Kleene algebra axioms are complete with respect to both language models and binary relation models. In particular, two regular expressions recognise the same language if and only if they are universally equivalent in the model of binary relations. We consider Kleene allegories, i.e., Kleene algebras with two additional operations which are natural in binary relation models: intersection and converse. While regular languages are closed under those operations, the above characterisation breaks. Instead, we give a characterisation in terms of languages of directed and labelled graphs. We then design a finite automata model allowing to recognise such graphs, by taking inspiration from Petri nets. This model allows us to obtain decidability of identity-free relational Kleene lattices, i.e., the equational theory generated by binary relations on the signature of regular expressions with intersection, but where one forbids unit. This restriction is used to ensure that the corresponding graphs are acyclic. The decidability of graph-language equivalence in the full model remains open.

Kleene algebra axioms are complete with respect to both language models and binary relation models. In particular, two regular expressions recognise the same language if and only if they are universally equivalent in the model of binary relations. We consider Kleene allegories, i.e., Kleene algebras with two additional operations which are natural in binary relation models: intersection and converse. While regular languages are closed under those operations, the above characterisation breaks. Instead, we give a characterisation in terms of languages of directed and labelled graphs. We then design a finite automata model allowing to recognise such graphs, by taking inspiration from Petri nets. This model allows us to obtain decidability of identity-free relational Kleene lattices, i.e., the equational theory generated by binary relations on the signature of regular expressions with intersection, but where one forbids unit. This restriction is used to ensure that the corresponding graphs are acyclic. The decidability of graph-language equivalence in the full model remains open.

Kleene algebra axioms are complete with respect to both language models and binary relation models. In particular, two regular expressions recognise the same language if and only if they are universally equivalent in the model of binary relations. We consider Kleene allegories, i.e., Kleene algebras with two additional operations which are natural in binary relation models: intersection and converse. While regular languages are closed under those operations, the above characterisation breaks. Instead, we give a characterisation in terms of languages of directed and labelled graphs. We then design a finite automata model allowing to recognise such graphs, by taking inspiration from Petri nets. This model allows us to obtain decidability of identity-free relational Kleene lattices, i.e., the equational theory generated by binary relations on the signature of regular expressions with intersection, but where one forbids unit. This restriction is used to ensure that the corresponding graphs are acyclic. The decidability of graph-language equivalence in the full model remains open.

Families of binary relations are important interpretations of regular expressions, and the equivalence of two regular expressions with respect to their relational interpretations is decidable: the problem reduces to the equality of the denoted regular languages.

Putting together a few results from the literature, we first make explicit a generalisation of this reduction, for regular expressions extended with converse and intersection: instead of considering sets of words (i.e., formal languages), one has to consider sets of directed and labelled graphs.

We then focus on identity-free regular expressions with converse—a setting where the above graphs are acyclic—and we show that the corresponding equational theory is decidable. We achieve this by defining an automaton model, based on Petri Nets, to recognise these sets of acyclic graphs, and by providing an algorithm to compare such automata.

Families of binary relations are important interpretations of regular expressions, and the equivalence of two regular expressions with respect to their relational interpretations is decidable: the problem reduces to the equality of the denoted regular languages.

Putting together a few results from the literature, we first make explicit a generalisation of this reduction, for regular expressions extended with converse and intersection: instead of considering sets of words (i.e., formal languages), one has to consider sets of directed and labelled graphs.

We then focus on identity-free regular expressions with converse—a setting where the above graphs are acyclic—and we show that the corresponding equational theory is decidable. We achieve this by defining an automaton model, based on Petri Nets, to recognise these sets of acyclic graphs, and by providing an algorithm to compare such automata.

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. We reformulate some of their proofs in syntactic and elementary terms, and we provide a new algorithm to decide the corresponding theory. This algorithm is both simpler and more efficient; it relies on an alternative automata construction, that allows us to prove that the considered equational theory lies in the complexity class PSpace. Specific regular languages appear at various places in the proofs. Those proofs were made tractable by considering appropriate automata recognising those languages, and exploiting symmetries in those automata.