Paul Brunet
email: paul.brunet@ens-lyon.fr

Damien Pous
email: damien.pous@ens-lyon.fr

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.

I. INTRODUCTION

We consider binary relations and the operations of union (∪), intersection (∩), composition (⋅), converse (⋅ ⌣ ), transitive closure (⋅ + ), reflexive-transitive closure (⋅ ⋆ ), and the constants identity [START_REF] Andréka | The equational theory of Kleene lattices[END_REF] and empty relation (0). This model gives rise to an (in)equational theory: a pair of terms e, f made from those operations and some variables a, b, . . . is a valid equation, denoted Rel ⊧ e = f , if the corresponding equality holds universally. Similarly, an inequation Rel ⊧ e ≤ f is valid when the corresponding containment holds universally. Here are valid equations and inequations: they hold whatever the relations we assign to variables a, b, and c.

Rel ⊧ (a ∪ b) ⋆ ⋅ b ⋅ (a ∪ b) ⋆ = (a ⋆ ⋅ b ⋅ a ⋆ ) + (1) Rel ⊧ a ⋆ ≤ 1 ∪ a ⋅ a ⌣ ⋅ a + (2) Rel ⊧ a ⋅ b ∩ c ≤ a ⋅ (b ∩ a ⌣ ⋅ c) (3) Rel ⊧ a + ∩ 1 ≤ (a ⋅ a) + (4)
Various fragments of this theory have been studied in the literature:

• Kleene algebra [START_REF] Conway | Regular algebra and finite machines[END_REF], where one removes intersection and converse, so that terms are plain regular expressions. The theory is decidable by Kleene's work [START_REF] Kleene | Representation of Events in Nerve Nets and Finite Automata[END_REF], and actually PSPACE-complete [START_REF] Meyer | The equivalence problem for regular expressions with squaring requires exponential space[END_REF], [START_REF] Meyer | Word problems requiring exponential time[END_REF]. Equation [START_REF] Andréka | The equational theory of Kleene lattices[END_REF] lies in this fragment, and one can notice that the two expressions recognise the same language. • Kleene algebra with converse, where one only removes intersection, is also a decidable fragment [START_REF] Bloom | Notes on equational theories of relations[END_REF]. It remains PSPACE [START_REF] Brunet | Kleene algebra with converse[END_REF]. Inequation [START_REF] Andréka | The equational theory of union-free algebras of relations[END_REF] belongs to this fragment. • (representable, distributive) allegories [START_REF] Freyd | Categories, Allegories[END_REF], sometimes called positive relation algebras, where transitive and reflexive-transitive closures are not allowed. They are decidable [8, page 208]; Inequation (3) is known as the modularity law in this setting. To the best of our knowledge, the decidability of the whole theory, Kleene allegories, is open. Here we obtain several important steps towards the resolution of this problem:

1) we give a characterisation of the full (in)equational theory in terms of graph languages; 2) we design an automata model inspired by Petri nets, that makes it possible to recognise such graphs; 3) we show how to associate such a graph automaton to any term of Kleene allegories; 4) using these graph automata, we give a decision procedure for the fragment where converse and identity are forbidden. The latter fragment was studied recently by Andréka et al. [START_REF] Andréka | The equational theory of Kleene lattices[END_REF]; its decidability was open as far as we know. The restriction to this fragment allows us to exploit simplifying assumptions about the produced automata, and to obtain a coinductive algorithm for language inclusion (Section V). We actually show that language inclusion for these automata is EXPSPACEcomplete (Section VI).

The next problem, which remains open, consists in obtaining the decidability of language inclusion in the full automata model: together with the presented results, this would entail decidability of Kleene allegories. We outline some of the difficulties arising with converse or unit in presence of intersection in Section V-D.

We continue this introductory section by an informal description of the graph language characterisation and our automata model.

A. Languages

In the simple case of Kleene algebra, i.e., without converse and intersection, the (in)equational theory generated by relations can be characterised by using regular languages. Write e for the language denoted by a regular expression e; for any two regular expressions e, f , we have

Rel ⊧ e ≤ f if and only if e ⊆ f .

(

) 5
(This result is easy and folklore; proving that this is also equivalent to provability using Kleene algebra axioms [START_REF] Boffa | Une condition impliquant toutes les identités rationnelles[END_REF], [START_REF] Kozen | A completeness theorem for Kleene Algebras and the algebra of regular events[END_REF], [START_REF] Krob | A Complete System of B-Rational Identities[END_REF] is much harder.) While regular languages are closed under intersection and converse, the above characterisation does not extend to those operations. For intersection, consider two distinct variables a G(a): The extended regular expressions a ∩ b and 0 both recognise the empty language, while Rel ⊧ a ∩ b = 0: one can interpret a and b with intersecting relations. For converse, the extended regular expressions a and a ⌣ both recognise the singleton language consisting of the single-letter word a. Yet Rel ⊧ a = a ⌣ , as there are non-symmetric relations.

B. Graphs

Freyd and Scedrov' decision procedure for representable allegories [8, page 208] relies on a notion of directed, labelled, 2-pointed graph. The same notion was proposed independently by Andréka and Bredikhin [START_REF] Andréka | The equational theory of union-free algebras of relations[END_REF], in a more comprehensive way.

Call ground terms the terms in the syntax of allegories (composition, intersection, converse, and unit). A ground term u can be represented as a labelled directed graph G(u) with two distinguished vertices called the input and the output. We give some examples in Figure 1, see Definition 1 for a precise definition.

These graphs can be endowed with a preorder relation: we write G ◂ F when there exists a graph homomorphism from F to G preserving labels, inputs, and outputs. For instance the graph corresponding to (a ⋅ (b ∩ c)) ∩ d is smaller than the graph of (a ⋅ b) ∩ (a ⋅ c), thanks to the homomorphism depicted in Figure 2 using dotted arrows. Notice that the homomorphism needs not be injective or surjective, so that this preorder has nothing to do with the respective sizes of the graphs: a graph may very well be smaller than another in the sense of ◂, while having more vertices or edges (and vice versa).

The key result from Freyd and Scedrov [8, page 208], or Andréka and Bredikhin [2, Theorem 1], is that for any two ground terms u, v, we have

Rel ⊧ u ≤ v if and only if G(u) ◂ G(v) . (6)
The graphs are finite so that one can search exhaustively for a homomorphism, whence the decidability result.

C. Graph languages

To extend the above graph-theoretical characterisation to Kleene allegories, we need to handle union and (reflexive-) transitive closures. It suffices for that to consider sets of graphs: to each expression e, we associate a set of graphs G (e). This set is most often infinite when the expression e contains (reflexive-)transitive closures.

Writing ◂ X for the downward closure of a set of graphs X by the preorder ◂ on graphs, we obtain the following generalisation of both ( 5) and ( 6): for any two expressions e and f ,

Rel ⊧ e ≤ f if and only if ◂ G (e) ⊆ ◂ G (f ) . (7)
This is Theorem 6 in the sequel, and this result is almost there in the work by Andréka et al. [START_REF] Andréka | The equational theory of Kleene lattices[END_REF], [START_REF] Andréka | The equational theory of union-free algebras of relations[END_REF]. To the best of our knowledge this explicit formulation is new, as well as its use towards decidability results. When e and f are ground terms, we recover the characterisation [START_REF] Brunet | Web appendix to this abstract[END_REF] for representable allegories: G (e) and G (f ) are singleton sets in this case. For plain regular expressions, the graphs are just words and the preorder ◂ reduces to isomorphism. We thus recover the characterisation (5) for Kleene algebra. This result also generalises the characterisation provided by Ésik et al. [START_REF] Bloom | Notes on equational theories of relations[END_REF] for Kleene algebra with converse: graphs of expressions without intersection are just words over a duplicated alphabet, and the corresponding restriction of the preorder ◂ precisely corresponds to the word rewriting system they use (see Remark 7).

D. Petri automata

In order to exploit the above characterisation and obtain decidability results, one has first to represent graph languages in a finitary way. We propose for that a new finite automata model, largely based on Petri nets [START_REF] Murata | Petri nets: Properties, analysis and applications[END_REF]- [START_REF] Petri | Kommunikation mit Automaten[END_REF]. We describe this model below, ignoring converse and unit for the sake of clarity.

Recall that a Petri net consists of • a finite set of places, denoted with circles;

• a set of transitions, denoted with rectangles;

• for each transition, a set of input places and a set of output places, denoted with arrows; • an initial place, denoted by an entrant arrow;

• a set of final markings, denoted by dotted boxes (a marking, or configuration, being a set of places). The execution model is the following: start by putting a token on the initial place; choose a transition whose input places all contain a token, remove those tokens and put new tokens in the output places of the transition; repeat this process until a final marking is reached. The obtained sequence of transitions is called an accepting run. (We actually restrict ourselves to safe Petri nets, to ensure that there is always at most one token in a given place when playing this game.)

A Petri automaton is just a safe Petri net 1 with variables labelling the outputs of each transition. The automaton depicted G : To read a graph in such an automaton, we try to find an accepting run that matches the graph up to homomorphism (Definitions 10 and 11). We do that by using an evolving function from the tokens to the vertices of the graph. We start with the function mapping the unique token, in the initial place, to the input vertex of the graph. To fire a transition, we must check that all its input tokens are mapped to the same vertex in the graph, and that this vertex has several outgoing edges, labelled according to the outputs of the transition. If this is the case, we update the function by removing the mappings corresponding to the deleted tokens, and by adding new mappings for each of the created tokens (using the target vertices of the aforementioned outgoing edges, according to the labels). The graph is accepted by the Petri automaton if we can reach a final marking of the Petri automaton, with all tokens mapped to the output vertex of the graph.

For instance, the previous automaton accepts the graph of a ⋅ b ∩ a ⋅ c (F in Figure 2). We start with the function {A ↦ 0}. We can fire the first transition, updating the function into {B ↦ 1, C ↦ 2} (We could also choose to update the function into {B ↦ 2, C ↦ 1}, or {B, C ↦ 1}, or {B, C ↦ 2} but this would lead to a dead-end). Then we can fire the upper transition, evolving the function into {D ↦ 3, C ↦ 2}, and we finish by firing the remaining transition, obtaining the function {D, E ↦ 3}.

We call language of A the set of graphs L (A ) accepted by a Petri automaton A . This language is downward-closed:

L (A ) = ◂ L (A ).
For instance, the previous automaton also accepts the graph G from Figure 2, which is smaller than F . Indeed, when we fire the first transition, we can associate the two newly created tokens (in places B and C) to the same vertex [START_REF] Brunet | Kleene algebra with converse[END_REF]. This actually corresponds to composing the functions used to accept F with the homomorphism depicted with dotted arrows.

This automata model is expressive enough for Kleene allegories: for any expression e, we can construct a Petri automaton A (e) such that L (A (e)) = ◂ G (e) (Section IV).

We give three other examples of Petri automata to give more intuition on their behaviour.

The first transition in the previous Petri automaton splits the initial token into two tokens, which are moved concurrently in the remainder of the run. This corresponds to an intersection in the considered expression. This is to be contrasted with the behaviour of the following automaton, which we would construct for the non-ground expression a⋅b ∪ a⋅c. This automaton has two accepting runs: {A} , {B} , {D} and {A} , {C} , {E}, which can be used to accept the (graphs of the) ground terms a ⋅ b and a ⋅ c. In a sense, two transitions competing for the same tokens represent a non-deterministic choice, i.e., a union in the starting expression. Still in the first example, the two tokens created by the first transition are later collected in the final marking. Tokens may also be collected and merged by a transition. Consider for instance the following automaton for (a ∩ b ⋅ c) ⋅ d. It has only one accepting run, {A} , {B, C} , {B, D} , {E}, and this run can be used to read the fourth graph from Figure 1. As a last example, consider the following automaton for the expression a ∩ b + ⋅ c. The upper transition introduces a loop, so that there are infinitely many accepting runs. For any n > 0, the graph of the ground term a ∩ b n ⋅ c is accepted by this automaton. According to characterisation [START_REF] Conway | Regular algebra and finite machines[END_REF], the next step is to decide whether the containment L (A ) ⊆ L (B) holds, for two given Petri automata A and B. Several difficulties arise, that do not appear with classical word automata. Our solution nevertheless uses a standard coinductive approach, where we define an appropriate notion of simulation (Section V-C).

G(1) ∶= G(a) ∶= a G(w ⌣ ) ∶= G(w) G(u ⋅ v) ∶= G(u) G(v) G(u ∩ v) ∶= G(u) G(v)

II. GRAPH-THEORETICAL CHARACTERISATION

We consider the signature ⟨∩, ∪, ⋅, ⋅ + , ⋅ ⌣ , 0, 1⟩ of Kleene allegories, where e ⋆ is an abbreviation for 1 ∪ e + . We fix a set X of variables, and we denote by Reg ⌣∩ X the set of expressions e, f . . . built from variables in X with these connectives. Ground terms are the expressions u, v, w . . . built from X only with the sub-signature ⟨∩, ⋅, ⋅ ⌣ , 1⟩. If σ ∶ X → P (S × S) is an interpretation of the alphabet X into some space of relations, we write σ for the unique homomorphism extending σ into a function from Reg ⌣∩ X to P (S × S). An inequation between two expressions e and f is valid, written Rel ⊧ e ≤ f , if for any relational interpretation σ we have σ(e) ⊆ σ(f ).

We let G range over 2-pointed labelled directed graphs, which we simply call graphs in the sequel. Those are tuples ⟨V, E, ι, o⟩ with V a finite set of vertices, E ⊆ V × X × V a set of edges labelled with X, and ι, o ∈ V the two distinguished vertices, respectively called input and output.

Definition 1 (Graph of a ground term: G(w))

To each ground term w, we associate a graph G(w), by induction on w. The graph of a ∈ X has one edge labelled by a linking its input to its output. The graph for 1 has only one vertex, both input and output. The composition of two graphs with disjoint sets of vertices can be performed by identifying the output of the first graph and the input of the second one. The intersection on graphs consists in merging their inputs and merging their outputs. The converse consists simply in exchanging the input and the output of a graph. * See Figure 3 for a graphical description of this construction. Those graphs were introduced independently by Freyd and Scedrov [8, page 208], and Andréka and Bredikhin [START_REF] Andréka | The equational theory of union-free algebras of relations[END_REF].

Definition 2 (Graph homomorphism, preorders ◂ and ⊲) and(p, x, q) ∈ E 1 entails (ϕ(p), x, ϕ(q)) ∈ E 2 . We denote by ◂ the relation on graphs defined by G ◂ G ′ if there exists a graph homomorphism from G ′ to G. This relation gives rise to a preorder on ground terms, written ⊲ and defined by u

A graph homomorphism from ⟨V 1 , E 1 , ι 1 , o 1 ⟩ to ⟨V 2 , E 2 , ι 2 , o 2 ⟩ is a map ϕ ∶ V 1 → V 2 such that ϕ(ι 1 ) = ι 2 , ϕ(o 1 ) = o 2 ,
⊲ v if G(u) ◂ G(v). *
Given a set S of graphs, we write ◂ S for its downward closure: ◂ S ∶= {G G ◂ G ′ , G ′ ∈ S }. Similarly, we write ⊲ S for the downward closure of a set of ground terms w.r.t. ⊲.

As explained in the introduction, the above preorder on ground terms precisely characterises inclusion under arbitrary relational interpretations: [8, page 208]). For all ground terms u, v, we have

Theorem 3 ([2, Theorem 1], or
Rel ⊧ u ≤ v ⇔ u ⊲ v .
To extend this result to Kleene allegories, we introduce the following generalisation of the language of a regular expression. Sets of words become sets of ground terms.

Definition 4 (Terms and graphs of an expression)

The set of terms of an expression e ∈ Reg ⌣∩ X , written e , is the set of ground terms defined inductively as follows:

1 ∶= {1} 0 ∶= ∅ x ∶= {x} e ⋅ f ∶= {w ⋅ w ′ w ∈ e and w ′ ∈ f } e ∩ f ∶= {w ∩ w ′ w ∈ e and w ′ ∈ f } e ∪ f ∶= e ∪ f e ⋆ ∶= ⋃ n∈N {w 1 ⋅ ⋯ ⋅ w n ∀i, w i ∈ e } e ⌣ ∶= {w ⌣ w ∈ e } .
The set of graphs produced by an expression e, denoted by G (e) is the set of graphs associated to the ground terms in e :

G (e) ∶= {G(w) w ∈ e } . *

To obtain the characterisation announced in the introduction, we need a slight refinement of a lemma established by Andréka, Mikulás, and Németi [START_REF] Andréka | The equational theory of Kleene lattices[END_REF]: Lemma 5. For all expression e ∈ Reg ⌣∩ X X, and all relational interpretations σ ∶ X → P (S × S), we have

σ(e) = ⋃ u∈ e σ(u) = ⋃ w∈ ⊲ e σ(w) .
Proof. The first equality is exactly [1, Lemma 2.1]; for the second one, we use the fact that σ(w) ⊆ σ(u) whenever w ⊲ u, thanks to Theorem 3 (i.e., [2, Theorem 1]). Theorem 6. The following properties are equivalent, for all expressions e, f ∈ Reg ⌣∩ X :

(i) Rel ⊧ e ≤ f , (ii) e ⊆ ⊲ f , (iii) G (e) ⊆ ◂ G (f ).
Proof. We give a detailed proof in Appendix A. The implication (ii) ⇒ (i) follows easily from Lemma 5, and (iii) ⇒ (ii) is a matter of unfolding definitions. For (i) ⇒ (iii), we mainly use [2, Lemma 3].

(The exact characterisation announced in the introduction [START_REF] Conway | Regular algebra and finite machines[END_REF] follows: for any sets X, Y , we have Also notice that while G (f ) only contains graphs emanating from ground terms, this is not the case for its closure

◂ X ⊆ ◂ Y iff X ⊆ ◂ Y .)
◂ G (f ). For instance, ◂ G ((a ⋅ b) ∩ (c ⋅ d)) contains the follow-
ing graph, which is not the graph of any ground term.

III. PETRI AUTOMATA

We extend the set X of variables into a set X of labels: X ∶= X ∪{x ⌣ x ∈ X }∪{1}. A Petri automaton is a Petri net whose transition's outputs are labelled by X.

Definition 8 (Petri Automaton)

A Petri automaton A over the alphabet X is a tuple ⟨P, T , ι, F ⟩ where:

• P is a finite set of places,

• T ⊆ P (P ) × P X × P is a set of transitions,

• ι ∈ P is the initial place of the automaton,

• F ⊆ P (P ) is a set of final configurations, a configuration being a set of places. For each transition t = t, t ∈ T , t and t are assumed to be non-empty; t ⊆ P is the input of t; and t ⊆ X × P is the output of t. *

We use the graphical notation from the introduction to represent Petri automata; the Petri automaton from Figure 4 will be used as a running example.

From a configuration ξ ⊆ P , a transition

t = t, t ∈ T is enabled if t ⊆ ξ. If so, one may fire t, which produces a new configuration ξ ′ = ξ ∖t∪ p ∈ P ∃x ∈ X ∶ (x, p) ∈ t . We write ξ t → A ξ ′ in this case.
A set of transitions T ⊆ T is statically compatible (or just compatible) if their inputs are pairwise disjoint. If furthermore all transitions in T are enabled in a configuration ξ, one can observe that the configuration ξ ′ reached after firing them successively does not depend on the order in which they are fired. In that case we write ξ In the sequel, we assume all considered Petri automata to be safe. (I.e., in Petri nets terminology, such that any reachable marking has at most one token in each place [START_REF] Murata | Petri nets: Properties, analysis and applications[END_REF]). Formally, with our definitions: a Petri automaton ⟨P, T , ι, F ⟩ is safe if for all configuration ξ ⊆ P reachable from {ι} by firing any number of transitions, if t, t ∈ T is enabled from ξ, p ∈ ξ, and (x, p) ∈ t, then p ∈ t. Now we explain how to use Petri automata to define languages of graphs. We first define the runs of an automaton. Definition 9 (Run, accepting run, parallel run) A run is a sequence ξ = ⟨(ξ k ) 0⩽k⩽n , (t k ) 0⩽k<n ⟩ of configurations and transitions, such that ξ k ⊆ P , t k ∈ T and ∀k < n, ξ k t k → ξ k+1 . When ξ 0 = {ι} and ξ n ∈ F , we call ξ an accepting run.

T → A ξ ′ . A B G C E G D E G C E G D E G F G t 0 t 1 t 2 t 3 t 4 t 5
A parallel run is defined similarly, as a sequence

Ξ = ⟨(Ξ k ) 0⩽k⩽n , (T k ) 0⩽k<n ⟩, where the T k ⊆ T are compatible sets of transitions such that Ξ k T k → Ξ k+1 . *
(Note that a run ξ is uniquely determined by ξ 0 and the sequence (t k ): all subsequent configurations can be computed deterministically.) Consider the following sequence of transitions from the automaton in Figure 4:

ξ = ⟨(ξ 0 , ξ 1 , ξ 2 , ξ 3 , ξ 4 , ξ 5 , ξ 6 ) , (t 0 , t 1 , t 2 , t 3 , t 4 , t 5 )⟩, with ξ 0 ={A} , ξ 1 ={B, G} , ξ 2 = ξ 4 ={C, E, G} , ξ 3 = ξ 5 ={D, E, G} , ξ 6 ={F, G} . t 0 =({A} , {(b, B), (a, G)}) , t 1 =({B} , {(c, C), (b, E)}) , t 2 = t 4 =({C} , {(a, D)}) , t 3 =({D, E} , {(c, C), (b, E)}) , t 5 =({D, E} , {(d, F )}) .
We have

{A} t0 / / {B, G} t1 / / {C, E, G} t2,t4 / / {D, E, G} t3 o o t5 / / {F, G} ,
and since {A} is the initial configuration and {F, G} ∈ F , this sequence is an accepting run. It can be represented graphically as in Figure 5.

As for standard finite state automata, we now need to specify how to read a graph in an automaton. As explained in the introduction, this is done by linking the intermediate configurations of a run to vertices in the graph, and by imposing conditions to match transitions with labelled edges of the graph. Definition 10 (Reading, parallel reading, language of a run) A reading of G = ⟨V, E, ι, o⟩ along a run ξ = Figure 6: Graph produced by the run depicted in Figure 5.

⟨(ξ k ) 0⩽k⩽n , t k , t k 0⩽k<n ⟩ is a sequence (ρ k ) 0⩽k⩽n such that for all k, ρ k is a map from ξ k to V , ρ 0 (ξ 0 ) = {ι}, ρ n (ξ n ) =
{o}, and ∀k < n, the following holds:

• all tokens in the input of the transition are mapped to the same vertex in the graph: ∀p, q ∈ t k , ρ k (p) = ρ k (q); • the images of tokens in ξ k that are not in the input of the transition are unchanged: ∀p ∈ ξ k ∖ t k , ρ k (p) = ρ k+1 (p); • each pair in the output of the transition can be "validated" by the graph:

∀p ∈ t k , ∀(x, q) ∈ t k , x ∈ X ⇒(ρ k (p), x, ρ k+1 (q)) ∈ E, x = y ⌣ and y ∈ X ⇒(ρ k+1 (q), y, ρ k (p)) ∈ E, x = 1 ⇒ρ k (p) = ρ k+1 (q).
Similarly, we define a parallel reading ρ along some parallel run Ξ = ⟨(Ξ k ) 0⩽k⩽n , (T k ) 0⩽k<n ⟩ by requiring that: ρ 0 (Ξ 0 ) = {ι}, ρ n (Ξ n ) = {o}, and ∀k < n the following holds:

• ∀p ∈ Ξ k ∖ ⋃ t,t ∈T k t, ρ k+1 (p) = ρ k (p); • ∀ t, t ∈ T k , ∀p, q ∈ t, ρ k (p) = ρ k (q); • ∀ t, t ∈ T k , ∀p ∈ t, ∀(x, q) ∈ t, x ∈ X ⇒(ρ k (p), x, ρ k+1 (q)) ∈ E, x = y ⌣ and y ∈ X ⇒(ρ k+1 (q), y, ρ k (p)) ∈ E, x = 1 ⇒ρ k (p) = ρ k+1 (q).
The language of a run ξ, denoted by L (ξ) is the set of graphs that can be read along ξ. *

The language of a Petri automaton is finally obtained by considering all accepting runs.

Definition 11 (Language recognised by a Petri automaton)

The language recognised by A , written L (A ), is the following set of graphs:

L (A ) ∶= ⋃ ξ accepting in A L (ξ) . *
The language of a run ξ can be characterised by using a single graph which we call the graph produced by ξ: graphs are accepted by ξ exactly when they are smaller than the graph produced by ξ according to ◂ (Lemma 14 below). For instance, the run presented in Figure 5 produces the graph depicted in Figure 6.

This graph is obtained in two steps, by first considering a notion of trace, which is a graph labelled with X rather than X, and which actually corresponds to the notion of pomsettrace from standard Petri nets (see Section VII for more details on this correspondence).

The trace is constructed by creating a vertex k for each transition t k = t k , t k of the run, plus a final vertex n. We add an edge (k, x, l) whenever there is some place q such that (x, q) ∈ t k , and t l is the first transition after t k in the run with q among its inputs, or l = n if there is no such transition in the run.

Definition 12 (Trace of a run) Let ξ = ⟨(ξ k ) 0⩽k⩽n , t k , t k 0⩽k<n ⟩ be run. For an index k ⩽ n and a place q, let ν(k, q) be either the smallest index l such that k ⩽ l and q ∈ t l , or n if there is no such index.

The trace of ξ is the graph ξ ∶= ⟨{0, . . . , n} , E ξ , 0, n⟩ with

E ξ ∶= (k, x, ν(k + 1, q)) (x, q) ∈ t k . *
To get the final graph, which is labelled by X, one identifies nodes linked by edges labelled by 1, and one replaces each edge of the form (i, x ⌣ , j) by (j, x, i). Formally: Definition 13 (Graph produced by a run) Let ξ = ⟨(ξ k ) 0⩽k⩽n , t k , t k 0⩽k<n ⟩ be run. Let ≡ ξ be the smallest equivalence relation on {0, . . . , n} containing all pairs (i, j) such that (i, 1, j) ∈ E ξ .

The graph produced by ξ, is the graph G (ξ) defined by

G (ξ) ∶= ⟨{[i] ξ 0 ⩽ i ⩽ n } , E ′ ξ , [0] ξ , [n] ξ ⟩ [i] ξ ∶= {k ∈ {0, . . . , n} i ≡ ξ k } E ′ ξ ∶= ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ ([i] ξ , x, [j] ξ ) x ∈ X and ∃k ∈ [i] ξ , l ∈ [j] ξ ∶ (k, x, l) ∈ E ξ or (l, x ⌣ , k) ∈ E ξ ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ *
We write G (A ) for the set of graphs produced by accepting runs of a Petri automaton A . To avoid confusions with the language L (A ) of A , we write "G is produced by A " when G ∈ G (A ), reserving language theoretic terminology like "G is accepted by A " or "A recognises G" to cases where we mean G ∈ L (A ).

The graph produced by the run presented in Figure 5 happens to be equal to its trace, since it is labelled in X only. A more involved example is given in Figures 7 to 9. Notice that although the trace of a run is acyclic and can be endowed with a partial order structure (simply check that ∀p, ν(_, p) is increasing), it is not necessarily the case for its produced graph.

Lemma 14. For any accepting run ξ, we have

G ∈ L (ξ) if and only if G ◂ G (ξ).
Proof. Suppose there exists a graph homomorphism ϕ from G (ξ) to G. Then we can build a reading by defining ρ k (p) = ϕ([ν(k, p)] ξ ) for 0 ⩽ k ⩽ n and p ∈ ξ k . On the other hand, if we have a reading (ρ k ) 0⩽k⩽n of G, we can build a homomorphism ϕ by letting ϕ([k] ξ ) = ρ k (p) for any p ∈ t k . As (ρ k ) k is a reading, ϕ is well defined. The details of this proof can be found in Appendix B.

As an immediate corollary, we obtain the following characterisation of the language of a Petri automaton.

Corollary 15. L (A ) =

◂ G (A ). The left-hand side language is defined through readings along accepting runs, which is a local and incremental notion and which allows us to define simulations in Section V-C. By contrast, the right-hand side language is defined globally, which eases the following construction of an automaton recognising the language of an expression.

IV. FROM EXPRESSIONS TO AUTOMATA

We now show how to associate to any expression e ∈ Reg ⌣∩ X an automaton A (e) that recognises the language ◂ G (e). In fact the automaton we obtain has an even stronger connection with e: the graphs in G (e) are exactly those produced by accepting runs in A (e). To make the construction simpler, we first modify the expression so that the operator ⋅ ⌣ is only applied to variables, by using the following rewriting system:

(a ∪ b) ⌣ → a ⌣ ∪ b ⌣ 0 ⌣ → 0 (a + ) ⌣ → (a ⌣ ) + (a ⋅ b) ⌣ → b ⌣ ⋅ a ⌣ 1 ⌣ → 1 a ⌣⌣ → a (a ∩ b) ⌣ → a ⌣ ∩ b ⌣ .
(These rules preserve the set of graphs of the expression; also recall that e ⋆ is a shorthand for e + + 1, so that we do not need to handle it explicitly.)

The formal construction is inductive; it is given in Definition 16 below. We describe it first in informal terms. For the case of x ∈ X, we simply build an automaton with a single transition labelled by x, going from the initial place to a distinct final place 2 . The union consists in putting both automata side by side, and merging their initial places. For the composition of A 1 and A 2 on the other hand we put one automaton in front of the other:

• the initial place of the resulting automaton is that of A 1 ;

• the final configurations are those of A 2 ;

• for each final configuration f of A 1 , and for each initial transition (ι 2 , t) coming out of the initial place of A 2 , we add a transition with input f and output t. This last step amounts to adding epsilon transitions from the final configurations of A 1 to the initial place of A 2 , and then apply some epsilon-elimination procedure. We also put the two automata side by side for the intersection, but we merge their initial places, their initial transitions, and their final configurations:

• for any pair of initial transitions of the two automata ({ι 1 } , t 1 ), ({ι 2 } , t 2 ), we put in the intersection automaton the transition ({ι 1 } , t 1 ∪ t 2 ); • a final configuration of this automaton is the union of a final configuration from A 1 and a final configuration of A 2 . For the transitive closure (⋅ + ), we use the ideas for union and composition, adding loops from the final configurations using the initial transitions of the automaton.

Definition 16

To each expression e ∈ Reg ⌣∩ X , we associate a Petri automaton A (e) defined inductively as follows:

• x ∈ X, A (x) ∶= ⟨{0, 1} , {({0} , {(x, 1)})} , 0, {{1}}⟩ • A (0) ∶= ⟨{0} , ∅, 0, ∅⟩ • A (e 1 ∪ e 2 ) ∶= ⟨P 1 ∪ P 2 , T , ι 1 , F 1 ∪ F 2 ⟩ with T ∶= T 1 ∪ T 2 ∪ ({ι 1 } , t) ({ι 2 } , t) ∈ T 2 . • A (e 1 ⋅ e 2 ) ∶= ⟨P 1 ∪ P 2 , T , ι 1 , F 2 ⟩ with T ∶= T 1 ∪ T 2 ∪ (f, t) f ∈ F 1 and ({ι 2 } , t) ∈ T 2 . • A (e + 1 ) ∶= ⟨P 1 , T , ι 1 , F 1 ⟩ with T ∶= T 1 ∪ (f, t) f ∈ F 1 and ({ι 1 } , t) ∈ T 1 . • A (e 1 ∩ e 2 ) ∶= ⟨P 1 ∪ P 2 , T , ι 1 , F ⟩ with F ∶= {f 1 ∪ f 2 f 1 ∈ F 1 , f 2 ∈ F 2 } and T ∶= t, t ∃i ∈ {1, 2} ∶ t, t ∈ T i , ι i ∉ t ∪ ({ι 1 } , t 1 ∪ t 2 ) ∀i ∈ {1, 2} , ({ι i } , t i ) ∈ T i .
(In the inductive cases, we assume A (e i ) = ⟨P i , T i , ι i , F i ⟩ for i ∈ {1, 2}, with P 1 ∩ P 2 = ∅.) *

We prove by induction on e that A (e) is indeed a safe Petri automaton; for the safety requirement, we add to the induction hypothesis the fact that for any configuration ξ accessible in A (e), if there is a final configuration f ∈ F such that f ⊆ ξ, then f = ξ. Another invariant is that the initial place never appears in a final configuration, nor in the output of any transition. Note that the place ι 2 becomes unreachable by construction in the cases for union, composition and intersection, so that it could safely be removed, together with the associated transitions.

Theorem 17 (Correctness). For all expression e ∈ Reg ⌣∩ X , L (A (e)) = ◂ G (e).

Proof. We prove a stronger result: G (A (e)) = G (e) (up to graph isomorphisms-see Appendix C). This allows us to conclude thanks to Corollary 15.

Corollary 18. The (in)equational theory of Kleene allegories is co-recursively enumerable.

Proof. Construct Petri automata for the two expressions and enumerate all potential counter-examples, i.e., graphs. A graph is a counter-example if it can be read in one automaton but not in the other, which is a decidable property.

Remark 19. If e is an expression without intersection, converse or 1, it can be shown that the transitions in A (e) are all of the form ({p} , {(x, q)}), with only one input, one output and a label in X. As a consequence, the accessible configurations are singletons, and the resulting Petri automaton has the structure of a non-deterministic finite-state automaton (NFA). Actually, in that case, the construction we described above is just a variation on Thompson's construction [START_REF] Thompson | Regular expression search algorithm[END_REF], with inlined epsilon transition elimination.

V. COMPARING AUTOMATA

A. Simple automata

The above results hold for the whole syntax of regular expressions with converse and intersection. However, in the remainder of the paper, we have to focus on expressions without converse or identity. This is because in combination with intersection, these two operations introduce cycles in the graphs associated to ground terms. Consider for instance the graphs for a ∩ 1 and a ∩ b ⌣ :

G(a ∩ 1) = a G(a ∩ b ⌣ ) = a b .
Since reflexive-transitive closure (⋅ ⋆ ) implicitly contains an occurrence of the identity, we also have to forbid this operator. Instead, we add the transitive closure (⋅ + ). We thus work with expressions from Reg ∩- X , defined with the following syntax:

e, f ∈ Reg ∩- X ∶∶= x ∈ X e ∩ f e ∪ f e ⋅ f e + 0.
Accordingly, ground terms are restricted to the following syntax: u, v, w ∶∶= x ∈ X w ⋅ w w ∩ w. Automata built using Definition 16 from expressions without converse or unit only have transitions labelled with X. This corresponds to the notion of simple automata.

Definition 20 (Simple Petri automaton) A Petri automaton

A = ⟨P, T , ι, F ⟩ is called simple if ∀ t, t ∈ T , ∀(x, p) ∈ t, x ∈ X. *
For all e ∈ Reg ∩- X , A (e) is simple. Moreover for any run ξ of a simple Petri automaton, ξ = G (ξ) (up to isomorphism); in particular, a simple automaton only produces acyclic graphs.

B. Intuitions

In this section, we show how the notion of simulation relation, that allows to compare NFA, can be adapted to handle simple Petri automata. Consider two automata A 1 = ⟨P 1 , T 1 , ι 1 , F 1 ⟩ and A 2 = ⟨P 2 , T 2 , ι 2 , F 2 ⟩, we try to show that for any graph G accepted by A 1 , G is recognised by A 2 . By Lemma 14, this amounts to proving that for any accepting run ξ in A 1 , G (ξ) is recognised by some accepting run ξ ′ in A 2 . Leaving non-determinism apart, the first idea that comes to mind is to find a relation between the configurations in A 1 and the configurations in A 2 , that satisfy some conditions on the initial and final configurations, and such that if

ξ k ≼ ξ ′ k and ξ k t → A1 ξ k+1 , then there is a configuration ξ ′ k+1 in A 2 such that ξ k+1 ≼ ξ ′ k+1 , ξ ′ k t ′ → A2 ξ ′ k+1
, and these transition steps are compatible in some sense. However, such a definition will not give us the result we are looking for. Consider these two runs:

A B B C D 1 2 a b c W Y Y X Z 1 ′ 2 ′ b a c
The graphs produced by the first and the second runs correspond respectively to the ground terms a∩(b⋅c) and (a⋅c)∩b. These two terms are incomparable, but the relation ≼ depicted below satisfies the previously stated conditions.

{A} 1 / / {B, C} 2 / / {B, D} {W } ≼ 1' / / {X, Y } ≼ 2' / / {Y, Z} ≼
The problem here is that in Petri automata, runs are token firing games. To adequately compare two runs, we need to closely track the tokens. For this reason, we will relate a configuration ξ k in A 1 not only to a configuration ξ ′ k in A 2 , but to a map η k from ξ ′ k to ξ k . This will enable us to associate with each token situated on some place in P 2 another token placed on A 1 .

We want to find a reading of G (ξ) in A 2 , i.e., a run in A 2 together with a sequence of maps associating places in A 2 to positions in G (ξ). Consider the picture below. Since we already have a reading of G (ξ) along ξ (by defining ρ k (p) = ν(k, p), as in the proof of Lemma 14), it suffices to find maps from the places in A 2 to the places in A 1 (the maps η k ): the reading of G (ξ) in A 2 will be obtained by composing η k with ρ k .

G (ξ)

ξ 0 t0 / / ξ 1 t1 / / ⋯ tn-1 / / ξ n tn / / ξ n+1 ξ ′ 0 η0 O O t ′ 0 / / ξ ′ 1 t ′ 1 / / η1 O O ⋯ t ′ n-1 / / ξ ′ n ηn O O t ′ n / / ξ ′ n+1 ηn+1 O O ρ0 7 7 ρ1 = = ρn Z Z ρn+1 e e
We need to impose some constraints on the maps (η k ) to ensure that (ρ k ○ η k ) 0⩽k⩽n is indeed a correct reading in A 2 . First, we need to ascertain that a transition t ′ k in A 2 may be fired from the reading state ρ k ○ η k to reach the reading state ρ k+1 ○ η k+1 . Furthermore, as for NFA, we want transitions t k and t ′ k to be related: specifically, we require t ′ k to be included (via the homomorphisms η k and η k+1 ) in the transition t k . This is meaningful because transition t k contains a lot of information about the vertex k of G (ξ) and about ρ: the labels of the outgoing edges from k are the labels on the output of t k , and the only places that will ever be mapped to k in the reading ρ are exactly the places in the input of t k .

A B C 0 a b X Y Z 0 ′ a a
This already shows an important difference between the simulations for NFA and Petri automata. For NFA, we relate a transition p a → p ′ to a transition q a → q ′ with the same label a.

Here the transitions ξ k

t k → A1 ξ k+1 and ξ ′ k t ′ k → A2 ξ ′
k+1 may have different labels. Consider the step represented on the right, corresponding to a square in the above diagram. The output of 0 has a label b that does not appear in 0' , and 0' has two outputs labelled by a. Nevertheless this satisfies the conditions informally stated above, indeed, a ∩ b ⩽ a ∩ a holds.

However this definition is not yet satisfactory. Consider the two runs below:

A B C D 0 1 a b c X Y Z Z T T U 0 ′ 1 ′ 2 ′ a a b c
Their produced graphs correspond respectively to the ground terms a ⋅ (b ∩ c) and (a ⋅ b) ∩ (a ⋅ c). The problem is that a ⋅ (b ∩ c) ⩽ (a ⋅ b) ∩ (a ⋅ c), but with the previous definition, we cannot relate these runs: they do not have the same length. The solution here consists in grouping the transitions 1' and 2' together, and consider these two steps as a single step in a parallel run. This last modification gives us a notion of simulation that suits our needs.

C. Simulations

Definition 21 (Simulation) A relation ≼ ⊆ P (P 1 ) × P (P 2 ⇀ P 1 ) between the configurations of A 1 and the partial maps from the places of A 2 to the places of A 1 is called a simulation between A 1 and A 2 if:

• if ξ ≼ E and η ∈ E then the range of η must be included in ξ;

• {ι 1 } ≼ {[ι 2 ↦ ι 1 ]}; • if ξ ≼ E and ξ t,t → A1 ξ ′ , then ξ ′ ≼ E ′
where E ′ is the set of all η ′ such that there is some η ∈ E and a compatible set of transitions T ⊆ T 2 such that: • if ξ ≼ E and ξ ∈ F 1 , then there must be some η ∈ E such that dom (η) ∈ F 2 . *

-dom (η) T → A2 dom (η ′ ); -∀ t ′ , t ′ ∈ T, η(t ′ ) ⊆ t and ∀(x, q) ∈ t ′ ,(x, η ′ (q)) ∈ t; -∀p ∈ dom (η) , ∀ t ′ , t ′ ∈ T, p ∉ t ′ ⇒ η(p) = η ′ (p).
We will now prove that the language of A 1 is contained in the language of A 2 if and only if there exists such a simulation. We first introduce the following notion of embedding.

Definition 22 (Embedding) Let ξ = ⟨(ξ k ) 0⩽k⩽n , (t k ) 0⩽i<n ⟩ be a run in A 1 , and Ξ = ⟨(Ξ k ) 0⩽k⩽n , (T i ) 0⩽i<n ⟩ a parallel run in A 2 . An embedding of Ξ into ξ is a sequence (η i ) 0⩽i⩽n of maps such that for any i < n, we have:

• η i is a map from Ξ i to ξ i ; • the image of T i by η i is included in t i , meaning that
for any t, t ∈ T i , for any p ∈ t and (x, q) ∈ t, η i (p) is contained in the input of t i and (x, η i+1 (q)) is in the output of t i ; • the image of the tokens in Ξ i that do not appear in the input of T i are preserved (η i (p) = η i+1 (p)) and their image is not in the input of t i .

ξ i ti / / ξ i+1 Ξ i ηi O O Ti / / Ξ i+1 ηi+1 O O * Figure 10 illustrates the embedding of some parallel run, producing G (((b ⋅ c ⋅ a ⋅ b) ∩ (b ⋅ b ⋅ c ⋅ a)) ⋅ d)
, into the run presented in Figure 5. Notice that is it necessary to have a parallel run instead of a simple one: to find something that matches the second transition in the upper run, we need to fire two transitions in parallel in the lower run.

There is a close relationship between simulations and embeddings:

Lemma 23. Let A 1 and A 2 be two Petri automata, the following are equivalent:

1) there exists a simulation ≼ between A 1 and A 2 ;

2) for any accepting run ξ in A 1 , there is an accepting parallel run Ξ in A 2 that can be embedded into ξ.

Proof. If we have a simulation ≼, let ξ = ⟨(ξ k ) 0⩽k⩽n , (t k ) 0⩽k<n ⟩ be an accepting run in A 1 . By the definition of simulation, we can find a sequence of sets of maps (E k ) 0⩽k⩽n such that E 0 = {[ι 2 ↦ ι 1 ]} and ∀k, ξ k ≼ E k . Furthermore, we can extract from this a sequence of maps (η k ) 0⩽k⩽n and a sequence of parallel transitions (T k ) 0⩽k<n such that (η k ) is an embedding of ⟨(dom (η k )) 0⩽k⩽n , (T k ) 0⩽k<n ⟩ (which is accepting) into ξ. This follows directly from the definitions of embedding and simulation.

On the other hand, if we have property 2., then we can define a relation ≼ by saying that ξ ≼ E if there is an accepting run ξ ′ = ⟨(ξ ′ k ) 0⩽k⩽n , (t k ) 0⩽k<n ⟩ in A 1 such that there is an index k 0 : ξ = ξ ′ k0 ; and the following holds: η ∈ E if there is an accepting parallel run Ξ = ⟨(Ξ k ) 0⩽k⩽n , (T k ) 0⩽k<n ⟩ and (η ′ k ) 0⩽k⩽n an embedding of Ξ into ξ such that η = η ′ k0 . It is then immediate to check that ≼ is indeed a simulation.

If η is an embedding of Ξ into ξ, we can easily check that (ρ i ○ η i ) 0⩽i⩽n is a parallel reading of G (ξ) along Ξ in A 2 . Thus, it is clear that once we have such a run Ξ with the sequence of maps η, we have that G (ξ) is indeed in the language of A 2 . The more difficult question is the completeness of this approach: if G (ξ) is recognised by A 2 , is it always the case that we can find a run Ξ that may be embedded into ξ? The answer is affirmative, thanks to Lemma 24 below. If (ρ j ) 0⩽j⩽n is a reading of G along ξ = ⟨(ξ k ) 0⩽k⩽n , t k , t k 0⩽k<n ⟩, we write active(j) for the only position in ρ j (t j ) 3 . We call ⩿ a consistent ordering on G = ⟨V, E, ι, o⟩ if ⟨V, ⩿⟩ is a linear order and (p, x, q) ∈ E entails p ⩿ q.

Lemma 24. Let G ∈ L (A 2 ) and ⩿ be any consistent ordering on G. Then there exists a run ξ and a reading (ρ j ) 0⩽j⩽n of G along ξ such that ∀k, active(k) ⩿ active(k + 1).

Proof. The proof of this result is achieved by taking any run ξ accepting G, and then exchanging transitions in ξ according to ⩿, while preserving the existence of a reading. The details of this proof being a bit technical, we moved them to Appendix D.

(Notice that if G contains cycles, this lemma cannot apply because of the lack of consistent ordering.) Lemma 24 enables us to build an embedding from any reading of G (ξ) in A 2 .

Lemma 25. Let ξ a accepting run of A 1 . Then G (ξ) is in L (A 2 ) if and only if there is an accepting parallel run in A 2 that can be embedded into ξ.

Proof. The detailed proof of this result can be found in Appendix E.

For the if direction, we build a parallel reading from the embedding, as explained above. For the other direction, we consider a reading of G (ξ) in A 2 along some run ξ ′ . Notice that the natural ordering on N is consistent for G (ξ); we may thus change the order of the transitions in ξ ′ (using Lemma 24) and group them adequately to obtain a parallel reading Ξ that embeds in ξ.

So we know that the existence of embeddings is equivalent to the inclusion of languages, and we previously established 3 Recall that if (ρ j ) 0⩽j⩽n is a reading along ξ then for any p, q ∈ t j , we have ρ j (p) = ρ j (q). that it is also equivalent to the existence of a simulation relation. Hence, the following characterisation holds:

Theorem 26. Let A 1 and A 2 be two simple Petri automata. L (A 1 ) ⊆ L (A 2 ) if and only if there exists a simulation relation ≼ between A 1 and A 2 .

Proof. By Lemmas 14, 23 and 25.

As Petri automata are finite, there are finitely many relations in P (P (P 1 ) × P (P 2 ⇀ P 1 )). The existence of a simulation thus is decidable, allowing us to prove the main result: Theorem 27. Given two expressions e, f ∈ Reg ∩- X , testing whether Rel ⊧ e = f is decidable.

Proof. By Theorems 6, 17 and 26, and reasoning by double inclusion.

In practice, we can build the simulation on-the-fly, starting from the pair ({ι 1 } , {[ι 2 ↦ ι 1 ]}) and progressing from there. We have implemented this algorithm in OCAML [START_REF] Brunet | Web appendix to this abstract[END_REF]. Even though its theoretical worst case time complexity is huge 4 , we get a result almost instantaneously on simple one-line examples.

D. The problems with converse or unit

The previous algorithm is not complete in presence of converse or unit. More precisely, Lemma 25 does not hold for general automata. Indeed, it is not possible to compare two runs just by relating the tokens at each step, and checking each transition independently. Consider the automaton from Figure 11. This automaton has in particular an accepting run recognising 1 ∩ abc. Let us try to test if this is smaller than the following runs from another automaton (we represent the transitions simply as arrows, because they only have a single input and a single output):

x 0 x 1 x 2 x 3 x 4 x 5 x 6 a b c a b c y 0 y 1 y 2 y 3 y 4 y 5 y 6 y 7 a b c a b b c
It stands to reason that we would reach a point where for the first run:

{D, E} ≼ {[x 3 ↦ D]}
and for the second run:

{D, E} ≼ {[y 3 ↦ D]} .
So if it were possible to relate the end of the runs just with this information, they should both be bigger than 1 ∩ abc or both smaller or incomparable. But in fact the first run (recognising abcabc) is bigger than 1 ∩ abc but the second (recognising abcabbc) is not. This highlights the need for having some memory of previously fired transition when trying to compare runs of general Petri automata, thus preventing our local approach to bear fruits. The same kind of example could be found with the converse operation instead of 1.

VI. COMPLEXITY

The previous notion of simulation actually allows us to decide language inclusion of simple automata in EXPSPACE. We actually obtain that the problem is EXPSPACE-complete.

Lemma 28. Comparing simple Petri automata is EXPSPACEeasy.

Proof. Our measure for the size of an automaton here is its number of places (the number of transitions is at most exponential in this number). Here is a non-deterministic semialgorithm that tries to refute the existence of a simulation relation between A 1 and A 2 . 1: start with ξ ∶= {ι 1 } and

E ∶= {[ι 2 ↦ ι 1 ]}; 2: if ξ ∈ F 1 , check if there is some η ∈ E such that dom (η) ∈ F 2 , if not return FALSE; 3: choose non-deterministically a transition t, t ∈ T 1 such that t ⊆ ξ; 4: fire t, t , which means that ξ ∶= ξ ∖ t ∪ p ∈ P 1 ∃x ∈ X ∶ (x, p) ∈ t ;
5: have E progress along t, t as well, according to the conditions from Definition 21. 6: go to step 2. All these computations can be done in exponential space. In particular as ξ is a set of places in P 1 , it can be stored in space P 1 × log( P 1 ). Similarly, E, being a set of partial functions from P 2 to P 1 , each of which of size P 2 × log( P 1 + 1), can be stored in space P 1 + 1 P2 × P 2 × log( P 1 + 1). This nondeterministic EXPSPACE semi-algorithm can then be turned into an EXPSPACE algorithm by Savitch' theorem [START_REF] Savitch | Relationships between nondeterministic and deterministic tape complexities[END_REF].

One can check that the number of places in A (e) is linear in the size of e. (The exponential upper-bound on the number of transitions is asymptotically reached, consider for instance the automaton for (x 1 ∪ y 1 ) ∩ (x 2 ∪ y 2 ) ∩ ⋅ ⋅ ⋅ ∩ (x n ∪ y n ).) Therefore, the previous Lemma gives us a EXPSPACE algorithm for deciding the (in)equational theory of identity-free relational Kleene lattices.

Theorem 29. Comparing simple Petri automata is EXPSPACE-complete.

Proof. By Lemma 28, it suffices to show hardness. We perform a reduction from the equality of languages denoted by regular expressions with squaring (e 2 ∶= e ⋅ e), an EXPSPACEcomplete problem [START_REF] Meyer | The equivalence problem for regular expressions with squaring requires exponential space[END_REF]. To avoid confusion, the regular language denoted by the expression e will be written e . Any word u can be see uniquely as a linear graph λ(u). By extension, the set of graphs of words from e will be denoted by λ e . First, notice that if u and v are just words over X, λ(u) ◂ λ(v) is equivalent to u = v. Because of this, it is straightforward to check that for any e, f ∈ Reg 2 X the following holds

◂ (λ e ) = ◂ (λ f ) ⇔ e = f . (8)
Given an expression e on this signature, we can build in linear time a Petri automaton A , with a linear number of places and transitions. The closure of the language denoted by e is be exactly the language recognised by A . This automaton is not simple: some outgoing arcs are labelled with 1; therefore, this reduction only ensures that the equivalence of arbitrary Petri automata is EXPSPACE-hard. To get EXPSPACE-hardness for simple Petri automata, we need to refine the construction so that 1 is interpreted as a standard letter. (More details are given in Appendix F.)

The automata we produce here only have one final configuration, consisting in a singleton. The construction is a straightforward adaptation of Thompson's algorithm for NFA [START_REF] Thompson | Regular expression search algorithm[END_REF]. The only interesting case is for computing an automaton for e = (e 1 )

2 . We represent it graphically in Figure 12.

The transitions labelled by X are a shorthand for a set of transitions, containing for each letter x in X a transition with one output, labelled by x. This construction is linear: the automaton for e 1 is not copied. Furthermore, a run in this automaton will start by sending one token in ○ and one in ι 1 , the initial state of the automaton for e 1 . Then it will perform a run in this automaton until a single token reaches the final state for e 1 , f n 1 . At this point the tokens from ○ and f n 1 will be sent to • and ι 1 , starting a new run of e 1 . When a token is finally sent to f n 1 , it can be consumed together with the one in •, to reach the final configuration.

This proof does not allow us to deduce that also the (in)equational theory of Kleene allegories is EXPSPACE-hard: the Petri automata we construct are not associated to some expressions of polynomial size, a priori.

VII. RELATIONSHIP WITH STANDARD PETRI NET NOTIONS

Our notion of Petri automaton is really close to the standard notion of labelled (safe) Petri net, where the transitions themselves are labelled, rather than their outputs. We motivate this design choice, and we relate some of the notions we introduced to the standard ones [START_REF] Murata | Petri nets: Properties, analysis and applications[END_REF].

Any Petri automaton can be translated into a safe Petri net whose transitions are labelled by X ⊎ {τ }, the additional label τ standing for silent actions. For each automaton transition ({p 1 , . . . , p n } , {(x 1 , q 1 ), . . . , (x m , q m )}) with m > 1, we introduce m fresh places r 1 , . . . , r m and m + 1 transitions:

• a silent transition t 0 with preset {p 1 , . . . , p n } and postset {r 1 , . . . , r m }; • and for each 1 ⩽ k ⩽ m a transition t k labelled by x k , with preset {r k } and postset {q k }. The inductive construction from Section IV is actually simpler to write using labelled Petri nets, as one can freely use τlabelled transitions to assemble automata into larger ones, one does not need to perform the τ -elimination steps on the fly.

On the other side, we could not define an appropriate notion of simulation for Petri nets: we need to fire several transitions at once in the small net, to provide enough information for the larger net to answer; delimiting which transitions to group and which to separate is non-trivial; similarly, defining a notion of parallel step is delicate in presence of τ -transitions. By switching to our notion of Petri automata, we impose strong constraints about how those τ -transitions should be used, resulting in a more fitted model.

To describe a run in a Petri net N , one may use a process p ∶ K → N , where K is an occurrence net (a partially ordered Petri net) [START_REF] Goltz | The non-sequential behaviour of petri nets[END_REF]. The graphical representation (Figures 5, 7 and 10) we used to describe runs in an automaton are in fact a mere adaptation of this notion to our setting (with labels on arcs rather than on transitions).

Our notion ξ of trace of a run actually corresponds to the standard notion of pomset-trace, via dualisation (see Appendix H). Jategaonkar and Meyer showed that the pomsettrace equivalence problem for safe Petri nets is EXPSPACEcomplete [START_REF] Jategaonkar | Deciding true concurrency equivalences on safe, finite nets[END_REF]. However this equivalence is too strong and does not coincide with the one discussed in the present paper, even for simple Petri automata. The graph produced by a run is its trace in this case, so that pomset-trace equivalence for Petri nets corresponds to equivalence of the sets of graphs produced by Petri automata (G (A ) = G (B), up to graph isomorphism). However, for the equational theory we consider, we need to compare the languages, which are downward-closed sets of graphs, (

◂ G (A ) = ◂ G (B), i.e., L (A ) = L (B))
rather than the sets of graphs themselves. Also note that the class of sets of graphs produced by Petri automata ({G (A ) A a Petri automaton }) is not closed under downward closure. Intuitively, the width of any graph in G (A ) is bounded by the number number of places of A , but ◂ G (A ) usually contains graphs of arbitrary width. As a consequence, one cannot easily reduce our problem to pomsettrace equivalence of safe Petri nets.

VIII. DIRECTIONS FOR FUTURE WORK

The automata model we introduced to recognise downwardclosed graph languages allowed us to obtain the decidability of identity-free relational Kleene lattices, an (in)equational theory studied recently by Andréka et al. [START_REF] Andréka | The equational theory of Kleene lattices[END_REF]. Thanks to this model, we also obtained that the (in)equational theory of Kleene allegories is co-recursively enumerable. We leave several questions open.

First, is the (in)equational theory of Kleene allegories decidable? Two approaches could provide an affirmative answer: finding an algorithm for comparing arbitrary safe Petri automata, or finding a complete and recursively enumerable axiomatisation.

Second, can we obtain a Kleene-like theorem for Petri automata: is the language of any Petri automaton also the language of a Kleene allegory term? This question can be restricted to simple Petri automata; if one of the answers is negative, is there an algebraic way of representing these automata? Which are the missing operators? Lemma 32. Suppose t k and t k+1 are exchangeable for some 0 ⩽ k < n-1. We write

C ′ = ξ k ∖t k+1 ∪ p ∃x ∶ (x, p) ∈ t k+1 Then ξ k t k+1 → A C ′ and C ′ t k → A ξ k+2 . Furthermore, for any graph G, if G ∈ L (ξ), then G ∈ L (ξ[k ↔ k + 1]), where: ξ[k ↔ k + 1] ∶= ⟨ (ξ 0 , ξ 1 , ⋯, ξ k , C ′ , ξ k+2 ⋯, ξ n ) , (t 0 , t 1 , ⋯, t k+1 , t k , ⋯, t n-1 )⟩ Proof. The fact that ξ k t k+1 → A C ′ and C ′ t k → A ξ k+2
is trivial to check, with the definition of exchangeable.

Let (ρ j ) 0⩽j⩽n be a reading of G along ξ. If ρ ′ j 0⩽j⩽n is defined by:

ρ ′ j (p) = ⎧ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎩ ρ j (p) if j ≠ k + 1, ρ k+2 (p) if j = k + 1 and (x, p) ∈ t k+1 for some x, ρ k (p) otherwise. Then ρ ′ j 0⩽j⩽n is a reading of G along ξ[k ↔ k + 1].
Recall that if (ρ j ) 0⩽j⩽n is a reading of G along ξ we write active(j) for the only position in ρ j (t j ).

Lemma 33. Let ⩿ be any consistent ordering (a linear ordering compatible with the directed edges of the graph) on G. If (ρ j ) 0⩽j⩽n is a reading of G along ξ, and if active(k + 1) ⩿ active(k) for some k, then t k and t k+1 are exchangeable.

Proof. Let G = ⟨V, E, ι, o⟩. As (ρ i ) 0⩽j⩽n is a reading, for any

(x, p) ∈ t k , (active(k), x, ρ k+1 (p)) ∈ E, thus active(k) ⋖ ρ k+1 (p).
We know that active(k + 1) ⩿ active(k), meaning by transitivity that active(k + 1) ⋖ ρ k+1 (p). Hence active(k + 1) ≠ ρ k+1 (p) and because (ρ i ) 0⩽j⩽n is a reading we can infer that p ∉ t k+1 , thus proving that t k and t k+1 are exchangeable.

Proof of Lemma 24. Because G is in L (A ), we can find a reading ρ ′ along some run ξ. If that reading is not in the correct order, then by Lemma 33 we can exchange two transitions and Lemma 32 ensures that we can find a corresponding reading. We repeat this process until we get a reading in the correct order.

E. Omitted proof: Lemma 25

Let ξ = ⟨(ξ k ) 0⩽k⩽n , (t k ) 0⩽k<n ⟩ be a run, with t k = t k , t k for all k. Define ρ 1 k (p) ∶= ν(k, p) for all index k place p ∈ ξ k . We have that ρ 1 k 0⩽k⩽n is a reading of G (ξ) along ξ. • Assume an embedding (η k ) 0⩽k⩽n of an accepting parallel run Ξ into ξ. We define a parallel reading (ρ

2 k ) of G (ξ) in A 2 by letting ρ 2 k (p) ∶= ρ 1 k (η k (p)).
• On the other hand, notice that the natural ordering on N is consistent for G (ξ), and that ∀0 ⩽ k < n, ρ 1 k (t k ) = {k}. By Lemma 24 we gather that G (ξ) is in L (A 2 ) if and only if there exists a reading (ρ 2 j ) 0⩽j⩽n ′ of G (ξ) along some run ξ ′ = ⟨ ξ ′ j 0⩽j⩽n ′ , (t ′ j ) 0⩽j<n ′ ⟩ such that ∀j, active(j) ⩽ active(j + 1) (with active(j) the only position in ρ 2 j (t j )). Now, suppose we have such a reading; we can build an embedding (η k ) 0⩽k⩽n as follows. For k < n, define T k ∶= t ′ j , t ′ j active(j) = k . We describe the construction incrementally:

-

η 0 = [ι 2 ↦ ι 1 ]. -For all p ∈ dom (η k ) ∖ ⋃ t,t ∈T k t we simply set η k (p) = η k-1 (p). -Otherwise, ∀ t ′ j , t ′ j ∈ T k , let q ∈ t ′ j .
Then, for all (x, p) in t ′ j , because ρ 2 is a reading and by construction of G (ξ) we also know that there is some p ′ ∈ ξ k+1 that satisfies (x, p ′ ) ∈ t k and ρ 1 k+1 (p ′ ) = ρ 2 j+1 (p). That p ′ is a good choice for p, hence we define η k (p) = p ′ . It is then administrative to check that (η k ) 0⩽k⩽n is indeed an embedding.

F. Omitted proof: Lemma 29

We define the automaton of a regular expression with squaring with a single final state. We describe this construction graphically.

• 1:

0 1 1 • x: ι f x • e 1 ∪ e 2 : ι 1 f n 1 e 1 ι 2 f n 2 e 2 ι f n 1 1 1 1 • e 1 ⋅ e 2 : ι 1 f n 1 = ι 2 e 1
f n 2 e 2

• e ⋆ 1 :

ι 1 f n 1 e 1 ι f n 1 1 1 1
• e 2 1 :

ι 1 f n 1 e 1 ι f n ○ • 1 1 1 1 1 X X
This construction can be performed in linear time and space. By further analysing this construction, one can prove that 1) λ e ⊆ L (A (e));

2) for every G ∈ G (A (e)), there is a word w ∈ e such that G ◂ λ(w).

By combining Items 1 and 2 we establish that L (A (e)) = ◂ λ e .

Thus by Equation ( 8), we get that e = f is equivalent to L (A (e)) = L (A (f )). This gives us the EXPSPACEhardness of the equivalence of Petri automata.

G. Comparing simple automata is EXPSPACE-hard

We perform a reduction from the problem RSQ(X): deciding whether a regular expressions with squaring e (e 2 ∶= e ⋅ e) denotes the universal language X ⋆ . This problem was shown in [START_REF] Meyer | The equivalence problem for regular expressions with squaring requires exponential space[END_REF] to be EXPSPACE-complete. The proof will follow the method used in [START_REF] Jategaonkar | Deciding true concurrency equivalences on safe, finite nets[END_REF] to obtain a complexity lower bound on the trace equivalence of finite nets without hidden transitions. To avoid confusion, the regular language denoted by the expression e will be written e . Any word u can be see uniquely as a linear graph λ(u). By extension, the set of graphs of words from e will be denoted by λ e .

First, notice that if u and v are just words over X, λ(u) ◂ λ(v) is equivalent to u = v. Because of this, it is straightforward to check that for any e, f ∈ Reg 2 X the following holds

◂ (λ e ) = ◂ (λ f ) ⇔ e = f . (9)
We first reduce to the containment of Petri automata with 1.

Lemma 34. The problem of deciding whether the language of a regular expression with squaring is X ⋆ is polynomial-time reducible to the containment of languages recognised by Petri automata.

Proof. Given an expression e on this signature, we can build in linear time a Petri automaton A , with a linear number of places and transitions. The closure of the language denoted by e is be exactly the language recognised by A . The automata we produce here only have one final configuration, consisting in a singleton. The construction is a straight forward adaptation of Thompson's algorithm for NFA [START_REF] Thompson | Regular expression search algorithm[END_REF]. We describe this construction graphically.

• 1: • e 1 ⋅ e 2 :

0 1 1 • x: ι f x • e 1 ∪ e 2 :
ι 1 f n 1 e 1 ι 2 f n 2 e 2 1
• e ⋆ 1 :

ι 1 f n 1 e 1 ι f n 1 1 1 1
• e 2 1 :

ι 1 f n 1 e 1 ι f n ○ • 1 1 1 1 1 X X
The automaton for e has at most 4 × e places, and at most (2 × X + 4) × e transitions. It is quite obvious that this construction can be performed in linear time and space. By further analysing this construction, one can prove that 1) λ e ⊆ L (A (e));

2) for every G ∈ G (A (e)), there is a word w ∈ e such that G ◂ λ(w). By combining Items 1 and 2 we establish that L (A (e)) =

◂ λ e .

Thus by Equation ( 9), we get that e = f is equivalent to L (A (e)) = L (A (f )). Hence L (A (X ⋆ )) ⊆ L (A (e)) is equivalent to e = X ⋆ .

The previous automata are not simple, as they use 1 as a label. We can now get rid of this label, to obtain EXPSPACEhardness for simple Petri automata.

Lemma 35. The problem of deciding whether the language of a regular expression with squaring is X ⋆ is polynomialtime reducible to the containment of languages recognised by simple Petri automata.

Proof. We use a similar trick as in [START_REF] Jategaonkar | Deciding true concurrency equivalences on safe, finite nets[END_REF]: we reuse the previous automaton A (e) by considering it as a simple automaton over the alphabet X ∪ {1} (thus forgetting about the special semantics of 1, and seeing it simply as a standard letter). Notice that w ∈ e is equivalent to the existence of a word u ∈ (X ∪ 1) ⋆ such that λ(u) ∈ L (A (e)) and w can be obtained by erasing from u the occurences of the letter 1. By carefully analysing the automaton A (e), we may actually impose that u does not contain more that n e ∶= (2 × X + 4) × e consecutive 1. By adding to each place of A (e) a transition looping on that place and labelled by 1, one obtains an automaton A ′ (e) such that w ∈ e iff the the word w ′ ∈ (1 ne X) ⋆ 1 ne obtained from w by inserting 1s as necessary is accepted by A ′ (e). As a consequence e = X ⋆ iff L (B) ⊆ L (A ′ (e)), where B is a simple Petri automaton recognising the regular language (1 ne X) ⋆ 1 ne (there are automata of linear size for this language).

H. Traces as pomsets

Let ξ be a run in a simple Petri automaton, and let ξ ′ be the corresponding run in the corresponding labelled Petri net. Let G (ξ) = ⟨V, E, ι, o⟩. It is not difficult to check that the pomset-trace of ξ ′ is isomorphic to ⟨E, < E ⟩, where < E is the transitive closure of the relation < defined on E by ∀x, y, z ∈ V, a, b ∈ X, (x, a, y) < (y, b, z).

The correspondence is even stronger: two graphs produced by accepting runs in (possibly different) automata G (ξ 1 ) = ⟨V 1 , E 1 , ι 1 , o 1 ⟩ and G (ξ 2 ) = ⟨V 2 , E 2 , ι 2 , o 2 ⟩ are isomorphic if and only if their pomset-traces (E 1 , < E1 ) and (E 2 , < E2 ) are isomorphic. The proof of this relies on the fact that accepting runs produce graphs satisfying the following properties: Hence, pomset-trace language equivalence corresponds exactly to equivalence of the sets of produced graphs in our setting (up to isomorphism).

aGFigure 1 :

 1 Figure 1: Graphs associated to some ground terms.

Figure 2 :

 2 Figure 2: A graph homomorphism.

Figure 3 :

 3 Figure 3: Inductive construction of the graph of a ground term.

Figure 4 :

 4 Figure 4: A Petri automaton. The initial place is A, and the final configurations are {I} and {F, G}.

Remark 7 .

 7 The graphs associated to ground terms without intersection are isomorphic to words over a duplicated alphabet. A graph homomorphism between two such graphs is precisely what Ésik et al. call an admissible map[START_REF] Bloom | Notes on equational theories of relations[END_REF]. Theorem 6 can thus be seen as a generalisation of[START_REF] Bloom | Notes on equational theories of relations[END_REF] Theorem 5.3].

Figure 5 :

 5 Figure 5: An accepting run in the automaton from Figure 4.

Figure 8 :Figure 9 :

 89 Figure 7: A run ξ.

Figure 10 :

 10 Figure 10: Embedding of a parallel run into the run from Figure 5.

Figure 11 :

 11 Figure 11: A Petri automaton for 1 ∩ a ⋅ b + ⋅ c.

Figure 12 :

 12 Figure 12: Squaring of the automaton for e 1 .

∀

  (x, a, y) ∈ E, x ≠ ι ⇔ (∃z, b ∈ V × X ∶ (z, b, x) ∈ E) , ∀(x, a, y) ∈ E, y ≠ o ⇔ (∃z, b ∈ V × X ∶ (y, b, z) ∈ E) .

For every reachable marking in a safe net, there is at most one token in any given place.

Note that this covers uniformly the case of the unit, of variables, and of conversed variables.

A quick analysis gives a O 2 n+(n+1) m complexity bound, where n and m are the numbers of places of the automata.

It is not difficult to check that k ≡ ξ l ⇒ ∀p, q ∈ t k × t l , ρ k (p) = ρ l (q).

APPENDIX

A. Omitted proof: Theorem 6

We denote by W X the set of ground terms. We want to establish that for any regular expressions with intersection and converse e and f , the following are equivalent:

(i) Rel ⊧ e ≤ f , (ii) e ⊆ ⊲ f , (iii) G (e) ⊆ ◂ G (f ).

a) (iii)⇒(ii): Suppose G (e) ⊆ ◂ G (f ), let u ∈ e be a ground term. Necessarily there is some graph G ∈ G (f ) such that G(u) ◂ G. By definition of G (f ), there is some term v ∈ f such that G = G(v). This means that u ⊲ v, thus proving that u ∈ ⊲ f . b) (ii)⇒(i): Let e, f ∈ Reg ⌣∩ X two expressions such that e ⊆ ⊲ f , and σ ∶ X → P (S × S) some relational interpretation.

σ(e) = ⋃ w∈ e σ(w) (Lemma 5)

In order to prove this last implication, we need the following lemma, which is due to Andréka and Bredikhin.

The following are equivalent:

Let e, f ∈ Reg ⌣∩ X two expressions such that Rel ⊧ e ≤ f , and u ∈ e such that G(u) = ⟨V u , E u , ι u , o u ⟩; we can build an interpretation σ ∶ X → P (V u × V u ) by specifying:

It is quite simple to check that σ(u) = {(ι u , o u )}. By Lemma 5 and Rel ⊧ e ≤ f , we know that

Thus there is some v ∈ f such that (ι u , o u ) ∈ σ(v). By Lemma 30 we get that there is a map ϕ

Using the definition of σ, we rewrite this last condition as

B. Omitted proof: Lemma 14

Let G = ⟨V, E, ι, o⟩, ξ = ⟨{0, . . . , n} , E ξ , 0, n⟩, and

Suppose there exists a graph homomorphism ϕ from G (ξ) to G. We build a reading (ρ k ) k of G along ξ by letting ρ k (p) ∶= ϕ([ν(k, p)] ξ ) for 0 ⩽ k ⩽ n and p ∈ ξ k . We now have to check that ρ is truly a reading of G in A :

• for the initialisation and conclusion of the reading:

(ϕ is a homomorphism)

• for all p ∈ t k and (x, q) ∈ t k , we know that

Because ϕ is a homomorphism we can deduce that:

which can be rewritten (ρ k (p), x, ρ k+1 (q)) ∈ E.

-If x = y ⌣ , y ∈ X, we also have

Because ϕ is a homomorphism we can get like before (ρ k+1 (q), y, ρ k (p)) ∈ E.

-If finally x = 1, then we know that k ≡ ξ ν(k + 1, q), thus proving that

If on the other hand we have a reading

ξ is an edge of G (ξ), then it was produced from some edge (i, y, j) ∈ E ξ , with either x = y and i, j

There is some p ∈ t i and q such that (y, q) ∈ t j and j = ν(i + 1, q). By definition of ν we know that ∀i + 1 ⩽m < j, q ∉ t m . Thus, because (ρ k ) k is a reading, ρ i+1 (q) = ρ j (q) and either (ρ i (p), x, ρ i+1 (q)) ∈ E or (ρ i+1 (q), x, ρ i (p)) ∈ E, and thus (ϕ

C. Omitted proof: Lemma 17

We have to prove that G (A (e)) ≡ G (e), where ≡ denotes equality of sets of graphs, up to graph isomorphisms. We proceed by induction on e ∈ Reg ⌣∩ X (with the restrictions introduced in Section IV: ⋅ + ∪ 1 instead of ⋅ ⋆ and the converse only on variables); we recall the inductive definition of A (e) (Definition 16), giving the arguments for the correctness for each inductive case.

Proof. The only accepting run here is

In every case this is the graph of the only ground term in x .

• A (0) ∶= ⟨{0} , ∅, 0, ∅⟩ Proof. As there are no final configuration, no run is accepting in this automaton. Hence G (A (0)) = ∅ = G (0).

Proof. If ξ = ⟨(ξ k ) 0⩽k⩽n , (t k ) 0⩽k<n ⟩ is an accepting run in A (e 1 ∪ e 2 ), then ξ 0 = {ι 1 } and either ∀k, t k ∈ T 1 and ξ is accepting in A 1 , or t 0 = ({ι 1 } , t) and

thus proving that:

, then ξ 0 = {ι 1 }. There must also be some m such that:

-

Furthermore, it can be shown that G (ξ) ≡ G ξ 1 ⋅G ξ 2 . The isomorphism is:

Thus we can deduce that:

≡ G (A (e 1 ⋅ e 2 ))

Proof. The proof is extremely similar to the case of e 1 ⋅ e 2 , simply with multiple accepting runs separated by transitions in (f, t) with f final and ({ι 1 } , t) ∈ T 1 . Note that the construction does not add any transitions ending in ι 1 .

For i ∈ {1, 2}, define π i (ξ) ∶= ξ ∖ P 2-i , and δ i (t) ∶= {t} if t ∈ T i , and ∅ otherwise.

We check that the parallel run ξ i defined by the sequence of configurations ({ι i } , π i (ξ 1 ), ⋯π i (ξ n )) and the sequence of transitions ({ι i } , t i ), δ i (t 1 ), ⋯, δ i (t n-1 ) is an accepting parallel run in A (e i ), and that

which allows us to conclude. (Although we did not properly introduce the graph produced by a parallel run, this does not hold any difficulty. As stated when we introduced the notion of parallel transition, such a transition may be unfolded by sequentially firing the underlying transitions, in any order. Accordingly, all of the unfoldings of a parallel run produce the same graph (up to isomorphisms). We may thus take for the graph produced by a parallel run any of those graphs.)

D. Omitted proof: Lemma 24

In the following, let A = ⟨P, T , ι, F ⟩ be a Petri automaton, and ξ = ⟨(ξ k ) 0⩽k⩽n , (t k ) 0⩽k<n ⟩ a run of A with t k = t k , t k for every k.

Definition 31 (Exchangeable transitions) Two transitions t k and t k+1 are exchangeable in ξ if for all p ∈ ξ k , p is in t k+1 implies that there is no x ∈ X such that (x, p) ∈ t k . *