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

2016 Kleene

A Kleene theorem for Petri automata

Keywords: regular expressions, graph language, Petri nets, finite automata, allegories, intersection, converse, Kleene theorem

Introduction

Petri Automata are Petri net-based automata, and are equipped with an operational semantics allowing them to recognise sets of graphs. They were introduced in a recent paper [START_REF] Brunet | Petri automata for Kleene allegories[END_REF] to study Kleene Allegory expressions: terms built from a finite alphabet of variables, with the constants 0 and 1, the unary operators converse and Kleene star, and the binary operators union, composition and intersection. To any such expression, one can associate a set of Two Terminal Series Parallel graphs (called graphs in the sequel) such that two expressions are universally equivalent when interpreted as binary relations if and only if their associated sets of graphs are equal. In [START_REF] Brunet | Petri automata for Kleene allegories[END_REF] we gave a method to build from any Kleene Allegory expression a Petri automaton recognising the appropriate set of series parallel graphs.

It is then natural to wonder what is the class of graph languages recognised by Petri automata. For the usual notion of finite state automata, the well known Kleene Theorem states that the languages recognisable by automata are exactly those specifiable by regular expressions. In this paper we provide a similar theorem for Petri automata and Kleene Allegory expressions.

[Copyright notice will appear here once 'preprint' option is removed.]

In the remainder of this introduction, we explain informally what are the graphs associated with expressions and Petri automata and we give the outline of the computation of the expression corresponding to a given automaton.

Expressions

For the bulk of the development, we restrict ourselves to a simpler setting: we consider expressions over the syntax of Kleene lattices, that is to say without the converse operation. To any such expression e, we associate a set G (e) of labelled directed graphs with two distinguished vertices understood as input and output. A letter a is associated to a singleton set containing the following graph: a The input in this graph is the vertex with the unmarked incoming arrow, and the output is the other vertex, with the outgoing arrow. Similarly the constant 1 yields a singleton set containing the graph where the input is linked to the output by an edge labelled 1. We define the sequential composition of two such graphs by identifying the output of the first graph with the input of the second one. We also build the parallel composition (corresponding to the intersection operation) of two graphs by identifying both their inputs and their outputs. For instance G (a ⋅ (b ∩ 1)) simply contains the graph:

a b 1
With these constructs we can define the set of graphs associated to an expression by structural induction: G (1) and G (a) are defined as before, G (e ∪ f ) is the union of G (e) and G (f ); G (0) is the empty set; G (e ⋅ f ) (respectively G (e ∩ f )) is the set of graphs obtained by composing in sequence (resp. in parallel) a graph in G (e) with a graph in G (f ); and finally the graphs in G (e ⋆ ) are either the graph of 1 or built by sequentially composing any finite number of graphs from G (e).

Petri automata

A Petri automaton over the alphabet Σ is defined by:

• a finite set of places (denoted in graphical representations by round vertices),

• a finite set T of transitions (denoted by rectangular vertices). Each transition is equipped with a set of input places (incoming arrows) and a set of outputs. These outputs are pairs of a label in Σ ∪ {1}, and a place.

• an initial place and a finite set of final configurations, a configuration being a set of places.

Here is an example of Petri automaton: The initial place is A, as denoted by the unmarked incoming arrow.

There is a single final configuration, containing only the place F (as indicated by the red dotted rectangle). In this paper, we will restrict ourselves to automata having a single final configuration, composed of one place. Runs in such an automaton are plays of a token firing game: one starts by placing tokens on certain places, and if every place in the input of a transition holds a token, this transition is enabled and may be fired. Firing a transition will then remove one token from each of its inputs, and place one on each output. If the run starts with a single token on the initial place, we call it initial, and if it stops with one token on each place of a final configuration it is final. An accepting run is both initial and final. For instance, here is a graphical representation of an accepting run in the previous automaton:

A B C B E D E F 0 1 2 3 a b d c 1
We further impose that Petri automata should be safe, meaning that at any step of any initial run of the automaton at most one token is present on each place. The last step to get the language of an automaton is to generate a graph from any run of the automaton (called the trace of the run). We do so by considering a graph whose vertices are the transitions (plus an additional final vertex), and labelled edges are extrapolated from the outputs of the transitions.

For instance the run from the previous example yields the graph:

0 1 2 3 b a c d 1
We may thus define the language G (A ) of an automaton A as the set of the traces of its accepting runs. In this paper we only consider automata whose language contain exclusively parallel series graphs (because we are only interested in such graphs). As a byproduct of the construction presented here we show that this property is decidable.

Remark 1. The definitions we give here are sometimes different from those stated in [START_REF] Brunet | Petri automata for Kleene allegories[END_REF], but the results apply nonetheless. We discuss these differences in Section 5.1.

Main result

The main technical result of this paper is a construction allowing one to build from an automaton A an expression E (A ) such that:

G (A ) = G (E (A )).
Before properly describing the construction, we need a compositional way to represent a local and partial view of a graph. This will be achieved through the notions of boxes and types. In the same way a sequence of letters may be a factor of some word, boxes are meant to represent "slices" of graphs. Formally, if A and B are sets of places, a box going from A to B is a labelled directed graph G with maps from A to the vertices of G and from B to the vertices of G. For instance, in the run presented before as an example, we may associate a box to each transition. This yields the following sequence of boxes: We may compose these boxes by merging the outputs of the first box with the inputs of the second box, and reducing the graph by applying the operators ⋅ and ∩ on edges. For instance the first two boxes above compose to produce the box β, and the whole sequence can be composed as the box γ:

β = A a b ⋅ d B E γ = A ((a ⋅ c) ∩ (b ⋅ d)) ⋅ 1 F
Types in this setting are trees with leaves labelled with places. We can type a box β with a pair of trees σ ⊸ τ if the tree σ composed with the box β yields the tree τ . For instance the box β has the type:

A ⊸ B E
We build a finite state automata whose states are the types, and whose transitions between the states σ and τ are labelled with the boxes built from transitions of the Petri automaton with type σ ⊸ τ . Using the standard Kleene Theorem, this allows us to produce a regular expression over boxes e A . By changing the set of letters to finite sets of boxes labelled with expressions, we are then able to internalise all of the regular operations. This produces in the end a finite number of boxes with one input (corresponding to the initial place) and one output (corresponding to the final place), linked by an edge labelled with a expression. The union of these expressions is the expression E (A ), that denotes the same set of graphs as A .

The technical difficulty here is the computation of the star of a set of boxes. For instance, consider the box:

δ = A B a b A B
Its star yields all boxes of the following shape, for n ∈ N:

δ n = A B a n b n A B
This set of boxes cannot be represented by a finite number of boxes. However, one must realise that because the two branches of the box δ are disconnected, they must correspond to concurrent process in the Petri automaton, and thus can be iterated separately. Intuitively, the net cannot force two independent processes to perform exactly the same number of iterations. Because of this, the following box is the right choice to represent the star of the box δ:

δ ⋆ ≡ A B a ⋆ b ⋆ A B

Outline

We begin the paper by introducing in Section 2 the expressions and automata we consider here, and the sets of graphs they represent. After a few definitions and results about graphs, we detail in Section 3 the types and boxes we use, and we establish some facts about them. Section 4 is dedicated to the main contribution of the paper, the construction extracting expressions from Petri automata. Finally we list some consequences of this result, as well as some links with previous work, in Section 5.

Petri automata & expressions

Regular expressions and rationnal languages We recall a few standard definitions and notations about regular expressions. A regular expression over the alphabet Σ is a term built from variables taken in Σ, the constants 1 and 0, the binary operators ⋅ and ∪, and the unary _ ⋆ . The set is denoted by Reg⟨Σ⟩Σ. The language denoted by e, written e , is a set of words over Σ defined inductively by:

a ∶= {a} ; 1 ∶= { } ; 0 ∶= ∅; e ∪ f ∶= e ∪ f ; e ⋅ f ∶= {u ⋅ v u ∈ e and v ∈ f } ; e ⋆ ∶= {u1 ⋅ ... ⋅ un n ∈ N, ∀i, ui ∈ e } .
( being the empty word.) If e = f , we say that regular laws prove the equality of e and f , written KA ⊧ e = f .

Expressions

Expressions e, f . . . are built on the signature ⟨1, ⋅, ∪, ∩, _ + ⟩1 . We denote by Reg ∩ Σ the set of expressions over the finite alphabet Σ. A 2-pointed labelled directed graph G over Σ• ∶= Σ ∪ {1}, simply called graph in the sequel, is given by a tuple ⟨V, E, ι, o⟩ with a finite set of vertices V , a set of labelled edges E ⊆ V × Σ• × V , and ι, o ∈ V two distinguished vertices, respectively called input and output. The sequential composition (written _⋅_) 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. Their parallel composition (written _ ∩ _) consists in merging their inputs and merging their outputs. See Figure 1 for a graphical description of these constructions.

We assign to each expression a set of such graphs, called the graph language of the expression.

Definition 2 (Graph language of an expression: G (e))

The graph language is defined by structural induction as follows:

G (a) ∶= a G (1) ∶= 1 G (0) ∶= ∅ G (e ∪ f ) ∶= G (e) ∪ G (f ) G (e ⋅ f ) ∶= {E ⋅ F E ∈ G (e) and F ∈ G (f ) } G (e ∩ f ) ∶= {E ∩ F E ∈ G (e) and F ∈ G (f ) } G e + ∶= {E1 ⋅ ... ⋅ En n > 0, ∀i, Ei ∈ G (e) } *
Those graphs were introduced independently by Freyd and Scedrov [3, page 208], and Andréka and Bredikhin [START_REF] Andréka | The equational theory of union-free algebras of relations[END_REF] (except for the way 1 is handled). Notice that the graphs produced by this construction are exactly Two Terminal Series Parallel graphs labelled with Σ• [START_REF] Valdes | The recognition of series parallel digraphs[END_REF].

Petri automata

A Petri automaton is a Petri net whose transition's outputs are labelled by the set Σ•.

G ∩ F ∶= G F G ⋅ F ∶= G F

Definition 3 (Petri Automaton)

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

• P is a finite set of places,

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

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

• f ∈ P is the final place of the automaton.

For each transition t = t, t ∈ T , t and t are assumed to be nonempty; t ⊆ P is the input of t; and t ⊆ Σ• × P is the output of t. *

This definition of Petri automata correspond to what we call simple Petri automata in [START_REF] Brunet | Petri automata for Kleene allegories[END_REF]. However, this case is general enough, as discussed in Section 5.1. We use the graphical notation from the introduction to represent Petri automata; the Petri automaton from Figure 2 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 ξ ′ defined by

ξ ′ = ξ ∖ t ∪ p ∈ P ∃x ∈ Σ ∶ (x, p) ∈ t .
We write ξ t → A ξ ′ in this case. 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 recall how to use Petri automata to define languages of graphs. We first define the runs of an automaton.

Definition 4 (Run, accepting run) A run ξ in

A = ⟨P, T , ι, F ⟩ 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 → A ξ k+1
. When ξ0 = {ι} and ξn = {f }, we call ξ an accepting run. * (Note that a run ξ is uniquely determined by ξ0 and the sequence (t k ): all subsequent configurations can be computed deterministically.)

Example 5

Consider the following sequence of transitions from the automaton in Figure 2:

3 2016/1/19 A B G C E G D E G F G I t 0 t 1 t 2 t 3 t 4 b a c b a d 1
ξ = ⟨(ξ0, ξ1, ξ2, ξ3, ξ4, ξ5) , (t0, t1, t2, t3, t4)⟩, with ξ0={A} , ξ1={B, G} , ξ2={C, E, G} , ξ3={D, E, G} , ξ4={F, G} , ξ5={I} . t0=({A} , {(b, B), (a, G)}) , t1=({B} , {(c, C), (b, E)}) , t2=({C} , {(a, D)}) , t3=({D, E} , {(d, F )}) , t4=({F, G} , {(1, I)}) .
We have:

{A} t 0 / / {B, G} t 1 / / {C, E, G} t 2 / / {D, E, G} t 3 / / {F, G} t 4 / / {I} ,
and since {A} is the initial configuration and {I} is the final one, this sequence is an accepting run. It can be represented graphically as in Figure 3. ∎

In [START_REF] Brunet | Petri automata for Kleene allegories[END_REF], the language of a Petri automaton is defined via an operational semantics, describing the way an automaton "reads" a graph. For the sake of clarity, we use here a different definition, more directly related to the set of accepting runs of the automaton. We associate to each accepting run ξ a 2-graph, written G (ξ), called the trace of ξ. The language of the automaton is then defined as the set of traces of its accepting runs.

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 6 (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 G (ξ) ∶= ⟨{0, . . . , n} , E ξ , 0, n⟩ with

E ξ ∶= (k, x, ν(k + 1, q)) (x, q) ∈ t k . *
We write G (A ) for the language of a Petri automaton A , defined as the set of traces of its accepting runs. The trace of the run presented in Figure 3 is depicted in Figure 4. Remark 7. G (A ) is different from L (A ), as it is defined in [START_REF] Brunet | Petri automata for Kleene allegories[END_REF]. See section Section 5.1 for a more detailed discussion.

G (e) = G (A (e)) .

SP-Petri automata

When trying to build expressions out of Petri automata, one immediately encounters a problem: traces of accepting runs are not necessarily series parallel graphs, which means they cannot be generated by any expression from Reg ∩ Σ . For instance the automaton given in Figure 6 has a single accepting run, whose trace is the graph draw in Figure 5. To circumvent this problem, we consider only well-behaved automata: automata whose accepting runs have parallel-series graphs.

Definition 9 (SP-automata) An automaton A is said to be an SP-automaton if for any accepting run ξ in A , G (ξ) is an SP-graph. * Despite its infinitary formulation, this property is decidable. In fact, the procedure we describe later on would fail (in finite time) if it is given a non-SP automaton: hence it may be used to decide this property. 2

Boxes

Notations We call label space a structure ⟨L, ⋅, ∩⟩ such that ⋅ and ∩ are two internal associative binary operations, and ∩ is commutative. Examples of such spaces include: W X : the set of SP-graphs labelled by X. It is the free label space over a finite set of atomic variables X. We will make no distinctions between this set and the terms over the signature ⟨X, ⋅, ∩⟩ quotiented by the label space axioms.

1 : the unit label space. E X : the set of expressions Reg ∩ Σ (quotiented by the congruence generated by label space axioms).

Graphs

We introduce a few definitions and results about graphs. Unless otherwise stated, all graphs are labelled with some fixed label space L. DAGs and Series Parallel graphs Given a directed acyclic graph (DAG) G = ⟨V, E⟩, we may define min G to be the set of vertices in V with no incoming edge, and max G the set of vertices with no outgoing edge. A Two Terminal Parallel Series graph (SP-graph in the following) may be defined as a connected DAG that does not contain the graph from Figure 5 as a minor, and such that min G and max G are both singleton sets. A factor of ⟨V, E⟩ is a graph ⟨V ′ , E ′ ⟩ such that:

• V ′ ⊆ V and E ′ ⊆ E; • e ∈ E ′ if and only if both its extremities are in V ′ . A prefix of ⟨V, E⟩ is a factor ⟨V ′ , E ′ ⟩ such that if there is a path from x ∈ V to y ∈ V ′ , then x ∈ V ′ .
When considering the graph as a partial order, a prefix is a downward closed set of vertices. Similarly, A suffix of ⟨V, E⟩ is an upward closed set, meaning a factor ⟨V ′ , E ′ ⟩ such that if there is a path from x ∈ V ′ to y ∈ V , then y ∈ V ′ . Finally a slice of ⟨V, E⟩ is a convex set, i.e. a factor such that if there is a path from x ∈ V ′ to y ∈ V and one from y to z ∈ V ′ , then y ∈ V ′ . Any slice may be obtained by removing from the graph a prefix and a suffix. A graph G is called an SP-slice if it is a slice of some SP-graph.

We define the SP-rewriting system, enriched with labels taken from a label space: (This second rule can only be applied if the middle node on the left-hand side has no other adjacent edge.) Given a DAG G, we write G ↓ for the unique normal form of G with respect to this system. One may notice here that if G is a non-trivial SP-graph, then G ↓ has always the shape → • e → • → 3 , and G is isomorphic to G (e). This isomorphism means that we will often assimilate SP-graphs and terms built using the operators ⋅ and ∩.

Trees and bow ties A tree is a DAG T = ⟨V, E⟩ such that either min T or max T contains a single node called the root, and for any two nodes x, y ∈ V there exists at most one path from x to y. If min T is a singleton, then T is a top-down tree, otherwise it is a bottom-up tree. A tree is said to be proper if it does not contain any node with exactly one incoming edge and one outgoing edge. It is simple enough to check that there is only a finite number of proper trees with leaves chosen from a finite set.

A bow tie is a DAG G that does not contain the graph from Figure 5 as a minor and such that there is a node o such that every node in G either can reach o or is reachable from o. By applying the SP-rewriting system to a bow tie, we get a bottom-up tree concatenated with a top-down tree, as illustrated in figure Figure 7 (hence the name). It follows easily that G is an SP-slice if and only if it is a disjoint union of bow ties. 3 This is sometimes used as the definition of an SP-graph. • G is the quotient of the disjoint union of G1 and G2 by the relation ∼;

• the function p (respectively p) associates to x ∈ A (resp. ∈ B) the equivalence class of p

1 (x) (resp. p2 (x)).
It can be checked that this composition operation is associative and that for any two boxes β ∶ A → B and γ ∶ B → C, the following holds: ⌊β ⊙ γ⌋ = ⌊β⌋ ⊙ ⌊γ⌋.

(1) This operation is illustrated in Figure 8.

Definition 13 (Typed boxes) Let β ∶ A → B be a box over L, σ and τ be types respectively over A and B. β has the type σ ⊸ τ if the following holds:

⌊ σ ⊙ β⌋ = τ . (2)
We write B L σ⊸τ for the set of boxes over L of type σ ⊸ τ , and B L P for the set of typed boxes over L with types from T P . These boxes allow us to define the category B L of types and typed boxes over L where:

• the objects are types; • for any two objects σ, τ , the set of morphisms from σ to τ is B L σ⊸τ . * (Notice that the type of a box is not unique: a single box may have multiple types.)

For instance the box in Figure 10 has type σ ⊸ τ , with σ and τ as defined in Figure 9.

Let us verify that B L satisfies the axioms of a category. We already know that the composition of boxes is associative, but its remains to be shown that the composition of typed boxes is a typed box. In other words:

B L σ⊸τ ⊙ B L τ ⊸θ ⊆ B L σ⊸θ . Let β, γ ∈ B L σ⊸τ × B L τ ⊸θ . We need to check that β ⊙ γ ∈ B L σ⊸θ . ⌊ σ ⊙ (β ⊙ γ)⌋ =⌊( σ ⊙ β) ⊙ γ⌋ (Associativity) =⌊ σ ⊙ β⌋ ⊙ ⌊γ⌋ (Equation (1)) = τ ⊙ ⌊γ⌋ (β ∈ B L σ⊸τ ) =⌊ τ ⊙ γ⌋ (Equation (1)) = θ .
(γ ∈ B L τ ⊸θ ) The last thing we need is the identity over an arbitrary object τ . If L is the set of leaves of τ , then we define idτ = ⟨⟨L, ∅⟩, lτ , lτ ⟩. It is immediate to check that idτ ∈ B L τ ⊸τ and that for any typed boxes β, γ of appropriate types, β ⊙ idτ = β and idτ ⊙ γ = γ. The identity box on type τ is displayed in Figure 11.

Boxes over expressions

Consider boxes labelled with a label space E X . The elements of E X are expressions taken from Reg ∩ X , and thus denote languages of SP-graphs, as defined earlier. This means that we can generate from such a box a set of boxes labelled with W X , by replacing each edge labelled with e by a graph G ∈ G (e) ⊆ W X 4 . For instance, the box:

A B C D E a b a ∪ b a + ⋅ b 4
As mentioned before, we make no distinction between SP-graphs and terms built using letters and the operators ⋅ and ∩. can generate all boxes of the following shapes, for n > 0:

A B C D E a b a a n ⋅ b or A B C D E a b b a n ⋅ b
It is useful to notice that for any box B ∈ B E X σ⊸τ , if B generates the box β, then β ∈ B W X σ⊸τ . In the following, we will denote by B(B)

the set of boxes generated by a box B labelled with E X .

Automata and regular sets of boxes 4.1 A regular expression over boxes

It is then quite easy to generate from an SP-automaton A a regular expression over boxes e A ∈ Reg⟨B

W Σ• P ⟩ such that: β1⋯βn ∈ e A ⇔ β1 ⊙ ⋯ ⊙ βn = ⟨G, p,p⟩ with G ∈ G (A ) β1 ⊙ ⋯ ⊙ βn has type ι⊸ f .
Let us fix an SP-automaton A = ⟨P, T , ι, f ⟩ over an alphabet Σ. Its transitions are thus labelled with Σ•. Given automata configurations C and C ′ , and a transition t such that C t → A C ′ , we can define a box β t,C ∶ C → C ′ as follows. Suppose t = {(a1, q1), . . . , (am, qm)} and C ∖ t = {p1, . . . , pn}. Recall that because t is a valid transition from C to C ′ , the sets {q1, . . . , qm} and {p1, . . . , pn} are disjoint and C ′ = {p1, . . . , pn, q1, . . . , qm}. Thus β t,C is defined as ⟨V, E, p,p⟩ where:

• V contains an is the input node x0, a node xi for every place pi in C ∖ t and a node yi for every output qi.

• p maps every input place p to x0, every every other pi in C ∖ t to xi.

• p maps every output qi to yi, and the remaining pi to xi.

• for each output (ai, qi), we place an edge (x0, ai, yi) in E.

This construction is illustrated in Figure 12. We may extend this construction to runs: for every run of length n ξ = ⟨(ξ k ) 0⩽k⩽n , (t k ) 0⩽k<n ⟩ we define β(ξ) by:

β(ξ) ∶= β t 0 ,ξ 0 ⊙ ⋯ ⊙ β t n-1 ,ξ n-1 .
It is quite straight-forward to check that for every accepting run ξ,

β(ξ) = G (ξ) ι f
Thus there is no difference between the graphs produced by the automaton and the boxes corresponding to its accepting runs. We call a box valid if there is an accepting run ξ with a consecutive sub-run ξ[i..j] such that β = β(ξ[i..j]). We say in that case that the run ξ[i..j] witnesses the validity of β. Notice that because A is an SP-automaton, the graph of a valid box has to be an SP-slice.

The types help us here, as illustrated by the following lemma: Lemma 14. If β is a valid box with type σ ⊸ τ and γ is valid with type τ ⊸ υ, then β ⊙ γ is a valid box with type σ ⊸ γ.

We extend this to words and regular expressions over typed boxes. We may now define a deterministic finite-state automaton as follows:

• the set of states is T P , the types over the set P of places of A (as remarked before, this set is finite);

• for every pair of types σ, τ , if C is the set of leaves of σ, if t ∈ T can be fired from C and if

β t,C ∈ B W Σ•
σ⊸τ we add a transition (σ, β t,C , τ );

• the initial state is the type ι ;

• the final state is the type f .

Remark 18. This automaton can be computed partially, by enumerating all runs starting from {ι}, and computing the corresponding boxes and types. Because of the finite number of states in this automaton this procedure must terminate. If the automaton we were given is not SP, then the computation will reach a step where we have a reachable type σ with leaves C and a transition t enabled at C such that ⌊ σ ⊙ β t,C ⌋ does not reduce to a tree. This gives a decision procedure to check whether A is indeed an SP-automaton.

Using the classic Kleene theorem, we can then compile this automaton into a regular expression e A ∈ Reg⟨B

W Σ• P ⟩ such that:
1. e A and all its sub-expressions are valid and typed, as defined earlier, meaning that the words in their languages compile to valid boxes and that two boxes in the language of the same subexpression share a common type5 ;

2. if ξ is an accepting run of the Petri automaton A , then β(ξ) is the compilation of some word in e A . Thus e A ⊙ is the set of all valid boxes of type ι⊸ f . This allow us to state an important property of the expression e A :

Lemma 19. Let f, g ∈ Reg⟨B W Σ• P ⟩ be valid expressions of type σ ⊸ τ , such that f ⊆ g . If e A [f
g] is the expression obtained by replacing an occurrence of f with g in e A , then the box language of e A is equal to that of e A [f g].

Proof. We proceed by mutual inclusion. One direction is straight forward: all regular operations being increasing, we know that f ⊆ g entails e A ⊆ e A [f g] , thus ensuring e A ⊙ ⊆ e A [f g] ⊙ .

The property 2 allows us to check the other direction. The typing ensures that for any words u, v, w and w ′ , if w and w ′ compile to boxes with the same type then u ⋅ w ⋅ v is valid if and only if u ⋅ w ′ ⋅ v is valid as well, and they have the same type. Thus we know that e A [f g] ⊙ only contain valid boxes of the same type as the ones from e A ⊙ . As e A ⊙ is maximal for its type, it must contain e A [f g] ⊙ .

Compiling an expression over boxes into Reg ∩

Σ

What remains to do is to transform this regular expression over boxes into an expression from Reg ∩ Σ . We do so by moving from typed boxes labelled with W Σ• to finite sets of boxes sharing a common type and labelled with E Σ• ⊇ W Σ• , thus internalising the operators. By mapping each box β to {β}, we may translate this way the expression e A obtained in the previous section to a new expression e A . The operator ⊙ may be lifted here in a type preserving way, as a pointwise application:

S ⊙ S ′ ∶= B ⊙ B ′ B ∈ S, B ′ ∈ S ′ .
We also extend the notion of boxes over W Σ• generated by a box over E Σ• to a set S simply by stating that B(S) ∶= ⋃ B∈S B(B).

B(S).

We extend a definition from the previous section to this setting:

Definition 22 (Typed expression) An expression valid e ∈ Reg⟨P f B E Σ• P ⟩ has type σ ⊸ τ if all β ∈ e have the type σ ⊸ τ . *
We can now equate two expressions if they denote the same set of boxes, introducing the equivalence relation ≡ β :

e ≡ β f ∶= ( e = f )
Notice that Lemma 19 can be restated for e A :

Lemma 23. Let f, g ∈ Reg⟨P f B E Σ• ⟩ be valid expressions of type σ ⊸ τ , such that f ⊙ ⊆ g ⊙ . Then e A ≡ β e A [g f ].
The operator ∪ and ⋅ are easy enough to define on finite sets of boxes labelled over E Σ• :

S ⋅ S ′ ≡ β ⋃ B∈S ⋃ B ′ ∈S ′ B ⊙ B ′ S ∪ S ′ ≡ β B B ∈ S ∪ S ′
The case of _ ⋆ however is much more interesting. In fact, this is the main technical difficulty of the present paper, and where most of the machinery we have introduced up to this point will prove useful. For typing reasons, notice that we only need to compute the star of a set of boxes of an identity type σ ⊸ σ. In the next section, we show how to compute from a set S of boxes labelled over E Σ• and having type σ ⊸ σ a new finite set of boxes S ′ such that:

7 2016/1/19 ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ c a a + b b c A B C D E A B C D E , a b A B C D E A B C D E , b ∩ c A B C D E A B C D E , b a A B C D E A B C D E , c A B C D E A B C D E ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭
1. S ⋆ ⊆ S ′
2. and ∀β ∈ S ′ , β is valid and has type σ ⊸ σ.

By Lemma 23 this entails the following equivalence:

e A ≡ β e A S ′ S ⋆ .
Using these transformation, we now can "compile" the expression e A into a finite set of boxes of type ι⊸ f . Such a set may only have the shape:

e 1 ι f , ..., en ι f .
It is then straightforward to see that e A is isomorphic to G (e1 ∪ ⋯ ∪ en). If we call E (A ) the expression e1 ∪ ⋯ ∪ en, the following theorem holds:

Theorem 24 (Main result). For every SP-automaton A over Σ, there exists an expression E (A ) ∈ Reg ∩ Σ such that G (A ) = G (E (A )) .

Staring boxes

Instead of giving a formal description, which would be very involved, we describe the procedure on an example, outlining the important computation steps. Consider the following set of boxes, respectively named β and γ.

⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ a b c a a + b b c A B C D E A B C D E , b ∩ c b a c A B C D E A B C D E ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭
Both these boxes have type σ ⊸ σ, with the σ as shown in Figure 9. First, we decompose each box, by separating disjoint non-trivial connected components. The idea behind this step is that the different connected component correspond to concurrent processes, and as such may be iterated independently. This yields the set of five so-called elementary boxes displayed in Figure 13, respectively named η1 through η5.

One can show that the resulting boxes are always valid and have the type σ ⊸ σ(a formal proof of the properties of this decomposition is given in Appendix A). Because β = η1 ⊙ η2 and γ = η3 ⊙ η4 ⊙ η5, we get that: By Lemma 23, we know that we may replace in the expression e A the sub expression

(β ∪ γ) ⋆ ⊙ ⊆ (η1 ∪ η2 ∪ η3 ∪ η4 ∪ η5) ⋆ ⊙ box support η1 {C, D, E} η2 {A, B} η3 {A} η4 {C, D} η5 {E}
(β ∪ γ) ⋆ by (η1 ∪ η2 ∪ η3 ∪ η4 ∪ η5) ⋆
without changing the set of produced graphs. This means that we may continue the computation with the set of elementary boxes H = {η1, η2, η3, η4, η5}. We define the support of a box with a single non-trivial connected component as the set of ports that are mapped inside this component. Figure 14 lists the supports of the boxes ηi. Notice that for every two boxes η, η ′ in H, their supports are either included one in the other, or of empty intersection. This can be shown formally by realising that for a box with a single connected component of type σ ⊸ σ, the support is the set of leaves of a sub-tree of σ (i.e. the set of all leaves reachable from some node of σ). This means we can endow the set {η1, η2, η3, η4, η5} with a preorder relation ≼ defined by η ≼ η ′ if support(η) ⊆ support(η ′ ).

The graph of the order on our example set is given in Figure 15. The order has an interesting property: if η and η ′ are incomparable, then

η ⊙ η ′ = η ′ ⊙ η. Thus (η ∪ η ′ ) ⋆ ≡ β η ⋆ ⋅ η ′⋆ .
With that in mind we will compute the expression:

η ⋆ 3 ∪ η2 ⋆ ⋅ η ⋆ 4 ⋅ η ⋆ 5 ∪ η1 ⋆ .
The first step in this computation is the computation of the star of a single box. Notice that we may define easily the star of a "linear" elementary box, i.e. of the shape:

⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ ⋮ e A B 1 ⋮ Bn A B 1 ⋮ Bn ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ ⋆ ≡ β ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ ⋮ e + A B 1 ⋮ Bn A B 1 ⋮ Bn , ⋮ A B 1 ⋮ Bn A B 1 ⋮ Bn ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭
This construction gives us η ⋆ 3 and η ⋆ 5 . Now for general elementary boxes, notice that the non-trivial connected component of an elementary box is always a bow tie. Hence we can always decompose such a box η of type σ ⊸ σ as δ1 ⊙ δ2 such that the non-trivial connected component of δ1 is a bottom-up tree, and that of δ2 is a top-down tree, with the middle node o of the bow tie being the root of both trees. See Figure 16 for examples. This means that δ2 ⊙δ1 is a linear elementary box. Furthermore, the definition of δ1,2 ensures {η} ⋆ ≡ β ({δ1} ⋅ {δ2}) ⋆ . The regular laws entail that for every expressions e and f we have (e ⋅ f ) ⋆ = 1 ∪ e ⋅ (f ⋅ e) ⋆ ⋅ f . Thus we can use the previous construction to get a set of boxes representing ({δ2} ⋅ {δ1}) ⋆ ≡ β {δ2 ⊙ δ1} ⋆ , and then compute:

{η} ⋆ ≡ β {idσ} ∪ {δ1} ⋅ {δ2 ⊙ δ1} ⋆ ⋅ {δ2} .
The last thing to do is to compute stars of the shape (S ⋆ ∪ η) ⋆ where:

• S ⋆ is a finite set of boxes computed in an earlier step,

• support(η) contains the "support" of S ⋆ : the set of inputs mapped to a non trivial connected component in some

B ∈ S ⋆ . η1 = c a A B C D E A B o ⊙ a + b b c A B o A B C D E η2 = A B C D E o C D E ⊙ a b o C D E A B C D E η4 = A B C D E A B o E ⊙ b a A B o E A B C D E
Figure 16: Decomposition as a product of trees of η1, η2 and η4.

Again, we decompose η into δ1 and δ2 as in the previous construction, and notice that δ2 ⊙ S ⋆ ⊙ δ1 is set of a linear boxes, along the same line. We may thus bundle them together in a single box with a line labelled with the union of their labels. For example:

⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ e A B C A B C , f A B C A B C ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ ≡ β ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ e ∪ f A B C A B C ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭
This allow us to produce a set of (two) boxes representing the star of the box (δ2 ⊙ S ⋆ ⊙ δ1). The regular laws allow us to conclude, by stating that:

S ⋆ ∪ δ1 ⋅ δ2 ⋆ ≡ β S ⋆ ∪ δ1 ⊙ δ2 ⊙ S ⋆ ⊙ δ1 ⋆ ⊙ δ2
We can now give the bulk of the computation, in Figure 17. The result is then obtained by performing the composition

η ⋆ 3 ∪ η2 ⋆ ⊙ η ⋆ 4 ∪ η5 ⋆ ∪ η1 ⋆ , thus yielding 32 boxes: 8 for ((η ⋆ 4 ∪ η ⋆ 5 ) ∪ η1) ⋆ times 4 for (η ⋆ 4 ∪ η5) ⋆ .

Consequences

Kleene Allegories

The main motivation for this work was the study of the equational theory of Kleene Allegories (KAl). In this line of work we consider binary relations and the operations of union (∪), intersection (∩), composition (⋅), converse (_ ⌣ ), transitive closure (_ + ), and the constants identity (1) and empty relation (0). Terms made from those operations and some variables a, b, ⋅ ⋅ ⋅ ∈ Σ constitute the set Reg ⌣∩ Σ . A pair e, f ∈ Reg ⌣∩ Σ is then relationaly equivalent, denoted Rel ⊧ e = f , if the corresponding equality holds universally when the expressions are interpreted as binary relations. Notice that we may restrict expressions 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 ⌣ .
The result of this transformation on an expression e is an expression e ′ always satisfying Rel ⊧ e = e ′ . We may associate to these terms graph languages, as in Definition 2. The graph language is defined by structural induction as follows: G ′ e + ∶= E1 ⋅ ... ⋅ En n > 0, ∀i, Ei ∈ G ′ (e) . *

η ⋆ 3 =idσ ∪ (b ∩ c) + A B C D E A B C D E η ⋆ 3 ∪ η2 ⋆ = η ⋆ 3 ∪ η2 ∪ ex + 1 a b A B C D E A B C D E with ex1 = (a ∩ b) ∪ a ⋅ (b ∩ c) + ∩ b η ⋆ 4 =idσ ∪ η4 ∪ (b ∩ a) + b a A B C D E A B C D E η ⋆ 5 =idσ ∪ c + A B C D E A B C D E (η4 ∪ η5) ⋆ ∪ η1 ⋆ =η ⋆ 4 ⊙ η ⋆ 5 ∪ η1∪ c a ex + 2 a + b b c A B C D E A B C D E with ex2 = a + ⋅ (b ∩ c) ⋅ (b ∩ a) + ⋅ (b ∩ a) ⋅ c ∩ b ⋅ c + ⋅ a ∪ a + ⋅ (b ∩ c) ⋅ (b ∩ a) + ⋅ (b ∩ a) ⋅ c ∩ (b ⋅ a) ∪ a + ⋅ (b ∩ c) ⋅ (b ∩ a) ⋅ c ∩ b ⋅ c + ⋅ a ∪ a + ⋅ (b ∩ c) ⋅ (b ∩ a) ⋅ c ∩ (b ⋅ a) ∪ a + ⋅ (b ∩ c) ⋅ c ∩ b ⋅ c + ⋅ a
G ′ (a) ∶= a ; G ′ (a ⌣ ) ∶= a ; G ′ (0) ∶= ∅; G ′ (1) ∶= { } ; G ′ (e ∪ f ) ∶= G ′ (e) ∪ G ′ (f ) ; G ′ (e ⋅ f ) ∶= E ⋅ F E ∈ G ′ (
In [START_REF] Brunet | Petri automata for Kleene allegories[END_REF], we showed the following result:

Rel ⊧ e = f ⇔ ◂ G ′ (e) = ◂ G ′ (f ). 6Notice that the only two differences between G (_) and G ′ (_) are the construction for 1 and the case of _ ⌣ . We can mend that gap, by computing G ′ (e) from G (e). The first step is to consider the sub-expressions a ⌣ as letters, i.e. to see e ∈ Reg ⌣∩ Σ as an expression in Reg ∩ S with S ∶= Σ ∪ {a ⌣ a ∈ Σ }. This means we can apply G (_) on e, and produce a set of graphs labelled with S. We then introduce the graph transformation Φ: Definition 26 (Φ) Let G = ⟨V, E, ι, o⟩ be a graph labelled with S. Let ≡ G be the smallest equivalence relation on V containing all pairs (i, j) such that (i, 1, j) ∈ E. Then Φ(G) is the graph defined by

Φ(G) ∶= ⟨{[i] G i ∈ V } , E ′ , [ι] G , [o] G ⟩ [i] G ∶= {k ∈ V i ≡ G k } E ′ ∶= ⎧ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎩ ([i] G , x, [j] G ) x ∈ Σ and ∃k ∈ [i] G , l ∈ [j] G ∶ (k, x, l) ∈ E or (l, x ⌣ , k) ∈ E ⎫ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎭ *
It is then a simple matter to check that ∀e ∈ Reg ⌣∩ Σ , G ′ (e) = {Φ(G) G ∈ G (G) } . In the same paper we also introduced Petri automata, but again we used a different definition of the language L (A ) of an automaton A . However, this set can be expressed with our notations as L (A ) = ◂ Φ (G (A )). A function A (_) was provided, mapping an expression e ∈ Reg ⌣∩ Σ to a Petri automaton A (e) such that G (A (e)) = G (e). Theorem 24 allow us to relate the language of any SP-automaton A to the graph language of E (A ):

L (A ) = ◂ Φ (G (E (A ))).
This proves that from a decidability stand point, language equivalence of Petri automata and relational equivalence of KAl expressions. Formally:

One could also read this result from a graph theoretical viewpoint. What we show here is that the sets of SP-graphs one may express trough regular expressions enhanced with a parallel operator ∩ are exactly those generated by SP-automata.

Petri nets

The construction presented here can also provide a finite regular expression with intersection to represent all finite occurrence nets of a given Petri net N , provided this net is safe and Parallel Series. In terms of concurrent processes, these two conditions roughly amount to requiring that there is a bounded number of processes running at any given time, and that communication between processes is synchronous.

More precisely, suppose we are given a net N , with a finite set P of places and a finite set T ⊆ P (P ) × P (Σ × P ) of transitions. 8If I, F ⊆ P (P ) are respectively a source set and a target set, we can produce a Petri automaton A such that the set of occurrence nets of process going from a source configuration in I to a target configuration in F is isomorphic to G (A ). To achieve this, we add to the net:

• two new places ι and f and a fresh label #;

• for each source configuration {p1, ..., pn} ∈ I a transition ⟨{ι} , {⟨#, p1⟩, ..., ⟨#, pn⟩}⟩;

• for each target configuration {q1, ..., qn} ∈ F a transition ⟨{q1, ..., qn} , {⟨#, f ⟩}⟩.

It is then a simple matter of unfolding definitions to see that G (A ) indeed corresponds to the set of occurrence nets we wanted. Of course, this construction is ill-defined if the net N is not safe for one of the source configurations in I.

If furthermore the produced automaton is SP, which is again a property of the net N , then the construction of this paper yields an expression E (A ) representing faithfully the set of occurrence nets of processes going from any configuration in I to any configuration in F .

Figure 1 : 1 Figure 2 :

 112 Figure 1: Elementary graph constructions

Figure 3 : 1 Figure 4 :

 314 Figure 3: An accepting run in the automaton from Figure 2.

1 Figure 5 : 1 Figure 6 :

 1516 Figure 5: Non series parallel graph.

Figure 7 :

 7 Figure 7: Example of reduced bow tie

Figure 8 : 1 ,p 1 ⟩ 2 ,p 2

 81122 Figure 8: Composition of boxes

Figure 9 :Figure 11 :

 911 Figure 9: Some types σ and τ .

5 Figure 12 :

 512 Figure 12: Construction of β t,C

Definition 15 (

 15 Valid expression) An expression e ∈ Reg⟨B W Σ• ⟩ is valid if for all β1⋯βn ∈ e , the composition β1 ⊙ ⋯ ⊙ βn is well defined, and the resulting box is valid. * Given a word w = β1⋯βn, we call the box β1 ⊙ ⋯ ⊙ βn the compilation of w. Definition 16 (Box language of e) If e ∈ Reg⟨B W Σ• ⟩ is valid, then the box language of e, written e ⊙ , is the set of boxes obtained by compiling the words of e . * Definition 17 (Typed expression) A valid expression e ∈ Reg⟨B W Σ• P ⟩ has type σ ⊸ τ if for all β ∈ e ⊙ , β has the type σ ⊸ τ . *

Definition 20 (

 20 Valid expression) An expression e ∈ Reg⟨P f B E Σ• P ⟩ is valid if all S1⋯Sn ∈ e , the composition S1 ⊙ ⋯ ⊙ Sn = S is defined and B(S) only contains valid boxes. * The definition of _ ⊙ we had for valid expressions with letters in B W Σ• P can thus be salvaged for expressions with letters in P f B E Σ• P . Lemma 14 can be adapted to this setting: Lemma 21. Let S1 and S2 be finite sets of boxes over E Σ• , such that 1. ∀β ∈ B(S), β is a valid box with type σ ⊸ τ ; 2. ∀γ ∈ B(S ′ ), γ is a valid box with type τ ⊸ υ; then ∀β ∈ B(S ⊙ S ′ ), β is a valid box with type σ ⊸ γ. A regular expression e with letters in P f B E Σ• P represent the set of boxes e ∶= ⋃ S∈ e ⊙

Figure 13 :

 13 Figure 13: Elementary decomposition of {β, γ}.

Figure 14 : Supports of the ηi η 3 η 2 η 1 η 4 η 5 Figure 15 :

 144515 Figure 14: Supports of the ηi

Figure 17 :

 17 Figure 17: Computation steps

  e) and F ∈ G ′ (f ) ; G ′ (e ∩ f ) ∶= E ∩ F E ∈ G ′ (e) and F ∈ G ′ (f ) ;

7

 7 Thus:L (A (e)) = ◂ Φ (G (e)).

  ∀e, f, Rel ⊧ e = f ⇔ L (A (e)) = L (A (f )) (3) ∀A , B, L (A ) = L (B) ⇔ Rel ⊧ E (A ) = E (B)

2016/1/19

Notice that we don't use the Kleene star, but rather its positive variant. It is more convenient here to have e ⋆ be defined as 1 ∪ e + .

See Remark 18 for more details. 4 2016/1/19

2016/1/19

This property follows from results about typed Kleene Algebra. See for instance[START_REF] Kozen | Typed kleene algebra[END_REF][START_REF] Möller | Typed kleene algebras[END_REF][START_REF] Pous | Untyping typed algebras and colouring cyclic linear logic[END_REF].

2016/1/19

We need not concern ourselves with the definition of ◂ _ here, as it plays no role in the present result. 92016/1/19

The automaton A (e) always satisfied the Parallel Series condition we required in Section 2.3.

Here we stick to the setting of this paper by labelling the outputs of transitions rather than the transitions themselves. However, one can start with a net with usual labelled transition, and then simply copy the label of t to each of its outputs. This would lead to graphs where each node would have the same label on each outgoing edge, thus effectively labelling the node rather than the edge.

2016/1/19

Proof. We number the connected components of β from C1 to Cp.

Suppose β is valid, then there is a run ξ = ξ0

Notice that for any index i, the box β t i ,ξ i-1 is elementary (see the definition of β t,C ). Thus it can be associated with a single non-trivial connected component in β. We introduce the function c ∶ {1, ..., n} → {1, ..., p}, such that the transition i is associated with the component C c(i) .

The key argument is the following. For any index i, if the set of output places of transition ti contains a place that appears in the input of the transition ti+1, then the box β t i ,ξ i-1 ⊙ β t i+1 ,ξ i is elementary. This means that c(i) = c(i + 1). By contraposition, we may then deduce that if c(i) ≠ c(i + 1), then the intersection of the outputs of ti and the inputs of ti+1 is empty. This can in turn be used to build a configuration ξ ′ i such that:

• ξi-1

This means we may group the transitions that contribute to the same connected component. Formally we apply a permutation π to the run ξ, such that:

• π(ξ) can be decomposed as a sequence of runs:

We now define ηj ∶= β(χj). By construction ηj is valid, it contains only the connected component Cj so it is elementary, and β = β(ξ) = β(π(ξ)) = η1 ⊙ ⋯ ⊙ ηp. Furthermore, for each p ∈ ξ0, p ∈ support(ηj) if and only if p(p) ∈ Cj. As the connected components are pairwise disjoint, so are the supports of the ηj. Further analysis of the run π(ξ) also shows that ∀i < j, target(ηi) ∩ support(ηj) = ∅.

If β has type σ ⊸ σ, that means that in particular ξ0 = ξn. This entails the following equality:

(The remaining places are those untouched by the execution.) Hence:

We know that ∀1 < j, target(η1) ∩ support(ηj) = ∅, hence target(η1) ⊆ support(η1). To get the other direction, one has to notice that the run χ2⋯χp may be executed starting from ξ0 (rather than ξ ′ 1 ). This is again because of the possibility to exchange "independent" transitions. Safety of the automaton ensures that

Thus we obtain support(η1) ⊆ target(η1), finally proving support(η1) = target(η1). This in turn ensures that ξ ′ 1 = ξ0, and enable us to repeat the proof for η2, ..., ηn.

The last thing to do is to "type check" these elementary boxes. Let's detail the computation of the type β outputs when given a tree σ. Each connected component Cj is a bow tie of centre oj, with inputs Sj. For each of those, there must be a sub-tree Tj in σ with leaves Sj (otherwise there would be no way of reducing σ ⊙ β to a tree). We then remove that sub-tree, and replace it by the top-down tree rooted in oj. Because all Sj are pairwise disjoint, the trees Tj are also pairwise disjoint (otherwise they would share some leaves). With this description of the type-checking, one realises that 1) each of the ηj contribute to the final type on disjoint subtrees 2) and each of them leaves the rest of the tree alone. Because ∀j, Sj = support(ηj) = target(ηj) we can conclude that ηj replaces the tree with leaves Sj with the tree with leaves Sj, and thus preserves the type σ ⊸ σ.