Reversible Kleene lattices

Paul Brunet

► To cite this version:

Paul Brunet. Reversible Kleene lattices. 42nd International Symposium on Mathematical Foundations of Computer Science, Kim G. Larsen, Aug 2017, Aalborg, Denmark. pp.66:1–66:14, 10.4230/LIPIcs.MFCS.2017.66 . hal-01474911v3

HAL Id: hal-01474911

https://hal.science/hal-01474911v3

Submitted on 21 Jun 2017

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Reversible Kleene Lattices

Paul Brunet¹

1 University College London

paul@brunet-zamansky.fr

## Abstract

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.

**1998 ACM Subject Classification** F.4.3 Formal Languages, F.1.1 Models of Computation, F.3.2 Semantics of Programming Languages.

**Keywords and phrases** Kleene algebra, Automata, Petri nets, Decidability, Complexity.

**Digital Object Identifier** 10.4230/LIPIcs...

## 1 Introduction

We are interested in algebras of languages, equipped with the constants empty language ($0$), unit language ($1$), the language containing only the empty word), the binary operations of union ($+$), intersection ($\cap$), and concatenation ($\cdot$), and the unary operations of Kleene star ($\_*$) and mirror image, also called converse, ($\_\sim$). We call these algebras *reversible Kleene lattices*. Given a finite set of variables $X$, and two terms $e, f$ built from variables and the above operations, we say that the equation $e = f$ (respectively inequation $e \leq f$) is valid if the corresponding equality (resp. containment) holds universally. A *free representation* is a set $\mathcal{M}$ together with a map $h$ from terms to elements of $\mathcal{M}$ such that $e = f$ is valid if and only if $h$ maps $e$ and $f$ to the same element of $\mathcal{M}$.

It is well known that to any term over this syntax, one can associate a regular language, and that comparing regular languages is decidable. In fact, the problem of comparing regular expressions with intersection with respect to regular language equivalence is EXPSPACE-complete [11]. The difference with the work presented here is that we are considering equations which are stable under substitution. Formally, this means that we do not interpret the letter $a$ as the singleton language $\{a\}$, but rather as a universally quantified variable ranging over all languages. What is remarkable however is that testing the validity of equations in reversible Kleene lattices is still an EXPSPACE-complete problem, as we show in this paper. Several fragments of this algebra have been studied:

**Kleene algebra (KA) [8]:** if we restricts ourselves to the operators of regular expressions ($0$, $1$, $+$, $\cdot$, and $\_*$), then the free representation is the set of regular languages, with the usual definition of the language of an expression. Testing the validity of equations in KA is thus a PSPACE-complete problem [18, 13].

**Kleene algebra with converse (KAC) [3]:** if we add to KA the converse operation, then the free representation consists of regular expressions over a duplicated alphabet, with a

<figure><img src="image_2.png" /></figure>
letter $a'$ denoting the converse of the letter $a$. The associated decision problem is still in PSPACE.

**Identity-free Kleene lattices (KL⁻) [1]:** this algebra stems from the operators 0, +, ·, ∩ and _⁺_, where the latter is the non-zero iteration. Andréka Mikulás and Németi studied this fragment, and showed that the free representation of this algebra consists of languages of series-parallel graphs, downward closed with respect to some graph preorder. We reformulated their results with Pous [5], and introduced a new class of automata, called Petri automata, able to recognise these languages of graphs. In [5] we provided a decision procedure to compare these automata, thus yielding an EXPSPACE decision procedure for the equational theory of this algebra. It is in fact EXPSPACE-complete, thanks to some simple adaptation of a result by Fürer [11].

The present work is then an extension of identity-free Kleene lattices, by adding unit and mirror image. The addition of mirror image is fairly simple, relying mainly on ideas from [3]. However, the seemingly small addition of 1 yields some complications. In fact, in [1, 5] there is a free representation of Kleene allegories, an algebra over the same signature as reversible Kleene lattices, but whose intended model is binary relations rather than languages. In this context, adding 1 means moving from *series-parallel* graphs to graphs of tree-width 2, which might have cycles. This is a significant problem for automata based decision procedures.

In the context of languages, adding 1 yields other problems. However, the free representation we get for reversible Kleene lattices remains more tractable than that of Kleene allegories. In particular we do not create cycles in series parallel graphs, but rather have to collect additional information. Let us illustrate the kind of reasoning we develop to study these algebras with the following inequation:

$$c \cdot (1 \cap a) \leq a \cdot c. \qquad (1)$$

On the left hand side (LHS), the term $1 \cap a$ appears. This term is either equal to 1 if the empty word belongs to language $a$, or 0 otherwise. In the first case, the LHS is equal to $c$ and we have $1 \leq a$, meaning that $c = 1 \cdot c \leq a \cdot c$. In the second case the LHS is equal to 0, which is contained in $a \cdot c$ as well. The key observation here is that the second case does not really matter: in a term build out of concatenations, intersections, converse, variables and units, if 0 appears somewhere then the term will always evaluate to 0 and thus be contained in any other term. The free representations we develop for union-free terms consist of pairs of a representation of a 1-free term and a set of language variables which are assumed to contain the empty word. This allows us to make the reasoning we used to study (1) automatic.

Following an approach similar to [5], we construct in Section 2 the free representation of reversible Kleene lattices, and introducing a new Petri net-based automata model we show in Section 3 that testing the validity of equations is a decidable problem, and in fact an EXPSPACE-complete one. We conclude and list some perspectives in Section 4.

## Basic definitions and notations

For a pair $p = (x, y)$, we denote by $\pi_1(p) = x$ the first projection, and by $\pi_2(p) = y$ the second projection. The set of functions from a set $A$ to a set $B$ is written $A \to B$, and the set of partial functions from $A$ to $B$ is written $A \to B$. The number of elements of a finite set $A$ is written $|A|$. The empty word is denoted by $\varepsilon$, and the set of words over the alphabet $\Sigma$ is $\Sigma^*$. If $w = x_1...x_n$ is a word of length $n$, $w[i, j]$ is the word $x_i...x_j$ if $i \leq j$, and undefined otherwise. If $f$ is a function from some set $X$ to $\{0, ..., n\}$, $x, y$ are elements of $X$, and if $f(x) \leq f(y)$, we use the notation $w^f[x, y]$ for the word $w[f(x), f(y)]$.
<figure><img src="image_3.png" /><figcaption>Figure 1 Graphs associated to terms.</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Figure 2 Graph homomorphism.</figcaption></figure>

Let $X$ be a finite set of variables, we define $\tilde{A} := A \cup \{a^{\sim} | a \in A\}$ for every subset $A \subseteq X$.
The set $\tilde{X}$ is called the duplicated alphabet, we let $\alpha, \beta$ range over $\tilde{X}$. Expressions over $X$ are given by the following grammar:

$$e, f ::= 0 \mid 1 \mid x \mid e^{\sim} \mid e+f \mid e \cdot f \mid e \cap f \mid e^*. \qquad (x \in X)$$

The set of expressions over $X$ is written $\mathcal{E}\langle X \rangle$. The size of an expression $e$, written $|e|$, is its number of symbols, i.e. the number of vertices in its syntax tree. Most of the time, we will implicitly assume that the converse operator only appears as $x^{\sim}$, with $x \in X$. This is not restrictive, as every expression can be transformed linearly such that this property holds. Given a second alphabet $\Sigma$, an interpretation is a map $\sigma : X \to \mathcal{P}(\Sigma^*)$ which associates to every variable $a$ a language $\sigma(a)$. This map can be uniquely extended to a homomorphism $\hat{\sigma} : \mathcal{E}\langle X \rangle \to \mathcal{P}(\Sigma^*)$ defined inductively:

$$\begin{align*}
\hat{\sigma}(0) &= \emptyset & \hat{\sigma}(1) &= \{\varepsilon\} & \hat{\sigma}(a) &= \sigma(a) & \hat{\sigma}(e^{\sim}) &= \hat{\sigma}(e)^{\sim} &= \{x_n \dots x_1 \mid x_1 \dots x_n \in \hat{\sigma}(e)\} \\
\hat{\sigma}(e+f) &= \hat{\sigma}(e) \cup \hat{\sigma}(f) & \hat{\sigma}(e \cdot f) &= \hat{\sigma}(e) \cdot \hat{\sigma}(f) & \hat{\sigma}(e \cap f) &= \hat{\sigma}(e) \cap \hat{\sigma}(f) \\
& & \hat{\sigma}(e^*) &= \hat{\sigma}(e)^* &= \{w_1 \dots w_n \mid w_i \in \hat{\sigma}(e)\}.
\end{align*}$$

We say that $e = f$ (respectively $e \le f$) is valid, and write $\text{Lang} \models e = f$ (resp. $\text{Lang} \models e \le f$), when for every interpretation $\sigma$, we have $\hat{\sigma}(e) = \hat{\sigma}(f)$ (resp. $\hat{\sigma}(e) \subseteq \hat{\sigma}(f)$).

It is interesting to note that as decision problems, the validity of equations and that of inequations are equivalent. Indeed, the following equivalences hold:

$$\text{Lang} \models e = f \Leftrightarrow \text{Lang} \models e \le f \wedge \text{Lang} \models f \le e \qquad \text{Lang} \models e \le f \Leftrightarrow \text{Lang} \models e + f = f.$$

# 2 The free representation of reversible Kleene lattices

## 2.1 Intuitions

First introduced in the context of relation algebra [2, 10], directed labelled 2-pointed graphs can be used to describe the algebra of languages over the signature $\langle \cdot, \cap \rangle$. First, we associate to every term $u$ over this signature such a graph $G(u)$. See Figure 1 for examples. The set of such graphs is equipped with a preorder: $G$ is smaller than $H$ if there is a graph homomorphism from $H$ to $G$. Such a homomorphism is illustrated in Figure 2, with dotted arrows.

Already, this gives us a clue as to the (in)equational theory: the inequation $u \le v$ is valid if and only if $G(u)$ is smaller than $G(v)$. Moving to identity-free Kleene lattices, i.e. to
<figure><img src="image_5.png" /><figcaption>Figure 3 Weak graph morphism: $\langle G, \{a\} \rangle \triangleleft \langle H, \emptyset \rangle$</figcaption></figure>

the signature $\langle 0, + , \cdot , \cap , \_ + \rangle$, we associate to every term $e$ a set $\mathcal{G}(e)$ of such graphs, and then take its downward closure $\mathcal{G}(e) \downarrow$ with respect to the preorder. This yields the free representation of this algebra: the equation $e = f$ is valid if and only if $\mathcal{G}(e) \downarrow = \mathcal{G}(f) \downarrow$.

To move from identity free Kleene lattices to reversible Kleene lattices, two steps are necessary: we need to add the converse, and to add the constant 1. The first step is somewhat straightforward, thanks to results by Ésik et al. [3]: they showed that the free representation of the algebra of languages with the regular operations together with converse is simply the set of regular languages over a duplicated alphabet, where we add for every letter a new letter representing its converse. This approach works well in our setting, by considering graphs labelled with the duplicated alphabet.

For the second step, we draw our inspiration from Lemma 3.4 in [1], that established
that every term in $\mathcal{E}\langle X \rangle$ is equivalent to a finite sum of terms of the form $(1 \cap a \cap b \dots) \cdot e$, where $a, b, \dots \in X$ are letters, and 1 does not appear in $e$. For every interpretation $\sigma: X \to \mathcal{P}(\Sigma^*)$, if there is some variable $x \in \{a, b, \dots\}$ such that $\varepsilon \notin \sigma(x)$, then the interpretation of $1 \cap a \cap b \cap \dots$ is $\emptyset$. Otherwise, if the empty word is in the interpretation of each of the $a, b, \dots$, then the interpretation is $\{\varepsilon\}$. If we now look at the interpretation of the whole term, this means that:

$$
\hat{\sigma}((1 \cap a \cap b \cap \dots) \cdot e) = \begin{cases} \hat{\sigma}(e) & \text{if } \forall x \in \{a, b, \dots\}, \varepsilon \in \sigma(x); \\ \emptyset & \text{otherwise.} \end{cases}
$$

Consider now an inequation $f_1 \le f_2$, where $f_i = (1 \cap a_{i,1} \cap \cdots \cap a_{i,n_i}) \cdot e_i$ for $i \in \{1,2\}$. If there exists a variable $x \in \{a_{2,1}, \dots, a_{2,n_2}\} \setminus \{a_{1,1}, \dots, a_{1,n_1}\}$, we can build an interpretation $\sigma$ such that $(1) \ \varepsilon \notin \sigma(x)$ and $(2) \ \hat{\sigma}(f_1) \ne \emptyset$. The first condition ensures that the image of $f_2$ will be $\emptyset$, hence the inequation is not valid. Thus for the inequation to be valid, we need that $\{a_{2,1}, \dots, a_{2,n_2}\} \subseteq \{a_{1,1}, \dots, a_{1,n_1}\}$. Furthermore, for every $\sigma$ such that there is an $a_{1,i}$ whose interpretation does not contain the empty word, the image of $f_1$ will be $\emptyset$, which is trivially contained in the image of the $f_2$. We reach the following equivalence: $f_1 \le f_2$ is valid if and only if $(1) \ \{a_{2,1}, \dots, a_{2,n_2}\} \subseteq \{a_{1,1}, \dots, a_{1,n_1}\}$ and $(2) \ \text{for every interpretation} \ \sigma$ such that the empty word is in the interpretation of every } a_{1,j}, \text{ we have } \hat{\sigma}(e_1) \subseteq \hat{\sigma}(e_2)$. This means that we need to compare 1-free expressions under the assumption that certain variables contain the empty word.

This is the intuitions behind what we call weak graphs. Weak graphs are pairs of a graph and a set of test variables. They are equipped with a preorder relation $\triangleleft$, which relates $\langle G, A \rangle$ and $\langle H, B \rangle$ if $B \subseteq A$ and there is a map $\varphi$ from $H$ to $G$ such that every edge labelled outside of $A$ is preserved, but edges labelled with tests in $A$ are either preserved or contracted. Such a map is shown in Figure 3.

We then have theorems similar to those for identity free Kleene lattices and series
parallel graphs, in the sense that for every pair of terms $u, v$ over the syntax $\langle \cdot, \cap, 1, \_ \rangle$,
if we denote by $WG(u), WG(v)$ their associated weak graphs, $u \le v$ is valid if and only if
$WG(u) \triangleleft WG(v)$. Furthermore, if we associate to every expression $e$ in $\mathcal{E}\langle X \rangle$ a downwards closed set of weak graphs $\triangleleft\llbracket e \rrbracket$, the equation $e = f$ is valid if and only if $\triangleleft\llbracket e \rrbracket = \triangleleft\llbracket f \rrbracket$.

## 2.2 Weak terms

We define the following two sets of terms over the alphabet $X$:

**Ground terms:** $u, v \in GT\langle X \rangle ::= 1 \mid a \mid a^\sim \mid u \cdot v \mid u \cap v$.

**Simple ground terms:** $u, v \in GT^-\langle X \rangle ::= a \mid a^\sim \mid u \cdot v \mid u \cap v$.

We call the variables of the term $u$, and write $var(u)$, the set of variables $a \in X$ such that $a$ or $a^\sim$ appears in $u$. We call weak terms the elements of the set $(GT^-\langle X \rangle \cup \{1\}) \times \mathcal{P}(X)$, that is simple ground terms or 1 indexed with a set of test variables. The set of weak terms is written $WT\langle X \rangle$. This set is equipped with two products, denoted by $\bullet$ and $\parallel$, defined as follows:

$$1_A \bullet 1_B := 1_{A \cup B}$$

$$1_A \bullet u_B = u_A \bullet 1_B := u_{A \cup B}$$

$$u_A \bullet v_B := (u \cdot v)_{A \cup B}$$

$$1_A \parallel 1_B := 1_{A \cup B}$$

$$1_A \parallel u_B = u_A \parallel 1_B := 1_{A \cup B \cup var(u)}$$

$$u_A \parallel v_B := (u \cap v)_{A \cup B}$$

Given an interpretation $\sigma: X \to \mathcal{P}(\Sigma^*)$, the interpretation $\tilde{\sigma}(u_A)$ of the weak term $u_A$ is either $\emptyset$ if $\exists a \in A: \varepsilon \notin \sigma(a)$, or $\hat{\sigma}(u)$ otherwise. We define a translation $\tau$ from ground terms to weak terms:

$$\tau(u \cdot v) := \tau(u) \bullet \tau(v)$$

$$\tau(u \cap v) := \tau(u) \parallel \tau(v)$$

$$\forall u \in \{1\} \cup \dot{X}, \tau(u) := u_\emptyset.$$

This translation is faithful, in the sense that the following holds:

**Lemma 1.** $\forall u \in GT\langle X \rangle, \forall \sigma: X \to \mathcal{P}(\Sigma^*), \hat{\sigma}(u) = \tilde{\sigma} \circ \tau(u)$.

**Proof (Sketch).** The proof relies on the fact that for every pair of weak terms $x, y$ we have:

$$\tilde{\sigma}(x \bullet y) = \tilde{\sigma}(x) \cdot \tilde{\sigma}(y)$$

$$\tilde{\sigma}(x \parallel y) = \tilde{\sigma}(x) \cap \tilde{\sigma}(y)$$

We then conclude by a simple induction on $u$. For concision, the full proof is omitted here. ◀

We can also define a converse translation $\kappa: WT\langle X \rangle \to GT\langle X \rangle$ which associate to a weak term $u_{\{a_1, \dots, a_n\}}$ the ground term $(1 \cap a_1 \cap \dots \cap a_n) \cdot u$. It is immediate to check that for every term $x \in WT\langle X \rangle$ and every interpretation $\sigma$ we have $\tilde{\sigma}(x) = \hat{\sigma} \circ \kappa(x)$.

## 2.3 Weak graphs

A graph $G$ in our setting is a tuple $\langle V_G, E_G, i_G, o_G \rangle$, where $V_G$ is a finite set of vertices, $E_G \subseteq V_G \times \dot{X} \times V_G$ is a set of labelled and directed edges, and $i_G, o_G \in V_G$ are two vertices, called the input and output of the graph. Term graphs must further be series parallel[22], $i_G$ must be the unique source vertex (i.e. with no incoming edge), and $o_G$ the unique sink vertex (i.e. with no outgoing edge). We let $G, H$ range over graphs. Term graphs can be sequentially composed, by identifying the output of the first graph with the input of the second one, or composed in parallel, by identifying the inputs of both graphs and identifying theirs outputs. These two compositions are respectively denoted by $;$ and $|$. The set $\ell(G)$ of labels of a graph $G$ is defined as the set of letters $a \in X$ such that there is an edge in $E_G$ labelled with either $a$ or $a^\sim$.

The graph of a simple ground term $u$, written $\mathcal{G}(u)$, is a term graph defined inductively:

$$\mathcal{G}(\alpha) := \xrightarrow{\alpha} \bullet \xrightarrow{\alpha} \bullet$$

$$\mathcal{G}(u \cdot v) := \mathcal{G}(u); \mathcal{G}(v)$$

$$\mathcal{G}(u \cap v) := \mathcal{G}(u) | \mathcal{G}(v).$$
We define the graph $\mathbb{1}$ as $\xrightarrow{\phantom{\text{---}}\xrightarrow{\text{---}}\phantom{\text{---}}}$ . Notice that it is not a term graph, as it is not series parallel. We call weak graph a pair whose left part is either a term graph or $\mathbb{1}$, and whose right part is a set of test variables. We denote the weak graph $\langle G, A \rangle$ by $G_A$. For every weak term $x$ we associate a weak graph $WG(x)$ as one would expect:

$WG(1_A) := 1_A$

$WG(u_A) := G(u)_A.$

The weak graph $G_A$ is smaller than $H_B$, written $G_A \triangleleft H_B$, if $B \subseteq A$ and there exists a function $\varphi : V_H \to V_G$ such that $\varphi(i_H) = i_G$, $\varphi(o_H) = o_G$, and for every edge $\langle x, \alpha, y \rangle$ in $E_H$, either $\langle \varphi(x), \alpha, \varphi(y) \rangle \in E_G$ or $\alpha \in \dot{A}$ and $\varphi(x) = \varphi(y)$. The relation $\triangleleft$ is a preorder. We will show in the next section that for any two ground terms $u$ and $v$, the following holds:

$$ \text{Lang} \models u \leq v \Leftrightarrow WG(\tau(u)) \triangleleft WG(\tau(v)). $$

The first important lemma is the following. It generalises [1, Lemma 2.5] by including $\mathbb{1}$ and $\dot{\mathbb{1}}$, thus moving from series parallel graphs to weak graphs.

**Lemma 2.** $\forall u \in WT(X)$, there exists a word $w_u$ and an interpretation $\sigma_u$ such that for every $v \in WT(X)$, $w_u \in \tilde{\sigma}_u(v) \Leftrightarrow WG(u) \triangleleft WG(v)$.

**Proof.** Let $WG(u) = \langle\langle V_u, E_u, i_u, o_u \rangle, A \rangle$. Let $\mu : V_u \to \{1, \dots, |V_u|\}$ be a bijective map such that $\langle x, \alpha, y \rangle \in E_u \Rightarrow \mu(x) < \mu(y)^1$. In particular, $\mu(i_u) = 1$ and $\mu(o_u) = |V_u|$. Let $n = 2 \times (|V_u| - 1)$, and $\Sigma_u$ an alphabet composed of $n$ distinct letters $x_1, \dots, x_n$.

We define $w_u = x_1x_2\dots x_n$, and $f : V_u \to \{0, \dots, n\}$ such that $f(x) = 2(\mu(x) - 1)$. Notice that $f(i_u) = 0$ and $f(o_u) = n$. We now define $\sigma_u$:

$$ \sigma_u(a) := \left\{ \begin{array}{ll} \{w_u^f[x, y] \mid \langle x, a, y \rangle \in E_u\} \cup \{w_u^{\tilde{f}}[x, y] \mid \langle x, a, y \rangle \in E_u\} & \text{if } a \in A \\ \{w_u^f[x, y] \mid \langle x, a, y \rangle \in E_u\} \cup \{w_u^{\tilde{f}}[x, y] \mid \langle x, a, y \rangle \in E_u\} & \text{if } a \notin A \end{array} \right. $$

Notice that for every $\alpha \in \dot{X}$, $\varepsilon \in \hat{\sigma}_u(\alpha) \Leftrightarrow \alpha \in \dot{A}$, and that if $x \neq y$ then $w_u^f[x, y] \in \hat{\sigma}_u(\alpha)$ if and only if $\langle x, \alpha, y \rangle \in E_u$.

Let $v = t_B \in WT(X)$. First, suppose that $\exists a \in B \setminus A$. We know that $\varepsilon \notin \sigma_u(a)$, meaning that $\tilde{\sigma}_u(v) = \emptyset$. We also know by definition of $\triangleleft$ that $WG(u) \triangleleft WG(v)$. Thus the equivalence holds, as both sides are false. In the following, we thus assume that $B \subseteq A$.

If $t = 1$, then $\tilde{\sigma}_u(v) = \{\varepsilon\}$. This means that $w_u \in \tilde{\sigma}_u(v)$ if and only if $w_u = \varepsilon$. By definition, this is equivalent to $n = 0$, which is again equivalent to $|V_u| = 1$ thus to $u = 1_A$. It is not hard to check that the only graph $G$ such that $G_A \triangleleft 1_B$ is $\mathbb{1}$ itself, thus proving the desired equivalence.

The other case is when $t$ is a simple ground term. Then an induction much like in the proof of [1, Lemma 2.5] allows to conclude. We omit this part of the proof here. $\triangleleft$

The other important lemma is a generalisation of [1, Lemma 2.3]. It will allow us to factor any interpretation of $u$ through the weak graph $WG(u)$.

**Lemma 3.** For every simple ground term $u$, every interpretation $\sigma : X \to \mathcal{P}(\Sigma^*)$, and every word $w \in \Sigma^*$ of length $n$:

$$ w \in \hat{\sigma}(u) \Leftrightarrow \exists \varphi : V_u \to \{0, \dots, n\} : \left\{ \begin{array}{l} \varphi(i_u) = 0 \land \varphi(o_u) = n \\ \langle x, \alpha, y \rangle \in E_u \Rightarrow w^\varphi[x, y] \in \hat{\sigma}(\alpha). \end{array} \right. $$

It can be proved by a simple induction on $u$; for concision, we omit this proof.

<footnote n="1">¹ Remember that both term graphs and $\mathbb{1}$ are directed acyclic graphs.</footnote>
## 2.4 Freeness results

We can now establish our first freeness result:

**Theorem 4.** $\forall x, y \in \mathcal{GT}(X), \mathcal{WG}(\tau(x)) \triangleleft \mathcal{WG}(\tau(y)) \Leftrightarrow \text{Lang} \models x \leq y.$

**Proof.** The statement of the theorem is equivalent to the following, thanks in part to Lemma 1: $\forall x, y \in \mathcal{WT}(X), \mathcal{WG}(x) \triangleleft \mathcal{WG}(y) \Leftrightarrow \forall \Sigma, \forall \sigma : X \to \mathcal{P}(\Sigma^*), \tilde{\sigma}(x) \subseteq \tilde{\sigma}(y)$. We let $x = u_A$ and $y = v_B$, and proceed to prove both implications.

Suppose $\mathcal{WG}(x) \triangleleft \mathcal{WG}(y)$, let $\sigma$ be an interpretation, and $w$ a word of length $n$. The case of 1 being trivial, we consider here the case where both $u$ and $v$ are simple ground terms. Assume $w \in \tilde{\sigma}(x)$, then we need to prove that $w \in \tilde{\sigma}(y)$. First notice that because $\tilde{\sigma}(x) \neq \emptyset$ it must be the case that $\forall a \in A, \varepsilon \in \sigma(a)$. By Lemma 3, we have a function $\varphi: V_u \to \{0, \dots, n\}$ such that $\varphi(i_u) = 0$, $\varphi(o_u) = n$, and $\langle x, \alpha, y \rangle \in E_u \Rightarrow w^\varphi[x, y] \in \hat{\sigma}(\alpha)$. By definition of $\triangleleft$, we also have a function $\psi: V_v \to V_u$ such that $\psi(i_v) = i_u$, $\psi(o_v) = o_u$, and for every edge $\langle x, \alpha, y \rangle$ in $E_v$, either $\langle \psi(x), \alpha, \psi(y) \rangle \in E_u$ or $\alpha \in \hat{A}$ and $\psi(x) = \psi(y)$. We define $\Phi = \varphi \circ \psi$. Now we may check that $\Phi(i_v) = \varphi(i_u) = 0$; $\Phi(o_v) = \varphi(o_u) = n$; and if $\langle x, \alpha, y \rangle \in E_v$, then either

$\langle \psi(x), \alpha, \psi(y) \rangle \in E_u$, which means $w^\Phi[x, y] = w^\varphi[\psi(x), \psi(y)] \in \hat{\sigma}(\alpha)$;

or $\alpha \in \hat{A}$ and $\psi(x) = \psi(y)$, which entails $w^\Phi[x, y] = \varepsilon \in \hat{\sigma}(\alpha)$.

Using Lemma 3 again, we get that $w \in \hat{\sigma}(v)$. Because $B \subseteq A$, we also have that $\tilde{\sigma}(y) = \hat{\sigma}(v)$. Hence $\tilde{\sigma}(x) \subseteq \tilde{\sigma}(y)$.

For the converse, we now assume that $\mathcal{WG}(x) \triangleleft \mathcal{WG}(y)$. Using Lemma 2, we know that $w_x \in \tilde{\sigma}_x(x)$ and that $w_x \notin \tilde{\sigma}_x(y)$. This proves that $\tilde{\sigma}_x(x) \not\subseteq \tilde{\sigma}_x(y)$. $\triangleleft$

We define the set of weak terms $[[e]]$ of an expression $e$ by structural induction:

$$[[0]] := \emptyset$$

$$[[1]] := \{1_\emptyset\}$$

$$[[\alpha]] := \{\alpha_\emptyset\}$$

$$[[e+f]] := [[e]] \cup [[f]]$$

$$[[e \cdot f]] := \{u \bullet v \mid u \in [[e]] \wedge v \in [[f]]\}$$

$$[[e \cap f]] := \{u \parallel v \mid u \in [[e]] \wedge v \in [[f]]\}$$

$$[[e^*]] := \{u_1 \bullet \dots \bullet u_n \mid n \geq 0 \wedge \forall 0 \leq i \leq n, u_i \in [[e]]\}$$

The downward closure $\triangleleft S$ of a set of weak terms $S$ is the set of weak terms $x$ such that there exists a weak term $y \in S$ satisfying $\mathcal{WG}(x) \triangleleft \mathcal{WG}(y)$. The function $\triangleleft$ is a closure operator. The set of downward closed sets of weak terms is the free representation of reversible Kleene lattices:

**Theorem 5.** $\forall e, f \in \mathcal{E}(X): \triangleleft[[e]] \subseteq \triangleleft[[f]] \Leftrightarrow \text{Lang} \models e \leq f.$

**Proof.** We use the fact that for every interpretation $\sigma$,

$$\hat{\sigma}(e) = \bigcup_{u \in [[e]]} \tilde{\sigma}(u) = \bigcup_{u \in \triangleleft[[e]]} \tilde{\sigma}(u).$$

This can be proved using [1, Lemma 2.1], and Lemmas 1 and 2 and Theorem 4.

Suppose $\triangleleft[[e]] \subseteq \triangleleft[[f]]$, and let $\sigma$ be an interpretation.

$$\hat{\sigma}(e) = \bigcup_{u \in \triangleleft[[e]]} \tilde{\sigma}(u) \subseteq \bigcup_{u \in \triangleleft[[f]]} \tilde{\sigma}(u) = \hat{\sigma}(f).$$

For the converse, suppose $\triangleleft[[e]] \not\subseteq \triangleleft[[f]]$. Because $\triangleleft$ is a closure operator, this means $[[e]] \not\subseteq \triangleleft[[f]]$. Let $u \in [[e]] \setminus \triangleleft[[f]]$. By Lemma 2, we have $w_u \in \tilde{\sigma}_u(u) \subseteq \hat{\sigma}_u(e)$, but because $u \notin \triangleleft[[f]]$, for every $v \in [[f]]$, we have $\mathcal{WG}(u) \triangleleft \mathcal{WG}(v)$ thus $w_u \notin \tilde{\sigma}_u(v)$. Hence $w_u$ is not in the set $\bigcup_{v \in [[f]]} \tilde{\sigma}_u(v) = \hat{\sigma}_u(f)$. $\triangleleft$
<figure><img src="image_6.png" /><figcaption>Figure 4 Weak Petri automaton.</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>Figure 5 A run $R$ in the automaton of Figure 4.</figcaption></figure>

<figure><img src="image_8.png" /><figcaption>Figure 6 Trace of $R$.</figcaption></figure>

### 3 Decidability and complexity

To decide the equational theory of identity-free Kleene lattices, we used Petri automata[5]. This was a new style of automaton, which was designed to recognise sets of series parallel graphs. We modify this model slightly to recognise weak graphs, provide a construction to build automata out of expressions, and an algorithm to decide language containment (up-to closure by $\triangleleft$) for these automata. This algorithm itself is inspired by the simulation algorithm for simple Petri automata. We conclude this section by showing that the problem is complete of the class EXPSPACE.

#### 3.1 Weak Petri automata

A weak Petri automaton is a Petri automaton [5, 4] whose transitions are labelled with sets of letters<fnref n="2" />. Formally, an automaton $\mathcal{A}$ over the finite alphabet $X$ is a triple $\langle P, T, \iota \rangle$ where $P$ is a finite set of places, $\iota \in P$ is the initial place, and $T \subseteq \mathcal{P}(P) \times \mathcal{P}(X) \times \mathcal{P}(\dot{X} \times P)$ is a set of transitions. Each transition $t \in T$ is composed of three parts: its input $\succ t \subseteq P$, its set of tests $\hat{t} \subseteq X$, and its output $t \succ \dot{X} \times P$. It will also be useful to write $\pi_2(t \succ)$ for the set of output places of $t$, i.e. $\{p \in P \mid \exists \alpha \in \dot{X} : \langle \alpha, p \rangle \in t \succ\}$. The transition $t$ is called final if $t \succ = \emptyset$, and initial if $\succ t = \{\iota\}$.

We will add a few constraints on this definition along the way, but we need more definitions to state them. An example of such an automaton is depicted in Figure 4. The graphical representation used here draws round vertices for places and rectangular vertices for transitions, with the incoming and outgoing arcs to and from the transition corresponding respectively to the inputs and outputs of said transition. The set of tests of a transition is written inside the rectangle. The initial place is denoted by an unmarked incoming arc.

#### Runs and reachable states.

We define the operational semantics of weak Petri automata. Let us fix for the remainder of this section an automaton $\mathcal{A} = \langle P, T, \iota \rangle$. A state of this automaton is a set of places. In a given state $S \in \mathcal{P}(P)$, a transition $t$ is enabled if $\succ t \subseteq S$. In this case, we may

<footnote n="2">² In the following, we use the definitions from [4]. They differ slightly from those from [5], despite being overall equivalent.</footnote>
fire $t$, leading to a new state $S' = (S \setminus {}^\flat t) \cup \pi_2(t^\flat)$. This will be denoted in the following by $S \xrightarrow{t} {}_A S'$. We extend this notation to sequences of transitions in the natural way: if $S_0 \xrightarrow{t_1} {}_A S_1$ and $S_1 \xrightarrow{t_2;\dots;t_n} {}_A S_n$ then we write $S_0 \xrightarrow{t_1;t_2;\dots;t_n} {}_A S_n$. In this case we say that $\langle S_0, t_1; t_2; \dots; t_n, S_n \rangle$ is a valid run, or simply run, from $S_0$ to $S_n$. If $S_0 = \{\iota\}$ then the run is initial and if $S_n$ is empty then it is final. A run which is both initial and final is called accepting. An accepting run of the automaton from Figure 4 is depicted in Figure 5. A state $S$ is reachable in $\mathcal{A}$ if there is an initial run leading to $S$.

We may now state the first two constraints we impose on automata: if $S$ is reachable in $\mathcal{A}$ and $S \xrightarrow{t} {}_A S'$, then $(S \setminus {}^\flat t) \cap \pi_2(t^\flat) = \emptyset$, and for each transition $t \in T$, and every triple $\langle p, \alpha, \beta \rangle \in P \times \dot{X} \times \dot{X}$, we have: $\{\langle \alpha, p \rangle, \langle \beta, p \rangle\} \subseteq t^\flat \Rightarrow \alpha = \beta$. These constraints correspond to the classic Petri net property of safety, also called one-boundedness.

**Remark.** These constraints are decidable: the set of transitions is finite, and because reachable states are subsets of a fixed finite set, there are only finitely many. Thus checking whether an automaton satisfies these two requirements only entails a finite number of tests.

We introduce some attributes of a run $R$: its input $I_R$, its output $O_R$, its excess $E_R$, its tests $A_R$, and its internal labels $\Lambda_R$. Let $R = S_0 \xrightarrow{t_1} {}_A S_1 \dots \xrightarrow{t_n} {}_A S_n$ be a valid run in some automaton $\mathcal{A}$. $I_R$ is the set of tokens (places) in $S_0$ which are consumed during the run; $E_R$ is the rest of the tokens from $S_0$, those which are not moved; $\Lambda_R$ is the set of labels appearing in some $t_i^\flat$ such that the associated token is consumed later on; $A_R$ is the union of the sets of tests of $R$'s transitions; and $O_R$ is the set of outputs which are not consumed in the remainder of the run. Formally:

$$ I_R := \{p \in S_0 \mid \exists i : p \in {}^\flat t_i\} \qquad O_R := \{\langle \alpha, p \rangle \mid \exists i : \langle \alpha, p \rangle \in t_i^\flat \wedge (\forall j > i, p \notin {}^\flat t_j)\} $$

$$ A_R := \bigcup_i \widehat{t_i} \qquad E_R := S_0 \setminus I_R \qquad \Lambda_R := \{\alpha \mid \exists p, \exists i < j : \langle \alpha, p \rangle \in t_i^\flat \wedge p \in {}^\flat t_j\}. $$

In the example run of Figure 5, we have $I_R = \{1\}$, $E_R = \emptyset$, $O_R = \emptyset$, $A_R = \{a\}$, and $\Lambda_R = \{a, b, c\}$.

## Traces

The trace language of an automaton can be obtained by extracting from every accepting run a weak graph, called its *trace*. Consider an accepting run $\langle \{\iota\}, t_0; \dots; t_n, \emptyset \rangle$. The graph of its trace is constructed by creating a vertex $k$ for each transition $t_k$ of the run. We add an edge $\langle k, a, l \rangle$ whenever there is some place $q$ such that $\langle a, q \rangle \in t_k^\flat$, and $t_l$ is the first transition after $t_k$ in the run with $q$ among its inputs. The set of tests of the trace is $A_R$. The trace of the run in Figure 5 is presented in Figure 6. The definition we give below is a generalisation for arbitrary valid runs, which coincides with the informal presentation we just gave on accepting runs.

Let $R = \langle S, t_0; \dots; t_n, S' \rangle$ be a run in $\mathcal{A}$. For every $k$ and $p \in \pi_2(t_k^\flat) \setminus S'$, we define

$$ \nu(k, p) = \min \{l \mid l > k \text{ and } p \in {}^\flat t_l\}. $$

The trace of $R$, denoted by $G(R)$, is the pair $\langle G_R, A_R \rangle$, where $G_R$ has vertices $V_R = \{0, \dots, n\} \cup S'$ and edges defined by:

$$ E_R = \{\langle k, a, l \rangle \mid \langle a, p \rangle \in t_k^\flat \text{ and } (l = p \wedge p \in S') \lor (l = \nu(k, p))\}. $$

The language $\mathcal{L}(\mathcal{A})$ of an automaton $\mathcal{A}$ is the set of traces of accepting runs of $\mathcal{A}$. In the following, we will only consider automata such that if $\langle G, A \rangle \in \mathcal{L}(\mathcal{A})$, then either $G$ is either isomorphic to $1$ or is a term graph: that is, if $G_A$ is a weak graph.
## 3.2 From expressions to automata

In this section, we show how to build inductively from an expression *e* an automaton $\mathcal{A}_e$ whose language is $\mathcal{L}(\mathcal{A}_e) = \mathcal{WG}(\llbracket e \rrbracket)$, following [4]. For 0, 1 and atoms, we give a graphical description of the automata:

<figure><img src="image_9.png" /></figure>

For the inductive cases, let $\mathcal{A}_e = \langle P_e, T_e, \iota_e \rangle$ and $\mathcal{A}_f = \langle P_f, T_f, \iota_f \rangle$, and suppose $P_e \cap P_f = \emptyset$.

Intuitively, the automaton for $e+f$ is the union of $\mathcal{A}_e$ and $\mathcal{A}_f$, where we copy the initial transitions of $\mathcal{A}_f$ so that they start from $\iota_e$ instead of $\iota_f$. Formally:

$$ \mathcal{A}_{e+f} = \langle P_e \cup P_f, T_e \cup T_f \cup T, \iota_e \rangle, \text{ where } T = \{ \langle \{\iota_e\}, \hat{t}, t^\flat \rangle \mid \langle \{\iota_f\}, \hat{t}, t^\flat \rangle \in T_f \}. $$

For the product, we want an automaton $\mathcal{A}_{e.f}$ such that $\mathcal{L}(\mathcal{A}_{e.f}) = \mathcal{L}(\mathcal{A}_e) \bullet \mathcal{L}(\mathcal{A}_f)$. This property is satisfied by the automaton $\langle P_e \cup P_f, T_e^+ \cup T_f \cup T, \iota_e \rangle$ where $T_e^+$ is the set of non-final transitions in $T_e$, and $T = \{ \langle t^\flat, A \cup B, t^\flat \rangle \mid \langle t^\flat, A, \emptyset \rangle \in T_e \wedge \langle \{\iota_f\}, B, t^\flat \rangle \in T_f \}$.

Instead of defining directly an automaton for $e^*$, we give an automaton for the non-zero iteration $e^+$, and then define $\mathcal{A}_e^*$ to be $\mathcal{A}_{1 \cup e^+}$. Using the last two constructs, the automaton $\mathcal{A}_{e^+}$ is easy to define: $\mathcal{A}_{e^+} = \langle P_e, T_e \cup \{\langle t^\flat, A \cup B, t^\flat \rangle \mid \langle t^\flat, A, \emptyset \rangle \in T_e \wedge \langle \{\iota_e\}, B, t^\flat \rangle \in T_e \}, \iota_e \rangle$.

Finally, we then define $\mathcal{A}_{e \cap f}$ to be the automaton $\langle P_e \cup P_f \cup \{\iota\}, T_1 \cup T_2 \cup T_3 \cup T_4, \iota \rangle$, where $\iota$ is a fresh place, and:

- $T_1$ is the set of non-initial, non-final transitions of $T_e$ and $T_f$;

- $T_2$ is the set of triples $\langle \{\iota\}, \hat{t}_1 \cup \hat{t}_2, t_1^\flat \cup t_2^\flat \rangle$ such that $t_1$ (resp. $t_2$) is initial but not final in $T_e$ (resp. $T_f$);

- $T_3$ is the set of triples $\langle t^\flat t_1 \cup t^\flat t_2, \hat{t}_1 \cup \hat{t}_2, \emptyset \rangle$ such that $t_1$ (resp. $t_2$) is final but not initial in $T_e$ (resp. $T_f$);

- $T_4$ is the set of triples $\langle \{\iota\}, A, \emptyset \rangle$ such that $1_A \in \llbracket e \cap f \rrbracket$.

This definition is effective, as the set of $A \subseteq X$ such that $1_A \in \llbracket e \rrbracket$ can be computed in space $O(|e| \times 2^{|X|})$. Using the proofs for Petri automata as a guideline, it is a simple exercise to check that the correctness of the construction, that is $\mathcal{L}(\mathcal{A}_e) = \mathcal{WG}(\llbracket e \rrbracket)$.

## 3.3 Comparing automata

The algorithm to compare weak Petri automata relies on the notion of simulation. Similarly to many finite transition systems, the language of an automaton $\mathcal{A}$ is included in that of the automaton $\mathcal{B}$ if $\mathcal{B}$ can simulate $\mathcal{A}$.

**► Definition 6 (Simulation).** Let $\mathcal{A}_1 = \langle P_1, T_1, \iota_1 \rangle$ and $\mathcal{A}_2 = \langle P_2, T_2, \iota_2 \rangle$ be two automata, we say that $\mathcal{A}_2$ can simulate $\mathcal{A}_1$ if there exists a function $\llcorner$ associating to every subset of $X$ a set of triples from $\mathcal{P}(P_1) \times \mathcal{P}(X) \times \mathcal{P}(P_2 \to P_1)$, such that: (We denote the fact that the triple $\langle S, B, E \rangle$ is contained in the image by $\llcorner$ of the set $A$ by $S \llcorner_A^B E$.)

(correspondence) if $S \llcorner_A^B E$ and $\eta \in E$ then $\text{range}(\eta) \subseteq S$;

(initialisation) $\{\iota_1\} \llcorner_A^\emptyset \{[\iota_2 \mapsto \iota_1]\}$;

(totality) if $\emptyset \llcorner_A^A E$ then $\exists \eta \in E: \text{dom}(\eta) = \emptyset$;

(progress) if $S \llcorner_A^B E$ and $S \xrightarrow{t} \mathcal{A}_1 S'$, then $S' \llcorner_A^{B \cup \hat{t}} E'$, where $E'$ is the set of all $\eta'$ such that there is a map $\eta$ in $E$, and a run $R$ in $\mathcal{A}_2$ from $\text{dom}(\eta)$ to $\text{dom}(\eta')$ s.t.:

$$ I_R = \{p \mid \eta(p) \in t^\flat\} \qquad \Lambda_R \cup A_R \subseteq \dot{A} \qquad \forall \langle \alpha, p \rangle \in O_R, \langle \alpha, \eta'(p) \rangle \in t^\flat $$

$$ \forall p \in E_R, \eta(p) = \eta'(p). $$
**► Lemma 7.** $\mathcal{L}(\mathcal{A}_1) \subseteq \mathcal{L}(\mathcal{A}_2)$ if and only if $\mathcal{A}_2$ can simulate $\mathcal{A}_1$.

**Proof.** We start by showing the right to left direction: suppose that $\mathcal{A}_2$ can simulate $\mathcal{A}_1$, as witnessed by the function $\ll$, and consider an accepting run $R = (S_0, t_1; \dots; t_n; S_n)$ in $\mathcal{A}_1$:

$$S_0 = \{\iota_1\} \qquad \forall 1 \le i \le n, S_{i-1} \xrightarrow{t_i} \mathcal{A}_1 S_i \qquad S_n = \emptyset.$$

We write $B_i = \bigcup_{j<i} \widehat{t_j}$. Using the relations $\ll^{B_i}_{A_R}$, we can find a sequence of $E_i$ (for $0 \le i \le n$) such that $S_i \ll^{B_i}_{A_R} E_i$, $E_0 = \{[\iota_2 \mapsto \iota_1]\}$, and there is some $\eta_n \in E_n$ which has an empty domain. Backtracking from this $\eta_n$ using the progress condition allows us to find a sequence of maps $(\eta_i)_{0 \le i \le n}$, with domains $(T_i)_{0 \le i \le n}$ such that there are valid runs $R_i$ in $\mathcal{A}_2$ from $T_{i-1}$ to $T_i$, and satisfying:

$$T_0 = \{\iota_2\} \qquad T_n = \emptyset \qquad I_{R_i} = \{p \mid \eta_{i-1}(p) \in t_i^\flat\} \qquad \Lambda_{R_i} \cup A_{R_i} \subseteq \dot{A}_R \\ \forall \langle\alpha, p\rangle \in O_{R_i}, \langle\alpha, \eta_i(p)\rangle \in t_i^\flat \qquad \forall p \in E_{R_i}, \eta_{i-1}(p) = \eta_i(p).$$

We now build the run $R'$ by concatenating the $R_i$s. We obtain an accepting run in $\mathcal{A}_2$, whose set of tests is $\bigcup_i A_{R_i} \subseteq A_R$. To any transition $t'_j$ in $R'$, the function $\varphi$ associates the index $i$ of the run $R_i$ from which this transition was extracted. The function $\varphi$ witnesses $G(R) \triangleleft G(R')$.

For the converse direction, we prove an intermediary result. Let $R = (S_0, t_1; \dots; t_n, S_n)$ be an accepting run in $\mathcal{A}_1$ and $R'$ be an accepting run from $\mathcal{A}_2$ such that $G(R) \triangleleft G(R')$, with $\varphi$ as the witnessing function. Notice that if the transition $t'_i$ is a cause of $t'_{i+1}$ in $R'$ (i.e. they cannot be exchanged without changing the trace), either $\varphi(i) = \varphi(i+1)$, or $t_{\varphi(i)}$ is a cause of $t_{\varphi(i+1)}$ in $R$, thus $\varphi(i) < \varphi(i+1)$. This means that we may permute transitions in $R'$ without changing the trace, to obtain a run $R''$ such that $i < j \Rightarrow \varphi(i) \le \varphi(j)$.

Now, the sets of transitions sharing the same value $\varphi(i)$ are contiguous, meaning that $R''$ can be split as the sequence of sub-runs $R_1; \dots; R_n$, such that $\varphi$ maps every transitions in $R_i$ to $i$. (It may be the case that some of these runs are empty.) As $G(R) \triangleleft G(R'')$, we know that $A_{R''} \subseteq A_R$, which means that $\forall i, A_{R_i} \subseteq A_R$. Inside the run $R_i$, we know that the internal edges of the graph of $R_i$ are labelled with letters from $A_R$, as both their extremities are mapped to $i$. This means $\Lambda_{R_i} \subseteq \dot{A}_R$.

We know define the $\eta_i$. First, we set $\eta_0(\iota_2) = \iota_1$, and $\forall p \in E_{R_i}, \eta_{i-1}(p) = \eta_i(p)$. If on the other hand $\langle\alpha, p\rangle \in O_{R_i}$, let $k$ be the index in $R''$ corresponding to the output state of $R_i$, and $j = \nu_{R''}(p, k)$. As $j$ cannot be in $R_i$, we know $\varphi(j) > \varphi(k)$. Thus, in the graph of $R$ there is an edge $\langle\varphi(k), \alpha, \varphi(j)\rangle$. By definition of the graph of a run, there must be a pair $\langle\alpha, q\rangle \in t_{\varphi(k)}^\flat$ such that $\nu_R(q, \varphi(k)) = \varphi(j)$. Then this $q$ is a suitable choice for $\eta_i(p)$.

It is then a simple matter of unfolding the definitions to check that:

$$I_{R_i} = \{p \mid \eta_{i-1}(p) \in t_i^\flat\} \qquad \forall \langle\alpha, p\rangle \in O_{R_i}, \langle\alpha, \eta_i(p)\rangle \in t_i^\flat \qquad \forall p \in E_{R_i}, \eta_{i-1}(p) = \eta_i(p).$$

This means that whenever we have $R$ and $R'$ accepting runs from respectively $\mathcal{A}_1$ and $\mathcal{A}_2$ s.t. $G(R) \triangleleft G(R')$, we can find a sequence of $\eta_i$ satisfying all four conditions of a simulation. Thus, if $\mathcal{L}(\mathcal{A}_1) \subseteq \mathcal{L}(\mathcal{A}_2)$, for every reachable state $S$ of $\mathcal{A}_1$, we set $\ll_A^B$ to relate $S$ to the set of all maps $\eta$ such that there is an index $i$, an accepting run $R$ in $\mathcal{A}_1$, and an accepting run $R'$ of $\mathcal{A}_2$ satisfying (1) $A_R = A$, (2) $\bigcup_{j<i} \widehat{t_j} = B$, (3) $S = S_i$, (4) $G(R) \triangleleft G(R')$ and (5) the construction we just provided produces $\eta_i = \eta$. ▼
## 3.4 Complexity

**Corollary 8.** The theory of reversible Kleene lattices is EXPSPACE-complete.

*Proof.* The equational theory of identity-free Kleene lattices being already EXPSPACE-complete [7, Proposition 10.2], we know the problem at hand to be EXPSPACE-hard.

Let $e, f \in \mathcal{E} \langle X \rangle$, we ask whether $\mathrm{Lang} \models e \le f$. By Theorem 5, this reduces to testing if $\mathcal{D}[\![e]\!] \subseteq \mathcal{D}[\![f]\!]$, which is equivalent to $[e] \subseteq \mathcal{D}[\![f]\!]$ by the properties of the closure operator. Using the construction in Section 3.2, this is amounts to checking if $\mathcal{L}(\mathcal{A}_e) \subseteq \mathcal{D} \mathcal{L}(\mathcal{A}_f)$. This later question can be decided by looking for a simulation function, thanks to Lemma 7.

We now inspect the space complexity of this method. Let $n, m, x$ be respectively the size of $e$, the size of $f$ and the size of the alphabet. By analysing each step in Section 3.2, we get that the number of places of $\mathcal{A}_e$ is less than $2 \times n$ (similarly for $\mathcal{A}_f$). The number of transitions is harder to work out from the construction, but because $T \subseteq \mathcal{P}(P) \times \mathcal{P}(X) \times \mathcal{P}(\dot{X} \times P)$, we know it is bounded by $2^{2n+x+2x \times 2n}$. Using Savitch's theorem [21], we only need to show that there is a non-deterministic semi-algorithm to refute the existence of a simulation, which uses only exponential space in $n, m$ and $x$. Here is such a procedure:

1. choose $A \subseteq X$;

2. start with $S = \{\iota_1\}, B = \emptyset$ and $E = \{[\iota_2 \mapsto \iota_1]\}$;

3. if $\langle S, B \rangle = \langle \emptyset, A \rangle$ and $E$ does not contain a map $\eta$ whose domain is empty return False;

4. choose $t \in T_1$ such that $\mathcal{D}t \subseteq \pi_1(S)$, fire $t$ from $S$, and update $B$ as $\hat{t} \cup B$;

5. update $E$ according to the progress condition in Definition 6;

6. go to step 3.

All of these computations can be performed using exponential space. For instance, $S$, being a pair of a set of places in $\mathcal{A}_e$ and a set of letters, can be stored in space $2n \log (2n) \times x \log (x)$, and $E$ only needs space $(2n+1)^{2m} \times 2m \log (2n+1)$. $\quad$

# 4 Conclusion

We showed that the free representation of reversible Kleene lattices consists of downward closed sets of weak terms, or equivalently of downward closed sets of weak graphs. By considering a suitable variation of Petri automata, and producing an algorithm to decide language containment of these automata, we showed that testing the validity of equations in reversible Kleene lattices is an EXPSPACE-complete problem.

The results we obtained here could be naturally extended in a number of ways.

- We would like to add to our model some features of programming languages which have been studied independently, among which tests [15], and nominal structures [12, 17, 16, 6].

- Although Kleene algebra is known not to be finitely axiomatisable [19], several authors have proposed semi-axiomatisations [14, 8, 20]. A complete axiomatisation of Kleene algebra with converse, relative to an axiomatisation of KA, is also known [9]. As far as we know, no axiomatisation of reversible Kleene lattices exists. We believe the free representation we defined in Section 2 could help establishing such an axiomatisation.

- Since we provide here an algorithm, it would be interesting to implement it. Such a procedure could fit in very well in a proof assistant such as Coq.

Although the weak Petri automata introduced in this paper were just a means to an end, we are wondering whether this might be an interesting model of computation in itself. We are confident that we could reuse to technology of boxes introduced in [7, 4] to get a Kleene theorem for these automata. Their semantics could also be reformulated with transitions labelled with weights chosen from a finite lattice (instead of sets of letters from the alphabet).
References

1 Hajnal Andréka, Szabolcs Mikulás, and István Németi. The equational theory of Kleene lattices. *TCS*, 412(52):7099-7108, 2011. doi:10.1016/j.tcs.2011.09.024.

2 Hajnal Andréka and Dmitry A. Bredikhin. The equational theory of union-free algebras of relations. *Alg. Univ.*, 33(4):516-532, 1995. doi:10.1007/BF01225472.

3 Stephen L. Bloom, Zoltán Ésik, and Gheorghe Stefanescu. Notes on equational theories of relations. *Alg. Univ.*, 33(1):98-126, 1995. doi:10.1007/BF01190768.

4 Paul Brunet. *Algebras of Relations: From algorithms to formal proofs*. PhD thesis, Université de Lyon, 2016. URL: https://tel.archives-ouvertes.fr/tel-01455083v1.

5 Paul Brunet and Damien Pous. Petri Automata for Kleene Allegories. In *Proc. LICS*, pages 68-79, July 2015. doi:10.1109/LICS.2015.17.

6 Paul Brunet and Damien Pous. A formal exploration of Nominal Kleene Algebra. In *Proc. MFCS*, 2016.

7 Paul Brunet and Damien Pous. Petri automata. *Logical Methods in Computer Science*, 2017. submitted. arXiv:1702.01804.

8 John H. Conway. *Regular algebra and finite machines*. Chapman and Hall Mathematics Series, 1971. URL: http://store.doverpublications.com/0486485838.html.

9 Zoltán Ésik and Laszlo Bernátsky. Equational properties of Kleene algebras of relations with conversion. *TCS*, 137(2):237-251, 1995. doi:10.1016/0304-3975(94)00041-G.

10 Peter J. Freyd and Andre Scedrov. *Categories, Allegories*. NH, 1990. URL: http://store.elsevier.com/Categories-Allegories/P_J_Freyd/isbn-9780444703682/.

11 Martin Fürer. The complexity of the inequivalence problem for regular expressions with intersection. In *Proc. ICALP*, pages 234-245, 1980. doi:10.1007/3-540-10003-2_74.

12 Murdoch James Gabbay and Vincenzo Ciancia. Freshness and name-restriction in sets of traces with names. In *Proc. FoSSaCS*, pages 365-380. Springer, 2011.

13 Stephen C. Kleene. *Representation of Events in Nerve Nets and Finite Automata*. Memorandum. Rand Corporation, 1951. URL: http://wwwrand.org/content/dam/rand/pubs/research_memoranda/2008/RM704.pdf.

14 Dexter Kozen. A completeness theorem for Kleene Algebras and the algebra of regular events. In *Proc. LICS*, pages 214-225. IEEE Computer Society, 1991. doi:10.1109/LICS.1991.151646.

15 Dexter Kozen. Kleene algebra with tests. *Transactions on Programming Languages and Systems*, 19(3):427-443, 1997. doi:10.1145/256167.256195.

16 Dexter Kozen, Konstantinos Mamouras, Daniela Petrisan, and Alexandra Silva. Nominal Kleene coalgebra. In *Proc. ICALP*, pages 286-298. Springer, 2015.

17 Dexter Kozen, Konstantinos Mamouras, and Alexandra Silva. Completeness and incompleteness in nominal Kleene algebra. In *Proc. RAMICS*, pages 51-66, 2015.

18 Albert R. Meyer and Larry J. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential space. In *Proc. SWAT*, pages 125-129, 1972. doi:10.1109/SWAT.1972.29.

19 Volodimir Nikiforovych Redko. On defining relations for the algebra of regular events. *Ukrainskii Matematicheskii Zhurnal*, pages 120-126, 1964.

20 Arto Salomaa. Two complete axiom systems for the algebra of regular events. *J. ACM*, 13(1):158-169, 1966. doi:10.1145/321312.321326.

21 Walter J Savitch. Relationships between nondeterministic and deterministic tape complexities. *Journal of computer and system sciences*, 4(2):177-192, 1970.

22 Jacobo Valdes, Robert E. Tarjan, and Eugene L. Lawler. The recognition of series parallel digraphs. In *Proc. STOC*, STOC '79, pages 1-12. ACM, 1979. doi:10.1145/800135.804393.
A Restriction of the use of converse

We define the following mutually recursive functions:

$$
\begin{align*}
[0] &= 0 & [1] &= 1 & [a] &= a & [e+f] &= [e] + [f] & [e \cdot f] &= [e] \cdot [f] \\
[e \cap f] &= [e] \cap [f] & [e^*] &= [e]^* & [e^+] &= [e] & [e^-] &= [e] \\
[0] &= 0 & [1] &= 1 & [a] &= a^\sim & [e+f] &= [e] + [f] & [e \cdot f] &= [f] \cdot [e] \\
[e \cap f] &= [e] \cap [f] & [e^*] &= [e]^* & [e^+] &= [e] & [e^-] &= [e]
\end{align*}
$$

By a simple induction, one can check that $\mathrm{Lang} \models e = [e]$, that $|[e]| \le 2 \times |e|$, and that in
the expression $[e]$ the converse only appears applied to variables.

B Omitted proof: Lemma 1

► Lemma 9. $\forall \sigma, \forall u \in GT^{-} \langle X \rangle, (\forall a \in var(u), \varepsilon \in \sigma(a)) \Leftrightarrow \varepsilon \in \hat{\sigma}(u)$.

Proof. If $u \in \{a, a^\sim\}$ then $var(u) = \{a\}$, and because $\varepsilon = \varepsilon^\sim$ we have:

$$
(\forall a \in var(u), \varepsilon \in \sigma(a)) \Leftrightarrow \varepsilon \in \sigma(a) = \hat{\sigma}(a) \Leftrightarrow \varepsilon \in \hat{\sigma}(a^\sim)
$$

On the other hand, notice that $\varepsilon \in \hat{\sigma}(u \cdot v) \Leftrightarrow \varepsilon \in \hat{\sigma}(u \cap v) \Leftrightarrow \varepsilon \in \hat{\sigma}(u) \wedge \varepsilon \in \hat{\sigma}(v)$. By induction, this is equivalent to $\forall a \in var(u) \cup var(v), \varepsilon \in \sigma(a)$, which allows us to conclude since we have $var(u \cdot v) = var(u \cap v) = var(u) \cup var(v)$. $\quad \blacksquare$

► Lemma 10. $\tilde{\sigma}(x \bullet y) = \tilde{\sigma}(x) \cdot \tilde{\sigma}(y)$ and $\tilde{\sigma}(x \parallel y) = \tilde{\sigma}(x) \cap \tilde{\sigma}(y)$.

Proof. Let $x = u_A$ and $y = v_B$.

1. If $u=1$

a. If $v = 1$: then $x \bullet y = x \parallel y = 1_{A \cup B}$. If there is $a \in A$ such that $\varepsilon \notin \sigma(a)$, then $\tilde{\sigma}(x) = \emptyset = \tilde{\sigma}(1_{A \cup B})$, and $\tilde{\sigma}(x) \cdot \tilde{\sigma}(y) = \tilde{\sigma}(x) \cap \tilde{\sigma}(y) = \emptyset$. Similarly when there exists some $b \in B$ such that $\varepsilon \notin \sigma(b)$.

If on the other hand for every $a \in A \cup B$ we have $\varepsilon \in \sigma(a)$, then $\tilde{\sigma}(x) = \tilde{\sigma}(y) = \tilde{\sigma}(1_B) = \tilde{\sigma}(1_{A \cup B}) = \{\varepsilon\}$, thus $\tilde{\sigma}(x) \cdot \tilde{\sigma}(y) = \tilde{\sigma}(x) \cap \tilde{\sigma}(y) = \{\varepsilon\}$.

b. If $v \neq 1$: $x \bullet y = v_{A \cup B}$, and $x \parallel y = 1_{A \cup B \cup var(v)}$.

- if $\exists a \in A : \varepsilon \notin \sigma(a)$ then $\tilde{\sigma}(x) = \tilde{\sigma}(x \bullet y) = \tilde{\sigma}(x \parallel y) = \emptyset$, and furthermore
  $\tilde{\sigma}(x) \cdot \tilde{\sigma}(y) = \tilde{\sigma}(x) \cap \tilde{\sigma}(y) = \emptyset$;

- similarly if $\exists b \in B : \varepsilon \notin \sigma(b)$;

- otherwise, $\tilde{\sigma}(x \bullet y) = \hat{\sigma}(v) = \{\varepsilon\} \cdot \hat{\sigma}(v) = \tilde{\sigma}(x) \cdot \tilde{\sigma}(y)$;

- furthermore, if $\exists a \in var(v) : \varepsilon \notin \sigma(a)$, then by Lemma 9 we have $\varepsilon \notin \hat{\sigma}(v)$,
  which means that $\tilde{\sigma}(x) \cap \tilde{\sigma}(v) = \{\varepsilon\} \cap \hat{\sigma}(v) = \emptyset = \tilde{\sigma}(x \parallel v)$,

- finally, in the last case, Lemma 9 tells us that $\varepsilon \in \hat{\sigma}(v)$, thus that $\tilde{\sigma}(x) \cap \tilde{\sigma}(v) = \{\varepsilon\} \cap \hat{\sigma}(v) = \{\varepsilon\} = \tilde{\sigma}(x \parallel y)$.

2. If $u \neq 1$

a. If $v = 1$: same as 1b

b. If $v \neq 1$: then $x \bullet y = (u \cdot v)_{A \cup B}$, and $x \parallel y = (u \cap v)_{A \cup B}$. If $\exists a \in A : \varepsilon \notin \sigma(a)$, then $\tilde{\sigma}(x) = \emptyset$, and $\tilde{\sigma}(x) \cdot \tilde{\sigma}(y) = \tilde{\sigma}(x) \cap \tilde{\sigma}(y) = \emptyset$. Evidently, the case $\exists b \in B : \varepsilon \notin \sigma(b)$ is symmetric.

Otherwise, $\tilde{\sigma}(x \bullet y) = \hat{\sigma}(u \cdot v) = \hat{\sigma}(u) \cdot \hat{\sigma}(v) = \tilde{\sigma}(u) \cdot \tilde{\sigma}(v)$; and $\tilde{\sigma}(x \parallel y) = \hat{\sigma}(u \cap v) = \hat{\sigma}(u) \cap \hat{\sigma}(v) = \tilde{\sigma}(u) \cap \tilde{\sigma}(v)$. $\quad \blacksquare$
Using this fact, the proof of Lemma 1 by structural induction is straightforward:

- by definition of $\tilde{\sigma}$ we have $\tilde{\sigma}(u_\emptyset) = \hat{\sigma}(u)$. This ensures that the lemma holds for all base cases, i.e. 1, a, and a';

- For the sequence:

$$ 
\begin{align*}
\hat{\sigma}(u \cdot v) &= \hat{\sigma}(u) \cdot \hat{\sigma}(v) = \tilde{\sigma} \circ \tau(u) \cdot \tilde{\sigma} \circ \tau(v) \tag{Definition of $\hat{\sigma}$, induction} \\
&= \tilde{\sigma}(\tau(u) \bullet \tau(v)) \tag{Lemma 10} \\
&= \tilde{\sigma}(\tau(u \cdot v)) = \tilde{\sigma} \circ \tau(u \cdot v); \tag{Definitions of $\tau$ and $\circ$}
\end{align*}
$$

- For the intersection:

$$ 
\begin{align*}
\hat{\sigma}(u \cap v) &= \hat{\sigma}(u) \cap \hat{\sigma}(v) = \tilde{\sigma} \circ \tau(u) \cap \tilde{\sigma} \circ \tau(v) \tag{Definition of $\hat{\sigma}$, induction} \\
&= \tilde{\sigma}(\tau(u) \parallel \tau(v)) \tag{Lemma 10} \\
&= \tilde{\sigma}(\tau(u \cap v)) = \tilde{\sigma} \circ \tau(u \cap v). \tag{Definitions of $\tau$ and $\circ$}
\end{align*}
$$

### C Omitted proof: Lemma 2

For a term $s \in GT^- \langle X \rangle$, and two vertices $x_1, x_2 \in V_u$, we write $\text{Hom}_s(x_1, x_2)$ for the set of maps $\varphi: V_{\mathcal{G}(s)} \to V_u$ such that: $\varphi(i_H) = x_1$, $\varphi(o_H) = x_2$, and for every edge $\langle x, \alpha, y \rangle$ in $E_{\mathcal{G}(s)}$, either $\langle \varphi(x), \alpha, \varphi(y) \rangle \in E_u$ or $\alpha \in \dot{A}$ and $\varphi(x) = \varphi(y)$. We now prove by induction on $t$ that $\text{Hom}_t(x, y) \neq \emptyset \Leftrightarrow w_u^f(x, y) \in \hat{\sigma}_u(t)$.

If $s \in \dot{X}$, then $\mathcal{G}(s) = \{\langle 0, 1 \rangle, \{\langle 0, s, 1 \rangle\}, 0, 1 \rangle$, and $\varphi \in \text{Hom}_s(x, y)$ means that $\varphi(0) = x$, $\varphi(1) = y$, and either $\langle x, s, y \rangle \in E_u$ or $s \in \dot{A}$ and $x = y$. If $x \neq y$ then we've already noticed that $\langle x, s, y \rangle \in E_u$ is equivalent to $w_u^f(x, y) \in \hat{\sigma}_u(s)$. If on the other hand $x = y$ then $w_u^f(x, y) = \varepsilon$, and again we know that $\varepsilon \in \hat{\sigma}_u(s)$ is equivalent to $s \in \dot{A}$. In the end, we get that $\exists \varphi \in \text{Hom}_s(x, y) \Leftrightarrow w_u^f(x, y) \in \hat{\sigma}_u(s)$.

For the case $s = t \cdot t'$, we need to use the following property:

$$ \forall x, y, \exists \varphi \in \text{Hom}_{t \cdot t'}(x, y) \Leftrightarrow \exists z : \exists \langle \varphi_1, \varphi_2 \rangle \in \text{Hom}_t(x, z) \times \text{Hom}_{t'}(z, y). $$

The direct implication is straightforward, and the converse relies on the fact that the graphs of $t$ and $t'$ only overlap on the output of $t$ and input of $t'$.

Using this and the induction hypothesis, we get

$$ \exists \varphi \in \text{Hom}_{t \cdot t'}(x, y) \Leftrightarrow \exists z : w_u^f(x, z) \in \hat{\sigma}_u(t) \wedge w_u^f(z, y) \in \hat{\sigma}_u(t') \Rightarrow w_u^f(x, y) \in \hat{\sigma}_u(t \cdot t'). $$

For the last implication, if $w_u^f(x, y) \in \hat{\sigma}_u(t \cdot t')$, then there must be $\langle w_1, w_2 \rangle \in \hat{\sigma}_u(t) \times \hat{\sigma}_u(t')$ such that $w_u^f(x, y) = w_1 w_2$. To conclude, we use the fact that for every simple term $s$, if a sub-word $x_i...x_j$ of $w_u$ is in $\hat{\sigma}_u(s)$ then either $i = j$ or $\exists x, y : f(x) = i \wedge f(y) = j$. This can be established by a simple induction on $s$, and implies that there must be some $z$ such that $w_1 = w_u^f(x, z)$ and $w_2 = w_u^f(z, y)$.

The last case is the simplest one:

$$ 
\begin{align*}
\exists \varphi \in \text{Hom}_{t \cap t'}(x, y) &\Leftrightarrow \exists \varphi \in \text{Hom}_t(x, y) \wedge \exists \varphi \in \text{Hom}_{t'}(x, y) \\
&\Leftrightarrow w_u^f(x, y) \in \hat{\sigma}_u(t) \wedge w_u^f(x, y) \in \hat{\sigma}_u(t') \\
&\Leftrightarrow w_u^f(x, y) \in \hat{\sigma}_u(t \cap t')
\end{align*}
$$

We have now established that $\text{Hom}_t(x, y) \neq \emptyset \Leftrightarrow w_u^f(x, y) \in \hat{\sigma}_u(t)$. To conclude, notice that $w_u = w_u^f(i_u, o_u)$, and because $B \subseteq A$, $\tilde{\sigma}_u(v) = \hat{\sigma}_u(t)$, thus we get

$$ w_u \in \tilde{\sigma}_u(v) \Leftrightarrow w_u^f(i_u, o_u) \in \hat{\sigma}_u(t) \Leftrightarrow \exists \varphi \in \text{Hom}_t(i_u, o_u) \Leftrightarrow \mathcal{W}\mathcal{G}(u) \triangleleft \mathcal{W}\mathcal{G}(v). $$
D Omitted proof: Lemma 3

We proceed by induction on $u$.

If $u \in \check{X}$, its graph has only two vertices, and a single edge whose label is $u$ itself. Thus
$\varphi(i_u) = 0 \wedge \varphi(o_u) = n$ completely defines $\varphi$; and $\langle x, \alpha, y \rangle \in E_u \Rightarrow w^\varphi[x, y] \in \hat{\sigma}(\alpha)$ just
means $w[0, n] \in \hat{\sigma}(u)$. As $w[0, n] = w$, we are done.

For $u \cap v$, by induction $w \in \hat{\sigma}(u \cap v)$ is equivalent to the existence of two functions
$\varphi_1: V_u \to \{0, \dots, n\}$ and $\varphi_2: V_v \to \{0, \dots, n\}$ satisfying the conditions of the right hand
side. It is then a simple matter to check that these to functions can be merged into an
appropriate $\varphi$, and that any acceptable $\varphi: V_{u \cap v} \to \{0, \dots, n\}$ could be split into $\varphi_1$ and $\varphi_2$.

For the sequential product, by definition $w \in \hat{\sigma}(u_1 \cdot u_2)$ is equivalent to the existence of a pair of words $\langle w_1, w_2 \rangle \in \hat{\sigma}(u_1) \times \hat{\sigma}(u_2)$ such that $w = w_1 w_2$. By induction, we get that for $k \in \{1, 2\}$, $w_k \in \hat{\sigma}(u_k)$ if and only if there is a map $\varphi_k$ such that $\varphi_k(i_{u_k}) = 0$, $\varphi_k(o_{u_k}) = |w_k|$, and $\langle x, \alpha, y \rangle \in E_{u_k} \Rightarrow w_k^\varphi[x, y] \in \hat{\sigma}(\alpha)$. We need to show that this last condition is equivalent to the existence of a single $\varphi: V_{u_1 \cdot u_2} \to \{0, \dots, n\}$. Building such a $\varphi$ from $\varphi_1$ and $\varphi_2$ is simple: we define

$$
\varphi(x) := \begin{cases} \varphi_1(x) & \text{if } x \in V_{u_1}; \\ \varphi_2(x) + |w_1| & \text{otherwise.} \end{cases}
$$

If on the other hand we have $\varphi: V_{u_1 \cdot u_2} \to \{0, \dots, n\}$ such that $\varphi(i_{u_1 \cdot u_2}) = 0 \wedge \varphi(o_{u_1 \cdot u_2}) = n$
and $\langle x, \alpha, y \rangle \in E_{u_1 \cdot u_2} \Rightarrow w^{\varphi}[x, y] \in \hat{\sigma}(\alpha)$, then we define $w_1$ and $w_2$ as respectively
$w^{\varphi}[i_{u_1}, o_{u_1}]$ and $w^{\varphi}[i_{u_2}, o_{u_2}]$, and $\varphi_1(x) := \varphi(x)$, $\varphi_2(x) := \varphi(x) - \varphi(i_{u_2})$.

E Omitted proof: uniformity lemma

$$
\hat{\sigma}(e) = \bigcup_{u \in [e]} \tilde{\sigma}(u) = \bigcup_{u \in \trianglelefteq [e]} \tilde{\sigma}(u).
$$

First, We define the set of ground terms $\langle e \rangle$ as in [1] by structural induction:

$\langle 0 \rangle := \emptyset$

$\langle 1 \rangle := \{1\}$

$\langle \alpha \rangle := \{\alpha\}$

$\langle e + f \rangle := \langle e \rangle \cup \langle f \rangle$

$$
\langle e \cdot f \rangle := \{u \cdot v \mid u \in \langle e \rangle \wedge v \in \langle f \rangle\}
$$

$$
\langle e \cap f \rangle := \{ u \cap v \mid u \in \langle e \rangle \wedge v \in \langle f \rangle \}
$$

$$
\langle e^* \rangle := \{ u_1 \dots u_n \mid n \ge 0 \wedge \forall 0 \le i \le n, u_i \in \langle e \rangle \}
$$

It is straightforward to check that $[[e]] = \{\tau(u) \mid u \in \langle e \rangle\}$.

By [1, Lemma 2.1] we have that $\hat{\sigma}(e) = \bigcup_{u \in \langle e \rangle} \hat{\sigma}(u)$ thus using Lemma 1 and the fact
that $[[e]] = \{\tau(u) \mid u \in \langle e \rangle\}$ we get:

$$
\hat{\sigma}(e) = \bigcup_{u \in \langle e \rangle} \hat{\sigma}(u) = \bigcup_{u \in \langle e \rangle} \tilde{\sigma}(\tau(u)) = \bigcup_{u \in \llbracket e \rrbracket} \tilde{\sigma}(u).
$$

By Theorem 4 we get that for every $u$ such that $W\mathcal{G}(u) \triangleleft W\mathcal{G}(v)$, we have $\tilde{\sigma}(u) \subseteq \tilde{\sigma}(v)$.
This ensures that:

$$
\bigcup_{u \in [e]} \tilde{\sigma}(u) = \bigcup_{u \in \trianglelefteq [e]} \tilde{\sigma}(u).
$$
## F Computing the set of tests of an expression.

We define inductively two sets of variables associated with every expression:

$$ \begin{align*} \mathfrak{S}(0) &= \emptyset & \mathfrak{S}(1) &= \{\emptyset\} & \mathfrak{S}(a) &= \mathfrak{S}(a') &= \{\{a\}\} & \mathfrak{S}(e+f) &= \mathfrak{S}(e) \cup \mathfrak{S}(f) \\ \mathfrak{S}(e \cdot f) &= \mathfrak{S}(e \cap f) &= \{A \cup B \mid \langle A, B \rangle \in \mathfrak{S}(A) \times \mathfrak{S}(f)\} & & & & \\ \mathfrak{S}(e^*) &= \{A_1 \cup \cdots \cup A_n \mid A_i \in \mathfrak{S}(e)\} & & & & & \end{align*} $$

$$ \begin{align*} [[0]]^{-} &= [[a]]^{-} = [[a^{\intercal}]]^{-} = \emptyset & [[1]]^{-} &= \{\emptyset\} & [[e+f]]^{-} &= [[e]]^{-} \cup [[f]]^{-} \\ [[e \cdot f]]^{-} &= \{A \cup B \mid \langle A, B \rangle \in [[e]]^{-} \times [[f]]^{-}\} & [[e^{*}]^{-}} &= \{A_1 \cup \cdots \cup A_n \mid A_i \in [[e]]^{-}\} \\ [[e \cap f]]^{-} &= \{A \cup B \mid \langle A, B \rangle \in ([[e]]^{-} \times ([[f]]^{-} \cup \mathfrak{S}(f))) \cup (\mathfrak{S}(e) \times [[f]]^{-})\}. \end{align*} $$

A simple induction allows one to check that these sets satisfy the following properties:

$$ \mathfrak{S}(e) = \{A \cup \mathrm{var}(u) \mid u_A \in [[e]]\} \qquad [[e]]^{-} = \{A \mid 1_A \in [[e]]\}. $$

Furthermore, they can be effectively computed in space exponential in the size of $X$, and linear in the size of $e$.