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 and a constant which are natural in binary relation models: intersection, converse, and the full relation. While regular languages are closed under those operations, the above characterisation breaks. Putting together a few results from the literature, we give a characterisation in terms of languages of directed and labelled graphs. By taking inspiration from Petri nets, we design a finite automata model, Petri automata, allowing to recognise such graphs. We prove a Kleene theorem for this automata model: the sets of graphs recognisable by Petri automata are precisely the sets of graphs definable through the extended regular expressions we consider. Petri automata allow 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. We actually show that this decision problem is EXPSPACE-complete.

@phdthesis{brunet10-2016, school={Université de Lyon}, title="Algebras of relations: from algorithms to formal proofs", year={2016}, url={https://tel.archives-ouvertes.fr/tel-01455083v1}, author={Brunet, Paul} }

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 thesis was to export known results from Kleene algebra to some of its extensions.

We first considered a known extension: Kleene algebras with converse. Decidability of these algebras was already known, but the algorithm witnessing this result was too complicated to be practical. We proposed a simpler algorithm, which is more efficient, and whose correctness is easier to establish. It allowed us to prove that this problem lies in the complexity class PSpace-complete.

Then we studied Kleene allegories. Few results were known about this extension. Following results about closely related algebras, we established the equivalence between equality in Kleene allegories and the equality of certain sets of graphs. We then developed a new automaton model (so-called Petri automata), based on Petri nets. We proved the equivalence between the original problem and comparing these automata. In the restricted setting of identity-free Kleene lattices, we also provided an algorithm performing this comparison. This algorithm uses exponential space. However, we proved that the problem of comparing Petri automata lies in the class ExpSpace- complete.

Finally, we studied Nominal Kleene algebras. We realised that existing descriptions of these algebra were not suited to relational semantics of programming languages. We thus modified them accordingly, and doing so uncovered several natural variations of this model. We then studied formally the bridges one could build between these variations, and between the existing model and our new version of it. This study was conducted using the proof assistant Coq.

@inproceedings{brunet5-2016, booktitle={ITP}, title="Cardinalities of finite relations in Coq", year={2016}, url={http://dx.doi.org/10.1007/978-3-319-43144-4_29}, author={Brunet, Paul and Pous, Damien and Stucke, Insa} }

In this paper we present an extension of a Coq library for relation algebras and related algebraic structures. So far, the library did not provide any tools about the cardinalities of relations. Thus we add an algebraic axiomatisation of cardinalities. Its point-free nature makes it possible to reason about cardinal purely algebraically, which is well- suited for mechanisation. We present several applications, in the area of graph theory and program verification.

@article{brunet4-2016, journal={JLAMP}, title="Algorithms for Kleene algebra with converse", year={2016}, url={http://www.sciencedirect.com/science/article/pii/S2352220815000772}, author={Brunet, Paul and Pous, Damien} }

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.

@inproceedings{brunet3-2015, booktitle={LICS}, title="Petri automata for Kleene allegories", year={2015}, url={http://dx.doi.org/10.1109/LICS.2015.17}, author={Brunet, Paul and Pous, Damien} }

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 intersection (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.

@inproceedings{brunet1-2014, booktitle={RAMICS}, title="Kleene algebra with converse", year={2014}, url={http://dx.doi.org/10.1007/978-3-319-06251-8_7}, author={Brunet, Paul and Pous, Damien} }

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.