A Compositional Deadlock Detector for Android Java.

×
### Abstract

#### Go to paper

#### BibTeX entry:

A Compositional Deadlock Detector for Android Java.

We develop a static deadlock analysis for commercial Android Java applications, of sizes in the tens of millions of LoC, under active development at Facebook. The analysis runs primarily at code-review time, on only the modified code and its dependents; we aim at reporting to developers in under 15 minutes.

To detect deadlocks in this setting, we first model the real language as an abstract language with balanced re-entrant locks, nondeterministic iteration and branching, and non-recursive procedure calls. We show that the existence of a deadlock in this abstract language is equivalent to a certain condition over the sets of critical pairs of each program thread; these record, for all possible executions of the thread, which locks are currently held at the point when a fresh lock is acquired. Since the critical pairs of any program thread is finite and computable, the deadlock detection problem for our language is decidable, and in NP.

We then leverage these results to develop an open-source implementation of our analysis adapted to deal with real Java code. The core of the implementation is an algorithm which computes critical pairs in a compositional, abstract interpretation style, running in quasi-exponential time. Our analyser is built in the INFER verification framework and has been in industrial deployment for over two years; it has seen over two hundred fixed deadlock reports with a report fix rate of ∼54%.

@inproceedings{brunet26-2021, title="A Compositional Deadlock Detector for Android Java", author={Brunet, Paul and Brotherston, James and Gorogiannis, Nikos and Kanovich, Max}, year={2021}, booktitle={ASE}, }

Equivalence checking for weak bi-Kleene algebra.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

Equivalence checking for weak bi-Kleene algebra.

Pomset automata are an operational model of weak bi-Kleene algebra, which describes program that can fork an execution into parallel threads, upon completion of which execution can join to resume as a single thread. We characterize a fragment of pomset automata that admits a decision procedure for language equivalence. Furthermore, we prove that this fragment corresponds precisely to series-rational expressions, i.e., rational expressions with an additional operator for bounded parallelism. As a consequence, we obtain a new proof that equivalence of series-rational expressions is decidable.

@article{brunet16-2021, title="Equivalence checking for weak bi-Kleene algebra", author={Brunet, Paul and Kappé, Tobias and Luttik, Bas and Silva, Alexandra and Zanasi, Fabio}, year={2021}, journal={LMCS}, }

Partially Observable Concurrent Kleene Algebra.

In CONCUR,

2020.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

Partially Observable Concurrent Kleene Algebra.

In CONCUR,

2020.

We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. POCKA enables reasoning about programs that can access variables and values, which we illustrate through concrete examples. We prove that POCKA is a sound and complete axiomatisation of a model of partial observations, and show the semantics passes an important check for sequential consistency.

@inproceedings{brunet25-2020, title="Partially Observable Concurrent Kleene Algebra", author={Brunet, Paul and Docherty, Simon and Kappé, Tobias and Rot, Jurriaan and Silva, Alexandra and Wagemaker, Jana}, year={2020}, booktitle={CONCUR}, doi={"10.4230/LIPIcs.CONCUR.2020.20"}, }

Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra.

Concurrent Kleene Algebra is an elegant tool for equational reasoning about concurrent programs. An important feature of concurrent programs that is missing from CKA is the ability to restrict legal interleavings. To remedy this we extend the standard model of CKA, namely pomsets, with a new feature, called boxes, which can specify that part of the system is protect from outside interference. We study the algebraic properties of this new model. Another drawback of CKA is that the language used for expressing properties of programs is the same as that which is used to express programs themselves. This is often too restrictive for pratical purposes. We provide a logic, ‘pomset logic’, that is an assertion language for specifying such properties, and which is interpreted on pomsets with boxes. We develop the basic metatheory for the relationship between pomset logic and CKA and illustrate this relationship with simple examples.

@inproceedings{brunet22-2020, title="Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra", author={Brunet, Paul and Pym, David}, year={2020}, booktitle={FSCD}, doi={"10.4230/LIPIcs.FSCD.2020.8"}, }

Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness.

Concurrent Kleene Algebra (CKA) extends basic Kleene algebra with a parallel composition operator, which enables reasoning about concurrent programs. However, CKA fundamentally misses tests, which are needed to model standard programming constructs such as conditional and while-loops. It turns out integrating tests in CKA is subtle, due to their interaction with parallel threads. In this paper we provide a solution in the form of Concurrent Kleene Algebra with Observations (CKAO). Our main contribution is a completeness theorem for CKAO. Our result resorts on a more general study of CKA "with hypotheses", of which CKAO turns out to be an instance: this analysis is of independent interest, as it can be applied to extensions of CKA other than CKAO.

@inproceedings{brunet21-2020, title="Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness", author={Brunet, Paul and Kappé, Tobias and Silva, Alexandra and Wagemaker, Jana and Zanasi, Fabio}, year={2020}, booktitle={FoSSaCS}, doi={"10.1007/978-3-030-45231-5_20"}, }

A Complete Axiomatisation of a Fragment of Language Algebra.

In CSL,

2020.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

A Complete Axiomatisation of a Fragment of Language Algebra.

In CSL,

2020.

We consider algebras of languages over the signature of reversible Kleene lattices, that is the regular operations (empty and unit languages, union, concatenation and Kleene star) together with intersection and mirror image. We provide a complete set of axioms for the equational theory of these algebras. This proof was developed in the proof assistant Coq.

@inproceedings{brunet20-2020, title="A Complete Axiomatisation of a Fragment of Language Algebra", author={Brunet, Paul}, year={2020}, booktitle={CSL}, doi={"10.4230/LIPIcs.CSL.2020.11"}, }

A note on commutative Kleene algebra -- mathematician friendly version.

2019.

×
### Abstract

#### Go to paper

#### BibTeX entry:

A note on commutative Kleene algebra -- mathematician friendly version.

2019.

In this paper we present a detailed proof of an important result of algebraic logic: namely that the free commutative Kleene algebra is the space of semilinear sets. The first proof of this result was proposed by Redko in 1964, and simplified and corrected by Pilling in his 1970 thesis. However, we feel that a new account of this proof is needed now. This result has acquired a particular importance in recent years, since it is a key component in the completeness proofs of several algebraic models of concurrent computations (bi-Kleene algebra, concurrent Kleene algebra...). To that effect, we present a new proof of this result.

In this version of the paper, we change notations to make the paper more readable for mathematicians.

@techreport{brunet24-2019, title="A note on commutative Kleene algebra -- mathematician friendly version", author={Brunet, Paul}, year={2019}, institution={}, url={http://paul.brunet-zamansky.fr/Files/documents/commutative-kleene-algebra-math-notations.pdf}, }

A note on commutative Kleene algebra.

2019.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

A note on commutative Kleene algebra.

2019.

In this paper we present a detailed proof of an important result of algebraic logic: namely that the free commutative Kleene algebra is the space of semilinear sets. The first proof of this result was proposed by Redko in 1964, and simplified and corrected by Pilling in his 1970 thesis. However, we feel that a new account of this proof is needed now. This result has acquired a particular importance in recent years, since it is a key component in the completeness proofs of several algebraic models of concurrent computations (bi-Kleene algebra, concurrent Kleene algebra...). To that effect, we present a new proof of this result.

@techreport{brunet23-2019, title="A note on commutative Kleene algebra", author={Brunet, Paul}, year={2019}, institution={}, }

Kleene Algebra with Observations.

In CONCUR,

2019.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

Kleene Algebra with Observations.

In CONCUR,

2019.

Kleene algebra with tests (KAT) gives an algebraic perspective on reasoning about the control flow of sequential programs. However, when generalising KAT to reason about concurrent programs, axioms native to KAT in conjunction with axioms for reasoning about concurrency lead to a bizarre equation. In this paper, we propose Kleene algebra with observations (KAO), a variant of KAT, as an alternative foundation for extending KAT to a concurrent setting. We characterise the free model of KAO, and establish a decision procedure w.r.t. its equational theory.

@inproceedings{brunet19-2019, title="Kleene Algebra with Observations", author={Brunet, Paul and Kappé, Tobias and Rot, Jurriaan and Silva, Alexandra and Wagemaker, Jana and Zanasi, Fabio}, year={2019}, booktitle={CONCUR}, doi={"10.4230/LIPIcs.CONCUR.2019.41"}, }

Bracket Algebra, a nominal theory of interleaved scopes.

With Daniela Petrişan, and Alexandra Silva.

2019.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

Bracket Algebra, a nominal theory of interleaved scopes.

With Daniela Petrişan, and Alexandra Silva.

2019.

In this paper we present bracket algebra, a nominal framework that can be used in reasoning about programs with interleaved scopes. We construct a hierarchy of languages based on their memory and binding power. We present a decision procedure for program equivalence and containment for a large class of programs.

@techreport{brunet18-2019, title="Bracket Algebra, a nominal theory of interleaved scopes", author={Brunet, Paul and Petrişan, Daniela and Silva, Alexandra}, year={2019}, institution={}, }

A Kleene theorem for nominal automata.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

A Kleene theorem for nominal automata.

Nominal automata are a widely studied class of automata designed to recognise languages over infinite alphabets. In this paper, we present a Kleene theorem for nominal automata by providing a syntax to denote regular nominal languages. We use regular expressions with explicit binders for creation and destruction of names and pinpoint an exact property of these expressions – namely memory-finiteness – that identifies a subclass of expressions denoting exactly egular nominal languages.

@inproceedings{brunet17-2019, title="A Kleene theorem for nominal automata", author={Brunet, Paul and Silva, Alexandra}, year={2019}, booktitle={ICALP}, doi={"10.4230/LIPIcs.ICALP.2019.107"}, }

On Series-Parallel Pomset Languages: Rationality, Context-Freeness and Automata.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

On Series-Parallel Pomset Languages: Rationality, Context-Freeness and Automata.

Concurrent Kleene Algebra (CKA) is a formalism to study programs that exhibit concurrent behaviour. As with previous extensions of Kleene Algebra, an important tool to develop foundations and potential applications is a one-to- one correspondence between denotational and operational perspectives. This paper takes an important step towards such a correspondence, by precisely relating Bi-Kleene Algebra (BKA), a relaxed version of CKA, to a novel type of automata called pomset automata. We show that pomset automata can faithfully represent the BKA-semantics of series-parallel rational expressions, and that a (structurally restricted) class of pomset automata can be translated back to these expressions. Furthermore, we characterise the behavior of unrestricted automata in terms of context-free pomset grammars, thus yielding strong undecidability results.

@article{brunet15-2019, title="On Series-Parallel Pomset Languages: Rationality, Context-Freeness and Automata", author={Brunet, Paul and Kappé, Tobias and Luttik, Bas and Silva, Alexandra and Zanasi, Fabio}, year={2019}, journal={JLAMP}, doi={"10.1016/j.jlamp.2018.12.001"}, }

Concurrent Kleene Algebra: Free Model and Completeness.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

Concurrent Kleene Algebra: Free Model and Completeness.

Concurrent Kleene Algebra (CKA) was introduced by Hoare, Moeller, Struth and Wehrman in 2009 as a framework to reason about concurrent programs. We prove that the semantics proposed in the original paper is the free model of CKA with bounded parallel iteration, meaning the completeness of these axioms. This result settles a conjecture of Hoare and collaborators. Moreover, it allows us to establish a Kleene Theorem for CKA, extending an earlier Kleene Theorem for a fragment of CKA.

@inproceedings{brunet14-2018, title="Concurrent Kleene Algebra: Free Model and Completeness", author={Brunet, Paul and Kappé, Tobias and Silva, Alexandra and Zanasi, Fabio}, year={2018}, booktitle={ESOP}, doi={"10.1007/978-3-319-89884-1_30"}, }

On Decidability of Concurrent Kleene Algebra.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

On Decidability of Concurrent Kleene Algebra.

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.

@inproceedings{brunet13-2017, title="On Decidability of Concurrent Kleene Algebra", author={Brunet, Paul and Pous, Damien and Struth, Georg}, year={2017}, booktitle={CONCUR}, doi={"10.4230/LIPIcs.CONCUR.2017.28"}, }

Reversible Kleene lattices.

In MFCS,

2017.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

Reversible Kleene lattices.

In MFCS,

2017.

We investigate the equational theory of reversible Kleene lattices, that is algebras of languages with the regular operations (union, composition and Kleene star), together with the intersection and mirror image. Building on results by Andréka, Mikulás and Németi from 2011, we construct the free representation of this algebra. We then provide an automaton model to compare representations. These automata are adapted from Petri automata, which we introduced with Pous in 2015 to tackle a similar problem for algebras of binary relations. This allows us to show that testing the validity of equations in this algebra is decidable, and in fact ExpSpace-complete.

@inproceedings{brunet12-2017, title="Reversible Kleene lattices", author={Brunet, Paul}, year={2017}, booktitle={MFCS}, doi={"10.4230/LIPIcs.MFCS.2017.66"}, }

Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages.

Concurrent Kleene Algebra (CKA) is a mathematical formalism to study programs that exhibit concurrent behaviour. As with previous extensions of Kleene Algebra, characterizing the free model is crucial in order to develop the foundations of the theory and potential applications. For CKA, this has been an open question for a few years and this paper makes an important step towards an answer. We present a new automaton model and a Kleene-like theorem for pomset languages, which are a natural candidate for the free model. There are two substantial differences with previous work: from expressions to automata, we use Brzozowski derivatives, which enable a direct construction of the automaton; from automata to expressions, we provide a syntactic characterization of the automata that denote valid CKA behaviours.

@inproceedings{brunet11-2017, title="Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages", author={Brunet, Paul and Kappé, Tobias and Luttik, Bas and Silva, Alexandra and Zanasi, Fabio}, year={2017}, booktitle={CONCUR}, doi={"10.4230/LIPIcs.CONCUR.2017.25"}, }

Petri automata.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

Petri automata.

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.

@article{brunet8-2017, title="Petri automata", author={Brunet, Paul and Pous, Damien}, year={2017}, journal={LMCS}, doi={"10.23638/LMCS-13(3:33)2017"}, }

Algebras of relations: from algorithms to formal proofs.

PhD thesis, Université de Lyon,

2016.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

Algebras of relations: from algorithms to formal proofs.

PhD thesis, Université de Lyon,

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

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

A formal exploration of nominal Kleene algebra.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

A formal exploration of nominal Kleene algebra.

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.

@inproceedings{brunet6-2016, title="A formal exploration of nominal Kleene algebra", author={Brunet, Paul and Pous, Damien}, year={2016}, booktitle={MFCS}, doi={"10.4230/LIPIcs.MFCS.2016.22"}, }

Cardinalities of finite relations in Coq.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

Cardinalities of finite relations in Coq.

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.

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

Algorithms for Kleene algebra with converse.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

Algorithms for Kleene algebra with converse.

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{brunet4-2016, title="Algorithms for Kleene algebra with converse", author={Brunet, Paul and Pous, Damien}, year={2016}, journal={JLAMP}, doi={"10.1016/j.jlamp.2015.07.005"}, }

Petri automata for Kleene allegories.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

Petri automata for Kleene allegories.

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.

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

Decidability of identity-free relational Kleene lattices.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

Decidability of identity-free relational Kleene lattices.

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{brunet2-2015, title="Decidability of identity-free relational Kleene lattices", author={Brunet, Paul and Pous, Damien}, year={2015}, booktitle={JFLA}, url={https://hal.inria.fr/hal-01099137}, }

Kleene algebra with converse.

×
### Abstract

#### Go to paper

#### Related resources

#### BibTeX entry:

Kleene algebra with converse.

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.

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