Paul Brunet

Damien Pous

Georg Struth

On Decidability of Concurrent Kleene Algebra *

Keywords: Concurrent Kleene algebra, series-parallel pomsets, Petri nets 1

Concurrent Kleene algebras support equational reasoning about computing systems with concurrent behaviours. Their natural semantics is given by series(-parallel) rational pomset languages, a standard true concurrency semantics, which is often associated with processes of Petri nets. We use constructions on Petri nets to provide two decision procedures for such pomset languages motivated by the equational and the refinement theory of concurrent Kleene algebra. The contribution to the first problem lies in a much simpler algorithm and an ExpSpace complexity bound. Decidability of the second, more interesting problem is new and, in fact, ExpSpace-complete.

Introduction

Kleene algebras axiomatise the equational theory of rational expressions. Their canonical models are rational languages and their equational theories correspond to rational expression equivalence [START_REF] Krob | A Complete System of B-Rational Identities[END_REF][START_REF] Kozen | A completeness theorem for Kleene algebras and the algebra of regular events[END_REF][START_REF] Boffa | Une remarque sur les systèmes complets d'identités rationnelles[END_REF][START_REF] Boffa | Une condition impliquant toutes les identités rationnelles[END_REF]. Deciding identities in Kleene algebras is therefore PSpacecomplete [START_REF] Meyer | The equivalence problem for regular expressions with squaring requires exponential space[END_REF] by standard automata constructions. Variants of Kleene algebras provide simple algebraic semantics for while-programs, and, in particular, decision procedures for these.

Pomset languages [START_REF] Grabowski | On partial languages[END_REF], on the other hand, are a widely studied model of true concurrency in which words are generalised from linear orders to partial ones. Recent applications can be found, for instance, in weak memory model verification [START_REF] Horn | On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency[END_REF]. Algebras for pomsets have been proposed first by Gischer [START_REF] Gischer | The equational theory of pomsets[END_REF] and more recently, as concurrent Kleene algebra (CKA), by Hoare et al. [START_REF] Hoare | Concurrent Kleene algebra and its foundations[END_REF], with the aim of extending the pleasant properties of Kleene algebras into concurrency. Yet much less is known about their structure.

Formally, CKAs are structures (K, +, •, , , ( ) , 0, 1) that consist of a Kleene algebra (K, +, •, , 0, 1) and a commutative Kleene algebra (K, +, , ( ) , 0, 1), and satisfy the weak interchange law defined below. Commutative Kleene algebras axiomatise rational commutative expression equivalence, which is decidable [START_REF] Conway | Regular algebra and finite machines[END_REF] and coNExp-complete [START_REF] Haase | Tightening the complexity of equivalence problems for commutative grammars[END_REF]. In applications of CKA, the elements of K are typically actions of a system: The operation + models nondeterministic choices, • and sequential and parallel compositions, 1 the ineffective action, and 0 the abortive one. The sequential star models the finite sequential iteration of actions in terms of a least fixpoint, the parallel star ( ) their finite parallel iteration. It can be interpreted as the unbounded spawning of parallel processes.

Closed terms in the language of Kleene algebra correspond to rational expressions; their interpretation as word languages is standard. The extension to parallelism, hence to actionlabelled partial orders and pomsets, is best explained by example. The expression (a • b) c, for instance, is represented by the first of the following pomsets. Execution time-the order of the poset-is indicated by lines proceeding from left to right in this implicitly directed graph. Sequential composition thus orders actions, whereas parallel composition leaves them unordered. By analogy to word languages, expressions involving + or the stars require interpretations by sets of pomsets, that is, pomset languages. The expression (a • b) (c + (d • d)), for instance, denotes the language formed by the first two of the pomsets above. The third of the above pomsets is denoted by (a d) • (b d). It is obviously "more sequential" than the pomset to its left, which is denoted by (a • b) (d • d). A corresponding refinement order, which compares degrees of sequentiality, has been defined on pomsets (as the smoother-than relation) by Grabowski [START_REF] Grabowski | On partial languages[END_REF]. It is isomorphic to the inclusion order on refinement-closed pomset languages and induces a (refinement) order on CKA expressions. Gischer [START_REF] Gischer | The equational theory of pomsets[END_REF] has shown that this order is characterised precisely by the inequality (a c)•(b d) ≤ (a•b) (c•d) on CKA expressions (without the stars). This weak interchange law is also one of the standard CKA axioms.

Pomset languages are typically infinite when expressions contain stars. In addition, the width of individual pomsets can be unbounded when parallel stars occur; this star is therefore often omitted [START_REF] Lodaya | Series-parallel languages and the bounded-width property[END_REF]. Furthermore, CKA expressions generate subclasses of pomset languages. Those generated by expressions over the full CKA signature are called series-parallel-rational (spr-languages), those generated by using a signature without the parallel star are called series-rational (sr-languages). Expressions are named accordingly. All pomsets occurring in spr-or sr-languages, which are built inductively from singleton pomsets by sequential and parallel compositions, are series-parallel or, equivalently, free of N-shape subpomsets [19,[START_REF] Grabowski | On partial languages[END_REF].

Equivalence of spr-expressions, as induced by spr-language identity, is decidable and can be axiomatised by any set of axioms for Kleene algebras plus those for commutative Kleene algebras [START_REF] Laurence | Completeness theorems for bi-Kleene algebras and seriesparallel rational pomset languages[END_REF], but a reasonable upper complexity bound has not been established. In the context of CKA with the interchange axiom, completeness or decidability of the refinement of spr-expressions, or even sr-expressions, as induced by inclusion of refinement-closed spr-or sr-languages, remains open. These questions are of obvious interest for comparing concurrent systems with respect to their degree of sequentiality or linearisability Our first contribution consists in a simple new algorithm and a first complexity bound for sr-expression equivalence. First, using a construction similar to Thompson's [18] and Grabowski's [START_REF] Grabowski | On partial languages[END_REF], we show that every sr-language is the pomset trace language of a safe labelled Petri net. Using a result by Jategaonkar and Meyer on pomset languages of Petri nets [START_REF] Jategaonkar | Deciding true concurrency equivalences on safe, finite nets[END_REF], it then follows that sr-expression equivalence is in ExpSpace (Theorem 5).

Our second, more interesting contribution is a proof that sr-expression refinement is ExpSpace-complete (Theorem 26). Note that sr-expression equivalence is sr-expression refinement in both directions. This result requires comparing runs in Petri nets up-to Grabowski's refinement order, using the freedom provided by this formalism to reorder transitions, and a schedule for constructing a comparison function in a canonical way. Preservation of sequentiality or causality in this construction is somewhat intricate: it requires tracking the history and relationships between loci (Section 5.2 and 5.3). The Petri net approach seems natural once more due to the correspondence between nets and pomset languages, and our previous construction. Hardness of sr-expression refinement follows from a reduction from the equivalence problem for regular expressions with a shuffle operation [START_REF] Mayer | The complexity of word problems -this time with interleaving[END_REF], using results by Grabowski that relate pomset and shuffle languages.

2

Preliminary definitions

Pomsets

We fix a finite alphabet Σ. A labelled poset is a triple X, ≤, λ where X is a finite carrier set, ≤ is a partial order on X and the map λ : X → Σ labels every element in X with a letter in Σ. A (labelled poset) morphism is a function between labelled posets that preserves the order and the labels. A pomset is an isomorphism class of labelled posets; it is a labelled poset up-to bijective renaming of the elements in X. We represent pomsets as graphs that are implicitly directed from left to right. The vertices, which are the elements of the pomset, are labelled by λ; those edges that can be deduced by transitivity and reflexivity are omitted. We define the following pomsets and operations on pomsets:

The empty pomset, denoted by P 0 , is defined as ∅, ∅, [] ([] denoting the empty function); for a ∈ Σ, the singleton pomset

P a is {•} , { •, • } , [• → a] ; for pomsets P 1 = X 1 , ≤ 1 , λ 1 and P 2 = X 2 , ≤ 2 , λ 2 with X 1 ∩ X 2 = ∅;
the parallel product of P 1 and P 2 is the pomset obtained by putting them side by side:

P 1 P 2 X 1 ∪ X 2 , ≤ 1 ∪ ≤ 2 , λ 1 ∪ λ 2 ;
the sequential product of P 1 and P 2 is the pomset obtained by further declaring all elements of P 1 as smaller than those of P 2 :

P 1 ; P 2 X 1 ∪ X 2 , ≤ 1 ∪ ≤ 2 ∪ X 1 × X 2 , λ 1 ∪ λ 2 .
Pomset P 1 refines P 2 , written P 1 P 2 , if there exists a bijective morphism ϕ :

X 2 → X 1 .
By definition, therefore, ∀x ∈ X 2 , λ 1 (ϕ(x)) = λ 2 (x), i.e., the bijection preserves labels; and ∀x, y ∈ X 2 , x ≤ 2 y ⇒ ϕ(x) ≤ 1 ϕ(y), i.e., the morphism preserves edges in P 2 . The relation is a partial order on pomsets. We write S for the downward closure of a set S of pomsets with respect to it: S {P | ∃Q : P Q, Q ∈ S}. We then extend the refinement order to a preorder on sets of pomsets: S S S ⊆ S . (This definition is equivalent to S S S ⊆ S .)

Expressions and pomset languages

A series-rational expression, or more briefly expression, is a term derived from the following syntax. The set of expressions over the alphabet Σ is written Rat Σ .

e, f :

:= e + f | e • f | e f | e | 0 | 1 | a (a ∈ Σ)
The language of an expression is the set of pomsets defined inductively as follows:

1 {P 0 } e•f {P ; Q | P ∈ e , Q ∈ f } e f {P Q | P ∈ e , Q ∈ f } 0 ∅ e + f e ∪ f e n∈N {P 1 ; . . . ; P n | ∀i ≤ n, P i ∈ e } a {P a } .
A set of pomsets is called (series-)rational if it is the language of some expression. It is called downward-closed rational if it is the downward-closure of a rational language. Note that due to the structure of expressions, the pomsets we consider are always seriesparallel: they are built from trivial pomsets by using sequential and parallel compositions. four distinct elements x, y, z, t such that x ≤ y, z ≤ y, and z ≤ t, then either z ≤ x, t ≤ y, or x ≤ t.

x y z t

In the present work we are interested in the following two decision problems.

Definition 1. Given two expressions e, f , the problem biKA(e, f ) asks if e ⊆ f . Definition 2. Given two expressions e, f , the problem CKA(e, f ) asks if e f .

The first problem, biKA(e, f ), asks essentially about equivalence of the sr-expressions e and f . As outlined in the introduction, axioms for Kleene algebras plus those for commutative Kleene algebras (here in fact commutative idempotent semirings without a parallel star) are complete w.r.t. this equivalence. The second one, CKA(e, f ), asks whether e is a refinement of f , which relates to CKA with the interchange law, yet again without a parallel star. We conjecture that the aforementioned axioms together with weak interchange are complete for this semantics, but this problem remains open, to the best of our knowledge.

Labelled safe Petri nets

We now define labelled safe Petri nets-the machines that we use to recognise rational pomset languages. We write + (X) for the set of non-empty subsets of a set X.

A labelled Petri net is a tuple N = P, T, p in , p fin where: P is a finite set of places; T ⊆ + (P) × (Σ ∪ {τ })× + (P) is a set of labelled transitions; p ∈ ∈ P is the initial place; p fin ∈ P is the final place. If t = P, x, P is a transition, then P is its input set, written • t, x is its label, written (t), and P is its output set, written t • . Transitions labelled with τ are called silent; the others are called visible. Without loss of generality, we may restrict ourselves to Petri nets where all inputs and outputs of visible transitions are singleton sets. An example of such a Petri net is displayed in Figure 1.

A configuration is a set of places. A transition t is enabled from a configuration C if • t ⊆ C. Whenever t is enabled in C, then firing this transition leads to the configuration

C (C \ • t) ∪ t • , and we write C t - → N C . A run from C 0 to C n is a sequence t 1 ; . . . ; t n such that there exists configurations C 1 , . . . , C n-1 such that C 0 t1 -→ N C 1 t2 -→ N • • • C n-1 tn -→ N C n . We write C 0 t1;...;tn -----→ N C n in this case. If C 0 = {p in }, then the run is initial, if C n = {p fin },
then it is final, and if both conditions hold, it is accepting. Finally, a configuration C is reachable if some initial run ends in C. Figure 2 shows an example of an accepting run. In this representation, columns of circular nodes denote the successive configurations C i . We draw the transition t i as a rectangular node between C i-1 and C i , drawing directed edges from its inputs in C i-1 to its node, and to its outputs in C i . The remaining places, those in

C i-1 \ • t i that happen again in C i \ t • i , are linked with dotted lines. A Petri net is safe if (C \ • t) ∩ t • = ∅
holds for every reachable configuration C and every transition t enabled in C. In other words, there is always at most one token in every place of a safe Petri net. This justifies our use of sets rather than multisets for configurations a posteriori: we shall only use safe Petri nets.

The transition automaton A (N ) of a Petri net N is a non-deterministic finite state automaton over the alphabet of transitions of N ; its states are configurations of N (i.e. subsets of P), its initial state is {p in }, its only final state is {p fin }, and its transitions are the triples C, t, C such that C t -→ N C . Writing L (B) for the usual word language of an automaton B, the transition automaton is defined so that we have

L (A (N )) t 1 . . . t n {p in } t1;...;tn -----→ N {p fin } .

Language of a Petri net

Let R = C 0 t1;...;tn -----→ N C n be a run in a Petri net N . We define the immediate causality relation → R ⊆ [1..n] × [1..n] as i → R j i < j ∧ ∃p ∈ t • i ∩ • t j : ∀k, i < k < j ⇒ p / ∈ • t k .
The causality relation ≤ R is the reflexive transitive closure of → R . Intuitively, i ≤ R j holds if t j cannot be fired in a subrun of R without firing t i .

For each run one can define three kinds of traces [START_REF] Jategaonkar | Deciding true concurrency equivalences on safe, finite nets[END_REF]. For the run fromFigure 2, these are shown in Figure 3.

The graph-trace

G (R) of R is the graph [1..n], → R . The transition-pomset R is the pomset T (R) [1..n], ≤ R , λ R , where λ R (i) (t i ). The pomset-trace P (R), of R is the restriction of T (R) to the set {i | (t i ) ∈ Σ} of visible actions. C O N C U R 2 0 1 7

24:6 On Decidability of Concurrent Kleene Algebra

The pomset language of a Petri net N is the set N of pomset-traces of accepting runs in N . Moreover, we call a run R is series-parallel if its graph-trace is series-parallel. Note that this is strictly stronger than requiring that its pomset-trace be series-parallel.

The run in Figure 2 is series-parallel.

Reading a pomset in a Petri net

This section describes an operational way of reading and recognising pomsets with Petri nets, as one might read and recognise a word with a finite state automaton. It is independent from the rest of the paper, but might provide insight into the algorithm we develop below to compare languages of nets. Indeed, the guiding intuition behind this algorithm will be to read a net in another net.

Let N = P, T, p in , p fin be a safe labelled Petri net, P = X, ≤, λ a pomset, and

R = C 0 t1 -→ C 1 t2 -→ • • • C n-1 tn -→ C n a run in N . A reading of P in N along R is a sequence ρ 0 , X 0 , . . . , ρ n , X n such that:
1. for every 0 i n, X i ⊆ X and ρ i is a map from C i to (X i ); 2. for every 0 i < n, a. if (t i+1 ) ∈ Σ, and if p 0 , p 1 are respectively the input and output places of t i+1 , there is an element x ∈ ρ i (p 0 ) such that λ(x) = (t i+1 ) and:

X i+1 = X i \ {x} ; ρ i+1 (p) = {y ∈ X i+1 | x ≤ y} if p = p 1 ρ i+1 (p) = ρ i (p) \ {x} otherwise. b. if (t i+1 ) = τ , then X i+1 = X i ; ρ i+1 (p) = q∈ • ti+1 ρ i (q) if p ∈ t • i+1 ρ i (p) otherwise.
The reading is initial if C 0 = {p in } and ρ 0 (p in ) = X 0 = X. The reading is final if C n = {p fin } and X n = ∅. The reading is accepting if it is both initial and final. P is accepted by N if there is an accepting reading of P in N . The language recognised by N is the set of pomsets accepted by N . It should not be confused with the pomset language of N , as defined above.

Remark. Notice that, if R is accepting, the existence of an accepting reading of P along R can be tested by a simple history-independent non-deterministic algorithm. We start with X 0 = X and ρ 0 = [p in → X]. At step i + 1 we use condition 2b to compute ρ i+1 and X i+1 if t i+1 is silent,. If t i+1 is visible and there is no x ∈ ρ i ( • t i+1 ) such that λ(x) = (t i+1 ), then we conclude that there are no readings of P along R. Otherwise, we non-deterministically choose an appropriate x and use condition 2a to compute ρ i+1 and X i+1 . If this yields X n = ∅ we have obtained an accepting reading, otherwise we can conclude that there are no such readings. Lemma 3. If R is accepting, there is an accepting reading of P along R if and only if P P (R).

Proof. 1 Suppose P P (R) and call ϕ the corresponding bijection from P (R) to P . We define, for 0 i n and p ∈ C i :

X i = {ϕ (j) | i < j} ρ i (p) = {x ∈ X i | ∀j ∈ vpred p, i , ϕ (j) ≤ P x} .
We now prove that the sequence ( ρ i , X i ) 0 i n is an accepting reading of P along R. Clearly, X 0 = X, X n = ∅, and condition 1 is satisfied. Condition 2b being straightforward to check, we only detail the proof for condition 2a. If t i+1 is visible, we pick x = ϕ (i + 1). It belongs to ρ i ( • t i+1 ), because 1) i < i + 1 entails ϕ (i + 1) ∈ X i ; 2) for every j ∈ vpred • t i+1 , i , j ≤ R i + 1 which means ϕ (j) ≤ P ϕ (i + 1). Because ϕ witnesses P P (R), we know that the labels of t i+1 and ϕ (i + 1) are equal. We also get

X i+1 = {ϕ (j) | i + 1 < j} = {ϕ (j) | i < j and i = i + 1} = X i \ {ϕ (i + 1)}. If p / ∈ t • i+1 , then vpred p, i + 1 = vpred p, i which means that ρ i+1 (p) = ρ i (p) ∩ X i+1 = ρ i (p) \ {ϕ (i + 1)} .
Finally, for

ρ i+1 t • i+1 , notice that ∀j ∈ vpred t • i+1 , i + 1 , ϕ (j) ≤ P ϕ (k) ⇔ ϕ (i + 1) ≤ P ϕ (k) . If we have an accepting reading (ρ i , X i ) i of P along R, let {i 1 , • • • , i m }
be the visible events in R. We define ϕ(i k ) to be the single x contained in X i k \ X i k -1 (i.e. the one from condition 2a). The function ϕ establishes the required subsumption: it is bijective and if i ≤ R j then ϕ(i) ≤ ϕ(j).

Corollary 4. The language recognised by N is N .

Rational Petri nets

This section shows that every rational pomset language is the pomset language of a (safe labelled) Petri net. To this end, we recursively associate with every expression e a Petri net N (e) such that N (e) = e . Moreover, all accepting runs of this Petri net turn out to be series-parallel. The construction poses no difficulty; it is a simple adaptation of Thompson's construction for rational word languages [18], and an extension of a previous construction by Grabowski [START_REF] Grabowski | On partial languages[END_REF] for safe Petri nets and pomset languages. We only present this construction graphically here; a formal description is given in Appendix A.

N (0) = N (1) = N (a) = a N (e1 + e2) = e1 e2 τ τ τ τ N (e1 e2) = e1 e2 τ τ N (e1 • e2) = e1 e2 τ N (e ) = e τ τ τ τ
This construction yields decidability of biKA in exponential space. Indeed we may build the Petri nets N (e) and N (f ) from the expressions e and f (these are linear in the size of e and f ) and use Jategaonkar and Meyer's result [START_REF] Jategaonkar | Deciding true concurrency equivalences on safe, finite nets[END_REF] that testing containment of pomset-trace languages of two Petri nets is an ExpSpace-complete problem.

Comparing Petri nets modulo refinement

Next we show how to compare Petri nets modulo refinement. Thanks to the previous construction, this leads to decidability of the problem CKA. We fix two Petri nets N 1 and N 2 for this section and the following one. Our goal is to check whether N 1 N 2 , i.e., whether for each run R 1 ∈ L (N 1 ), there exists a corresponding run R 2 ∈ L (N 2 ) such that

P (R 1 ) P (R 2 ).
The first difficulty is that we may have to reorder runs in N 2 : due to concurrency, transitions might be triggered in different orders and still yield the same pomset.

Reordering runs

Let R = t 1 ; . . . ; t n be a run from C 0 to C n . Let π be a permutation of [1..n]. The action of π on R is defined as πR t π(1) ; . . .

; t π(n) . The permutation π is compatible with R if it is order-preserving: ∀i, j, i ≤ R j ⇒ π(i) π(j). Lemma 7. If π is compatible with R, then C 0 πR --→ N C n , G (R) = G (πR), and i ≤ R j ⇔ π(i) ≤ πR π(j).
Proof. We can exchange two successive transitions that are not causally linked without changing the graph (up-to isomorphism). We repeat this process until we obtain πR.

Accordingly, we say that a run R is equivalent to a run R if R = πR for some compatible permutation π.

Another important notion for the completeness of the method we propose is that of an economical run: a run that fires its silent transitions as late as possible. Definition 8. A run t 1 ; . . . ; t n is economical if for all i < j, if t i , . . . , t j-1 are silent transitions and t j is a visible transition, then i ≤ R j.

The run in Figure 2 is not economical: the fifth transition is a silent one, but it is not causally related to the next transition, which is visible. We will see that it can be reordered into an equivalent economical run (Proposition 10 and Example 11 below.)

Even more importantly when comparing two runs, we need to ensure that the visible transitions are fired in the same order. Definition 9. Given a run R 1 in N 1 and a run R 2 in N 2 such that P (R 1 ) P (R 2 ), we say that R 2 follows R 1 if the subsumption is witnessed by a bijection ϕ such that for every two visible indices i, j in R 2 we have i < j ⇔ ϕ(i) < ϕ(j). Proposition 10. Let R 1 and R 2 be series-parallel runs in N 1 and N 2 , respectively. If P (R 1 ) P (R 2 ) then there exists an economical and series-parallel run R 2 in N 2 that follows R 1 and is equivalent to R 2 .

Proof. Let ϕ be the order-preserving bijection from P (R 2 ) to P (R 1 ), and let R 2 = t 1 ; . . . ; t n . Because of the definition of an equivalent run, we want to find a permutation π that is compatible with R 2 , such that πR 2 follows R 1 and is economical. We define π using a total ordering of [1..n], which we build in several steps. First, we define an ordering 1 on [1..n]:

if i ≤ R2 j then i 1 j; if t i , t j are visible and ϕ(i) < ϕ(j) then i 1 j;

1 is closed by transitivity. This defines a partial ordering, as we cannot have simultaneously i < R2 j and ϕ(j) < ϕ (i):

i < R2 j ⇒ ϕ(i) < R1 ϕ(j) ⇒ ϕ(i) < ϕ(j).
We extend this ordering further as 2 : if i 1 j then i 2 j; if t i is visible, t j is silent, and i and j are independent with respect to 1 , then i 2 j; 2 is closed by transitivity.

Let

be a linear extension of 2 , and let π be the associated permutation, defined inductively as:

π -1 (0) = min [1..n] π -1 (i + 1) = succ π -1 (i).
Clearly, π is compatible with R 2 , as ≤ R2 ⊆ . Thus πR 2 is an accepting run and G (πR 2 ) = G (R 2 ). Hence P (R 1 ) P (R 2 ) = P (πR 2 ), and because R 2 is series-parallel, πR 2 is also series-parallel.

We now check that πR 2 is economical, by contradiction. Let t i be a silent transition in πR 2 , j 0 = min {k > i | t k visible}, and i ≤ πR2 j 0 . This later condition translates as π -1 (i) ≤ R2 π -1 (j 0 ). Then either π -1 (j 0 ) ≤ R2 π -1 (i) or the two are independent. In the first case, we would have π -1 (j 0 ) 1 π -1 (i), and in the second π -1 (j 0 ) 2 π -1 (i). In both cases, we get π -1 (j 0 ) π -1 (i), thus j 0 < i, which contradicts the definition of j 0 . The pomset of R 1 is P (R 1 ) = P a P b (P d ; P c ), and we may check that P (R 1 ) P (R 2 ).

To transform R 2 into a run that is economical and follows R 1 , we must (1) exchange the transitions labelled with c and d; and (2) delay the silent transition in the middle of R 2 until all visible transitions have been fired. Doing so, we get the following run R 2 , which follows R 1 and is equivalent to R 2 .

Loci

In this more technical section, we define loci, as a way to lift the causality relation between transitions to places in the successive configurations of the runs. Let R be a run, with

R = C 0 t1 -→ C 1 • • • C n-1 tn -→ C n , T (R) = [1.
.n], ≤ R , λ . A locus denotes a pair p, i where 0 i n and p ∈ C i . In some sense, loci are places with a time index. In the previous pictures those are the numbered circles: p is the number in the circle (the name of the place),

C O N C U R 2 0 1 7

24:10

On Decidability of Concurrent Kleene Algebra and i is the index of its column. Formally, the set of loci of the run R is 0 i n C i × {i}. We generate an equivalence relation ≈ R on loci using the following rule:

p / ∈ • t i ⇒ p, i ≈ R p, i -1 .
Graphically, equivalent loci are linked with dotted lines. Equivalences classes with respect to ≈ R are thus places with a time interval, rather than a single index. The source of a locus p, i is the smallest index of its equivalence class:

src p, i min {j i | p, i ≈ R p, j } .
Now we define a preorder R , generated by the following rules:

p, q ∈ • t i × t • i ⇒ p, i -1 R q, i , p, i ≈ R q, j ⇒ p, i R q, j .
Note that two loci in the same configuration are always incomparable. Finally, we inductively define the set of indices of predecessors of a locus:

pred p, 0 ∅. if p ∈ t • i , then pred p, i {i} ∪ q∈ • ti pred q, i -1 . if p / ∈ t • i , then pred p, i pred p, i -1 .
The set of visible predecessors of a locus, written vpred p, i , is the subset of indices of visible transitions in pred p, i .

Lemma 12.

The following properties hold:

∀i, ∀p ∈ t • i , pred p, i = {j | j ≤ R i} , (1) ∀i
, ∀p ∈ C i , pred p, i = {j | j ≤ R src p, i } , (2)
∀i, j, p, q, p, i ≈ R q, j ⇒ pred p, i = pred q, j ,

∀i, j, p, q, p, i R q, j ⇒ pred p, i ⊆ pred q, j , (

∀i, j, p, ∀q ∈ t • j , j ∈ vpred p, i ⇒ q, j R p, i , (

∀i j, ∃p ∈ C j : i ∈ pred p, j .

Notice that we managed to lift the causality relation ≤ R to the level of loci: this lemma implies that if i = j, p ∈ t • i and q ∈ t • j , then i ≤ R j if and only if p, i R q, j .

Schedules

We compare runs using the following notion of schedule, where we interleave two runs in such a way that they synchronise on visible transitions.

Definition 13.

Let R 1 and R 2 be two runs with

R i = C i 0 t i 1 -→ C i 1 • • • C i ni-1 t i n i --→ C i ni for i ∈ {1, 2}. An N -schedule from R 1 to R 2 is a function η : [0..N ] → [0..n 1 ] × [0..n 2 ] such that η(0) = 0, 0 and η(N ) = n 1 , n 2 ; if η(k) = i, j , then either 1. t 1 i+1 is a silent transition and η(k + 1) = i + 1, j , or 2. t 2
j+1 is a silent transition and η(k + 1) = i, j + 1 , or 3. t 1 i+1 and t 2 j+1 are visible, t 1 i+1 = t 2 j+1 and η(k + 1) = i + 1, j + 1 .

P. Brunet, D. Pous, G. Struth

24:11

Note that a schedule constructs a bijection between the visible transitions of R 1 and those of R 2 . Indeed, each of these transitions must be fired synchronously and agree on labels (case 3). Furthermore, since a schedule starts with η(0) = 0, 0 and ends with η(N ) = n 1 , n 2 , every transition in both runs must be fired. This means there is a label-preserving bijection ϕ, called the bijection induced by η, from the visible transitions of R 2 to those of R 1 that satisfies i < j if and only if ϕ(i) < ϕ(j).

The notion of schedule is still very weak: there are schedules from one run to another whenever they have the same visible transitions, in the same order. Causality between those transitions is not taken into account. We fix this with the following technical definition. Intuitively, we keep track of the history and relationships between the loci of the configurations, in order to ensure that the causality relation in the presumably smaller run R 1 refines that of R 2 . Definition 14. For each N -schedule we define the following sequence of binary relations

(≺ k ) k∈[0..N ] , where ≺ k ⊆ C 1 i × C 2 j when η(k) = i, j
, by induction:

≺ 0 = C 1 0 × C 2 0 ; if η(k) = i, j , then 1. if η(k + 1) = i + 1, j , we set p ≺ k+1 q p ≺ k q if p / ∈ (t 1 i+1 ) • , ∃p ∈ • t 1 i+1 , p ≺ k q otherwise. 2. if η(k + 1) = i, j + 1 , we set p ≺ k+1 q p ≺ k q if q / ∈ (t 2 j+1 ) • , ∀q ∈
• t 2 j+1 : p ≺ k q otherwise. 3. otherwise, let t 1 i+1 = {p 0 } , a, {p 1 } and t 2 j+1 = {q 0 } , a, {q 1 } ; we set p ≺ k+1 q p 0 ≺ k q or (q = q 1 and p 0 ≺ k q 0 ) if p = p 1 p ≺ k q and q = q 1 otherwise.

The schedule η is valid if for every visible index i in R 2 we have p ≺ k q for the unique k, p, q such that η(k) = ϕ(i), i , (t [START_REF] Grabowski | On partial languages[END_REF][START_REF] Gischer | The equational theory of pomsets[END_REF]; [START_REF] Grabowski | On partial languages[END_REF][START_REF] Grabowski | On partial languages[END_REF]; [START_REF] Grabowski | On partial languages[END_REF][START_REF] Haase | Tightening the complexity of equivalence problems for commutative grammars[END_REF]; [START_REF] Grabowski | On partial languages[END_REF][START_REF] Hoare | Concurrent Kleene algebra and its foundations[END_REF] We may then draw the two runs side by side according to this schedule: From this schedule, we can compute the successive ≺ k relations, and check that 4 ≺ 3 5, 5 ≺ 4 6, 6 ≺ 5 8, and 7 ≺ 6 7. Hence η is valid.

C O N C U R 2 0 1 7

24:12

On Decidability of Concurrent Kleene Algebra

Remark. If η(k) = i, j , η(k ) = i , j , p, i ≈ R1 p , i and q, j ≈ R2 q , j , then p ≺ k q if and only if p ≺ k q . Lemma 16. If η(k) = i, j , then p ≺ k q entails ϕ(vpred q, j ) ⊆ vpred p, i .

Proof. We proceed by induction on k. The statement is obvious for k = 0, as all sets of predecessors are empty at this point. For the inductive step, if η(k) = i, j , then either:

1. t 1
i+1 is a silent transition, η(k + 1) = i + 1, j ; suppose p ≺ k+1 q: if p / ∈ (t 1 i+1 ) • , then p ≺ k q and vpred p, i = vpred p, i + 1 ; we conclude using the induction hypothesis. if p ∈ (t 1 i+1 ) • , then there exists p ∈ • t 1 i+1 such that p ≺ k q. By induction we deduce that ϕ (vpred q, j ) ⊆ vpred p , i , hence

ϕ (vpred q, j ) ⊆ p ∈ • t 1 i+1 vpred p , i = vpred p, i + 1 2. or t 2 j+1 is a silent transition, η(k + 1) = i, j + 1 ; suppose p ≺ k+1 q: if q / ∈ (t 2
j+1 ) • , then p ≺ k q and vpred q, j = vpred q, j + 1 , we conclude by induction; if q ∈ (t 2 j+1 ) • , then for every q ∈ • t 2 j+1 we have p ≺ k q , and thus ϕ (vpred q , j ) ⊆ vpred p, i by induction; we finally get

ϕ (vpred q, j+1 ) = ϕ    q ∈ • t 2 j+1 vpred q , j    = q ∈ • t 2 j+1
ϕ (vpred q , j ) ⊆ vpred p, i 3. or t 1 i+1 and t 2 j+1 are visible, t 1 i+1 = t 2 j+1 and η(k + 1) = i + 1, j + 1 ; suppose t 1 i+1 = {p 0 } , a, {p 1 } , t 2 j+1 = {q 0 } , a, {q 1 } , and p ≺ k+1 q. There are three cases: either p, q = p 1 , q 1 and p 0 ≺ k q 0 , which means by induction that ϕ (vpred q 0 , j ) ⊆ vpred p 0 , i . Also notice that i + 1 and j + 1 are corresponding indices, in the sense that ϕ(j + 1) = i + 1, thus we have: ϕ (vpred q 1 , j + 1 ) = ϕ ({j + 1} ∪ vpred q 0 , j ) = {i + 1} ∪ ϕ (vpred q 0 , j ) ⊆ {i + 1} ∪ vpred p 0 , i = vpred p 1 , i + 1 or p = p 1 and p 0 ≺ k q, in which case we have ϕ (vpred q, j + 1 ) = ϕ (vpred q, j ) ⊆ vpred p 0 , i ⊆ vpred p 1 , i + 1 or p = p 1 and q = q 1 and we conclude by induction. The algorithm we define in the next section looks for valid schedules. The following proposition establishes soundness of this strategy. Proposition 17. If there exists a valid schedule from R 1 to R 2 , then P (R 1 ) P (R 2 ).

Proof. The bijection ϕ induced by η works. Let i, j be visible indices in R 2 such that i ≤ R2 j. We need to show that ϕ(i) ≤ R1 ϕ(j). Take the unique k, p, q such that η(k) = ϕ(j), j , (t 1 ϕ(j) ) • = {p} and (t 2 j ) • = {q}. By Lemma 12.(1) we have i ∈ vpred q, j . Since η is valid, we have p ≺ k q, and thus ϕ(vpred q, j ) ⊆ vpred p, ϕ(j) by Lemma 16. This means that ϕ(i) ∈ vpred p, ϕ(j) , and using Lemma 12.(1) again we obtain ϕ(i) ≤ R1 ϕ(j).

For the lower bound, we reduce the problem of universality of regular expressions with shuffle [START_REF] Mayer | The complexity of word problems -this time with interleaving[END_REF] to the containment of downward-closed rational languages. We briefly recall the former. Regular expressions with shuffle over the alphabet Σ are terms over the syntax e, f ∈ Rat Σ ::

= e + f | e • f | e f | e | 0 | 1 | a (a ∈ Σ).
Given two words u and v over Σ, the shuffle product of u and v, written u v, is the language of all words of the form u

1 v 1 u 2 v 2 • • • u k v k ; where u = u 1 • • • u k , v = v 1 • • • v k ,
and the words u i , v i can be of arbitrary length (including the empty word).

The language of a regular expression with shuffle is defined recursively as follows.

0 := ∅ 1 := {ε} a := {a} e + f := e ∪ f e • f := e • f e f := u∈ e , v∈ f u v e := n∈N {u 1 . . . u n | ∀i n, u i ∈ e } .
Theorem 24 (Mayer and Stockmeyer [16]). The problem of testing whether the language of a regular expression with shuffle is equal to Σ is ExpSpace-complete.

The key observations for our reduction are due to Grabowski [START_REF] Grabowski | On partial languages[END_REF]: words are isomorphic to totally ordered pomsets, and given two words u and v, the set of totally ordered pomsets in u v is isomorphic to the shuffle product of u and v.

Concretely, we associate a series-parallel expression e to any regular expression with shuffle e by replacing every occurrence of with . This encoding has the following property.

Lemma 25. For every word w ∈ Σ , we have w ∈ e if and only if w seen as a totally ordered pomset is in e .

Proof. By a simple induction on e, using the above observation for the shuffle case. (Each subcase can be found in [START_REF] Grabowski | On partial languages[END_REF].)

As a consequence, the language of e is Σ if and only if Σ e . We thus have a linear encoding of the universality of regular expressions with shuffle into containment of downward-closed rational languages, hence our final theorem.

Theorem 26. The problem CKA is ExpSpace-complete.

An implementation of the algorithm is available at http://paul.brunet-zamansky.fr/cka.html.

Related work

Several constructions in the literature are similar to those presented in Section 4. Here we list some of them, highlighting the differences between these developments and our own. Lodaya and Weil introduced branching automata that recognise series-parallel rational pomset languages [START_REF] Lodaya | Series-parallel languages and the bounded-width property[END_REF], which include the series-rational languages we use here. These automata impose a strong notion of bracketing (opening and closing τ -transitions must match exactly), which we do not know how to handle when it comes to comparing automata. This is why we used plain Petri nets instead.

Jategaonkar and Meyer presented a construction almost equivalent to ours [START_REF] Jategaonkar | Deciding true concurrency equivalences on safe, finite nets[END_REF], albeit for different purposes: their goal was to obtain a lower complexity bound by a reduction from the universality problem of regular languages with shuffle. The main differences in the constructions are that we use an initial place instead of an initial marking, and that C O N C U R 2 0 1 7

24:16

On Decidability of Concurrent Kleene Algebra we consider a unique final place while they have a distinguished final transition. These differences mainly impact the star and parallel product constructs. Jategaonkar and Meyer's construction could in fact be adapted to obtain an alternative proof of Theorem 5. However, their construction does not satisfy the structural constraints needed for the completeness of the algorithm we develop in Section 5: the runs of the automata produced by their construction are not always series-parallel.

Finally, a third construction that produces safe Petri nets from expressions was developed by Lodaya [START_REF] Lodaya | Hierarchical structure of 1-safe petri nets[END_REF]. It is, however, quite different from the present approach. In particular, it requires initial and final markings, and it is not appropriate for a precise complexity analysis, as it produces nets that are exponentially large with respect to input expressions.

Figure 1

 1 Figure 1 Example of labelled safe Petri net.

Figure 2 Figure 3

 23 Figure 2 An accepting run of the Petri net in Figure 1.

Theorem 5 .Proposition 6 .

 56 The problem biKA lies in the class ExpSpace. The language recognised by N (e) is e .Proof. By construction we have N (e) = e . We conclude using Corollary 4.

Example 11 .

 11 Consider the run R 2 from Figure2and the following run R 1 :

  Recall the runs R 2 and R 1 from Example 11. The following sequence is a schedule from R 1 to R 2 .

	1 ϕ(i) ) • = {p} and (t 2 i ) • = {q}.
	Example 15. η = (0, 0); (1, 0); (1, 1); (2, 2); (3, 3); (4, 4); (5; 5);

This proof uses the notion of locus and some of the notations to be introduced in Section 5.2.

* Extended version of the This work was supported by the European Research Council (ERC) under the Horizon 2020 programme (CoVeCe, grant agreement No 678157) and the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007)

24:13

For completeness of the algorithm we need to exhibit valid schedules. Under appropriate assumptions-see Proposition 19 below-the following canonical schedule η from R 1 to R 2 will work. We define it recursively. Intuitively, we schedule the silent transitions of R 1 as early as possible and those of R 2 as late as possible: η(0) = 0, 0 ; if η(k) = i, j then

i+1 is visible and t 2 j+1 is silent then η(k + 1) = i, j + 1 ; 3. if t 1 i+1 and t 2 j+1 are visible, then η(k + 1) = i + 1, j + 1 . We write ϕ for the bijection induced by η. The schedule from Example 15 is actually the canonical schedule. The converse of Lemma 16 holds for the canonical schedule: Lemma 18. If R 2 is series-parallel and economical, then, for every k with η(k) = i, j , if ϕ(vpred q, j ) ⊆ vpred p, i , then p ≺ k q.

Proof. See Appendix B.

Proposition 19. If R 1 and R 2 are series-parallel, if P (R ) P (R 2 ), and if R 2 is economical and follows R 1 then the canonical schedule η from R 1 to R 2 is valid.

Proof. First note that since R 2 follows R 1 , ϕ and the bijection witnessing P (R 1 ) P (R 2 ) must coincide. Let i be a visible index in R 2 , and let k, p, q such that η

We have to prove p ≺ k q. By Lemma 18, it suffices to prove the inclusion ϕ(vpred q, i ) ⊆ vpred p, ϕ(i) , i.e., that for every j ∈ vpred q, i , we have ϕ(j) ∈ vpred p, ϕ(i) . This is equivalent to checking that for every visible j, j ≤ R2 i implies ϕ(j) ≤ R1 ϕ(i), which is true because ϕ is an order preserving bijection from the pomsets of R 2 to that of R 1 .

Note that this lemma relies on the fact that R 2 is series-parallel. Indeed, there can be pairs of runs R 1 and R 2 satisfying P (R 1 ) P (R 2 ), and R 2 being economical and following R 1 , but such that the canonical schedule is not valid.

Reduction to finite automata

Now that we have the notion of valid schedule, we use a technique similar to [START_REF] Jategaonkar | Deciding true concurrency equivalences on safe, finite nets[END_REF] to reduce the problem of comparing Petri nets modulo subsumption to the comparison of plain automata. For this end, we define the following automaton that aims at recognising those runs of N 1 for which there exists a valid schedule to some run in N 2 .

Definition 20. The composite automaton N 1 ≺ N 2 is the nondeterministic finite state automaton with epsilon-transitions Q, T 1 , q 0 , F where: the alphabet is the set of transitions of N

3. if t 1 and t 2 are visible transitions of N 1 and N 2 with the same label, inputs p 0 and q 0 and outputs p 1 and q

there is a transition labelled with t 1 going to the state

By definition of this composite automaton, we have Lemma 21. The language of the automaton N 1 ≺ N 2 is the set of accepting runs R 1 in N 1 such that there is an accepting run R 2 in N 2 and a valid schedule from R 1 to R 2 .

Finally, we can reduce the comparison of Petri nets modulo subsumption to that of (word) automata.

Proposition 22. If the runs in N 1 and those in N 2 are all series-parallel, then

. By assumption we also have

, which means, by Lemma 21, that there is an accepting run R 2 in N 2 and a valid schedule η from R 1 to R 2 . Proposition 17 then tells us that P (R 1 ) P (R 2 ), thus proving P ∈ N 2 . Conversely, assume that N 1 N 2 . Let R 1 ∈ L (A (N 1 )) be an accepting run in N 1 . By assumption, there is an accepting run R 2 in N 2 such that P (R 1 ) P (R 2 ). By hypothesis, both R 1 and R 2 are series-parallel. By Proposition 10, there exists an economical seriesparallel run R 2 that follows R 1 and is equivalent to R 2 . Hence using Proposition 19, there is a valid schedule from R 1 to R 2 . With Lemma 21 we conclude that R 1 ∈ L (N 1 ≺ N 2 ).

6

Decidability & Complexity of CKA Putting together the results from Sections 4 and 5 yields the announced algorithm.

Proposition 23. CKA lies in the class ExpSpace.

Proof. We build the Petri nets N (e) and N (f ), and then the finite automata A (N (e)) and N (e) ≺ N (f ). By Proposition 22, to answer the original question, we simply need to test these automata for language inclusion. It is well known that this requires polynomial space with respect to the size of the automata.

Let n be the size of e and m the size of f (their number of symbols). The Petri nets N (e) and N (f ) are linear in the size of e and f , with at most 2n and 2m places. The automaton A (N (e)) uses at most 2 2n states (recall these are sets of places). The automaton N (e) ≺ N (f ) uses at most 2 2n × 2 2m × 2 2n×2m states. Hence testing language equivalence of these two automata will use an amount of space polynomial in 2 2n and 2 2n+2m+4nm , whence the announced result.

24

A Construction of rational Petri nets

N (e 1 e 2 ): let N (e i ) = P i , T i , p i , q i for i = 1, 2, with

B Proof of Lemma 18

We first prove two preliminary lemmas.

Lemma 27. If R is a series-parallel run, and if in some intermediate configuration

Proof. Recall that every series-parallel pomset is N-free [19, Theorem 3.1]. This means that for every quadruple of distinct elements a, b, c, d such that:

) is series-parallel, then its set of loci forms such a pomset. Consider q ∈ C i such that k 1 , k 2 ∈ vpred q, i , with k 1 and k 2 are incomparable, and p ∈ C i such that k 1 ∈ vpred p, i . Let us call p 1 , p 2 the places respectively in the outputs of t k1 and t k2 (recall that k 1 and k 2 are visible, which means they have a singleton output).

We know that p 1 , k 1 , p 2 , k 2 R q, i and p 1 , k 1 R p, i . Because k 1 and k 2 are incomparable, so are p 1 , k 1 and p 2 , k 2 . Being in the same configuration, q, i and p, i must also be incomparable. Using the previous remark, we get that p 2 , k 2 R p, i , thus proving k 2 ∈ vpred p, i . Lemma 28. If R is economical and t i is a visible transition, then for all p ∈ C i , either src p, i is visible, or there exists p ∈ C i such that src p , i is visible and pred p, i ⊆ pred p , i .

24:18

On Decidability of Concurrent Kleene Algebra Proof. Suppose t i is a visible transition, and consider p ∈ C i , such that k = src p, i is silent. Let us write l = min {j > k | t j visible}. By definition of economy, k ≤ R l. As t i is visible and i > k, we have l i. This means that there exists p ∈ C i such that l ∈ pred p , i . If src p , i = l then we are done, otherwise we repeat the argument with p instead of p, but notice that the source of p is strictly larger (for the ordering of natural numbers) than that of p, and still smaller than i, hence this search will eventually terminate. Now we can prove Lemma 18. (If R 2 is series-parallel and economical, then for every k with η(k) = i, j , if ϕ(vpred q, j ) ⊆ vpred p, i , then p ≺ k q.) Proof. We proceed by induction on k, the base case being obvious.

If t 1

i+1 is silent, there are two cases: Either p / ∈ (t 1 i+1 ) • , and then vpred p, i + 1 = vpred p, j . Therefore the assumption ϕ (vpred q, j ) ⊆ vpred p, i + 1 yields ϕ (vpred q, j ) ⊆ vpred p, i . induction we get p ≺ k q, allowing us to check that p ≺ k+1 q. Or we have p ∈ (t 1 i+1 ) • . Assume ϕ (vpred q, j ) ⊆ vpred p, i + 1 ; in order to prove that p ≺ k+1 q we need to find some p ∈

• t 1 i such that ϕ (vpred q, j ) ⊆ vpred p , i . We know that vpred p, i + 1 = p ∈ • t 1 i vpred p , i . We use Lemma 28, as R 2 is economical, and the last transition it fired was visible. This allows us to split once more into two cases:

if src q, j is visible, then there must be some p 0 ∈ • t 1 i such that ϕ (src q, j ) ∈ vpred p 0 , i , meaning ϕ (src q, j ) ≤ R2 src p 0 , i . Thus we get:

if there is q 0 such that j 0 = src q 0 , j is visible and pred q, j ⊆ pred q 0 , j . We know that there is a previous k 0 k when η(k 0 ) = ϕ(j 0 ), j 0 . If we write i 0 = ϕ(j 0 ) and p 0 for the output of t 1 i0 , at that point we have ϕ (vpred q 0 , j 0 ) ⊆ vpred p 0 , i 0 . This means that there is p 1 ∈ C 1 i such that: ϕ (pred q, j ) ⊆ ϕ (vpred q 0 , j 0 ) ⊆ vpred p 1 , i . Now, consider the set of maximal events in ϕ (pred q, j ). By definition they are incomparable. By the previous remark there are all contained in the set of visible predecessors of some locus p 1 , i . To conclude, just pick one maximal event j 1 in ϕ (pred q, j ). As we know j 1 ∈ p ∈ • t 1 i vpred p , i , thus there is p ∈ • t 1 j i such that j 1 ∈ vpred p , i . By Lemma 27 we get that ϕ (pred q, j ) ⊆ vpred p , i .

If t 2

j+1 is silent, there are also cases to consider: Either q / ∈ (t 2 j+1 ) • , and then vpred q, j + 1 = vpred q, j . The assumption is ϕ (vpred q, j + 1 ) ⊆ vpred p, i ; it entails ϕ (vpred q, j ) ⊆ vpred p, i , and thus p ≺ k q by induction. From this we get p ≺ k+1 q. Or we have q ∈ (t 2 j+1 ) • and vpred q, j + 1 = q ∈ • t 2 j+1 vpred q , j . The assumption ϕ (vpred q, j + 1 ) ⊆ vpred p, i means that ∀q ∈ • t 2 j+1 , vpred q , j ⊆ vpred p, i , so ∀q ∈

• t 2 j+1 , p ≺ k q, hence p ≺ k+1 q. 3. Otherwise, let p 0 , p 1 be the input and output of t 1 i+1 and q 0 , q 1 be the input and output of t 2 j+1 . There are again two cases to consider:

24:19

If p = p 1 , then vpred p, i + 1 = vpred p 0 , i ∪ {i + 1}. By assumption we have ϕ (vpred q, j + 1 ) ⊆ vpred p, i + 1 , and thus either i + 1 = ϕ(j + 1) ∈ ϕ (vpred q, j + 1 ), in which case q must be q 1 , thus p = p 1 ≺ k+1 q 1 = q; or ϕ (vpred q, j ) ⊆ vpred p 0 , i , which means that p 0 k q, hence p 1 = p ≺ k+1 q. otherwise q must be different from q 1 , as ϕ(j + 1) = i + 1 / ∈ vpred p, i + 1 . Thus vpred q, j + 1 = vpred q, j and vpred p, i + 1 = vpred p, i , so we conclude by induction.