main-content

## Weitere Artikel dieser Ausgabe durch Wischen aufrufen

26.03.2021 | Ausgabe 4/2021 Open Access

# Finite Sequentiality of Unambiguous Max-Plus Tree Automata

Zeitschrift:
Theory of Computing Systems > Ausgabe 4/2021
Autor:
Erik Paul
Wichtige Hinweise
This article belongs to the Topical Collection: Special Issue on Theoretical Aspects of Computer Science (2019)
Guest Editors: Rolf Niedermeier and Christophe Paul
This work was supported by Deutsche Forschungsgemeinschaft (DFG), Graduiertenkolleg 1763 (QuantLA).

## Publisher’s Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

## 1 Introduction

A max-plus automaton is a finite automaton which assigns real numbers to words over a given alphabet. The transitions of a max-plus automaton each carry a weight from the real numbers. To every run of the automaton, a weight is associated by summing over the weights of the transitions which constitute the run. The weight of a word is given by the maximum over the weights of all runs on this word.
More generally, max-plus automata and their min-plus counterparts are weighted automata [ 7, 13, 26, 37, 38] over the max-plus or min-plus semiring. Min-plus automata were originally introduced by Imre Simon as a means to show the decidability of the finite power property [ 41, 42]. Since their introduction, max-plus and min-plus automata have enjoyed a continuing interest [ 8, 12, 15, 18, 22, 25] and they have been employed in many different contexts. To only name some examples, they can be used to determine the star height of a language [ 17], to prove the termination of some string rewriting systems [ 43], and to model certain discrete event systems [ 23]. Additionally, they appear in the context of natural language processing [ 29], where for reasons of numerical stability, probabilities are often computed in the min-plus semiring as negative log-likelihoods.
A very prominent open question about max-plus automata is the sequentiality problem, the problem of deciding whether for an arbitrary max-plus automaton there exists a deterministic equivalent. A max-plus automaton is called deterministic or sequential if at most one of its states is initial and for each pair of a state and an input symbol, there is at most one valid transition into a next state. Although the decidability of this problem is unknown for max-plus automata in general, it is known to be decidable for the subclasses of unambiguous [ 29], finitely ambiguous [ 22], and even polynomially ambiguous [ 21] automata. A max-plus automaton is called unambiguous if there exists at most one accepting run on every word. It is called finitely ambiguous if the number of runs on each word is bounded by a global constant. If on every word the number of accepting runs is bounded polynomially in the length of the word, the automaton is said to be polynomially ambiguous. Note that the ambiguity of a max-plus automaton is a decidable property, as it is easily reduced to deciding the ambiguity of a finite automaton. Deciding the sequentiality of a finite automaton is trivial, polynomial time algorithms for deciding the unambiguity, the finite ambiguity, and the polynomial ambiguity of a finite automaton can be found in [ 9, 40, 44]. Furthermore, the classes of functions definable by deterministic, unambiguous, finitely ambiguous, polynomially ambiguous, and arbitrary max-plus automata form a strictly ascending hierarchy [ 19, 22, 28].
A decidability problem which is closely related to the sequentiality problem is the finite sequentiality problem. The finite sequentiality problem asks whether a given max-plus automaton can be represented as a pointwise maximum of finitely many deterministic max-plus automata. In [ 18], it was left as an open question to determine the decidability of the finite sequentiality problem for finitely ambiguous max-plus automata. It was shown only recently that for the classes of unambiguous as well as finitely ambiguous automata, the finite sequentiality problem is decidable [ 3, 4]. The class of functions which allow a finitely sequential representation by max-plus automata lies strictly between the classes of functions definable by deterministic and by finitely ambiguous max-plus automata, and it is incomparable to the class of functions definable by unambiguous max-plus automata [ 22].
In this paper, we show that the finite sequentiality problem is decidable for unambiguous max-plus tree automata. Max-plus tree automata are a generalization of max-plus automata and operate on trees instead of words. In particular, max-plus tree automata are weighted tree automata [ 1, 6, 14, 16] over the max-plus semiring. Applications for max-plus tree automata include proving the termination of certain term rewriting systems [ 24], and they are also commonly employed in natural language processing [ 33] in the form of probabilistic context-free grammars. Our approach to show the decidability of the finite sequentiality problem employs ideas from [ 4]. In [ 4], the fork property is shown to be a decidable criterion to determine the existence of a finitely sequential equivalent. More precisely, unambiguous max-plus word automata are shown to possess a finitely sequential representation if and only if they do not satisfy the fork property. It is shown elementarily that an unambiguous automaton satisfying the fork property cannot possess a finitely sequential equivalent. The proof for the existence of a finitely sequential representation in case that the fork property is not satisfied, on the other hand, relies on the construction of finitely many unambiguous max-plus automata whose pointwise maximum is equivalent to the original automaton, and which all satisfy the twins property. It was shown by Mohri [ 29] that an unambiguous max-plus automaton which satisfies the twins property is determinizable. A finitely sequential representation is thus found by determinizing the unambiguous automata.
For tree automata, we generalize the fork property to the tree fork property by adding a condition which accounts for the nonlinear structure of trees. We then prove that an unambiguous max-plus tree automaton possesses a finitely sequential representation if and only if it does not satisfy the tree fork property. As in the word case, the most challenging part of the proof is to show the existence of a finitely sequential representation whenever the tree fork property is not satisfied. Like in the proof for word automata, we construct finitely many unambiguous max-plus tree automata which possess a deterministic equivalent. However, we need to take a different approach in order to obtain these automata. In [ 4], a modified Schützenberger covering [ 35, 36, 39] is first constructed from the unambiguous max-plus automaton, from which in turn an automaton is constructed which monitors the occurrence of certain states of the modified Schützenberger covering. This latter automaton is then decomposed into the finitely many unambiguous automata. This approach, however, is not applicable to trees, as the monitoring of states requires all relevant states to occur linearly. This happens trivially for word automata due to the inherent linear structure of words, but for tree automata examples can be found where relevant states occur nonlinearly. The approach we use here relies on constructing a max-plus automaton which tracks certain pairs of states of the original automaton. When applied to word automata, this immediately yields an automaton which can be decomposed into the desired unambiguous automata. Unfortunately, for tree automata this tracking of pairs of states again fails due to states occurring nonlinearly. Surprisingly however, our construction can be applied to the Schützenberger covering of the original tree automaton, as the states relevant for tracking all occur pairwise linearly in the Schützenberger covering. The most difficult part of our proof is to show that the Schützenberger covering indeed has the property we just indicated.
An extended abstract of this paper appeared as [ 32]. This paper differs from it in the following way. First, full proofs are included. Second, we combine some known results and ideas to obtain the decidability of the sequentiality problem for unambiguous max-plus tree automata. This result has never been stated explicitly, but follows rather easily from the main result of [ 11] and an idea from [ 29]. As this result fits the theme of our paper quite nicely, we decided to include it. Third, we show that it is decidable in PSPACE whether an unambiguous max-plus tree automaton satisfies the tree fork property. In [ 32], we only outlined the decidablity of the tree fork property. Fourth, we now give some examples to better illustrate the properties of the Schützenberger covering. Finally, we have added a section in which we investigate additional properties of the Schützenberger covering. The main motivation for this last section is to provide a deeper insight into the Schützenberger covering, but it also outlines a slightly different path we could have taken for our proof.

## 2 Preliminaries

For a set X, we denote the power set of X by $$\mathcal {P}(X)$$ and the cardinality of X by | X|. For two sets X and Y and a mapping f : XY, we call X the domain of f, denoted by dom( f), and Y the range of f, denoted by range( f). For a subset $$X^{\prime } \subseteq X$$, we call the set $$f(X^{\prime }) = \{ y \in Y \mid \exists x \in X^{\prime } \colon f(x) = y \}$$ the image or range of $$X^{\prime }$$ under f. The restriction of f to $$X^{\prime }$$, denoted by $$f {\upharpoonright }_{X^{\prime }}$$, is the mapping $$f {\upharpoonright }_{X^{\prime }} \colon X^{\prime } \to Y$$ defined by $$f {\upharpoonright }_{X^{\prime }}(x) = f(x)$$ for every $$x \in X^{\prime }$$. For an element yY, we call the set f − 1( y) = { xXf( x) = y} the preimage of y underf. For a second mapping g: XY, we write f = g if for all xX we have f( x) = g( x).
Let $$\mathbb {N} = \{0,1,2,\ldots \}$$. By $$\mathbb {N}^{*}$$ we denote the set of all finite words over $$\mathbb {N}$$. The empty word is denoted by ε, and the length of a word $$w \in \mathbb {N}^{*}$$ by | w|. The set $$\mathbb {N}^{*}$$ is partially ordered by the prefix relation ≤ p and totally ordered with respect to the lexicographic ordering ≤ l. Two words from $$\mathbb {N}^{*}$$ are called prefix-dependent if they are in prefix relation, and otherwise they are called prefix-independent.
A ranked alphabet is a pair ( Γ,rk Γ), often abbreviated by Γ, where Γ is a finite set and $$\text {rk}_{\varGamma }\colon \varGamma \to \mathbb {N}$$ a mapping which assigns a rank to every symbol. For every m ≥ 0 we define $$\varGamma ^{(m)} = \text {rk}_{\varGamma }^{-1}(m)$$ as the set of all symbols of rank m. The rank of Γ is defined as $$\text {rk}(\varGamma ) = \max \limits \{\text {rk}_{\varGamma }(a) \mid a \in \varGamma \}$$.
The set of ( finite, labeled, and ordered) Γ-trees, denoted by T Γ, is the set of all pairs t = (pos( t),label t), where $$\text {pos}(t) \subset \mathbb {N}^{*}$$ is a finite non-empty prefix-closed set of positions, label t: pos( t) → Γ is a mapping, and for every w ∈pos( t) we have wi ∈pos( t) iff 1 ≤ i ≤rk Γ(label t( w)). We write t( w) for label t( w) and | t| for |pos( t)|. We also refer to the elements of pos( t) as nodes, to ε as the root of t, and to prefix-maximal nodes as leaves. The height of t is defined as $$\text {height}(t) = \max \limits _{w \in \text {pos}(t)} |w|$$. For a leaf w ∈pos( t), the set { v ∈pos( t)∣ vp w} is called a branch of t.
Now let s, tT Γ and w ∈pos( t). The subtree of tat w, denoted by $$t{\upharpoonright }_{w}$$, is a Γ-tree defined as follows. We let $$\text {pos}(t{\upharpoonright }_{w}) = \{ v \in \mathbb {N}^{*} \mid wv \in \text {pos}(t)\}$$ and for $$v \in \text {pos}(t{\upharpoonright }_{w})$$, we let $$\text {label}_{t{\upharpoonright }_{w}}(v) = t(wv)$$.
The substitution of s into w of t, denoted by tsw〉, is a Γ-tree defined as follows. We let pos( tsw〉) = (pos( t) ∖{ v ∈pos( t)∣ wp v}) ∪{ wvv ∈pos( s)}. For v ∈pos( tsw〉), we let label tsw( v) = s( u) if v = wu for some u ∈pos( s), and otherwise label tsw( v) = t( v).
For aΓ (m) and trees t 1,…, t mT Γ, we also write a( t 1,…, t m) to denote the tree t with pos( t) = { ε}∪{ iwi ∈{1,…, m}, w ∈pos( t i)}, label t( ε) = a, and label t( iw) = t i( w). For aΓ (0), the tree a() is abbreviated by a.
For a ranked alphabet Γ, a tree over the alphabet Γ = ( Γ∪{◇},rk Γ ∪{◇↦0}) is called a Γ-context. Let $$t \in T_{\varGamma _{{\diamond }}}$$ be a Γ-context and let w 1,…, w n ∈pos( t) be a lexicographically ordered enumeration of all leaves of t labeled ◇. Then we call t an n- Γ-context and define ⋄ i( t) = w i for i ∈{1,…, n}. For an n- Γ-context t and contexts $$t_{1}, \ldots , t_{n} \in T_{\varGamma _{{\diamond }}}$$, we define t( t 1,…, t n) = tt 1 →⋄ 1( t)〉…〈 t n →⋄ n( t)〉 by substitution of t 1,…, t n into the ◇-leaves of t. A 1- Γ-context is also called a Γ-word. For a Γ-word s, we define s 0 = ◇ and s n+ 1 = s( s n) for n ≥ 0.
A commutative semiring is a tuple ( K, ⊕, ⊙, , ), abbreviated by K, with operations sum ⊕ and product ⊙ and constants and such that ( K, ⊕, ) and ( K, ⊙, ) are commutative monoids, multiplication distributes over addition, and for every κK. In this paper, we only consider the max-plus semiring $$\mathbb {R}_{\max \limits } = {}(\mathbb {R} \cup \{-\infty \},\max \limits ,+,-\infty ,0)$$ where the sum and the product operations are $$\max \limits$$ and + , respectively, extended to $$\mathbb {R} \cup \{-\infty \}$$ in the usual way.
A max-plus weighted bottom-up finite state tree automaton (short: max-plus-WTA) over Γ is a tuple $$\mathcal {A} = (Q,\varGamma ,\mu ,\nu )$$ where Q is a finite set (of states), Γ is a ranked alphabet (of input symbols), $$\mu \colon \bigcup _{m=0}^{\text {rk}(\varGamma )} Q^{m} \times \varGamma ^{(m)} \times Q \to \mathbb {R}_{max}$$ (the function of transition weights), and $$\nu \colon Q \to \mathbb {R}_{\max \limits }$$ (the function of final weights). We define $$\varDelta _{\mathcal {A}} = \text {dom}(\mu )$$. A tuple $$(\bar {p},a,q) \in \varDelta _{\mathcal {A}}$$ is called a transition and $$(\bar {p},a,q)$$ is called valid if $$\mu (\bar {p},a,q) \neq -\infty$$. A state qQ is called final if $$\nu (q) \neq -\infty$$.
For a tree tT Γ, a mapping r: pos( t) → Q is called a quasi-run of $$\mathcal {A}$$ on t. For a quasi-run r on t and a position w ∈pos( t) with t( w) = aΓ (m), the tuple
$$\begin{array}{@{}rcl@{}} \mathbbm{t}(t,r,w) = (r(w1), \ldots, r(wm), a, r(w)) \end{array}$$
is called the transition at w. The quasi-run r is called a (valid) run if for every w ∈pos( t) the transition $$\mathbbm {t}({t},{r},{w})$$ is valid with respect to $$\mathcal {A}$$. We call a run r accepting if r( ε) is final. By $$\text {Run}_{\mathcal {A}}(t)$$ and $$\text {Acc}_{\mathcal {A}}(t)$$ we denote the sets of all runs and all accepting runs of $$\mathcal {A}$$ on t, respectively. For a state qQ, we denote by $$\text {Run}_{\mathcal {A}}(t,q)$$ the set of all runs $$r \in \text {Run}_{\mathcal {A}}(t)$$ such that r( ε) = q.
For a run $$r \in \text {Run}_{\mathcal {A}}(t)$$, the weight of r is defined by
$$\begin{array}{@{}rcl@{}} \text{wt}_{\mathcal{A}}(t,r) = \sum\limits_{w \in \text{pos}(t)} \mu(\mathbbm{t}(t,r,w)). \end{array}$$
The behavior of $$\mathcal {A}$$, denoted by $${\llbracket }{\mathcal {A}}{\rrbracket }$$, is the mapping defined for every tT Γ by
$${\llbracket}{\mathcal{A}}{\rrbracket}(t) = \max_{r \in \text{Acc}_{\mathcal{A}}(t)} (\text{wt}_{\mathcal{A}}(t,r) + \nu (r(\varepsilon))),$$
where the maximum over the empty set is $$-\infty$$ by convention.
For a max-plus-WTA $$\mathcal {A} = (Q, \varGamma , \mu , \nu )$$, a run of $$\mathcal {A}$$ on a Γ-context t is a run of the max-plus-WTA $$\mathcal {A}^{\prime } = (Q, \varGamma _{{\diamond }}, \mu ^{\prime }, \nu )$$ on t, where $$\mu ^{\prime }({\diamond },q) = 0$$ for all qQ and $$\mu ^{\prime }(d) = \mu (d)$$ for all $$d \in \varDelta _{\mathcal {A}}$$. We denote $$\text {Run}_{\mathcal {A}}^{{\diamond }}(t) = \text {Run}_{\mathcal {A}^{\prime }}(t)$$ and for $$r \in \text {Run}_{\mathcal {A}}^{{\diamond }}(t)$$ write $$\text {wt}_{\mathcal {A}}^{{\diamond }}(t, r) = \text {wt}_{\mathcal {A}^{\prime }}(t, r)$$. For an n- Γ-context $$t \in T_{\varGamma _{{\diamond }}}$$ and states q 0,…, q n, we denote by $$\text {Run}_{\mathcal {A}}^{{\diamond }}(q_{1}, \ldots , q_{n}, t, q_{0})$$ the set of all runs $$r \in \text {Run}_{\mathcal {A}}^{{\diamond }}(t)$$ such that r( ε) = q 0 and r(⋄ i( t)) = q i for every i ∈{1,…, n}. For a Γ-word s, we write $$p \xrightarrow {s \mid x} q$$ if there exists a run $$r \in \text {Run}_{\mathcal {A}}^{{\diamond }}(p,s,q)$$ with $$\text {wt}_{\mathcal {A}}^{{\diamond }}(s, r) = x$$. In this case, r is said to realize $$p {{\xrightarrow {s \mid x}}} q$$. Note that $$r \in \text {Run}_{\mathcal {A}}^{{\diamond }}(s)$$ implies $$x \neq -\infty$$.
Similar to trees, we define restrictions, substitutions, and powers of runs as follows. Let t, sT Γ, $$r \in \text {Run}_{\mathcal {A}}(t)$$, w ∈pos( t), and $$r_{s} \in \text {Run}_{\mathcal {A}}(s)$$ with r s( ε) = r( w). Then we define $$r {\upharpoonright }_{w} \in \text {Run}_{\mathcal {A}}(t {\upharpoonright }_{w})$$ by $$r {\upharpoonright }_{w}(v) = r(wv)$$ for every $$v \in \text {pos}(t {\upharpoonright }_{w})$$. We define $$r \langle r_{s} \to w \rangle \in \text {Run}_{\mathcal {A}}(t \langle s \to w \rangle )$$ by rr sw〉( v) = r s( u) if v = wu for some u ∈pos( s), and rr sw〉( v) = r( v) otherwise. For a Γ-word s and a run $$r \in \text {Run}_{\mathcal {A}}^{{\diamond }}(s)$$ with r( ε) = r(⋄ 1( s)), we let v = ⋄ 1( s) and define r 0〈v = { εr( ε)} and $$r^{n+1 \langle v \rangle } = r \langle r^{n \langle v \rangle } \to v \rangle \in \text {Run}_{\mathcal {A}}^{{\diamond }}(s^{n+1})$$ for n ≥ 0.
For a max-plus-WTA $$\mathcal {A}$$, we define a relation ≤ on Q by pq iff there exists a Γ-word $$s \in T_{\varGamma _{{\diamond }}}$$ such that $$\text {Run}_{\mathcal {A}}^{{\diamond }}(q,s,p) \neq \emptyset$$. We call $$\mathcal {A}$$ trim if for every pQ there exists tT Γ, $$r \in \text {Acc}_{\mathcal {A}}(t)$$, and w ∈pos( t) with r( w) = p. The trim part of $$\mathcal {A}$$ is the automaton obtained from $$\mathcal {A}$$ by removing all states pQ for which no such t, r, and w exist. This process obviously has no influence on $${\llbracket }{\mathcal {A}}{\rrbracket }$$.
A max-plus-WTA $$\mathcal {A}$$ is called deterministic or sequential if for every m ≥ 0, aΓ (m), and $$\bar {p} \in Q^{m}$$, there exists at most one qQ with $$\mu (\bar {p},a,q) \neq -\infty$$. We call $$\mathcal {A}$$ unambiguous if $$|\text {Acc}_{\mathcal {A}}(t)| \leq 1$$ for every tT Γ. We call the behavior $${\llbracket }{\mathcal {A}}{\rrbracket }$$ of $$\mathcal {A}$$ finitely sequential if there exist finitely many deterministic max-plus-WTA $$\mathcal {A}_{1}, \ldots , \mathcal {A}_{n}$$ over Γ such that $${\llbracket }{\mathcal {A}}{\rrbracket } = \max \limits _{i = 1}^{n} {\llbracket }{\mathcal {A}_{i}}{\rrbracket }$$, where the maximum is taken pointwise.

## 3 Main Result

We will show that for an unambiguous max-plus-WTA $$\mathcal {A}$$, it is decidable whether its behavior $${\llbracket }{\mathcal {A}}{\rrbracket }$$ is finitely sequential. Moreover, if it is finitely sequential, we will obtain that the deterministic max-plus-WTA $$\mathcal {A}_{1}, \ldots , \mathcal {A}_{n}$$ can be effectively constructed. For this, we follow ideas from [ 4], where the decidability of the finite sequentiality problem was proved for unambiguous max-plus word automata.
The general outline of our proof is similar to that of [ 4] and presents itself as follows. We introduce the tree fork property and show that it is decidable whether an unambiguous max-plus-WTA $$\mathcal {A}$$ satisfies this property. Then we show that the behavior of an unambiguous max-plus-WTA is finitely sequential if and only if it does not satisfy the tree fork property. In conclusion, we obtain the decidability of the finite sequentiality problem for unambiguous max-plus-WTA.
Elementary proof methods can be used to show that $${\llbracket }{\mathcal {A}}{\rrbracket }$$ is not finitely sequential if $$\mathcal {A}$$ satisfies the tree fork property. On the other hand, if $$\mathcal {A}$$ does not satisfy the tree fork property, we show how to construct finitely many unambiguous max-plus-WTA whose pointwise maximum is $${\llbracket }{\mathcal {A}}{\rrbracket }$$, and which all satisfy the twins property [ 29]. Every unambiguous max-plus-WTA which satisfies the twins property possesses an effectively constructable deterministic equivalent [ 11]. Thus, we obtain finitely many deterministic max-plus-WTA whose pointwise maximum is $${\llbracket }{\mathcal {A}}{\rrbracket }$$, which is hence finitely sequential.
We begin by showing that the Lipschitz property of deterministic max-plus word automata [ 22, 29] also holds for deterministic max-plus tree automata. On words, this Lipschitz property can be formulated follows. Let $$\mathcal {A}$$ be a deterministic max-plus word automaton and let L be the largest weight, in terms of absolute value, occurring in $$\mathcal {A}$$ (excluding $$-\infty$$). Then for two words w 1 = uv 1 and w 2 = uv 2 which have an accepting run in $$\mathcal {A}$$, the difference between $${\llbracket }{\mathcal {A}}{\rrbracket }(w_{1})$$ and $${\llbracket }{\mathcal {A}}{\rrbracket }(w_{2})$$ can be at most | L|(| v 1| + | v 2| + 2). This is clear since the unique runs of $$\mathcal {A}$$ on w 1 and w 2 will be identical on the prefix u, and then with every remaining letter of each word the difference between both runs cannot grow more than | L|. For deterministic max-plus-WTA, we can show a similar statement as follows.
Lemma 1 (c.f. [ 22, End of Section 2.4][ 29, Section 3.2])
Let $$\mathcal {A} = (Q, \varGamma , \mu , \nu )$$ be a deterministic max-plus-WTA, let $$X = (\mu (\varDelta _{\mathcal {A}}) \cup \nu (Q)) \setminus \{-\infty \}$$, and let $$L = \max \limits _{x \in X} |x|$$. Furthermore, let t 1, t 2T Γ be two trees with $${\llbracket }{\mathcal {A}}{\rrbracket }(t_{1}) \neq -\infty$$ and $${\llbracket }{\mathcal {A}}{\rrbracket }(t_{2}) \neq -\infty$$ and let w 1pos( t 1) and w 2pos(t 2) be two positions such that $$t_{1}{\upharpoonright }_{w_{1}} = t_{2}{\upharpoonright }_{w_{2}}$$. Then with $$t = t_{1}{\upharpoonright }_{w_{1}}$$ we have
$$\begin{array}{@{}rcl@{}} |{\llbracket}{\mathcal{A}}{\rrbracket}(t_{1}) - {\llbracket}{\mathcal{A}}{\rrbracket}(t_{2})| \leq L (|t_{1}| + |t_{2}| - 2|t| + 2). \end{array}$$
Proof
Since $$\mathcal {A}$$ is deterministic, there exists exactly one run $$r_{1} \in \text {Acc}_{\mathcal {A}}(t_{1})$$ and exactly one run $$r_{2} \in \text {Acc}_{\mathcal {A}}(t_{2})$$. Likewise, there exists exactly one run $$r \in \text {Run}_{\mathcal {A}}(t)$$. Due to $$t_{1}{\upharpoonright }_{w_{1}} = t_{2}{\upharpoonright }_{w_{2}} = t$$, we thus have $$r_{1}{\upharpoonright }_{w_{1}} = r_{2}{\upharpoonright }_{w_{2}} = r$$. It follows that
$$\begin{array}{@{}rcl@{}} &&|{\llbracket}{\mathcal{A}}{\rrbracket}(t_{1}) - {\llbracket}{\mathcal{A}}{\rrbracket}(t_{2})|\\ &&= \left|{\sum}_{w \in \text{pos}(t_{1})} \mu(\mathbbm{t}(t_{1},r_{1},w)) + \nu(r_{1}(\varepsilon)) - \left( \sum\limits_{w \in \text{pos}(t_{2})} \mu(\mathbbm{t}({t_{2}},{r_{2}},{w}) ) + \nu(r_{2}(\varepsilon)) \right) \right|\\ &&= \left|\sum\limits_{~}\begin{array}{ll}w {\in} \text{pos}(t_{1})\\ \lnot (w_{1} \leq_{p} w)\end{array} \mu(\mathbbm{t}(t_{1},{r_{1}},{w})) + \nu(r_{1}(\varepsilon)) - \left( \sum\limits_{~}\begin{array}{l}w {\in} \text{pos}(t_{2})\\ \lnot (w_{2} \leq_{p} w)\end{array} \mu(\mathbbm{t}({t_{2}},{r_{2}},{w}) ) + \nu(r_{2}(\varepsilon)) \right)\right|\\ &&\leq L (|t_{1}| - |t| + 1) + L(|t_{2}| - |t| + 1)\\ &&= L (|t_{1}| + |t_{2}| - 2|t| + 2). \end{array}$$
Next, we recall the twins property. Let Γ be a ranked alphabet. We begin by introducing the concepts of siblings and twins. Intuitively, two states are called siblings if they can be “reached” by the same tree. Two siblings are called twins if for every Γ-word which can “loop” in both states, the maximal weight for the loop is the same in both states.
Definition 1
Let $$\mathcal {A} = (Q, \varGamma , \mu , \nu )$$ be a max-plus-WTA. Two states p, qQ are called siblings if there exists a tree uT Γ such that $$\text {Run}_{\mathcal {A}}(u,p) \neq \emptyset$$ and $$\text {Run}_{\mathcal {A}}(u,q) \neq \emptyset$$. We recall that $$\text {Run}_{\mathcal {A}}(u,p)$$ and $$\text {Run}_{\mathcal {A}}(u,q)$$ contain only valid runs.
Two siblings p, q are called twins if for every Γ-word s and weights
$$\begin{array}{@{}rcl@{}} x = \max_{r \in \text{Run}_{\mathcal{A}}^{{\diamond}}(p,s,p) } \text{wt}_{\mathcal{A}}^{{\diamond}}(s,r) \qquad y = \max_{r \in \text{Run}_{\mathcal{A}}^{{\diamond}}(q,s,q) } \text{wt}_{\mathcal{A}}^{{\diamond}}(s,r), \end{array}$$
we have x = y whenever $$x \neq -\infty$$ and $$y \neq -\infty$$ holds. Here, the maximum over the empty set is $$-\infty$$ by convention.
A max-plus-WTA is said to satisfy the twins property if all of its siblings are twins. For unambiguous max-plus-WTA, the twins property is a criterion for deciding the sequentiality problem. An unambiguous max-plus-WTA possesses a deterministic equivalent if and only if it satisfies the twins property. For words, this result is due to [ 29, Theorem 12], for trees, we cite the following cite the following theorem which states that the twins property is a sufficient condition for determinizability.
Theorem 1 ([ 11, Lemma 5.10])
Let $$\mathcal {A}$$ be a trim unambiguous max-plus-WTA. If $$\mathcal {A}$$ satisfies the twins property, there exists a deterministic max-plus-WTA $$\mathcal {A}^{\prime }$$ with $${\llbracket }{\mathcal {A}}{\rrbracket } = {\llbracket }{\mathcal {A}^{\prime }}{\rrbracket }$$ which can be effectively constructed.
The converse, namely that the twins property is also a necessary condition for determinizability, follows from the Lipschitz property of deterministic max-plus automata. For max-plus word automata, consider the following. If an unambiguous max-plus word automaton $$\mathcal {A}$$ does not satisfy the twins property, we can find states p and q which are siblings and not twins. We assume that our witnesses for this are u and s as above. Then we consider words of the form w 1 = us N v p and w 2 = us N v q, where v p and v q are two fixed words which lead from p and q, respectively, to some final state. For every fixed $$L \in \mathbb {R}$$, we can choose N sufficiently large to ensure that $$|{\llbracket }{\mathcal {A}}{\rrbracket }(w_{1}) - {\llbracket }{\mathcal {A}}{\rrbracket }(w_{2})| > |L|(|v_{p}| + |v_{q}| + 2)$$. Due to the Lipschitz property of deterministic max-plus automata, it is thus not possible to determinize $$\mathcal {A}$$ if it does not satisfy the twins property. For trees, we can proceed in the same way.
Lemma 2
Let $$\mathcal {A}$$ be a trim unambiguous max-plus-WTA. If there exists a deterministic max-plus-WTA $$\mathcal {A}^{\prime }$$ with $${\llbracket }{\mathcal {A}}{\rrbracket } = {\llbracket }{\mathcal {A}^{\prime }}{\rrbracket }$$, then $$\mathcal {A}$$ satisfies the twins property.
Proof
We follow the idea for the proof of [ 29, Theorem 9]. Let $$\mathcal {A} = (Q, \varGamma , \mu , \nu )$$ be a trim unambiguous max-plus-WTA and let p, qQ be siblings, i.e., there exists a tree uT Γ and runs $$r^{p} \in \text {Run}_{\mathcal {A}}(u,p)$$ and $$r^{q} \in \text {Run}_{\mathcal {A}}(u,q)$$. Let $$s \in T_{\varGamma _{{\diamond }}}$$ be a Γ-word such that $$p {{\xrightarrow {s \mid x}}} p$$ and $$q {{\xrightarrow {s \mid y}}} q$$ for weights $$x,y \in \mathbb {R}$$. Since $$\mathcal {A}$$ is trim, there exist Γ-words $$\hat {u}_{p}, \hat {u}_{q} \in T_{\varGamma _{{\diamond }}}$$ such that $$p {{\xrightarrow {\hat {u}_{p} \mid z_{p}}}} p^{\prime }$$ and $$q {{\xrightarrow {{\hat {u}_{q} \mid z_{q}}}}} q^{\prime }$$ for two final states $$p^{\prime },q^{\prime } \in Q$$ and weights $$z_{p},z_{q} \in \mathbb {R}$$. We let $$\kappa _{p} = \text {wt}_{\mathcal {A}}(u,r^{p}) + z_{p} + \nu (p^{\prime })$$ and $$\kappa _{q} = \text {wt}_{\mathcal {A}}(u,r^{q}) + z_{q} + \nu (q^{\prime })$$ and for n ≥ 1 define the trees $$t_{p}^{(n)} = \hat {u}_{p}(s^{n} (u) )$$ and $$t_{q}^{(n)} = \hat {u}_{q}(s^{n} (u) )$$. Due to the unambiguity of $$\mathcal {A}$$, we see that for every n ≥ 1 we have
$$\begin{array}{@{}rcl@{}} {\llbracket}{\mathcal{A}}{\rrbracket}(t_{p}^{(n)}) &= \kappa_{p} + nx\\ {\llbracket}{\mathcal{A}}{\rrbracket}(t_{q}^{(n)}) &= \kappa_{q} + ny. \end{array}$$
Assume that there exists a deterministic max-plus-WTA $$\mathcal {A}^{\prime }$$ with $${\llbracket }{\mathcal {A}}{\rrbracket } = {\llbracket }{\mathcal {A}^{\prime }}{\rrbracket }$$. Then by Lemma 1, there exists $$L \in \mathbb {R}$$ such that for all n ≥ 1 we have
$$\begin{array}{@{}rcl@{}} | {\llbracket}{\mathcal{A}}{\rrbracket}(t_{p}^{(n)}) - {\llbracket}{\mathcal{A}}{\rrbracket}(t_{q}^{(n)}) | \leq |L| (|\hat{u}_{p}| + |\hat{u}_{q}| + 2). \end{array}$$
From the equations above we thus obtain that for every n ≥ 1 we have
$$\begin{array}{@{}rcl@{}} |\kappa_{p} - \kappa_{q} + n(x - y)| \leq |L| (|\hat{u}_{p}| + |\hat{u}_{q}| + 2). \end{array}$$
This can only hold if x = y. It follows that $$\mathcal {A}$$ satisfies the twins property. □
The twins property is decidable for both max-plus word automata [ 2, 5, 20, 29, 30] and max-plus tree automata [ 10, Section 3]. Thus, by combining Lemma 2 with the results from [ 11] (see Theorem 1) and [ 10], we obtain the decidability of the sequentiality problem for unambiguous max-plus tree automata.
Theorem 2
For an unambiguous max-plus-WTA $$\mathcal {A}$$ it is decidable whether there exists a deterministic max-plus-WTA $$\mathcal {A}^{\prime }$$ with $${\llbracket }{\mathcal {A}}{\rrbracket } = {\llbracket }{\mathcal {A}^{\prime }}{\rrbracket }$$. If such an automaton $$\mathcal {A}^{\prime }$$ exists, it can be effectively constructed.
Deciding whether a max-plus word automaton satisfies the twins property is PSPACE-complete [ 20]. For max-plus tree automata, the problem is thus PSPACE-hard, but no upper complexity bound is stated in [ 10]. Note that in general, it is undecidable whether two given siblings are twins [ 20], but for so-called cycle-unambiguous max-plus automata, it was shown to be decidable on both words [ 2, Section 4] and trees [ 11, Section 5.4]. A max-plus tree automaton $$\mathcal {A} = (Q, \varGamma ,$$ μ, ν) is called cycle-unambiguous if for every Γ-word $$s \in T_{\varGamma _{{\diamond }}}$$ and every state qQ, there is at most one run which loops s in q, i.e., the set $$\text {Run}_{\mathcal {A}}^{{\diamond }}(q,s,q)$$ is either a singleton or empty. It is easy to see that every trim unambiguous max-plus tree automaton is cycle-unambiguous. Thus, for every two states of an unambiguous max-plus tree automaton, it is decidable whether they are twins. As we will employ the reasoning from [ 11] in more detail, we provide a short direct proof.
Lemma 3 ([ 11, Section 5.4])
Let $$\mathcal {A} = (Q, \varGamma , \mu , \nu )$$ be a cycle-unambiguous max-plus-WTA. Two states p, qQ are siblings if and only if there exists a tree uT Γ of height at most |Q| 2 such that $$\text {Run}_{\mathcal {A}}(u,p) \neq \emptyset$$ and $$\text {Run}_{\mathcal {A}}(u,q) \neq \emptyset$$. Two siblings p, qQ are not twins if and only if there exists a Γ- word s of height at most 4|Q| 2 such that $$p {{\xrightarrow {s \mid x}}} p$$ and $$q {{\xrightarrow {s \mid y}}} q$$ with xy.
Proof
Let p, qQ be two states. First, to check whether p and q are siblings, we see as follows that it suffices to check whether they can both be reached by a tree u of height at most | Q| 2. Assume we have a tree uT Γ and two runs $$r^{p} \in \text {Run}_{\mathcal {A}}(t,p)$$ and $$r^{q} \in \text {Run}_{\mathcal {A}}(t,q)$$. If height( u) > | Q| 2, then by pigeon hole principle, we can find a simultaneous loop in r p and r q; that is, we can find two positions w 1 < p w 2 in u with r p( w 1) = r p( w 2) and also r q( w 1) = r q( w 2). By removing everything between w 1 and w 2 from u, we obtain the smaller tree $$u \langle u{\upharpoonright }_{w_{2}} \to w_{1} \rangle$$ which still reaches p and q.
If p and q are siblings, we see as follows that we only need to check Γ-words s of height at most 4| Q| 2 to decide whether p and q are twins. Assume p and q are not twins and our witness for this is the Γ-word s with height( s) > 4| Q| 2. Let $$r_{p} \in \text {Run}_{\mathcal {A}}^{{\diamond }}(p,s,p)$$ be the run on s which loops in p with weight $$x = \text {wt}_{\mathcal {A}}^{{\diamond }}(s,r_{p})$$ and let $$r_{q} \in \text {Run}_{\mathcal {A}}^{{\diamond }}(q,s,q)$$ be the run on s which loops in q with weight $$y = \text {wt}_{\mathcal {A}}^{{\diamond }}(s,r_{q})$$. Furthermore, let w ∈pos( s) with | w| = height( s) and let $$w^{\prime } \in \text {pos}(s)$$ be the longest common prefix of w and ⋄ 1( s). Then either $$|w^{\prime }| > 2|Q|^{2}$$ or $$|w| - |w^{\prime }| > 2|Q|^{2}$$, or both. In the first case, there exist two disjoint simultaneous loops in r p and r q above ⋄ 1( s). More precisely, by pigeon hole principle we can find positions w 1 < p w 2p w 3 < p w 4 with $$w_{4} \leq _{p} w^{\prime } \leq _{p} {\Diamond }_1(s)$$ in s for which ( r p( w 1), r q( w 1)) = ( r p( w 2), r q( w 2)) and ( r p( w 3), r q( w 3)) = ( r p( w 4), r q( w 4)). In the second case, there exist two disjoint simultaneous loops in r p and r q which are prefix-independent from ⋄ 1( s). That is, there exist positions w 1 < p w 2p w 3 < p w 4 with $$w^{\prime } <_{p} w_{1}$$ and w 4p w in s for which ( r p( w 1), r q( w 1)) = ( r p( w 2), r q( w 2)) and ( r p( w 3), r q( w 3)) = ( r p( w 4), r q( w 4)).
Let x 12 and x 34 be the weights of the loops in the run r p, and let y 12 and y 34 be the weights of the loops in the run r q. We obtain a smaller Γ-word $$s^{\prime }$$ and runs $$r_{p}^{\prime }$$ and $$r_{q}^{\prime }$$ of distinct weights which loop in p and q, respectively, by removing either one of the two loops or both loops as follows. If xx 12yy 12, we remove the w 1- w 2 loop. Otherwise, if xx 34yy 34, we remove the w 3- w 4 loop. If we have both xx 12 = yy 12 and xx 34 = yy 34, we obtain that 2 xx 12x 34 = 2 yy 12y 34. From xy, it follows that xx 12x 34yy 12y 34, so we remove both loops. From the cycle-unambiguity of $$\mathcal {A}$$, we see that these two runs are the only runs on the smaller Γ-word, so we have found a smaller witness. □
There exist unambiguous max-plus automata which cannot be determinized, but whose behavior is finitely sequential [ 22, Section 3.1], see also Fig.  1. Thus, for the finite sequentiality problem we inevitably have to deal with unambiguous automata in which not all siblings are twins. In the following, we will call two such states rivals. For cycle-unambiguous automata, thus in particular for unambiguous automata, the following definition is equivalent to being siblings and not twins.
Definition 2
Let $$\mathcal {A} = (Q, \varGamma , \mu , \nu )$$ be a max-plus-WTA. Two states p, qQ are called rivals if there exists a tree uT Γ such that $$\text {Run}_{\mathcal {A}}(u,p) \neq \emptyset$$ and $$\text {Run}_{\mathcal {A}}(u,q) \neq \emptyset$$ and a Γ-word s such that $$p {{\xrightarrow {s \mid x}}} p$$ and $$q {{\xrightarrow {s \mid y}}} q$$ with xy. In this case, u and s are also said to be witnesses for the fact that p and q are rivals.
If $$\mathcal {A}$$ is cycle-unambiguous, p and q are rivals if and only if they are siblings and not twins as we do not have to consider a maximum over runs. Also note that by our definition of $$\text {Run}_{\mathcal {A}}^{{\diamond }}(s)$$, we have $$x \neq -\infty$$ and $$y \neq -\infty$$ above.
We now turn to the tree fork property which, as we will show, is satisfied by an unambiguous max-plus-WTA if and only if its behavior is not finitely sequential. The property consists of two separate conditions. The first condition intuitively states that there exist two rivals p and q and a Γ-word t which can loop in p, and which can also lead from p to q. The second condition states that there exist two rivals which can occur at prefix-independent positions.
Definition 3
Let $$\mathcal {A} = (Q, \varGamma , \mu , \nu )$$ be a max-plus-WTA. We say that $$\mathcal {A}$$ satisfies the tree fork property if at least one of the following two conditions is satisfied.
(i)
There exist rivals p, qQ and a Γ-word t with $$p {{\xrightarrow {t \mid z_{p}}}} p$$ and $$p {{\xrightarrow {t \mid z_{q}}}} q$$ for some weights $$z_{p},z_{q} \in \mathbb {R}$$. In this case, t is also called a p- q-fork.

(ii)
There exist rivals p, qQ, a 2- Γ-context $$t \in T_{\varGamma _{{\diamond }}}$$, and a run $$r \in \text {Run}^{{\diamond }}_{\mathcal {A}}(t)$$ with r(⋄ 1( t)) = p and r(⋄ 2( t)) = q.

The tree fork property can be regarded as an extension of the fork property which was introduced in [ 4] and which for max-plus word automata plays the same role as the tree fork property does for max-plus tree automata. Condition (i) is essentially a tree version of the fork property. Casually put, if we take only condition (i) and replace “ Γ-word” by “word”, we obtain the fork property. The automaton depicted in Fig.  2 is unambiguous and satisfies the fork property. Condition (ii) is new and possesses no counterpart in the fork property.
We have the following theorem which relates the tree fork property to the finite sequentiality problem.
Theorem 3
Let $$\mathcal {A} = (Q, \varGamma , \mu , \nu )$$ be a trim unambiguous max-plus-WTA over Γ. Then there exist deterministic max-plus-WTA $$\mathcal {A}_{1}, \ldots , \mathcal {A}_{n}$$ over Γ with $${\llbracket }{\mathcal {A}}{\rrbracket } = \max \limits _{i = 1}^{n} {\llbracket }{\mathcal {A}_{i}}{\rrbracket }$$ if and only if $$\mathcal {A}$$ does not satisfy the tree fork property. If such automata $$\mathcal {A}_{1},\ldots ,\mathcal {A}_{n}$$ exist, they can be effectively constructed. Furthermore, there is a PSPACE-algorithm to decide whether $$\mathcal {A}$$ satisfies the tree fork property. In particular, the finite sequentiality problem is decidable for unambiguous max-plus-WTA.
Proof
Here, we only show that it is decidable whether $$\mathcal {A}$$ satisfies the tree fork property. The existence of a PSPACE-algorithm for deciding the tree fork property is deferred to Lemma 4. The rest of the proof is deferred to Sections  3.1 and  3.2, where we show that the behavior of $$\mathcal {A}$$ is finitely sequential if and only if $$\mathcal {A}$$ does not satisfy the tree fork property.
To decide whether $$\mathcal {A}$$ satisfies condition (i), we first show that if there exists a p- q-fork t for two rivals p and q, then there exists a p- q-fork $$t^{\prime }$$ of height at most 2| Q| 2. The argumentation for this is similar to the proof of Lemma 3 that the property of being siblings is decidable. Assume that t is a p- q-fork with height( t) > 2| Q| 2 and that r p and r q are runs that realize $$p {{\xrightarrow {t \mid z_{p}}}} p$$ and $$p {{\xrightarrow {t \mid z_{q}}}} q$$ for some weights $$z_{p},z_{q} \in \mathbb {R}$$. We let w ∈pos( t) be a position with | w| = height( t) and let $$w^{\prime }$$ be the longest common prefix of w and ⋄ 1( t). Then either $$|w^{\prime }| > |Q|^{2}$$ or $$|w| - |w^{\prime }| > |Q|^{2}$$, or both. In the first case, there exist by pigeon hole principle two positions w 1 < p w 2 in t with $$w_{2} \leq _{p} w^{\prime } \leq _{p} {\Diamond }_1(t)$$ and ( r p( w 1), r q( w 1)) = ( r p( w 2), r q( w 2)). In the second case, there exist two positions w 1 < p w 2 in t with $$w^{\prime } <_{p} w_{1}$$ and ( r p( w 1), r q( w 1)) = ( r p( w 2), r q( w 2)). By removing the part of t between w 1 and w 2, we obtain that $$t^{\prime } = t \langle t{\upharpoonright }_{w_{2}} \to w_{1} \rangle$$ is a p- q-fork as well. Iterating this process, we obtain a p- q-fork of height at most 2| Q| 2.
Next, we identify all pairs of rivals, which is possible since by Lemma 3, we can decide for every pair of states whether they are siblings and not twins. Then, for every pair of rivals p, q and all Γ-words t of height at most 2| Q| 2, we check whether t is a p- q-fork. If this yields no p- q-fork, $$\mathcal {A}$$ does not satisfy condition (i).
In order to decide whether $$\mathcal {A}$$ satisfies condition (ii), we first compute the relation ≤ on Q. This is possible since Q is a finite set and ≤ is the smallest transitive and reflexive relation satisfying $$\mu (q_{1}, \ldots , q_{m}, a, q_{0}) \neq -\infty \to q_{0} \leq q_{i}$$ for all transitions $$(q_{1}, \ldots , q_{m}, a, q_{0}) \in \varDelta _{\mathcal {A}}$$ and i ∈{1,…, m}. Then, by the trimness of $$\mathcal {A}$$, condition (ii) is satisfied if and only if there exist two rivals p and q, a transition $$(q_{1}, \ldots , q_{m}, a, q_{0}) \in \varDelta _{\mathcal {A}}$$ with $$\mu (q_{1}, \ldots , q_{m}, a, q_{0}) \neq -\infty$$, and indices i, j ∈{1,…, m} with ij, q ip, and q jq. □
Let $$\mathcal {A} = (Q, \varGamma , \mu , \nu )$$ be a cycle-unambiguous max-plus-WTA. In the following lemma, we present a nondeterministic PSPACE-algorithm which admits a successful run if and only if $$\mathcal {A}$$ satisfies the tree fork property. By Savitch’s determinization theorem, deciding the tree fork property is thus in PSPACE. We do not make any statement about the hardness of the problem. We define the size $$|\mathcal {A}|$$ of $$\mathcal {A}$$ as the size of its representation, i.e.,
$$\begin{array}{@{}rcl@{}} |\mathcal{A}| = |Q| + \sum\limits_{~}\begin{array}{l}(q_{1}, \ldots, q_{m}, a, q_{0}) {\in} \varDelta_{\mathcal{A}}\\\mu(q_{1}, \ldots, q_{m}, a, q_{0}) {\neq} -\infty\end{array} (m +2),\end{array}$$
where we assume that weights can be stored in constant space. Then we have the following lemma.
Lemma 4
The problem of deciding whether a cycle-unambiguous max-plus-WTA satisfies the tree fork property is in PSPACE.
Proof
Let $$\mathcal {A} = (Q, \varGamma , \mu , \nu )$$ be a cycle-unambiguous max-plus-WTA and let $$\varDelta = \{ d \in \varDelta _{\mathcal {A}} \mid \mu (d) \neq -\infty \}$$ be the set of all valid transitions of $$\mathcal {A}$$.
For the algorithm, we nondeterministically guess two states p, q and deterministically verify whether they are rivals and satisfy either condition (i) or condition (ii) of the tree fork property. If they are rivals and satisfy at least one of the conditions, the algorithm terminates successfully, otherwise it does not. Thus, the algorithm admits a successful run if and only if $$\mathcal {A}$$ satisfies the tree fork property.
Enumerating All Pairs of Siblings We enumerate all siblings of $$\mathcal {A}$$ using the following reachability algorithm. We initialize the set of all pairs $$S \subseteq Q \times Q$$ which are siblings with S = . Then we iterate the following operation.
Let $$S^{\prime } = S$$. For every two transitions ( p 1,…, p m, a, p 0),( q 1,…, q m, a, q 0) ∈ Δ, add ( p 0, q 0) to $$S^{\prime }$$ if $$\{ (p_{1},q_{1}), \ldots , (p_{m},q_{m})\} \subseteq S$$. If $$S^{\prime } = S$$, store S as the set of all siblings and terminate. If $$S \subsetneq S^{\prime }$$, let $$S = S^{\prime }$$ and continue the iteration. This iteration terminates after at most | Q × Q| = | Q| 2 steps and therefore runs in polynomial time. In particular, this part of the algorithm is in PSPACE and the output S can be stored in polynomial space.
Test for Siblings If ( p, q) ∈ S, then p and q are siblings and the algorithm continues, otherwise it is not successful.
Deciding Condition (i) We initialize the set of all pairs of states reachable from ( p, p) by R = {( p, p)}. Then we iterate the following operation.
Let $$R^{\prime } = R$$. For every two transitions ( p 1,…, p m, a, p 0),( q 1,…, q m, a, q 0) ∈ Δ, add ( p 0, q 0) to $$R^{\prime }$$ if $$\{ (p_{1},q_{1}), \ldots , (p_{m},q_{m})\} \subseteq S$$ and R ∩{( p 1, q 1),…,( p m, q m)}≠ . If $$(p,q) \in R^{\prime }$$, there exists a p- q-fork and the algorithm continues to “Test for rivals”. If $$(p,q) \notin R^{\prime }$$ and $$R \subsetneq R^{\prime }$$, the algorithm sets $$R = R^{\prime }$$ and continues the iteration in search for a p- q-fork. If $$(p,q) \notin R^{\prime }$$ and $$R = R^{\prime }$$, the search for a p- q-fork failed and the algorithm continues to “Deciding condition (ii)”. This iteration also terminates after at most | Q| 2 steps and is thus in PSPACE.
Deciding Condition (ii) We initialize set of states reachable from p by R p = { p}. Then we iterate the following operation.
Let $$R_{p}^{\prime } = R_{p}$$. For every transition ( p 1,…, p m, a, p 0) ∈ Δ, add p 0 to $$R_{p}^{\prime }$$ if R p ∩{ p 1,…, p m}≠ . If $$R_{p}^{\prime } = R_{p}$$, store R p as the set of all states reachable from p. If $$R_{p} \subsetneq R_{p}^{\prime }$$, let $$R_{p} = R_{p}^{\prime }$$ and continue the iteration.
In the same fashion, we compute the set R q of all states reachable from q. This part of the algorithm runs in polynomial time and the sets R p and R q can thus be stored in polynomial space.
Next, we verify for every transition ( p 1,…, p m, a, p 0) ∈ Δ whether there exist indices i, j with 1 ≤ i < jm such that p iR p and p jR q. If such a transition is found, condition (ii) is satisfied and the algorithm continues to “Test for rivals”. Otherwise, p and q satisfy neither condition (i) nor condition (ii) of the tree fork property and the algorithm is not successful.
Test for Rivals Finally, we verify that there exists a Γ-word s such that $$p {{\xrightarrow {s \mid x}}} p$$ and $$q {{\xrightarrow {s \mid y}}} q$$ with xy. By Lemma 3, it suffices to consider Γ-words of height at most 4| Q| 2. As even with this size restriction, we can not necessarily store such a Γ-word s in polynomial space, we guess s dynamically and verify that it satisfies $$p {{\xrightarrow {s \mid x}}} p$$ and $$q {{\xrightarrow {s \mid y}}} q$$ with xy.
More precisely, we guess the positions of s and their labels in lexicographic order. Whenever we have guessed all subtrees below a node w ∈pos( s), we compute two tuples of weights for this node, one each for p and q. The tuple for p is defined as follows. If $$s {\upharpoonright }_{w}$$ contains a leaf ◇, the tuple contains for each state p 0Q an entry with the weight of the unique run from $$\text {Run}_{\mathcal {A}}^{{\diamond }}(p,s {\upharpoonright }_{w},p_{0})$$. If s does not contain a leaf ◇, the tuple contains for each state p 0Q an entry with the weight of the unique run from $$\text {Run}_{\mathcal {A}}^{{\diamond }}(s {\upharpoonright }_{w},p_{0})$$. The tuple for q is defined similarly. After this computation, the subtrees below w and all data stored about them is discarded.
This procedure allows us to compute the weights of the unique runs from $$\text {Run}_{\mathcal {A}}^{{\diamond }}(p,s,p)$$ and $$\text {Run}_{\mathcal {A}}^{{\diamond }}(q,s,q)$$ without fully storing the runs in memory. Since s is bounded in height by 4| Q| 2 and the rank of our symbols is bounded by rk( Γ), at every point in time we have to store information for at most rk( Γ) ⋅ 4| Q| 2 + 1 positions of s, where the “ $$\mathop {+} 1$$” stems from the root. For each of these positions, we store the position itself, which is of length at most 4| Q| 2, the label of this position, and two tuples of weights, each of length | Q|. Thus, guessing s and computing the weights x and y above can be realized in polynomial space.
In the following, we present a more detailed version of the algorithm we just described. We fix an enumeration Q = { q 1,…, q n} of Q. First, we initialize a single bit b with 0 in which we store whether we have already guessed a context symbol ◇ for s. Then we set w = ε as the next position to process and execute the following algorithm.
Part 1.
Guess label for w

If | w| < 4| Q| 2 and b = 0, guess a letter aΓ∪{◇}.
If | w| < 4| Q| 2 and b = 1, guess a letter aΓ.
If | w| = 4| Q| 2 and b = 0, guess a letter aΓ (0) ∪{◇}.
If | w| = 4| Q| 2 and b = 1, guess a letter aΓ (0).
Store the pair ( w, a).
If a = ◇, set b to 1.
If aΓ (0) ∪{◇}, continue to “Part 2”.
If rk Γ( a) > 0, set w = w1 as the next position to process and continue to “Part 1”.
Part 2.
Combine weights for w

Let a be the label we guessed for w, i.e., the letter a for which we have stored the pair ( w, a) in our memory. Let $$m = \text {rk}_{\varGamma _{{\diamond }}}(a)$$ be the rank of a. By assumption, we have already processed all subtrees below w and thus, for each i ∈{1,…, m} we have tuples $$\bar {x}^{(i)}, \bar {y}^{(i)} \in \mathbb {R}^{n}max$$ for wi. If a = ◇, then for each j ∈{1,…, n}, let x j = 0 if q j = p and $$x_{j} = -\infty$$ otherwise, and let y j = 0 if q j = q and $$y_{j} = -\infty$$ otherwise. If a≠◇, compute for every j ∈{1,…, n} the weights
$$\begin{array}{@{}rcl@{}} x_{i} &=& \max_{1 \leq j_{1}, \ldots, j_{m} \leq |Q|} (\mu(q_{j_{1}}, \ldots, q_{j_{m}},a,q_{i}) + x^{(1)}_{j_{1}} + {\ldots} + x^{(m)}_{j_{m}} )\\ y_{i} &=& \max_{1 \leq j_{1}, \ldots, j_{m} \leq |Q|} (\mu(q_{j_{1}}, \ldots, q_{j_{m}},a,q_{i}) + y^{(1)}_{j_{1}} + {\ldots} + y^{(m)}_{j_{m}} ). \end{array}$$
Store the tuples $$\bar {x} = (x_{1}, \ldots , x_{n})$$ and $$\bar {y} = (y_{1}, \ldots , y_{n})$$ for w and discard the tuples $$\bar {x}^{(i)}, \bar {y}^{(i)}$$ for all positions w1,…, wm and discard all tuples of the form $$(wi, a^{\prime })$$. Then choose the next position to process as follows. If w = ε, continue to “Part 3”. Otherwise, we can write w = vi with $$i \in \mathbb {N}$$. Let $$a^{\prime }$$ be the label we guessed for v. If $$i = \text {rk}_{\varGamma }(a^{\prime })$$, redefine w = v as the next position to process and continue to “Part 2”. If $$i < \text {rk}_{\varGamma }(a^{\prime })$$, redefine w = v( i + 1) as the next position to process and continue to “Part 1”.
Part 3.
By assumption, we have computed tuples of weights $$\bar {x}, \bar {y} \in \mathbb {R}^{n}max$$ for ε. Let i, j be the indices such that p = q i and q = q j. If b = 1 and x iy j, the algorithm terminates successfully. Otherwise, the algorithm is not successful.

The following two sections are dedicated to completing the proof of Theorem 3.

### 3.1 Necessity

In this section, we show that if an unambiguous max-plus-WTA $$\mathcal {A}$$ satisfies either condition (i) or condition (ii) of the tree fork property, then $${\llbracket }{\mathcal {A}}{\rrbracket }$$ is not finitely sequential. For condition (i), we adapt the corresponding proof from the word case [ 4, Theorem 2]. The proof relies on the Lipschitz property of deterministic max-plus automata and its approach is similar to the proof of Lemma 2 that the twins property is a necessary condition for determinizability.
Theorem 4
Let $$\mathcal {A}$$ be a trim unambiguous max-plus-WTA over Γ. If $$\mathcal {A}$$ satisfies condition (i) of the tree fork property, then there do not exist deterministic max-plus-WTA $$\mathcal {A}_{1}, \ldots , \mathcal {A}_{n}$$ over Γ with $${\llbracket }{\mathcal {A}}{\rrbracket } = \max \limits _{i = 1}^{n} {\llbracket }{\mathcal {A}_{i}}{\rrbracket }$$.
Proof
For contradiction, assume that $$\mathcal {A}$$ satisfies condition (i) of the tree fork property and that there exist deterministic max-plus-WTA $$\mathcal {A}_{1}, \ldots , \mathcal {A}_{n}$$ over Γ with $${\llbracket }{\mathcal {A}}{\rrbracket } = \max \limits _{i = 1}^{n} {\llbracket }{\mathcal {A}_{i}}{\rrbracket }$$. We write $$\mathcal {A}_{i} = (Q_{i}, \varGamma , \mu _{i}, \nu _{i})$$ and let $$N = \max \limits _{i = 1}^{n} |Q_{i}|$$. Let p, q, t, z p, z q be as in condition (i) of the tree fork property and for the rivals p and q, let u, s, x, y be as in the definition of rivals. We let $$r^{p} \in \text {Run}_{\mathcal {A}}(u,p)$$ and define $$z_{u} = \text {wt}_{\mathcal {A}}(u, r^{p})$$. Furthermore, by trimness there exists a Γ-word $$\hat {u}$$ with $$q {{\xrightarrow { \hat {u} \mid z_{\hat {u}}}}} q_{f}$$ for some weight $$z_{\hat {u}} \in \mathbb {R}$$ and some state q fQ with $$\nu (q_{f}) \neq -\infty$$.
We define the constant $$L \in \mathbb {R}$$ to be the largest weight, in terms of absolute value, which occurs in the automata $$\mathcal {A}_{1}, \ldots , \mathcal {A}_{n}$$ as follows. We let $$X = \bigcup _{i = 1}^{n} \mu _{i}(\varDelta _{\mathcal {A}_{i}}) \cup \nu _{i}(Q_{i})$$ and define $$L = \max \limits _{x \in X \setminus \{-\infty \}} |x|$$. Furthermore, we define natural numbers N 0,…, N n inductively as follows. We let N n = 0 and if N l+ 1,…, N n are defined, then we define N l such that for all k ∈{ l + 1,…, n} we have
$$\begin{array}{@{}rcl@{}} N_{l} |x - y| &>{} & L \left( (k-l) |t| + \left( \sum\limits_{i = l + 1}^{k} N_{i}|s|\right) + 2|\hat{u}| + 2 \right) \\&& + (k - l)|z_{p}| + \left( \sum\limits_{i = l + 1}^{k-1} N_{i}|x|\right) + N_{k}|y|. \end{array}$$
We define trees $$t_{0}^{\prime }, \ldots , t_{n}^{\prime }$$ inductively by $$t_{0}^{\prime } = s^{N_{0}}(t(u))$$ and $$t_{k + 1}^{\prime } = s^{N_{k + 1}}(t(t_{k}^{\prime }))$$; for clarity, in the word case we would have $$t_{k}^{\prime } = uts^{N_{0}}ts^{N_{1}} {\cdots } ts^{N_{k}}$$. Then for k ∈{1,…, n}, we let $$t_{k} = \hat {u}(t_{k}^{\prime })$$. Due to the unambiguity of $$\mathcal {A}$$, we see that for every k ∈{1,…, n} we have
$$\begin{array}{@{}rcl@{}} {\llbracket}{\mathcal{A}}{\rrbracket}(t_{k}) = z_{u} + k z_{p} + \left( \sum\limits_{i = 0}^{k - 1} N_{i} x\right) + z_{q} + N_{k} y + z_{\hat{u}} + \nu(q_{f}). \end{array}$$
Thus, for k > l, we have
$$\begin{array}{@{}rcl@{}} | {\llbracket}{\mathcal{A}}{\rrbracket}(t_{k}) - {\llbracket}{\mathcal{A}}{\rrbracket}(t_{l}) | &=& |N_{l}(x - y) + (k - l) z_{p} + \left( \sum\limits_{i = l + 1}^{k - 1} N_{i} x\right) + N_{k} y |\\ &\geq& N_{l} |x - y| - (k-l) |z_{p}| - \left( \sum\limits_{i = l + 1}^{k - 1} N_{i} |x|\right) - N_{k} |y|\\ & >& L \left( (k-l) |t| + \left( \sum\limits_{i = l + 1}^{k} N_{i}|s|\right) + 2|\hat{u}| + 2 \right). \end{array}$$
Note that the first inequality is an application of the reverse triangle inequality. The second inequality follows from the definition of N l. Now let j ∈{1,…, n}, then by choice of L and because $$\mathcal {A}_{j}$$ is deterministic, we have by Lemma 1 that
$$\begin{array}{@{}rcl@{}} | {\llbracket}{\mathcal{A}_{j}}{\rrbracket} (t_{k}) - {\llbracket}{\mathcal{A}_{j}}{\rrbracket} (t_{l}) | \leq L \left( (k-l) |t| + \left( \sum\limits_{i = l + 1}^{k} N_{i}|s|\right) + 2|\hat{u}| + 2 \right). \end{array}$$
In conclusion, we have n + 1 trees t i, and n automata $$\mathcal {A}_{i}$$, so by pigeonhole principle and the assumption that $${\llbracket }{\mathcal {A}}{\rrbracket } = \max \limits _{i = 1}^{n} {\llbracket }{\mathcal {A}_{i}}{\rrbracket }$$, there must be j ∈{1,…, n} and k, l ∈{0,…, n} with k > l such that $${\llbracket }{\mathcal {A}}{\rrbracket }(t_{k}) = {\llbracket }{\mathcal {A}_{j}}{\rrbracket } (t_{k})$$ and $${\llbracket }{\mathcal {A}}{\rrbracket }(t_{l}) = {\llbracket }{\mathcal {A}_{j}}{\rrbracket } (t_{l})$$. However, we have $$| {\llbracket }{\mathcal {A}}{\rrbracket }(t_{k}) - {\llbracket }{\mathcal {A}}{\rrbracket }(t_{l}) | > | {\llbracket }{\mathcal {A}_{j}}{\rrbracket } (t_{k}) - {\llbracket }{\mathcal {A}_{j}}{\rrbracket } (t_{l}) |$$, which is a contradiction. □
Next, we address condition (ii) of the tree fork property. On words, states cannot occur in prefix-independent positions. Thus, this condition is new for the tree case. Intuitively, the reason that the behavior of an unambiguous max-plus-WTA $$\mathcal {A}$$ cannot be finitely sequential if it satisfies condition (ii) is as follows. Assume we have a 2- Γ-context t and two rivals p and q as in condition (ii) and let u and s be as in the definition of rivals. Then we can construct trees of the form t( s n( u), s n( u)) such that, by increasing n, the difference between the weights on the two subtrees s n( u) is arbitrarily large. However, every deterministic automaton necessarily assigns the same weight to both subtrees.
Theorem 5
Let $$\mathcal {A}$$ be a trim unambiguous max-plus-WTA over Γ. If $$\mathcal {A}$$ satisfies condition (ii) of the tree fork property, then there do not exist deterministic max-plus-WTA $$\mathcal {A}_{1}, \ldots , \mathcal {A}_{n}$$ over Γ with $${\llbracket }{\mathcal {A}}{\rrbracket } = \max \limits _{i = 1}^{n} {\llbracket }{\mathcal {A}_{i}}{\rrbracket }$$.
Proof
For contradiction, we assume that $$\mathcal {A}$$ satisfies condition (ii) of the tree fork property and that there exist deterministic max-plus-WTA $$\mathcal {A}_{1}, \ldots , \mathcal {A}_{n}$$ over Γ with $${\llbracket }{\mathcal {A}}{\rrbracket } = \max \limits _{i = 1}^{n} {\llbracket }{\mathcal {A}_{i}}{\rrbracket }$$. First, we construct a tree of the above mentioned form t( s n( u), s n( u)) and choose n large enough to ensure that in each of the deterministic automata, some sub- Γ-word s m of s n loops in some state. Then we show that every choice of a weight for such a loop leads to a contradiction.
Let p, q, t, r be as in condition (ii) of the tree fork property, v 1 = ⋄ 1( t), and v 2 = ⋄ 2( t). For the rivals p and q, let u and s be as in the definition of rivals and v = ⋄ 1( s). We let $${r^{p}_{u}} \in \text {Run}_{\mathcal {A}}(u,p)$$, $${r^{q}_{u}} \in \text {Run}_{\mathcal {A}}(u,q)$$, $${r^{p}_{s}} \in \text {Run}_{\mathcal {A}}^{{\diamond }}(p,s,p)$$, and $${r^{q}_{s}} \in \text {Run}_{\mathcal {A}}^{{\diamond }}(q,s,q)$$. Furthermore, we write $$\mathcal {A}_{i} = (Q_{i}, \varGamma , \mu _{i}, \nu _{i})$$ and let $$N = \max \limits _{i = 1}^{n} |Q_{i}|$$.
By the following argument, we may assume that $$\nu (r(\varepsilon )) \neq -\infty$$. By trimness, there exists a Γ-word $$s^{\prime \prime }$$ and a run $$r^{\prime \prime } \in \text {Run}_{\mathcal {A}}^{{\diamond }}(s^{\prime \prime })$$ with $$r^{\prime \prime }({\Diamond }_1(s^{\prime \prime })) = r(\varepsilon )$$ and $$\nu (r^{\prime \prime }(\varepsilon )) \neq -\infty$$. Thus, if $$\nu (r(\varepsilon )) = -\infty$$, we can consider the 2- Γ-context $$s^{\prime \prime }(t)$$ with the run $$r^{\prime \prime } \langle r \to {\Diamond }_1(s^{\prime \prime }) \rangle$$ instead of t and r.
We now consider the tree $$t^{\prime } = t(s^{N}(u), s^{N}(u))$$ together with the run
$$r^{\prime} = r \langle ({{r^{p}_{s}}})^{N\langle v \rangle}\langle {r^{p}_{u}} \to v^{N} \rangle \to v_{1} \rangle \langle ({{r^{q}_{s}}})^{N\langle v \rangle} \langle {r^{q}_{u}} \to v^{N} \rangle \to v_{2} \rangle.$$
Since $$r^{\prime } \in \text {Run}_{\mathcal {A}}(t^{\prime })$$ and $$\nu (r^{\prime }(\varepsilon )) \neq -\infty$$, we have $${\llbracket }{\mathcal {A}}{\rrbracket }(t^{\prime }) \neq -\infty$$, so for some j ∈{1,…, n} we have $${\llbracket }{\mathcal {A}_{j}}{\rrbracket } (t^{\prime }) = {\llbracket }{\mathcal {A}}{\rrbracket }(t^{\prime })$$. By pigeonhole principle, since N ≥| Q j|, we have $$r^{\prime }(v_{1}v^{n_{1}}) = r^{\prime }(v_{1}v^{n_{2}})$$ for some n 1, n 2 ∈{0,…, N} with n 1 < n 2. Since $$\mathcal {A}_{j}$$ is deterministic, we also obtain $$r^{\prime }(v_{2}v^{n_{1}}) = r^{\prime }(v_{2}v^{n_{2}}) = r^{\prime }(v_{1}v^{n_{1}})$$. Let m = n 2n 1 and let $$x,y,z \in \mathbb {R}$$ be the weights such that $$p {{\xrightarrow { s \mid x }}} p$$ and $$q {{\xrightarrow { s \mid y }}} q$$ in $$\mathcal {A}$$ and $$r^{\prime }(v_{1}v^{n_{1}}) {{\xrightarrow { s^{m} \mid z }}} r^{\prime }(v_{1}v^{n_{1}})$$ in $$\mathcal {A}_{j}$$. In particular, xy. We may assume that x < y. We consider two cases.
First, if $$z \geq \frac {m}{2}(x + y)$$, then for the tree t + = t( s N+m( u), s N( u)) we obtain
$$\begin{array}{@{}rcl@{}} \max_{i = 1}^{n} {\llbracket}{\mathcal{A}_{i}}{\rrbracket} (t^{+}) &\geq& {\llbracket}{\mathcal{A}_{j}}{\rrbracket} (t^{+}) = {\llbracket}{\mathcal{A}_{j}}{\rrbracket} (t^{\prime}) + z \\ &\geq& {\llbracket}{\mathcal{A}_{j}}{\rrbracket} (t^{\prime}) + \frac{m}{2}(x + y)\\ &>& {\llbracket}{\mathcal{A}_{j}}{\rrbracket} (t^{\prime}) + mx = {\llbracket}{\mathcal{A}}{\rrbracket}(t^{+}). \end{array}$$
Note that this follows because $$\mathcal {A}$$ and $$\mathcal {A}_{j}$$ are both unambiguous, i.e., if we construct an accepting run on a given tree, we know that the weight of this run must be the weight assigned to the tree by the automaton.
For the other case, namely that $$z \leq \frac {m}{2}(x + y)$$, we see that for the tree t = t( s N( u), s Nm( u)) we obtain
$$\begin{array}{@{}rcl@{}} \max_{i = 1}^{n} {\llbracket}{\mathcal{A}_{i}}{\rrbracket} (t^{-}) &\geq& {\llbracket}{\mathcal{A}_{j}}{\rrbracket} (t^{-}) = {\llbracket}{\mathcal{A}_{j}}{\rrbracket} (t^{\prime}) - z\\ &\geq& {\llbracket}{\mathcal{A}_{j}}{\rrbracket} (t^{\prime}) - \frac{m}{2}(x + y) \\ &>& {\llbracket}{\mathcal{A}_{j}}{\rrbracket} (t^{\prime}) - my = {\llbracket}{\mathcal{A}}{\rrbracket}(t^{-}). \end{array}$$
In both cases, we see that $${\llbracket }{\mathcal {A}}{\rrbracket } = \max \limits _{i = 1}^{n} {\llbracket }{\mathcal {A}_{i}}{\rrbracket }$$ does not hold, which is a contradiction. □
Together, Theorems 4 and 5 show that if a trim unambiguous max-plus-WTA satisfies the tree fork property, then its behavior is not finitely sequential.

### 3.2 Sufficiency

In this section, we show that the behavior of an unambiguous max-plus-WTA $$\mathcal {A}$$ which does not satisfy the tree fork property is finitely sequential. For simplicity, we begin with a description of our method of proof on max-plus word automata and compare it to the proof method of Bala and Koniński [ 4].
Both proofs work by distributing the runs of $$\mathcal {A}$$ across a finite set of unambiguous max-plus word automata such that all of these automata satisfy the twins property. This distribution essentially has the aim of separating the rivals of $$\mathcal {A}$$. By Theorem 1, these unambiguous automata can then be determinized. The major difference between our approach and that of [ 4] lies in the way we obtain these unambiguous automata. To understand our approach, let p and q be two rivals of $$\mathcal {A}$$. Furthermore, let u = u 1u n be a word for which there exist valid runs $$r^{p} = p_{0} {{\xrightarrow {u_{1}}}} p_{1} {{\xrightarrow {u_{2}}}} \ldots {{\xrightarrow {u_{n-1}}}} p_{n-1} {{\xrightarrow {u_{n}}}} p$$ and $$r^{q} = q_{0} {{\xrightarrow {u_{1}}}} q_{1} {{\xrightarrow {u_{2}}}} {\ldots } {{\xrightarrow {u_{n-1}}}} q_{n-1} {{\xrightarrow {u_{n}}}} q$$ of $$\mathcal {A}$$ on u. We also define p n = p and q n = q.
We now show that the first occurrence of either p or q in the runs r p and r q serves as a “distinguisher” between the two runs. We let i be the smallest index with the property that p i ∈{ p, q}. Similarly, we let j be the smallest index with the property that q j ∈{ p, q}. We obtain valid runs $$p_{i} {{\xrightarrow {u_{i+1} \cdots u_{n}}}} p$$ and $$q_{j} {{\xrightarrow {u_{j+1} {\cdots } u_{n}}}} q$$.
Now assume it would hold that i = j and p i = q j, i.e., the first occurrences are at the same position in the word, and also the states at this position are the same in both runs. Then with t = u i+ 1u n, we see that we have valid runs $$p_{i} \xrightarrow {t} p$$ and $$p_{i} \xrightarrow {t} q$$, where p i ∈{ p, q}. Thus, $$\mathcal {A}$$ would satisfy the fork property. Since our assumption is that $$\mathcal {A}$$ does not satisfy the fork property, we have either ij or p iq j.
This fundamental property is also used in the corresponding proof of [ 4], but our way of exploiting it differs from [ 4]. In their proof for word automata, Bala and Koniński use this property implicitly to show that certain states of a modified Schützenberger covering of $$\mathcal {A}$$ occur at most once in every run [ 4, Lemma 6]. They can therefore construct a new max-plus automaton which for each run keeps a record of all occurrences of these states. The above mentioned unambiguous automata are then obtained by separating runs with differing records into different automata. For tree automata, the number of these occurrences is unfortunately not bounded, for reasons which we will also indicate below.
For now, we continue outlining our new approach, which is to construct an automaton which adds a distinguishing marker to every run when first encountering one of the rivals p or q. This marker consists of a number, which is used to distinguish occurrences at different positions, and the state from { p, q} which was visited first. Whenever reading a letter which causes some valid run to visit p or q for the first time, the automaton selects the smallest marker which was not used by any valid run on the prefix read so far, and annotates it to the run. For example, assume that neither p nor q occur in any valid run the word u, but that our run r on ua leads to p. Then r obtains the marker 1 p. Now assume there is a valid run on uaa which leads to p and which visited neither p nor q before that. Then this run obtains the marker 2 p, since 1 p is already assigned to r. Next, assume that after reading uaaa another marker for p has to be assigned, and that r cannot be extended to a valid run on uaa. Then we assign the marker 1 p, as now no valid run on uaa exists to which the marker 1 p is assigned. See Fig.  3 for an example of this annotation process on the word aaa for the automaton depicted there.
With this procedure, runs like r p and r q above receive different markers since either one run obtains a marker later than the other, and therefore a different marker, or at least the states they visit first are different, which also leads to different markers. To separate the rivals of $$\mathcal {A}$$, we can thus make a copy of $$\mathcal {A}$$ for every marker, and only allow runs which carry the respective automaton’s marker. Whenever a different marker would be assigned, the execution of the run is blocked.
Note here that the number of markers we need for this annotation process is bounded. Since the automaton $$\mathcal {A}$$ is unambiguous, the number of valid runs on every given word is bounded by the number of states in $$\mathcal {A}$$. If this were not the case, there would exist two distinct valid runs on the same word which lead to the same state, from which a counterexample to the unambiguity of $$\mathcal {A}$$ could be constructed. In particular, the number of markers assigned at any given “time” is bounded by the number of states of $$\mathcal {A}$$.
All of this can easily be generalized to the situation where there is more than one pair of rivals. Then, runs simply obtain a marker for each pair of rivals of the automaton, and the copies of $$\mathcal {A}$$ allow a distinguished marker for each of these pairs.
Unfortunately, these ideas do not translate to trees as easily. For example, consider the runs in Fig.  4. Intuitively, both runs should obtain the marker 1 p. However, since p and q are rivals, this marker does not serve the purpose of distinguishing runs as it does in the word case. The first p occurs in different subtrees of both runs, thus the annotation of distinct markers is not possible. Also, it is easy to construct an automaton where a rival p can occur at arbitrarily many pairwise prefix-independent positions, thus a simple lexicographic distinction is not possible. This is also the reason why the approach from [ 4] does not work for tree automata.
Our solution is to distribute not the runs of the automaton $$\mathcal {A}$$, but the runs of its Schützenberger covering. The Schützenberger covering of a max-plus automaton $$\mathcal {A}$$ is a max-plus automaton which possesses the same behavior as $$\mathcal {A}$$. It has already been employed in a number of decidability results for max-plus automata [ 3, 4, 22, 31]. Its construction is inspired by a paper of Schützenberger [ 39] and was made explicit by Sakarovitch in [ 35], see also [ 36].
To better explain the idea behind its construction, we first point out a certain aspect of the classical powerset construction for finite automata [ 34]. Assume that $$\mathcal {D}$$ is the result of applying the powerset construction to an NFA $${\mathscr{B}}$$. Then we might say that for a word w = w 1 w 2, the state which $$\mathcal {D}$$ is in after reading the prefix w 1 is the set of all states which $${\mathscr{B}}$$ could be in after reading w 1. Similarly, the Schützenberger covering of a max-plus automaton $$\mathcal {A}$$ annotates to every state of a run of $$\mathcal {A}$$ on a word w the set of all states which “ $$\mathcal {A}$$ could be in” at this point, i.e., which can be reached by some valid run on the considered prefix of w. Like the powerset construction, these ideas easily carry over to trees.
The reason we consider the Schützenberger covering of $$\mathcal {A}$$ is that each pair p, q of its rivals satisfies the following property. For every tree t, either (1) p and q do not occur together in any run on t or (2) p and q occur only linearly, i.e., there is a distinguished branch of t such that for every run on t, all occurrences of p and q lie on this branch. In particular, the situation of Fig.  4 is not possible. All pairs which satisfy the first condition can simply be separated into different automata, all pairs which satisfy the second condition can be handled like in the word case. The proof of this is non-trivial and needs some preparation. We begin with the formal definition of the Schützenberger covering.
For the rest of this section, let $$\mathcal {A} = (Q, \varGamma , \mu , \nu )$$ be a trim unambiguous max-plus-WTA which does not satisfy the tree fork property.
Definition 4 (Schützenberger covering, 35)
The Schützenberger covering $$\mathcal {S} = (Q_{\mathcal {S}}, \varGamma , \mu _{\mathcal {S}}, \nu _{\mathcal {S}})$$ of $$\mathcal {A}$$ is the trim part of the max-plus-WTA $$(Q \times \mathcal {P}(Q), \varGamma , \mu ^{\prime }, \nu ^{\prime })$$ defined for aΓ with rk Γ( a) = m and $$(p_{0}, P_{0}), \ldots , (p_{m}, P_{m}) \in Q \times \mathcal {P}(Q)$$ by
$$\begin{array}{@{}rcl@{}} \begin{array}{c} {}\mu^{\prime}((p_{1}, P_{1}), \ldots, (p_{m}, P_{m}), a, (p_{0}, P_{0}))=\\ \left\{\begin{array}{lll} \mu(p_{1}, \ldots, p_{m}, a, p_{0})\quad \text{if } P_{0} = \{ q_{0} \in Q \mid &\exists (q_{1}, \ldots, q_{m}) \in P_{1} \times {\ldots} \times P_{m} \text{ with}\\ &\mu(q_{1}, \ldots, q_{m}, a, q_{0}) \neq -\infty \}\\ -\infty &{\kern-6.2pc} \text{otherwise} \end{array}\right.\\ \nu^{\prime}(p_{0}, P_{0}) = \nu(p_{0}).{\kern-.8pc} \end{array} \end{array}$$
We let $$\pi _{1} \colon Q \times \mathcal {P}(Q) \to Q$$, ( p, P)↦ p and $$\pi _{2} \colon Q \times \mathcal {P}(Q) \to \mathcal {P}(Q)$$, ( p, P)↦ P be the projections.
It is elementary to show that for a run of $$\mathcal {S}$$ on a tree t, the second entry of the state at a position w consists of all states of $$\mathcal {A}$$ which can be reached by a valid run of $$\mathcal {A}$$ on $$t {\upharpoonright }_{w}$$. In particular, every two runs on the same tree coincide on their second entries. Furthermore, projecting all states of a run of $$\mathcal {S}$$ to their first coordinate yields a run of $$\mathcal {A}$$, and the weights of these runs coincide. It follows that $$\mathcal {S}$$ is unambiguous and satisfies $${\llbracket }{\mathcal {S}}{\rrbracket } = {\llbracket }{\mathcal {A}}{\rrbracket }$$. Also, $$\mathcal {S}$$ is trim by definition.
We can also make the following observation about the rivals of $$\mathcal {S}$$. Let p and q be rivals of $$\mathcal {S}$$ and let u and s be as in the definition of rivals. Since all runs of $$\mathcal {S}$$ on u coincide on the second entry of the state at the root, p and q also coincide on their second entry. Moreover, as projecting the runs of $$\mathcal {S}$$ on u and s to their first entries yields runs of $$\mathcal {A}$$ on u and s, respectively, we additionally see that the first entries of p and q are rivals in $$\mathcal {A}$$. Thus, if two states $$\mathbf {p}, \mathbf {q} \in Q_{\mathcal {S}}$$ are rivals in $$\mathcal {S}$$, then p = ( p, P) and q = ( q, P) for some set $$P \subseteq Q$$ and two states p, qQ which are rivals in $$\mathcal {A}$$.
In the Schützenberger covering of the automaton from Fig.  4, only the states ( p,{ p, q}) and ( q,{ p, q}) are rivals. See also Fig.  5 for the runs of the Schützenberger covering on the trees from Fig.  4. In the following lemma, we formally show that the properties we just described indeed hold for $$\mathcal {S}$$.
Lemma 5
Let tT Γ be a tree. Then the following statements hold.
(i)
For every run $$r \in \text {Run}_{\mathcal {S}}(t)$$ and position wpos( t) we have $$\pi _{2} \circ r(w) = \{ p \in Q \mid \exists r^{\prime } \in \text {Run}_{\mathcal {A}}(t {\upharpoonright }_{w}, p) \}$$.

(ii)
For every two runs $$r_{1}, r_{2} \in \text {Run}_{\mathcal {S}}(t)$$, it holds that π 2r 1= π 2r 2.

(iii)
The projection π 1 induces a bijection $$\pi _{1} \colon \text {Run}_{\mathcal {S}}(t) \to \text {Run}_{\mathcal {A}}(t)$$ by rπ 1r.

(iv)
For every run $$r \in \text {Run}_{\mathcal {S}}(t)$$ and every position wpos( t), we have π 1r( w) ∈ π 2r( w).

(v)
$$\mathcal {S}$$ is trim, unambiguous, and satisfies $${\llbracket }\mathcal {S}{\rrbracket } = {\llbracket }{\mathcal {A}}{\rrbracket }$$.

(vi)
For every Γ -word s and two states $$\mathbf {p}, \mathbf {q} \in Q_{\mathcal {S}}$$ with $$\mathbf {p} {{\xrightarrow {s \mid x}}} \mathbf {q}$$, we have $$\pi _{1}(\mathbf {p}) {{\xrightarrow {s \mid x}}} \pi _{1}(\mathbf {q})$$.

(vii)
If two states $$\mathbf {p}, \mathbf {q} \in Q_{\mathcal {S}}$$ are rivals in $$\mathcal {S}$$, then p = ( p, P) and q = ( q, P) for some set $$P \subseteq Q$$ and two states p, qQ which are rivals in $$\mathcal {A}$$.

Proof
(i)
Let tT Γ and $$r \in \text {Run}_{\mathcal {S}}(t)$$ and for contradiction, let w ∈pos( t) be a prefix-maximal position for which (i) does not hold. We deduce that (i) holds for w. We let a = t( w), m = rk Γ( a), and write r( w) = ( p, P) and r( wi) = ( p i, P i) for i ∈{1,…, m}.
First, let qP, then there are states ( q 1,…, q m) ∈ P 1 ×… × P m with $$\mu (q_{1}, \ldots , q_{m}, a, q) \neq -\infty$$. By assumption, for every i ∈{1,…, m} we find a run $$r_{i} \in \text {Run}_{\mathcal {A}}(t {\upharpoonright }_{wi}, q_{i})$$. Then the quasi-run $$r^{\prime } \colon \text {pos}(t {\upharpoonright }_{w}) \to Q$$ defined by $$r^{\prime }(\varepsilon ) = q$$ and $$r^{\prime }(iv) = r_{i}(v)$$ is a run of $$\mathcal {A}$$ on $$t {\upharpoonright }_{w}$$ with $$r^{\prime }(\varepsilon ) = q$$.
On the other hand, let $$r^{\prime } \in \text {Run}_{\mathcal {A}}(t {\upharpoonright }_{w})$$ and let $$q = r^{\prime }(\varepsilon )$$. Then for every i ∈{1,…, m} we have that $$r^{\prime } {\upharpoonright }_{i} \in \text {Run}_{\mathcal {A}}(t {\upharpoonright }_{wi})$$, so by assumption, $$r^{\prime }(i) \in P_{i}$$. Moreover, $$\mu (r^{\prime }(1), \ldots , r^{\prime }(m), a, q) \neq -\infty$$, so qP. Thus, (i) holds for w, which is a contradiction, so w does not exist.

(ii)
follows from (i).

(iii)
Let tT Γ. By definition of $$\mu _{\mathcal {S}}$$, it is clear that for $$r \in \text {Run}_{\mathcal {S}}(t)$$ we have $$\pi _{1} \circ r \in \text {Run}_{\mathcal {A}}(t)$$. The injectivity of $$\pi _{1} \colon \text {Run}_{\mathcal {S}}(t) \to \text {Run}_{\mathcal {A}}(t)$$ follows from (ii) since for every two runs $$r_{1}, r_{2} \in \text {Run}_{\mathcal {S}}(t)$$ we have π 2r 1 = π 2r 2. For surjectivity, we let $$r^{\prime } \in \text {Run}_{\mathcal {A}}(t)$$ and define a run $$r \in \text {Run}_{\mathcal {S}}(t)$$ inductively as follows. For a leaf w ∈pos( t), we let $$r(w) = (r^{\prime }(w), \{ p_{0} \in Q \mid \mu (t(w), p_{0}) \neq -\infty \})$$. For w ∈pos( t) with rk Γ( t( w)) = m such that r is defined on w1,…, wm with π 2r( wi) = P i, we let $$r(w) = (r^{\prime }(w), \{ p_{0} \in Q \mid \exists (p_{1}, \ldots , p_{m}) \in P_{1} \times {\ldots } \times P_{m} \text { with } \mu (p_{1}, \ldots , p_{m}, a, p_{0}) \neq -\infty \})$$. Then $$r \in \text {Run}_{\mathcal {S}}(t)$$ and $$\pi _{1} \circ r = r^{\prime }$$.

(iv)
follows from (i) and (iii).

(v)
$$\mathcal {S}$$ is trim by definition. Let tT Γ. By definition of $$\mu _{\mathcal {S}}$$, for every run $$r \in \text {Run}_{\mathcal {S}}(t)$$ we have $$\text {wt}_{\mathcal {S}}(t, r) = \text {wt}_{\mathcal {A}}(t, \pi _{1} \circ r)$$. By definition of $$\nu _{\mathcal {S}}$$, we also have $$\nu _{\mathcal {S}}(r(\varepsilon )) = \nu (\pi _{1} \circ r(\varepsilon ))$$. By (iii), we thus have $$|\text {Acc}_{\mathcal {S}}(t)| = |\text {Acc}_{\mathcal {A}}(t)| \leq 1$$, which means $$\mathcal {S}$$ is unambiguous, and $${\llbracket }\mathcal {S}{\rrbracket }(t) = {\llbracket }{\mathcal {A}}{\rrbracket }(t)$$.

(vi)
Let s be a Γ-word and $$\mathbf {p},\mathbf {q} \in Q_{\mathcal {S}}$$ be two states with $$\mathbf {p} \xrightarrow {s \mid x} \mathbf {q}$$, then there exists a run $$r \in \text {Run}_{\mathcal {S}}^{{\diamond }}(\mathbf {p},s,\mathbf {q})$$ with $$\text {wt}_{\mathcal {S}}^{{\diamond }}(s,r) = x$$. By definition of $$\mu _{\mathcal {S}}$$, we have $$\pi _{1} \circ r \in \text {Run}_{\mathcal {A}}^{{\diamond }}(s)$$ and $$\text {wt}_{\mathcal {S}}^{{\diamond }}(s, r) = \text {wt}_{\mathcal {A}}^{{\diamond }}(s, \pi _{1} \circ r)$$, so $$\pi _{1}(\mathbf {p}) \xrightarrow {{s \mid x}} \pi _{1}(\mathbf {q})$$.

(vii)
Let $$\mathbf {p}, \mathbf {q} \in Q_{\mathcal {S}}$$ be rivals in $$\mathcal {S}$$ and write p = ( p, P p), q = ( q, P q). Let uT Γ and $$s \in T_{\varGamma _{{\diamond }}}$$ be as in the definition of rivals and let $$r^{\mathbf {p}} \in \text {Run}_{\mathcal {S}}(u,\mathbf {p})$$ and $$r^{\mathbf {q}} \in \text {Run}_{\mathcal {S}}(u,\mathbf {q})$$. By (ii), we have P p = π 2r p( ε) = π 2r q( ε) = P q. By (iii), we have $$\pi _{1} \circ r^{\mathbf {p}} \in \text {Run}_{\mathcal {A}}(u, p)$$ and $$\pi _{1} \circ r^{\mathbf {q}} \in \text {Run}_{\mathcal {A}}(u, q)$$, so p and q are siblings. Finally, from $$(p, P_{p}) \xrightarrow {s \mid x} (p, P_{p})$$ and $$(q, P_{q}) \xrightarrow {s \mid y} (q, P_{q})$$, we obtain by (vi) that $$p \xrightarrow {s \mid x} p$$ and $$q \xrightarrow {s \mid y} q$$. Since xy, p and q are rivals in $$\mathcal {A}$$.

In the theorems to follow, we will use fact (vii) of Lemma 5 without explicit further notice.
In order to prove some deeper results about the rivals of $$\mathcal {S}$$, we need two preparatory lemmata. As a first simplification, we show that we may assume that two rivals p and q of $$\mathcal {A}$$ are always comparable with respect to the relation ≤. To see this, note that by condition (ii) of the tree fork property, p and q may not occur in prefix-independent positions in a run. If in addition, p and q can also not appear in prefix-dependent positions in a run, they never appear together in the same run of $$\mathcal {A}$$. Thus, we can create two copies of $$\mathcal {A}$$, one in which we remove p and one in which we remove q, and the pointwise maximum of these two automata will be equivalent to the behavior of $$\mathcal {A}$$.
Lemma 6
We may assume that for all rivals p, qQ we have either pq or qp, or both.
Proof
Let p, qQ be rivals for which neither pq nor qp. Then we can show that p and q never occur together in the same run as follows. Assume we have a tree tT Γ, a run $$r \in \text {Run}_{\mathcal {A}}(t)$$, and positions w 1, w 2 ∈pos( t) with r( w 1) = p and r( w 2) = q. Then w 1 and w 2 may not be prefix-independent since p and q are rivals, and by assumption $$\mathcal {A}$$ does not satisfy condition (ii) of the tree fork property. However, if w 1 and w 2 are prefix-dependent, we have a witness for either pq or qp. This is a contradiction, and thus r as chosen does not exist.
We let Q 1 = Q ∖{ p}, Q 2 = Q ∖{ q}, and let $$\mathcal {A}_{i} = (Q_{i}, \varGamma , \mu _{i}, \nu _{i})$$ for i = 1,2, where μ i and ν i are the appropriate restrictions of μ and ν to the state sets Q i. As p and q do not occur together in any run of $$\mathcal {A}$$, every run of $$\mathcal {A}$$ is also a run of at least one of the automata $$\mathcal {A}_{1},\mathcal {A}_{2}$$. Thus, we have $${\llbracket }{\mathcal {A}}{\rrbracket } = \max \limits _{i = 1}^{2} {\llbracket }{\mathcal {A}_{i}}{\rrbracket }$$ and both $$\mathcal {A}_{1}$$ and $$\mathcal {A}_{2}$$ are trim and unambiguous and do not satisfy the tree fork property.
This procedure can be iterated to separate all rivals which are not in ≤-relation. The termination of this procedure is guaranteed by the fact that the set of states becomes strictly smaller with every iteration. Eventually, we find trim unambiguous max-plus-WTA $$\mathcal {A}_{1}, \ldots , \mathcal {A}_{n}$$, all of which do not satisfy the tree fork property, such that $${\llbracket }{\mathcal {A}}{\rrbracket } = \max \limits _{i = 1}^{n} {\llbracket }{\mathcal {A}_{i}}{\rrbracket }$$ and all rivals in an automaton $$\mathcal {A}_{i}$$ are pairwise in ≤-relation. □
Next, we note an elementary statement about self-maps f : XX. Namely, if X is a finite set and f : XX a mapping, then for every aX there exists some element bX and an integer n ≥ 1 such that after n iterations of f, both a and b are mapped to b. To see this, consider the elements a, f( a), f 2( a),…, f |X|( a). By pigeon hole principle, there are numbers 0 ≤ m 1 < m 2 ≤| X| with $$f^{m_{1}}(a) = f^{m_{2}}(a)$$. Then if we choose nm 1 as a multiple of m 2m 1 and b = f n( a), we see that f n( a) = b = f n( b).
Lemma 7
Let X be a finite set and f : XX a mapping. Then for every aX, there exists an element bX and an integer n ≥ 1 with f n( a) = b = f n( b). Here, f n is the n- th iterate of f, i.e., $$f^{0} = \text {id}_{X}$$ and f m+ 1 = ff m.
We now identify the first important property which all rivals of $$\mathcal {S}$$ satisfy. Namely, if $$P \subseteq Q$$ is the second entry of some rival, then it cannot occur in the form of a “triangle” in any valid run of $$\mathcal {S}$$. More precisely, if we have a run r and positions w, wv 1, and wv 2 such that the second entry of r( w), r( wv 1), and r( wv 2) is P, then wv 1 and wv 2 are prefix-dependent.
Lemma 8
Let $$(p, P), (q, P) \in Q_{\mathcal {S}}$$ be rivals in $$\mathcal {S}$$. Furthermore, let $$t^{\prime } \in T_{\varGamma }$$ be a tree, $$r^{\prime } \in \text {Run}_{\mathcal {S}}(t^{\prime })$$ a run of $$\mathcal {S}$$ on $$t^{\prime }$$, and $$w_{1}, w_{2} \in \text {pos}(t^{\prime })$$ be positions in $$t^{\prime }$$. If $$\pi _{2} \circ r^{\prime }(\varepsilon ) = \pi _{2} \circ r^{\prime }(w_{1}) = \pi _{2} \circ r^{\prime }(w_{2}) = P$$, then w 1 and w 2 are prefix-dependent.
Proof
We proceed by contradiction and assume that $$t^{\prime },r^{\prime },w_{1},w_{2}$$ as in the statement of the lemma exist such that w 1 and w 2 are prefix-independent. We show that then, $$\mathcal {A}$$ satisfies condition (i) of the tree fork property. For the rivals ( p, P) and ( q, P), let u and s be as in the definition of rivals and let v = ⋄ 1( s). As the proof is rather technical, we first provide a proof sketch and then follow up with a more precise presentation of the argumentation. See also Fig.  6 for some visual aid.
By assumption, u can reach ( p, P) and s can loop in ( p, P), thus the trees s |P|( u) and $$s^{|P|^{|P|}}(u)$$ can reach ( p, P). Due to the construction of $$\mathcal {S}$$, this means both of these trees can also reach the states of $$r^{\prime }$$ at w 1 and w 2. In particular, there exists a run of $$\mathcal {S}$$ on the tree $$t = t^{\prime } \langle s^{|P|}(u) \to w_{1} \rangle \langle s^{|P|^{|P|}}(u) \to w_{2} \rangle$$ and for this run, the second entry of every state at the beginning or end of an s-loop is P. In addition, t leads to a state with second entry P, so there in fact exist | P| runs of $$\mathcal {S}$$ on t, one for each state in P. We let r 1,…, r |P| be the projections of these runs to their first entry and obtain | P| runs of $$\mathcal {A}$$ on t where for each run the state at the root and all states at the beginning or end of an s-loop are from P.
By pigeonhole principle, there is some subloop s n below w 2 which loops in all runs at the same time, i.e., where for some n 1 we have $$r_{i}(w_{2}v^{n_{1}}) = r_{i}(w_{2}v^{n_{1} + n})$$ for all runs r i. For each r i, we let $$q_{i} = r_{i}(w_{2}v^{n_{1}}) \in P$$ be the state which r i loops in and let x i be the weight of this loop.
If x ix j for some i and j, the states q i and q j are rivals in $$\mathcal {A}$$ with witnesses u and s n. By Lemma 6, we may therefore assume q iq j. Again by pigeon hole principle, the run r i loops below w 1 in s m for some m ≥ 1 with some state p iP, say with weight y i. Due to x ix j, we have mx iny i or mx jny i. Since u can reach every state from P, the state p i is thus a rival of q i or q j with witnesses u and s nm. From the existence of r i and the assumption that q iq j, we see that p i can occur prefix-independently both from q i and from q j. This is a contradiction to the assumption that $$\mathcal {A}$$ does not satisfy the tree fork property. It must therefore hold that x 1 = … = x |P|.
We let x and y be the weights such that $$\mathcal {A}$$ loops s in p with weight x and in q with weight y. Then from xy it follows that nxx 1 or nyx 1, so the states q i are either all rivals of p or all rivals of q with witnesses u and s n. We assume all q i to be rivals of p and apply Lemma 7 to the mapping f : P →{ q 1,…, q |P|}, r i( ε)↦ q i with a = p to obtain q jP and m ≥ 1 such that f m( p) = q j = f m( q j). Then with $$\tilde {s} = t \langle {\diamond } \to w_{2}v^{n_{1}} \rangle$$, we see that the Γ-word $$\tilde {s}^{m}$$ is a q j- p-fork, i.e., $$\mathcal {A}$$ satisfies condition (i) of the tree fork property.
We now turn to the more technical presentation of the proof. We define the tree $$t = t^{\prime } \langle s^{|P|}(u) \to w_{1} \rangle \langle s^{|P|^{|P|}}(u) \to w_{2}\rangle$$ and construct a run $$r \in \text {Run}_{\mathcal {S}}(t)$$ of $$\mathcal {S}$$ on t as follows. By assumption, there exists a run $$r^{\mathbf {p}} \in \text {Run}_{\mathcal {S}}(u,(p,P))$$ and a run $$r_{s} \in \text {Run}_{\mathcal {S}}^{{\diamond }} ((p,P),s,(p,P))$$. We let $$r_{1}^{\prime } = r_{s}^{|P| \langle v \rangle } \langle r^{\mathbf {p}} \to v^{|P|} \rangle$$ and $$r_{2}^{\prime } = r_{s}^{|P|^{|P|}\langle v \rangle } \langle r^{\mathbf {p}} \to v^{|P|^{|P|}} \rangle$$. Then $$r_{1}^{\prime } \in \text {Run}_{\mathcal {S}}(s^{|P|}(u),(p,P))$$ and $$r_{2}^{\prime } \in \text {Run}_{\mathcal {S}}(s^{|P|^{|P|}}(u),(p,P))$$.
By Lemma 5(iv), we have $$\pi _{1} \circ r^{\prime }(w_{1}), \pi _{1} \circ r^{\prime }(w_{2}) \in P$$, so by Lemma 5(i) we can find $$r_{1}^{\prime \prime } \in \text {Run}_{\mathcal {A}}(s^{|P|}(u))$$ with $$r_{1}^{\prime \prime }(\varepsilon ) = \pi _{1} \circ r^{\prime }(w_{1})$$ and $$r_{2}^{\prime \prime } \in \text {Run}_{\mathcal {A}}(s^{|P|^{|P|}}(u))$$ with $$r_{2}^{\prime \prime }(\varepsilon ) = \pi _{1} \circ r^{\prime } (w_{2})$$. Then $$r = r^{\prime } \langle \pi _{1}^{-1}(r_{1}^{\prime \prime }) \to w_{1} \rangle \langle \pi _{1}^{-1}(r_{2}^{\prime \prime }) \to w_{2} \rangle \in \text {Run}_{\mathcal {S}}(t)$$ is a run of $$\mathcal {S}$$ on t and we have π 2r( w 1 v i) = P for 0 ≤ i ≤| P| and π 2r( w 2 v i) = P for 0 ≤ i ≤| P| |P|.
By Lemma 5(i) and because π 2r( ε) = P, we can now find | P| runs $$r_{1}, \ldots , r_{|P|} \in \text {Run}_{\mathcal {A}}(t)$$ on t such that { r 1( ε),…, r |P|( ε)} = P. We have r j( w 2 v i) ∈ P for every j ∈{1,…,| P|} and every i ∈{0,…,| P| |P|}. For each i ∈{0,…,| P| |P|}, we define the tuple $$\bar {q}_{i} = (r_{1}(w_{2}v^{i}), \ldots , r_{|P|}(w_{2}v^{i}))$$. Since $$\bar {q}_{i} \in P^{|P|}$$ for every i, we can find n 1 < n 2 with $$\bar {q}_{n_{1}} = \bar {q}_{n_{2}}$$ by pigeonhole principle. Let n = n 2n 1 and write $$\bar {q}_{n_{1}} = (q_{1}, \ldots , q_{|P|})$$.
We now show that q 1,…, q |P| are either all rivals of p, or they are all rivals of q. For this, note first that $$q_{j} \xrightarrow {s^{n} \mid x_{j} } q_{j}$$ for all j ∈{1,…,| P|} with weights $$x_{1}, \ldots , x_{|P|} \in \mathbb {R}$$. Also, by the existence of the run r p on u and Lemma 5(i), all states in P are siblings.
We show first that x 1 = … = x |P|. We assume that by contradiction, x ix j for some ij. Then q i and q j are rivals in $$\mathcal {A}$$ with witnesses u and s n. By Lemma 6, we can therefore assume that q iq j or q jq i. We assume q iq j and let $${s^{i}_{j}}$$ be a Γ-word such that there exists a run $${r^{i}_{j}} \in \text {Run}^{{\diamond }}_{\mathcal {S}}(q_{j}, {s^{i}_{j}}, q_{i})$$. Furthermore, by pigeonhole principle, we can find m 1, m 2 ∈{0,…,| P|} with $$r_{i}(w_{1}v^{m_{1}}) = r_{i}(w_{2}v^{m_{2}})$$ and m 1 < m 2. We let $$p_{i} = r_{i}(w_{1}v^{m_{1}})$$ and m = m 2m 1 and show that p i is a rival of either q i or q j. We have $$p_{i} {{\xrightarrow { s^{m} \mid y_{i} }}} p_{i}$$ for some weight $$y_{i} \in \mathbb {R}$$. Since p iP, we know that p i, q i, and q j are all siblings. Also, we have $$p_{i} {{\xrightarrow { s^{nm} \mid ny_{i}}}} p_{i}$$, $$q_{i} \xrightarrow { s^{nm} \mid mx_{i}} q_{i}$$, and $$q_{j} \xrightarrow { s^{nm} \mid mx_{j}} q_{j}$$. Since x ix j, we have ny imx i or ny imx j, or both. Thus, p i is a rival of either q i or of q j.
Under these assumptions, we see that $$\mathcal {A}$$ satisfies condition (ii) of the tree fork property as follows. Either the 2- Γ-context $$t_{1} = t \langle {\diamond } \to w_{1} v^{m_{1}} \rangle \langle {\diamond } \to w_{2}v^{n_{1}} \rangle$$ together with the run $$r_{i} {\upharpoonright }_{\text {pos}(t_{1})}$$ or the 2- Γ-context $$t_{2} = t_{1}({\diamond }, {s^{i}_{j}})$$ together with the run $$r_{i} {\upharpoonright }_{\text {pos}(t_{1})} \langle {r^{i}_{j}} \to {\Diamond }_{2}(t_{1}) \rangle$$ is a witness for condition (ii) to be satisfied. Since our assumption for this section is that $$\mathcal {A}$$ does not satisfy the tree fork property, this is a contradiction. In conclusion, x 1 = … = x |P|.
To see that q 1,…, q |P| are either all rivals of p, or they are all rivals of q, consider the following. Using the same arguments as above, we find for every i ∈{1,…,| P|} a run $$r^{q_{i}} \in \text {Run}_{\mathcal {A}}(u, q_{i})$$. Furthermore, we have $$p \xrightarrow { s^{n} \mid nx } p$$, $$q \xrightarrow { s^{n} \mid ny } q$$, and $$q_{i} \xrightarrow { s^{n} \mid x_{1} } q_{i}$$ for every i ∈{1,…,| P|}. Since xy, we have either nxx 1 or nyx 1. Without loss of generality, we assume nxx 1, thus all q i are rivals of p.
We now show that $$\mathcal {A}$$ satisfies condition (i) of the tree fork property. We define a mapping f : P →{ q 1,…, q |P|} by r i( ε)↦ q i for i ∈{1,…,| P|}; recall that $$\{q_{1}, \ldots , q_{|P|} \} \subseteq P$$, { r 1( ε),…, r |P|( ε)} = P, and r i( ε)≠ r j( ε) for ij. By Lemma 7, there exists m ≥ 1 and i ∈{1,…,| P|} with f m( p) = q i = f m( q i). From this, we obtain that with $$\tilde {s} = t \langle {\diamond } \to w_{2}v^{n_{1}} \rangle$$ we have $$q_{i} {{\xrightarrow {\tilde {s}^{m} \mid z }}} q_{i}$$ and $$q_{i} {{\xrightarrow {\tilde {s}^{m} \mid z^{\prime } }}} p$$ for weights $$z,z^{\prime } \in \mathbb {R}$$. As p and q i are rivals, this means that $$\mathcal {A}$$ satisfies condition (i) of the tree fork property. □
In the previous lemma, we showed that if P is the second entry of some rival from $$\mathcal {S}$$, then states with second entry P do not occur in the form of a triangle. In the next lemma, we show that even prefix-independent occurrences are restricted to a certain degree. Namely, if we have two rivals ( p, P) and ( q, P) with pq, then all occurrences of P as a second entry are prefix-dependent on ( p, P).
Lemma 9
Let $$(p, P), (q, P) \in Q_{\mathcal {S}}$$ be rivals in $$\mathcal {S}$$ with pq. Furthermore, let $$t^{\prime } \in T_{\varGamma }$$ be a tree, $$r^{\prime } \in \text {Run}_{\mathcal {S}}(t^{\prime })$$ a run of $$\mathcal {S}$$ on $$t^{\prime }$$, and $$w_{1} \in \text {pos}(t^{\prime })$$ a position in $$t^{\prime }$$ with $$r^{\prime }(w_{1}) = (p, P)$$. Then all positions $$w_{2} \in \text {pos}(t^{\prime })$$ with $$\pi _{2} \circ r^{\prime } (w_{2}) = P$$ are prefix-dependent on w 1.
Proof
We proceed by contradiction and take $$(p, P), (q, P), t^{\prime }, r^{\prime },w_{1}$$ as in the statement of the lemma and assume that there exists a position $$w_{2} \in \text {pos}(t^{\prime })$$ which is prefix-independent from w 1 and for which $$\pi _{2} \circ r^{\prime }(w_{2}) = P$$. We show that under these assumptions, $$\mathcal {A}$$ satisfies condition (ii) of the tree fork property. For the rivals ( p, P) and ( q, P), let u and s be as in the definition of rivals and let v = ⋄ 1( s). As in the proof of the previous lemma, we first provide a short proof sketch, see also Fig.  7 for some visual aid.
As we have seen in the proof of Lemma 8, the tree s |P|( u) can reach ( p, P), so due to the construction of $$\mathcal {S}$$, it can also reach the state of $$r^{\prime }$$ at w 2. Thus, there exists a run of $$\mathcal {S}$$ on the tree $$t = t^{\prime } \langle s^{|P|}(u) \to w_{2} \rangle$$ for which the state at w 1 is ( p, P) and for which the second entry of every state at the beginning or end of an s-loop is P. We let r be the projection of this run to the first entries of the states.
By pigeonhole principle, we find some subloop s n below w 2 in r which loops in a state $$p^{\prime } \in P$$. Let z be the weight of this loop and let x and y be the weights such that $$\mathcal {A}$$ loops s in p with weight x and in q with weight y. Due to xy, we have nxz or nyz. Since u can reach every state from P, the state $$p^{\prime }$$ is a rival of p or q with witnesses u and s n. From the fact that r( w 1) = p and the assumption that pq, we see that $$p^{\prime }$$ can occur prefix-independently both from p and from q. This is a contradiction to the assumption that $$\mathcal {A}$$ does not satisfy the tree fork property.
In more detail, the proof is as follows. We define the tree $$t = t^{\prime } \langle s^{|P|}(u) \to w_{2} \rangle$$ and construct a run $$r \in \text {Run}_{\mathcal {A}}(t)$$ of $$\mathcal {A}$$ on t as follows. By assumption, there exists a run $$r^{\mathbf {p}} \in \text {Run}_{\mathcal {S}}(u,(p,P))$$ and a run $$r_{s} \in \text {Run}_{\mathcal {S}}^{{\diamond }} ((p,P),s,(p,P))$$. We let $$r_{2}^{\prime } = r_{s}^{|P| \langle v \rangle } \langle r^{\mathbf {p}} \to v^{|P|} \rangle$$. Then $$r_{2}^{\prime } \in \text {Run}_{\mathcal {S}}(s^{|P|}(u),(p,P))$$.
By Lemma 5(iv), we have $$\pi _{1} \circ r^{\prime }(w_{2}) \in P$$, so by Lemma 5(i) we can find $$r_{2}^{\prime \prime } \in \text {Run}_{\mathcal {A}}(s^{|P|}(u))$$ with $$r_{2}^{\prime \prime }(\varepsilon ) = \pi _{1} \circ r^{\prime }(w_{2})$$. Then $$r = \pi _{1}(r^{\prime }) \langle r_{2}^{\prime \prime } \to w_{2} \rangle \in \text {Run}_{\mathcal {A}}(t)$$ is a run of $$\mathcal {A}$$ on t and we have r( w 2 v i) ∈ P for 0 ≤ i ≤| P|.
By pigeonhole principle, we can find n 1, n 2 ∈{0,…,| P|} with $$r(w_{2}v^{n_{1}}) = r(w_{2}v^{n_{2}})$$ and n 1 < n 2. We let $$p^{\prime } = r(w_{1}v^{n_{1}})$$ and n = n 2n 1 and show that $$p^{\prime }$$ is a rival of either p or q. We know that $$p^{\prime } \xrightarrow { s^{n} \mid z } p^{\prime }$$ for some weight $$z \in \mathbb {R}$$. Since $$p^{\prime } \in P$$, we can also find a run $$r^{p^{\prime }} \in \text {Run}_{\mathcal {A}}(u,p^{\prime })$$ which means that $$p^{\prime }$$ is a sibling of both p and q. We now have $$p^{\prime } {{\xrightarrow { s^{n} \mid z}}} p^{\prime }$$, $$p {{\xrightarrow { s^{n} \mid nx}}} p$$, and $$q {{\xrightarrow { s^{n} \mid ny}}} q$$. Since xy, we have nxz or nyz, or both. Thus, $$p^{\prime }$$ is a rival of either p or of q.
We see that $$\mathcal {A}$$ satisfies condition (ii) of the tree fork property as follows. Since we assumed pq, there exists a Γ-word $${s^{p}_{q}}$$ and a run $${r^{p}_{q}} \in \text {Run}_{\mathcal {A}}^{{\diamond }}(q,{s^{p}_{q}},p)$$. Therefore, either the 2- Γ-context $$t_{1} = t \langle {\diamond } \to w_{1} \rangle \langle {\diamond } \to w_{2}v^{n_{1}} \rangle$$ together with the run $$r {\upharpoonright }_{\text {pos}(t_{1})}$$ or the 2- Γ-context $$t_{2} = t_{1}({s^{p}_{q}}, {\diamond })$$ together with the run $$r {\upharpoonright }_{\text {pos}(t_{1})} \langle {r^{p}_{q}} \to {\Diamond }_{1}(t_{1}) \rangle$$ is a witness for condition (ii) to be satisfied. Since our assumption for this section is that $$\mathcal {A}$$ does not satisfy the tree fork property, this is a contradiction. □
We can now prove that every run of $$\mathcal {S}$$ satisfies at least one of the following two conditions. If ( p, P) and ( q, P) are rivals in $$\mathcal {S}$$ with pq, then for every run r of $$\mathcal {S}$$ on a tree t either (i) ( p, P) does not occur in r or (ii) all states with second entry P occur along a distinguished branch of t. This property enables us to apply the idea from the word case of using markers to indicate the first visit of a rival in a run. If u is a witness for ( p, P) and ( q, P) to be siblings, there is in particular a run on u which leads to ( p, P). This run then satisfies condition (ii) and since by Lemma 5(ii) the second entries of runs on the same tree coincide, all states with second entry P occur along a distinguished branch of u in every run of $$\mathcal {S}$$ on u. This is true in particular for the two rivals ( p, P) and ( q, P).
Theorem 6
Let $$(p, P), (q, P) \in Q_{\mathcal {S}}$$ be rivals in $$\mathcal {S}$$ with pq. Then for every tree tT Γ and every run $$r \in \text {Run}_{\mathcal {S}}(t)$$ of $$\mathcal {S}$$ on t, at least one of the following two conditions holds.
(i)
The state (p, P) does not occur in r, i.e., r( w)≠( p, P) for all wpos(t).

(ii)
All states with second entry P occur linearly in r, i.e., for all w 1, w 2pos( t) with π 2r( w 1) = π 2r( w 2) = P we have w 1p w 2 or w 2p w 1.

Proof
Let ( p, P),( q, P), t, r be as in the statement of the theorem. Assume that (i) does not hold, i.e., there is a position w ∈pos( t) with r( w) = ( p, P). Let w 1, w 2 ∈pos( t) be two positions with π 2r( w 1) = π 2r( w 2) = P. By Lemma 9, we see that then w 1 and w 2 are prefix-dependent on w. From the definition of the prefix relation, we see that if either w 1p w or w 2p w, then all three positions are in prefix relation. We thus consider the case that wp w 1 and wp w 2. In this case, we see from Lemma 8 that w 1 and w 2 are prefix-dependent as follows. We write w 1 = wv 1 and w 2 = wv 2 and define $$t^{\prime } = t {\upharpoonright }_{w}$$ and $$r^{\prime } = r{\upharpoonright }_{w}$$. Then we have $$r^{\prime } \in \text {Run}_{\mathcal {S}}(t^{\prime })$$, $$r^{\prime }(\varepsilon ) = (p, P)$$, and $$\pi _{2} \circ r^{\prime }(v_{1}) = \pi _{2} \circ r^{\prime }(v_{2}) = P$$. Thus, by Lemma 8 the positions v 1 and v 2 are prefix-dependent. □
In the following example, we illustrate some more complex interactions which may exist between rivals, in particular between the rivals of a Schützenberger covering.
Example 1
We extend the max-plus-WTA from Fig.  4 to an automaton $$\mathcal {A} = (\{ q_{0}, p, p^{\prime }, p^{\prime \prime }, q \}, \varGamma , \mu , \nu )$$ over the alphabet Γ = { a, b, c, d, e, f} where fΓ (3), cΓ (2), a, b, eΓ (1), and dΓ (0). As this example is somewhat complex, we first give some intuition of what we are trying to show with the example and how we achieve this.
Let $$P = \{p,p^{\prime },p^{\prime \prime },q\}$$ and let $$\mathcal {S}$$ be the Schützenberger covering of $$\mathcal {A}$$. We construct $$\mathcal {A}$$ such that it satisfies the following conditions.
(i)
$$\mathcal {A}$$ is unambiguous and does not satisfy the tree fork property. We achieve unambiguity simply by making $$\mathcal {A}$$ top-down deterministic.

(ii)
The problem showcased in Fig.  4 still occurs, i.e., a nonlinearity in the first occurrence of rivals.

(iii)
The state q is a rival of all of p, $$p^{\prime }$$, and $$p^{\prime \prime }$$.

(iv)
We have $$p^{\prime \prime } \leq q \leq p \leq q \leq p^{\prime }$$. In particular, we cannot trivially separate these states to different automata.

(v)
In $$\mathcal {S}$$, the state ( q, P) is a rival of all of ( p, P), $$(p^{\prime }, P)$$, and $$(p^{\prime \prime }, P)$$.

(vi)
In $$\mathcal {S}$$, we have $$(p^{\prime \prime }, P) \leq (q, P) \leq (p, P) \leq (q, P)$$, i.e., these three states cannot be trivially separated, and we have $$(p^{\prime \prime }, P) \leq (p^{\prime }, P)$$.

(vii)
In $$\mathcal {S}$$, the state $$(p^{\prime }, P)$$ may occur at arbitrarily many pairwise prefix-independent positions in the same run.

The sole purpose of the letter c is to ensure condition (ii). The purpose of b is to ensure conditions (iii) and (v), the purpose of a is to ensure the first part of condition (vi), the purpose of e is to ensure the second part of condition (vi), and the purpose of f is to ensure condition (vii).
It is surprising that an automaton with the properties above exists since (1) Theorem 6 tells us that whenever $$(p^{\prime \prime }, P)$$ occurs in a run, then all states with second entry P occur at pairwise prefix-dependent positions, (2) both $$(p^{\prime \prime }, P)$$ and $$(p^{\prime }, P)$$ may occur together in the same run, and (3) the state $$(p^{\prime }, P)$$ may occur at two prefix-independent positions in the same run. We define μ and ν as follows.
$$\begin{array}{@{}rcl@{}} \mu(d, q_{0}) = \mu(d, p) = \mu(d, p^{\prime}) &= 0\\ \mu(p, q_{0}, c, p) = \mu(q_{0}, p, c, q) = \mu(p^{\prime}, q_{0}, c, p^{\prime}) = \mu(p^{\prime}, q_{0}, c, p^{\prime\prime}) &= 0\\ \mu(p, b, p) = \mu(p^{\prime}, b, p^{\prime}) = \mu(p^{\prime\prime}, b, p^{\prime\prime}) &= 1\\ \mu(q, b, q) &= -1\\ \mu(p, a, q) = \mu(q, a, p) = \mu(p^{\prime}, a, p^{\prime}) = \mu(q, a, p^{\prime\prime}) &= 0\\ \mu(p,e,p) = \mu(q,e,q) = \mu(p^{\prime},e,p^{\prime}) = \mu(p^{\prime},e,p^{\prime\prime}) &= 0\\ \mu(q_{0}, p^{\prime}, q_{0}, f, q) = \mu(p^{\prime}, q_{0}, p^{\prime}, f, p^{\prime}) &= 0\\ \nu(p^{\prime\prime}) &= 0 \end{array}$$
All unspecified weights are $$-\infty$$. The trees in Fig.  8 together with the runs given on them showcase the above transitions in a more graphical way.
With witnesses u = c( d, d) and s = b(◇), we see that conditions (iii) and (v) above are satisfied. Due to $$(q, P) {{\xrightarrow {a({\diamond }) \mid 0}}} (p, P) {{\xrightarrow {a({\diamond }) \mid 0}}} (q, P) {{\xrightarrow {a({\diamond }) \mid 0}}} (p^{\prime \prime }, P)$$ and $$(p^{\prime }, P) {{\xrightarrow { e({\diamond }) \mid 0 }}} (p^{\prime \prime }, P)$$, we see that condition (vi) is also satisfied. Let $$P_{0} = \{q_{0}, p, p^{\prime } \}$$, then the tree in Fig.  9 together with the run of $$\mathcal {S}$$ on it illustrates that $$(p^{\prime }, P)$$ may occur nonlinearly, i.e., condition (vii) is satisfied as well.
This scenario does not violate Theorem 6 since $$(p^{\prime }, P)$$ can occur nonlinearly only “below” an f. By construction of $$\mathcal {A}$$, there is a prefix-minimal position labeled f in every tree which both contains an f and possesses a valid run of $$\mathcal {A}$$. Below this prefix-minimal f, only q 0 and $$p^{\prime }$$ may occur, and all occurrences of $$p,q,p^{\prime \prime }$$ are between the root and the prefix-minimal f. In $$\mathcal {S}$$, one can check that P cannot occur as the second entry of a state above the prefix-minimal f in any run; to see this, note that the second entry of the state at f is necessarily one of $$\{p^{\prime }\},\{q\},\{p^{\prime },q\}$$. Thus, if $$(p^{\prime }, P)$$ occurs nonlinearly in a run on a tree, then no run on this tree can visit any of the states $$(p, P), (q, P), (p^{\prime \prime }, P)$$.
We note that the states p and $$p^{\prime }$$ are also rivals in $$\mathcal {A}$$ with witnesses u = d and s = a( b( a(◇))). Furthermore, $$\mathcal {S}$$ contains many more rivals than the ones mentioned above, among others the rivals $$(p^{\prime }, \{p^{\prime }, q\})$$ and $$(q, \{p^{\prime }, q\})$$ with witnesses u = f( d, d, d) and s = b(◇) and the rivals $$(p, \{p, p^{\prime }, p^{\prime \prime }\})$$ and $$(p^{\prime }, \{p, p^{\prime }, p^{\prime \prime }\})$$ with witnesses u = a( f( d, d, d)) and s = a( b( a(◇))).
We are now ready to construct the automaton which tracks the first occurrences of rivals, and whose runs we will later distribute across multiple automata in order to separate all rivals.
Construction 1
Let $$R_{1}, \ldots , R_{n} \subseteq Q_{\mathcal {S}}$$ be an enumeration of all (unordered) pairs of rivals of $$\mathcal {S}$$, i.e., for all i ∈{1,…, n} we have R i = {( p i, P i),( q i, P i)} such that ( p i, P i) and ( q i, P i) are rivals in $$\mathcal {S}$$ and for every two rivals $$(p, P), (q, P) \in Q_{\mathcal {S}}$$, we have R i = {( p, P),( q, P)} for some i ∈{1,…, n}. Since by Lemma 6, we may assume that all rivals in $$\mathcal {A}$$ are in ≤-relation, we assume in the following that p i and q i are named such that p iq i for all i ∈{1,…, n}.
For each pair of rivals R i, we define a set of markers by I i = {0,| Q| + 1}∪ ({1,…,| Q|}× R i). The set of all combined records of markers is defined by I = I 1 ×… × I n. For $$\bar {a} \in I$$, we denote by $$\bar {a}[i]$$ the i-th entry of $$\bar {a}$$.
Intuitively, the states of our new automaton will consist of a state from $$\mathcal {S}$$ together with a record of markers from I. However, in order to properly update markers, we need to know in each step the records of all other runs as well. Thus, our states will be from $$Q_{\mathcal {S}} \times I \times \mathcal {P} (Q_{\mathcal {S}} \times I)$$.
In order to define the transition function of our new automaton, we first define how markers are updated. In some sense, this is similar to the context successor defined in [ 4]. Assume we transition into the state $$\mathbf {q} \in Q_{\mathcal {S}}$$, we have m subtrees below our current position in the tree, the runs we consider on these subtrees have obtained markers $$\bar {a}_{1}, \ldots , \bar {a}_{m} \in I$$, and the sets of states we could be in on these trees, together with their markers, are given by $$A_{1}, \ldots , A_{m} \subseteq Q_{\mathcal {S}} \times I$$.
Every pair $$(\mathbf {p}, \bar {a}) \in A_{k}$$ corresponds to exactly one run of $$\mathcal {S}$$ on the k-th subtree together with its markers. Since $$\mathcal {S}$$ is unambiguous, we can therefore assume that | A k|≤| Q|. Also, since $$\bar {a}_{k}$$ is the marker of a run on the k-th subtree, we may assume that $$(Q_{\mathcal {S}} \times \{ \bar {a}_{k} \}) \cap A_{k} \neq \emptyset$$.
For k ∈{1,…, m} and i ∈{1,…, n}, we define the sets of unassigned counters $$B_{k}[i] \subseteq \{1, \ldots , |Q|\}$$ by
$$B_{k}[i] = \{ 1, \ldots, |Q| \} \setminus \{ j \mid \exists (\mathbf{p}, \bar{a}) \in A_{k} \text{ with } \bar{a}[i] \in \{ j \} \times R_{i} \}.$$
Then if for all k ∈{1,…, m} we have | A k|≤| Q| and $$(Q_{\mathcal {S}} \times \{ \bar {a}_{k} \}) \cap A_{k} \neq \emptyset$$, we define the record of markers $$\bar {b}$$ for our current position by (explanations below)
$$\begin{array}{@{}rcl@{}} \bar{b}[i] = \begin{cases} 0 & \text{if } m = 0 \text{ and } \mathbf{q} \notin R_{i}\\ (1,\mathbf{q}) & \text{if } m = 0 \text{ and } \mathbf{q} \in R_{i}\\ \bar{a}_{k}[i] & \text{if } k \in \{1, \ldots, m\} \text{ satisfies:} \\ &\bar{a}_{l}[i] = 0 \text{ for all } l \neq k \text{ and either } \bar{a}_{k}[i] \neq 0 \text{ or } \mathbf{q} \notin R_{i} \\ (\min B_{k}[i], \mathbf{q}) & \text{if } \mathbf{q} \in R_{i} \text{ and } k \in \{1, \ldots, m\} \text{ satisfies: } \bar{a}_{k}[i] = 0 \text{ and}\\&\text{for all } l \neq k \text{ and all } (\mathbf{p}, \bar{a}) \in A_{l} \colon \bar{a}[i] = 0\\ |Q| + 1 & \text{otherwise} \end{cases} \end{array}$$
for i ∈{1,…, n}. If | A k| > | Q| or $$Q_{\mathcal {S}} \times \{ \bar {a}_{k} \} \cap A_{k} = \emptyset$$ for some k, we let $$\bar {b}[1] = {\ldots } = \bar {b}[n] = |Q| + 1$$.
Note that $${\min \limits } B_{k}[i]$$ in above case distinction always exists since | A k|≤| Q|, $$(Q_{\mathcal {S}} \times \{\bar {a}_{k}\}) \cap A_{k} \neq \emptyset$$, and in the case in question we have $$\bar {a}_{k}[i] = 0$$. We define $$\mathcal {I}(\mathbf {q}, \bar {a}_{1}, \ldots , \bar {a}_{m}, A_{1}, \ldots , A_{m}) = \bar {b}$$.
Case 1 of the definition above means our current position is a leaf and q is not from R i, so we assign the dummy marker 0. Case 2 means our current position is a leaf and q is from R i, so we assign the marker (1, q). Case 3 means that either (1) there is exactly one subtree below our current position which already obtained a marker different from 0 and we keep this marker for our current position, or (2) the markers of all subtrees are 0 and q is also not from R i, so we continue with the dummy marker 0.
Case 4 means the markers of all subtrees below our current position are 0, the state q is from R i, and there is at most one subtree on which runs exist that obtained a marker for R i. Then, we take the smallest number which is not already used in a marker for R i in any run on this subtree, and use this number together with q as the marker for our current position.
Case 5, the “otherwise-case”, applies in two situations. This case means that either (1) two distinct subtrees below our current position have already obtained a marker, or that (2) all markers below our current position are 0 and q is from R i, but we cannot apply case 4 as there are two distinct subtrees on which runs exist which obtained markers for R i. In other words, markers were assigned nonlinearly, and our run satisfies only condition (i) of Theorem 6. In this case, we assign the dummy marker | Q| + 1.
The extra case covers the situation where in case 4, the set B k[ i] would be empty. This case is necessary to ensure our definition is formally complete, but in our applications of the operator $$\mathcal {I}$$ it will not actually occur.
We define our “run-marking” max-plus-WTA $${\mathscr{B}} = (\tilde {Q}, \varGamma , \tilde {\mu }, \tilde {\nu })$$ as follows. We let $$\tilde {Q}^{\prime } = Q_{\mathcal {S}} \times I \times \mathcal {P} (Q_{\mathcal {S}} \times I )$$ and let $${\mathscr{B}}$$ be the trim part of the automaton $${\mathscr{B}}^{\prime } = (\tilde {Q}^{\prime }, \varGamma , \tilde {\mu }^{\prime }, \tilde {\nu }^{\prime })$$ defined for aΓ with rk Γ( a) = m and $$(\mathbf {p}_{0}, \bar {a}_{0}, A_{0}), \ldots , (\mathbf {p}_{m}, \bar {a}_{m}, A_{m}) \in Q_{\mathcal {S}} \times I \times \mathcal {P} (Q_{\mathcal {S}} \times I )$$ by
\begin{array}{@{}rcl@{}} \begin{aligned} \tilde{\mu}^{\prime}((\mathbf{p}_{1}, \bar{a}_{1}, A_{1}), \ldots, (\mathbf{p}_{m}, \bar{a}_{m}, A_{m}), a, (\mathbf{p}_{0}, \bar{a}_{0}, A_{0})) = \\ \begin{cases} \mu_{\mathcal{S}}(\mathbf{p}_{1}, \ldots, \mathbf{p}_{m}, a, \mathbf{p}_{0}) & \text{if } \bar{a}_{0} = \mathcal{I}(\mathbf{p}_{0}, \bar{a}_{1}, \ldots, \bar{a}_{m}, A_{1}, \ldots, A_{m}) \text{ and } A_{0} = {}\\ & \{ (\mathbf{q}_{0}, \bar{b}_{0}) \in Q_{\mathcal{S}} \times I \mid \exists ((\mathbf{q}_{1}, \bar{b}_{1}), \ldots, (\mathbf{q}_{m}, \bar{b}_{m})) \in {}\\ & A_{1} \times {\ldots} \times A_{m} \text{ with } \mu_{\mathcal{S}}(\mathbf{q}_{1}, \ldots, \mathbf{q}_{m}, a, \mathbf{q}_{0}) \neq -\infty\\ &\text{and } \bar{b}_{0} = \mathcal{I}(\mathbf{q}_{0}, \bar{b}_{1}, \ldots, \bar{b}_{m}, A_{1}, \ldots, A_{m}) \}\\ -\infty & \text{otherwise} \end{cases}\\ \tilde{\nu}^{\prime}(\mathbf{p}_{0}, \bar{a}_{0}, A_{0}) = \nu_{\mathcal{S}}(\mathbf{p}_{0}).{\kern10pc} \end{aligned} \end{array}
For the rest of this section, we show that the automaton $${\mathscr{B}}$$ “does what we want”: We show that $${\mathscr{B}}$$ is unambiguous, that it has the same behavior as $$\mathcal {A}$$, and that we can indeed separate its rivals by distributing runs with a different marker across different automata which then satisfy the twins property.
Let $$\tilde {\pi }_{1} \colon Q_{\mathcal {S}} \times I \times \mathcal {P} (Q_{\mathcal {S}} \times I ) \to Q_{\mathcal {S}}$$, $$(\mathbf {p}, \bar {a}, A) \mapsto \mathbf {p}$$, $$\tilde {\pi }_{2} \colon Q_{\mathcal {S}} \times I \times \mathcal {P} (Q_{\mathcal {S}} \times I ) \to I$$, $$(\mathbf {p}, \bar {a}, A) \mapsto \bar {a}$$, and $$\tilde {\pi }_{3} \colon Q_{\mathcal {S}} \times I \times \mathcal {P} (Q_{\mathcal {S}} \times I ) \to \mathcal {P}(Q_{\mathcal {S}} \times I)$$, $$(\mathbf {p}, \bar {a}, A) \mapsto A$$ be the projections. We prove the following basic observations about $${\mathscr{B}}$$.
Lemma 10
Let tT Γ be a tree. Then the following statements hold.
(i)
For every run $$r \in \text {Run}_{{\mathscr{B}}}(t)$$ we have $$(\tilde {\pi }_{1} \circ r(w), \tilde {\pi }_{2} \circ r(w)) \in \tilde {\pi }_{3} \circ r(w)$$. In particular, in the construction above the operator $$\mathcal {I}$$ is only applied to sets A k and tuples $$\bar {a}_{k}$$ with $$(Q_{\mathcal {S}} \times \{ \bar {a}_{k}\}) \cap A_{k} \neq \emptyset$$.

(ii)
For every two runs $$r_{1}, r_{2} \in \text {Run}_{{\mathscr{B}}}(t)$$ and every position wpos(t) we have $$\tilde {\pi }_{3} \circ r_{1} (w) = \tilde {\pi }_{3} \circ r_{2} (w)$$.

(iii)
For every run $$r \in \text {Run}_{{\mathscr{B}}}(t)$$ and position wpos(t) we have $$\tilde {\pi }_{3} \circ r(w) = \{ (\mathbf {q}, \bar {b}) \in Q_{\mathcal {S}} \times I \mid \exists r^{\prime } \in \text {Run}_{{\mathscr{B}}}(t {\upharpoonright }_{w})$$ with $$r^{\prime }(\varepsilon ) = (\mathbf {q}, \bar {b}, \tilde {\pi }_{3} \circ r(w)) \}$$.

(iv)
The projection $$\tilde {\pi }_{1}$$ induces a bijection $$\tilde {\pi }_{1} \colon \text {Run}_{{\mathscr{B}}}(t) \to \text {Run}_{\mathcal {S}}(t)$$ by $$r \mapsto \tilde {\pi }_{1} \circ r$$.

(v)
$${\mathscr{B}}$$ is trim, unambiguous, and satisfies $${\llbracket }{\mathcal {A}_{i}}{\rrbracket }{{\mathscr{B}}} = {\llbracket }{\mathcal {A}}{\rrbracket }$$.

(vi)
For every run $$r \in \text {Run}_{{\mathscr{B}}}(t)$$ and position wpos( t) we have $$|\tilde {\pi }_{3} \circ r(w)| \leq |Q|$$. In particular, in the construction above the operator $$\mathcal {I}$$ is only applied to sets A k with |A k|≤| Q|.

(vii)
For every Γ- word s and two states $$\tilde {p}, \tilde {q} \in \tilde {Q}$$ with $$\tilde {p} \xrightarrow {s \mid x} \tilde {q}$$, we have $$\tilde {\pi }_{1}(\tilde {p}) \xrightarrow {s \mid x} \tilde {\pi }_{1}(\tilde {q})$$.

Proof
(i)
Let tT Γ and $$r \in \text {Run}_{{\mathscr{B}}}(t)$$ and for contradiction, let w ∈pos( t) be a prefix-maximal position for which (i) does not hold. We let m = rk Γ( t( w)) and write $$r(w) = (\mathbf {p},\bar {a}, A)$$ and $$r(wj) = (\mathbf {p}_{j}, \bar {a}_{j}, A_{j})$$ for j ∈{1,…, m}. Since r is a run of $${\mathscr{B}}$$ on t, we have $$\mu _{\mathcal {S}}(\mathbf {p}_{1}, \ldots , \mathbf {p}_{m}, a, \mathbf {p}) \neq -\infty$$ and $$\bar {a} = \mathcal {I}(\mathbf {p}, \bar {a}_{1}, \ldots , \bar {a}_{m}, A_{1}, \ldots , A_{m})$$. By assumption, we have $$(\mathbf {p}_{j}, \bar {a}_{j}) \in A_{j}$$ for all j ∈{1,…, m}, so $$(\mathbf {p}, \bar {a}) \in A$$ follows from the definition of $$\tilde \pi {\mu }$$. This is a contradiction, thus w does not exist.

(ii)
Let tT Γ and $$r_{1},r_{2} \in \text {Run}_{{\mathscr{B}}}(t)$$ and let w ∈pos( t) be a prefix-maximal position for which (ii) does not hold. From the definition of $$\tilde \pi {\mu }$$, it is immediately clear that $$\tilde {\pi }_{3} \circ r_{1} (w) = \tilde {\pi }_{3} \circ r_{2} (w)$$, so w does not exist.

(iii)
Let tT Γ and $$r \in \text {Run}_{{\mathscr{B}}}(t)$$ and let w ∈pos( t) be a prefix-maximal position for which (iii) does not hold. We will deduce that (iii) holds for w. We let m = rk Γ( t( w)) and write $$r(w) = (\mathbf {p},\bar {a}, A)$$ and $$r(wj) = (\mathbf {p}_{j}, \bar {a}_{j}, A_{j})$$ for j ∈{1,…, m}.
First, let $$(\mathbf {q}, \bar {b}) \in A$$, then there are states $$((\mathbf {q}_{1}, \bar {b}_{1}), \ldots , (\mathbf {q}_{m}, \bar {b}_{m})) \in A_{1} \times {\ldots } \times A_{m}$$ with $$\mu (\mathbf {q}_{1}, \ldots , \mathbf {q}_{m}, a, \mathbf {q}) \neq -\infty$$ and $$\bar {b} = \mathcal {I}(\mathbf {q}, \bar {b}_{1},$$ $$\ldots , \bar {b}_{m}, A_{1}, \ldots , A_{m})$$. By assumption on w, for every j we find $$r_{j} \in \text {Run}_{{\mathscr{B}}}(t {\upharpoonright }_{wj})$$ with $$r_{j}(\varepsilon ) = (\mathbf {q}_{j}, \bar {b}_{j}, A_{j})$$. Then by definition of $$\tilde \pi {\mu }$$, we see that the quasi-run $$r^{\prime } \colon \text {pos}(t {\upharpoonright }_{w}) \to \tilde {Q}$$ defined by $$r^{\prime }(\varepsilon ) = (\mathbf {q}, \bar {b}, A)$$ and $$r^{\prime }(jv) = r_{j}(v)$$ is a run of $${\mathscr{B}}$$ on $$t {\upharpoonright }_{w}$$ with $$r^{\prime }(\varepsilon ) = (\mathbf {q}, \bar {b}, A)$$.
On the other hand, let $$r^{\prime } \in \text {Run}_{{\mathscr{B}}}(t {\upharpoonright }_{w})$$, with $$r^{\prime }(\varepsilon ) = (\mathbf {q}, \bar {b}, A)$$ for some $$(\mathbf {q}, \bar {b}) \in Q_{\mathcal {S}} \times I$$. Then from (i) we obtain $$(\mathbf {q}, \bar {b}) \in A$$. Thus, (iii) holds for w.

(iv)
Let tT Γ. By definition of $$\tilde {\mu }$$, it is clear that for $$r \in \text {Run}_{{\mathscr{B}}}(t)$$ we have $$\tilde {\pi }_{1} \circ r \in \text {Run}_{\mathcal {S}}(t)$$. For the injectivity of $$\tilde {\pi }_{1} \colon \text {Run}_{{\mathscr{B}}}(t) \to \text {Run}_{\mathcal {S}}(t)$$, let $$r_{1}, r_{2} \in \text {Run}_{{\mathscr{B}}}(t)$$ with $$\tilde {\pi }_{1} \circ r_{1} = \tilde {\pi }_{1} \circ r_{2}$$. Let w ∈pos( t) be a prefix-maximal position from the set { v ∈pos( t)∣ r 1( v)≠ r 2( v)}. Then $$\tilde {\pi }_{1} \circ r_{1}(w) = \tilde {\pi }_{1} \circ r_{2}(w)$$ and for all j ∈{1,…,rk Γ( t( w))} we have r 1( wj) = r 2( wj). From the definition of $$\tilde \pi {\mu }$$, it is immediately clear that r 1( w) = r 2( w) follows, i.e., w as chosen does not exist.
For surjectivity, we let $$r^{\prime } \in \text {Run}_{\mathcal {S}}(t)$$ and define a run $$r \in \text {Run}_{{\mathscr{B}}}(t)$$ inductively as follows. For a leaf w ∈pos( t), we let $$\mathbf {p} = r^{\prime }(w)$$, $$\bar {a} = \mathcal {I}(\mathbf {p})$$, $$A = \{ (\mathbf {q}_{0}, \mathcal {I}(\mathbf {q}_{0}) \mid \mu _{\mathcal {S}}(t(w), \mathbf {q}_{0}) \neq -\infty \}$$, and $$r(w) = (\mathbf {p}, \bar {a}, A)$$.
Now let w ∈pos( t) with rk Γ( t( w)) = m such that r is defined on w1,…, wm. We write $$\mathbf {p} = r^{\prime }(w)$$ and $$r(wj) = (\mathbf {p}_{j}, \bar {a}_{j}, A_{j})$$ for j ∈{1,…, m}. We let $$\bar {a}_{0} = \mathcal {I}(\mathbf {p}_{0}, \bar {a}_{1}, \ldots , \bar {a}_{m}, A_{1}, \ldots , A_{m})$$ and $$A = \{ (\mathbf {q}_{0}, \bar {b}_{0}) \in Q_{\mathcal {S}} \times I \mid \exists ((\mathbf {q}_{1}, \bar {b}_{1}), \ldots , (\mathbf {q}_{m}, \bar {b}_{m})) \in A_{1} \times {\ldots } \times A_{m} \text { with } \mu _{\mathcal {S}}(\mathbf {q}_{1}, \ldots , \mathbf {q}_{m}, a, \mathbf {q}_{0}) \neq -\infty \text { and } \bar {b}_{0} = \mathcal {I}(\textbf {q}_{0}, \bar {b}_{1}, \ldots , \bar {b}_{m}, A_{1}, \ldots , A_{m}) \}$$, and $$r(w) = (\mathbf {p}, \bar {a}, A)$$. Thus, we obtain a run $$r \in \text {Run}_{{\mathscr{B}}}(t)$$ with $$\tilde {\pi }_{1} \circ r (w) = r^{\prime }$$.

(v)
$${\mathscr{B}}$$ is trim by definition. Let tT Γ. By definition of $$\tilde \pi {\mu }$$, for every run $$r \in \text {Run}_{\mathcal {S}}(t)$$ we have $$\text {wt}_{{\mathscr{B}}}(t, r) = \text {wt}_{\mathcal {S}}(t, \tilde {\pi }_{1} \circ r)$$. By definition of $$\tilde \pi {\nu }$$, we also have $$\tilde \pi {\nu }(r(\varepsilon )) = \nu (\tilde {\pi }_{1} \circ r(\varepsilon ))$$. By (iv), we have $$|\text {Acc}_{{\mathscr{B}}}(t)| = |\text {Acc}_{\mathcal {S}}(t)| \leq 1$$, which means $${\mathscr{B}}$$ is unambiguous, and we have $${\llbracket }{\mathcal {A}_{i}}{\rrbracket }{{\mathscr{B}}}(t) = {\llbracket }\mathcal {S}{\rrbracket }(t) = {\llbracket }{\mathcal {A}}{\rrbracket }(t)$$.

(vi)
The automaton $$\mathcal {A}$$ is assumed to be trim and unambiguous, so we have $$|\text {Run}_{\mathcal {A}}(t)| \leq |Q|$$ for every tT Γ. Furthermore, the projections π 1 and $$\tilde {\pi }_{1}$$ are bijections by Lemma 5(iii) and (iv) above. Let tT Γ, $$r \in \text {Run}_{{\mathscr{B}}}(t)$$, and w ∈pos( t). From (iii), we see that $$|\tilde {\pi }_{3} \circ r(w)| \leq |\text {Run}_{{\mathscr{B}}}(t {\upharpoonright }_{w})| = |\text {Run}_{\mathcal {S}}(t {\upharpoonright }_{w})| = |\text {Run}_{\mathcal {A}}(t {\upharpoonright }_{w})| \leq |Q|$$.

(vii)
Let s be a Γ-word and $$\tilde {p}, \tilde {q} \in \tilde {Q}$$ be two states with $$\tilde {p} {{\xrightarrow {s \mid x}}} \tilde {q}$$, then there is a run $$r \in \text {Run}_{{\mathscr{B}}}^{{\diamond }}{({\tilde {p}},s,\tilde {q})}$$ with $$\text {wt}_{{\mathscr{B}}}^{{\diamond }}(s,r) = x$$. By definition of $$\tilde {\mu }$$, we have $$\tilde \pi {1} \circ r \in \text {Run}_{\mathcal {S}}^{{\diamond }}(s)$$ and $$\text {wt}_{{\mathscr{B}}}^{{\diamond }}(s, r) = \text {wt}_{\mathcal {S}}^{{\diamond }}(s, \tilde {\pi }_{1}(r))$$, so we have $$\tilde {\pi }_{1}(\tilde {p}) \xrightarrow {s \mid x} \tilde \pi {1}(\tilde {q})$$.

Next, we prove two basic statements about how $${\mathscr{B}}$$ sets markers. Assume we have some run in which a state $$(\mathbf {p}, \bar {a}, A)$$ occurs. First, we show that if $$\bar {a}[i] \neq 0$$ for some i, then in the past, we must have visited one of the rivals in R i. Second, we show that if A contains a state $$(\mathbf {q}, \bar {b})$$ with $$\bar {b}[i] \neq 0$$ for some i, then we must have visited some state with second entry P i in the past.
Lemma 11
Let tT Γ be a tree, $$r \in \text {Run}_{{\mathscr{B}}}(t)$$ be a run of $${\mathscr{B}}$$ on t, let wpos(t) be a position in t, assume that $$r(w) = (\mathbf {p}, \bar {a}, A)$$, and let i ∈{1,…, n}. Then the following statements hold.
(i)
If $$\bar {a}[i] \neq 0$$, then there is a position vpos( t) with wp v and $$\tilde {\pi }_{1} \circ r(v) \in R_{i}$$.

(ii)
If there exists $$(\mathbf {q}, \bar {b}) \in A$$ with $$\bar {b}[i] \neq 0$$, then there is a position vpos(t) with wp v such that $$\pi _{2} \circ \tilde {\pi }_{1} \circ r(v) = P_{i}$$.

Proof
(i)
Assume $$\bar {a}[i] \neq 0$$. We choose v prefix-maximal from the set $$\{ w^{\prime } \in \text {pos}(t) \mid w \leq _{p} w^{\prime } \text { and } r(w^{\prime }) = (\mathbf {q}, \bar {b}, B) \text { with } \bar {b}[i] \neq 0\}$$. This set is not empty since it contains w. We write $$r(v) = (\mathbf {q}, \bar {b}, B)$$. If qR i would hold, we see from the definition of $$\tilde {\mu }$$, the definition of the operator $$\mathcal {I}$$, and the fact that we chose v prefix-maximal from above set, that either case 1 or case 3 of the definition of $$\mathcal {I}$$ would apply in the definition of $$\bar {b}[i]$$. Thus, $$\bar {b}[i] = 0$$ would hold, which is not the case. Therefore, qR i holds.

(ii)
Assume there is $$(\mathbf {q}, \bar {b}) \in A$$ with $$\bar {b}[i] \neq 0$$. By Lemma 10(iii), there is a run $$r^{\prime } \in \text {Run}_{{\mathscr{B}}}(t {\upharpoonright }_{w})$$ with $$r^{\prime }(\varepsilon ) = (\mathbf {q}, \bar {b}, A)$$. Then by (i), there exists $$v \in \text {pos}(t {\upharpoonright }_{w})$$ with $$\tilde {\pi }_{1} \circ r^{\prime }(v) \in R_{i}$$. Furthermore, we have $$r {\upharpoonright }_{w} \in \text {Run}_{{\mathscr{B}}}(t {\upharpoonright }_{w})$$. Combining Lemma 10(iv) and Lemma 5(ii), we have $$P_{i} = \pi _{2} \circ \tilde {\pi }_{1} \circ r^{\prime }(v) = \pi _{2} \circ \tilde {\pi }_{1} \circ r {\upharpoonright }_{w}(v)$$. Thus, we see that $$\pi _{2} \circ \tilde {\pi }_{1} \circ r(wv) = P_{i}$$.

Next, we essentially prove that markers for R i are properly set in runs where states with P i as a second entry occur only linearly. That is, we show that in these runs, a marker for R i is only set when a rival from R i is actually visited, and that it cannot be altered afterwards.
Lemma 12
Let tT Γ, i ∈{1,…, n}, and $$r \in \text {Run}_{{\mathscr{B}}}(t)$$ such that for all positions v 1, v 2pos(t) with $$\pi _{2} \circ \tilde {\pi }_{1} \circ r(v_{1}) = \pi _{2} \circ \tilde {\pi }_{1} \circ r(v_{2}) = P_{i}$$ we have v 1p v 2 or v 2p v 1. If wpos(t) is the prefix-largest position of t with $$\tilde {\pi }_{1} \circ r(w) \in R_{i}$$ then the following properties are satisfied
(i)
The marker $$\tilde {\pi }_{2} \circ r(w)$$ is defined using case 2 or case 4 of the definition of the operator $$\mathcal {I}$$.

(ii)
For all positions vpos(t) with vp w we have $$\tilde {\pi }_{2} \circ r(v)[i] = \tilde {\pi }_{2} \circ r(w)[i] \in \{1, \ldots , |Q| \} \times \{ \tilde {\pi }_{1} \circ r(w) \}$$.

(iii)
For all positions vpos(t) ∖{ w} such that either v and w are prefix-independent or wp v, we have $$\tilde {\pi }_{2} \circ r(v)[i] = 0$$.

Proof
Let m = rk Γ( t( w)). If m = 0, $$\tilde {\pi }_{2} \circ r(w)[i]$$ is obviously defined using case 2. Otherwise, since w is the prefix-largest among all positions $$w^{\prime }$$ with $$\tilde {\pi }_{1} \circ r(w^{\prime }) \in R_{i}$$, we have by Lemma 11(i) that $$\tilde {\pi }_{2} \circ r(v)[i] = 0$$ for all v ∈pos( t) ∖{ w} with wp v. In particular, we have $$\tilde {\pi }_{2} \circ r(wj)[i] = 0$$ for all j ∈{1,…, m}. Thus, by Lemma 11(ii) and our assumptions on r and w, we see that case 4 of the definition of the operator $$\mathcal {I}$$ applies in the definition of $$\tilde {\pi }_{2} \circ r(w)[i]$$. Thus, $$\tilde {\pi }_{2} \circ r(w)[i] \in \{1, \ldots , |Q| \} \times \{ \tilde {\pi }_{1} \circ r(w) \}$$.
We show (ii). For contradiction, let v ∈pos( t) be the prefix-largest position with vp w and $$\tilde {\pi }_{2} \circ r(v)[i] \neq \tilde {\pi }_{2} \circ r(w)[i]$$. Let m = rk Γ( t( v)) and j ∈{1,…, m} such that $$w = v j v^{\prime }$$ for some $$v^{\prime }$$. Then $$\tilde {\pi }_{2} \circ r(vj)[i] = \tilde {\pi }_{2} \circ r(w)[i] \neq 0$$, and by Lemma 11(i) and our assumption on r, we have $$\tilde {\pi }_{2} \circ r(vk)[i] = 0$$ for all kj. Thus, case 3 of the definition of $$\mathcal {I}$$ applies in the definition of $$\tilde {\pi }_{2} \circ r(v)[i]$$, so $$\tilde {\pi }_{2} \circ r(v)[i] = \tilde {\pi }_{2} \circ r(vj)[i] = \tilde {\pi }_{2} \circ r(w)[i]$$. This means v as chosen does not exist.
Finally let v ∈pos( t) ∖{ w} be such that either v and w are prefix-independent or wp v. Then from Lemma 11(i) and our assumption on r we immediately obtain $$\tilde {\pi }_{2} \circ r(v)[i] = 0$$. □
In the next lemma, we show that if two states are rivals in $${\mathscr{B}}$$, then their records of markers differ. The reasoning for this is exactly the same as in our intuitive description at the beginning of this section.
Lemma 13
If $$(\mathbf {p}, \bar {a}, A)$$ and $$(\mathbf {q}, \bar {b}, B)$$ are rivals in $${\mathscr{B}}$$, then p and q are rivals in $$\mathcal {S}$$ and for i ∈{1,…, n} with R i = { p, q}, we have $$\bar {a}[i] \neq \bar {b}[i]$$ and $$\bar {a}[i], \bar {b}[i] \in \{1, \ldots , |Q| \} \times \{\mathbf {p}, \mathbf {q} \}$$.
Proof
Let $$\tilde {p} = (\mathbf {p}, \bar {a}, A)$$ and $$\tilde {q} = (\mathbf {q}, \bar {b}, B)$$ be rivals in $${\mathscr{B}}$$. Let u and s be as in the definition of rivals and let $$r^{\tilde {p}} \in \text {Run}_{{\mathscr{B}}}^{{\diamond }}(u,\tilde {p})$$ and $$r^{\tilde {q}} \in \text {Run}_{{\mathscr{B}}}^{{\diamond }}(u,\tilde {q})$$. Then by Lemma 10(iv), we have $$\tilde {\pi }_{1}(r^{\tilde {p}}) \in \text {Run}_{\mathcal {S}}(u, \mathbf {p})$$ and $$\tilde {\pi }_{1}(r^{\tilde {q}}) \in \text {Run}_{\mathcal {S}}(u, \mathbf {q})$$. By Lemma 10(vii), we also have $$\mathbf {p} \xrightarrow {s \mid x} \mathbf {p}$$ and $$\mathbf {q} {{\xrightarrow {s \mid y}}} \mathbf {q}$$ with xy, thus p and q are rivals in $$\mathcal {S}$$. Let i ∈{1,…, n} with R i = { p, q}. We may assume that p = ( p i, P i) and q = ( q i, P i).
We show that $$\bar {a}[i], \bar {b}[i] \notin \{ 0, |Q| + 1 \}$$. We let $$r^{\mathbf {p}} = \tilde {\pi }_{1} \circ r^{\tilde {p}}$$ and $$r^{\mathbf {q}} = \tilde {\pi }_{1} \circ r^{\tilde {q}}$$. We have r p( ε) = ( p i, P i) and we assumed p iq i, so by Theorem 6 we obtain that for every two positions v 1, v 2 ∈pos( u) with π 2r p( v 1) = π 2r p( v 2) = P i, we have v 1p v 2 or v 2p v 1. This also holds for r q since by by Lemma 5(ii) we have π 2r p = π 2r q.
Let w p ∈pos( u) be the prefix-largest position of u with r p( w p) ∈ R i and w q ∈pos( u) be the prefix-largest position with r q( w q) ∈ R i. That w p and w q exist is clear from the fact that r p( ε) ∈ R i and r q( ε) ∈ R i. By Lemma 12(ii), we have $$\bar {a}[i] = \tilde {\pi }_{2} \circ r^{\tilde {p}}(w_{p})[i] \in \{1, \ldots , |Q| \} \times \{ \tilde {\pi }_{1} \circ r^{\tilde {p}}(w_{p}) \}$$ and $$\bar {b}[i] = \tilde \pi _{2} \circ r^{\tilde {q}}(w_{q})[i] \in \{1, \ldots , |Q| \} \times \{ \tilde {\pi }_{1} \circ r^{\tilde {q}}(w_{q}) \}$$.
We show that $$\bar {a}[i] \neq \bar {b}[i]$$ and consider two cases. First, if w p = w q we assume for contradiction that $$\bar {a}[i] = \bar {b}[i]$$. Then we see that r p( w p) = r q( w q) ∈ R i, and we also have r p( ε) = p and r q( ε) = q. It follows that with s = u〈◇→ w p〉, we have $$\pi _{1} \circ r^{\mathbf {p}}(w_{p}) {{\xrightarrow {s \mid z_{1}}}} p_{i}$$ and $$\pi _{1} \circ r^{\mathbf {p}}(w_{p}) \xrightarrow {s \mid z_{2}} q_{i}$$ for weights $$z_{1},z_{2} \in \mathbb {R}$$. Thus, $$\mathcal {A}$$ satisfies condition (i) of the tree fork property, which is a contradiction. Therefore, $$\bar {a}[i] = \bar {b}[i]$$ cannot hold when w p = w q.
Now assume without loss of generality that w pp w q with w pw q and write w q = w p jv and $$r^{\tilde \pi {q}}(w_{p}j) = (\mathbf {q}^{\prime }, \bar {b}^{\prime }, A_{j})$$. By Lemma 10(i) and Lemma 10(ii), we then have $$(\mathbf {q}^{\prime }, \bar {b}^{\prime }) \in A_{j} = \tilde {\pi }_{3} \circ r^{\tilde {p}}(w_{p}j)$$. By Lemma 12(i), we know that $$\tilde \pi _{2} \circ r^{\tilde {p}}(w_{p})[i]$$ is defined using case 4 of the definition of $$\mathcal {I}$$, so $$\bar {a}[i] \neq \bar {b}[i]$$ must hold. □
We turn to our final construction where we distribute the runs of $${\mathscr{B}}$$ across multiple automata. For every record of markers $$\bar {c} \in I$$, we construct one automaton $${\mathscr{B}}_{\bar {c}}$$ which for each pair of rivals R i admits only runs using the markers 0 and $$\bar {c}[i]$$. All runs in which rivals occur nonlinearly are covered by admitting the marker | Q| + 1. All other runs are covered by admitting an appropriate marker from {1,…,| Q|}× R i.
Construction 2
For every tuple $$\bar {c} \in I$$, we define a max-plus-WTA $${\mathscr{B}}_{\bar {c}} = (\tilde {Q}_{\tilde {c}}, \varGamma , \tilde {\mu }, \tilde {\nu })$$ by removing states from $${\mathscr{B}}$$ through
\begin{array}{@{}rcl@{}} \tilde{Q}_{\bar{c}} &= \{ (\mathbf{p}, \bar{a}, A) \in \tilde{Q} \mid \begin{aligned}[t] &\text{for all } i \in \{ 1, \ldots, n \} \text{ it holds:}\\ &\text{if } \bar{c}[i] = |Q| + 1 \text{ then } \mathbf{p} \neq (p_{i}, P_{i}) , \text{and}\\ &\text{if } \bar{c}[i] \neq |Q| + 1 \text{ then } \bar{a}[i] \in \{ 0, \bar{c}[i] \} \}. \end{aligned} \end{array}
Finally, we formally prove that the automata $${\mathscr{B}}_{\bar {c}}$$ are unambiguous, that their pointwise maximum is equivalent to the behavior of $$\mathcal {A}$$, and that they all satisfy the twins property, which means that they can be determinized. We note that the construction of the automata $${\mathscr{B}}_{\bar {c}}$$ is optimized for provability, so we omit analyzing their size and the complexity of their construction.
Theorem 7
We have $${\llbracket }{\mathcal {A}}{\rrbracket } = \max \limits _{\bar {c} \in I} {\llbracket }{{\mathscr{B}}_{\bar {c}}{\rrbracket }}$$ and for every $$\bar {c} \in I$$, the automaton $${\mathscr{B}}_{\bar {c}}$$ is unambiguous and satisfies the twins property.
Proof
The unambiguity of $${\mathscr{B}}_{\bar {c}}$$ follows from the unambiguity of $${\mathscr{B}}$$. To see that $${\mathscr{B}}_{\bar {c}}$$ satisfies the twins property, let $$(\mathbf {p}, \bar {a}, A),(\mathbf {q}, \bar {b}, B) \in \tilde {Q}_{\bar {c}}$$ be rivals in $${\mathscr{B}}_{\bar {c}}$$. Then $$(\mathbf {p}, \bar {a}, A)$$ and $$(\mathbf {q}, \bar {b}, B)$$ are also rivals in $${\mathscr{B}}$$, so by Lemma 13 for some i ∈{1,…, n} we have $$\bar {a}[i] \neq \bar {b}[i]$$ and $$\bar {a}[i], \bar {b}[i] \notin \{0, |Q| + 1 \}$$. By definition of $${\mathscr{B}}_{\bar {c}}$$, this means $$(\mathbf {p}, \bar {a}, A),(\mathbf {q}, \bar {b}, B) \in \tilde {Q}_{\bar {c}}$$ is impossible, so there are no rivals in $${\mathscr{B}}_{\bar {c}}$$ and $${\mathscr{B}}_{\bar {c}}$$ satisfies the twins property.
To show that $${\llbracket }{\mathcal {A}}{\rrbracket } = \max \limits _{\bar {c} \in I} {\llbracket }{{\mathscr{B}}_{\bar {c}}{\rrbracket }}$$, we show that for every tree tT Γ we have $$\text {Run}_{{\mathscr{B}}}(t) = \bigcup _{\bar {c} \in I} \text {Run}_{{\mathscr{B}}_{\bar {c}}}(t)$$. From this, it follows that $$\max \limits _{\bar {c} \in I} {\llbracket }{{\mathscr{B}}_{\bar {c}}{\rrbracket }} = {\llbracket }{{\mathscr{B}}}{\rrbracket } = {\llbracket }{\mathcal {A}}{\rrbracket }$$. The inclusion “ $$\supseteq$$” is clear.
Let tT Γ, $$r \in \text {Run}_{{\mathscr{B}}}(t)$$, and let O = { i ∈{1,…, n}∣ there is a position $$w \in \text {pos}(t) \text { with } \tilde {\pi }_{1} \circ r(w) = (p_{i}, P_{i})\}$$. Let iO and assume we have two positions v 1, v 2 ∈pos( t) such that $$\pi _{2} \circ \tilde {\pi }_{1} \circ r(v_{1}) = \pi _{2} \circ \tilde {\pi }_{1} \circ r(v_{2}) = P_{i}$$. Then, since $$\tilde {\pi }_{1}(r) \in \text {Run}_{\mathcal {S}}(t)$$ by Lemma 10(iv), we obtain by Theorem 6 that v 1p v 2 or v 2p v 1. We can therefore let w i ∈pos( t) be the prefix-largest position in t with $$\tilde {\pi }_{1} \circ r(w_{i}) \in R_{i}$$. Then from Lemma 12(ii) and Lemma 12(iii), we obtain that for all positions v ∈pos( t) with vp w i we have $$\tilde {\pi }_{2} \circ r(v)[i] = \tilde {\pi }_{2} \circ r(w_{i})[i] \in \{1, \ldots , |Q| \} \times \{ \tilde {\pi }_{1} \circ r(w_{i}) \}$$, and for all other positions v ∈pos( t) we have $$\tilde {\pi }_{2} \circ r(v)[i] = 0$$.
We define a tuple $$\bar {c} \in I$$ as follows. If iO, we let $$\bar {c}[i] = \tilde {\pi }_{2} \circ r(w_{i})[i]$$, where w i is defined as above. If iO, we let $$\bar {c}[i] = |Q| + 1$$. Then we have $$r \in \text {Run}_{{\mathscr{B}}_{\bar {c}}}(t)$$. Thus, $$\text {Run}_{{\mathscr{B}}}(t) = \bigcup _{\bar {c} \in I} \text {Run}_{{\mathscr{B}}_{\bar {c}}}(t)$$. □
We now obtain a finitely sequential representation of $$\mathcal {A}$$ by applying Theorem 1 to the automata $${\mathscr{B}}_{\bar {c}}$$. In particular, we see that the behavior of a trim unambiguous max-plus-WTA is finitely sequential if it does not satisfy the tree fork property. This concludes the proof of Theorem 3.

## 4 Further Insights

In this section, we show some additional properties of the rivals of the Schützenberger covering $$\mathcal {S}$$. These properties are not necessary for the proof of Theorem 3, but they do give a better idea of the limits of interaction there may exist between the rivals of $$\mathcal {S}$$. Also, they reveal a different approach we could have taken to the constructions in Section  3.2.
If two rivals ( p, P) and ( q, P) of $$\mathcal {S}$$ cannot occur together in the same run, they can be trivially separated like in Lemma 6. Therefore, in the following we only consider the case that ( p, P) ≤ ( q, P). Under this assumption, the first property we show is that Theorem 6 is true even if we replace ( p, P) by ( q, P) in (i), i.e., we have the following theorem.
Theorem 8
Let $$(p, P), (q, P) \in Q_{\mathcal {S}}$$ be rivals in $$\mathcal {S}$$ with pq. Then for every tree tT Γ and every run $$r \in \text {Run}_{\mathcal {S}}(t)$$ of $$\mathcal {S}$$ on t, at least one of the following two conditions holds.
(i)
The state (q, P) does not occur in r, i.e., r( w)≠( q, P) for all wpos(t).

(ii)
All states with second entry P occur linearly in r, i.e., for all w 1, w 2pos( t) with π 2r( w 1) = π 2r( w 2) = P we have w 1p w 2 or w 2p w 1.

Theorem 8 follows from Theorem 6 by applying Lemma 14 below. In short, Lemma 14 tells us that from ( p, P) ≤ ( q, P), it follows that there is a rival $$(q^{\prime }, P)$$ of ( q, P) with $$(q, P) \leq (q^{\prime }, P)$$. Thus, Theorem 8 follows by applying Theorem 6 to the rivals ( q, P) and $$(q^{\prime }, P)$$. Together, Theorems 6 and 8 tell us that whenever we have two rivals ( p, P) and ( q, P) with ( p, P) ≤ ( q, P) in $$\mathcal {S}$$, then whenever one of ( p, P), ( q, P) occurs in a run on a tree t, then for every run on that tree all states with second entry P occur along a distinguished branch of t. We prove Lemma 14.
Lemma 14
Let $$(p, P), (q, P) \in Q_{\mathcal {S}}$$ be rivals in $$\mathcal {S}$$ with witnesses u and s such that (p, P) ≤ ( q, P). Then there exists a state $$q^{\prime } \in P$$ with $$(q, P) \leq (q^{\prime }, P)$$ such that $$(q^{\prime }, P)$$ and (q, P) are rivals in $$\mathcal {S}$$ with witnesses u and s n for some n ≥ 1.
Proof
Let ( p, P), ( q, P), u, and s be as in the statement of the lemma. Furthermore, let $$s^{\prime }$$ be a Γ-word such that $$\text {Run}_{\mathcal {S}}^{{\diamond }}((q,P), s^{\prime }, (p,P)) \neq \emptyset$$, which exists due to ( p, P) ≤ ( q, P)
By construction of $$\mathcal {S}$$ and our assumption on $$s^{\prime }$$, there exists for every $$p^{\prime } \in P$$ at least one $$q^{\prime } \in P$$ with $$\text {Run}_{\mathcal {S}}^{{\diamond }}((q^{\prime }, P), s^{\prime }, (p^{\prime }, P) ) \neq \emptyset$$. On the other hand, we obtain from the unambiguity of $$\mathcal {S}$$ that for every $$p^{\prime } \in P$$, there can be at most one $$q^{\prime } \in P$$ with $$\text {Run}_{\mathcal {S}}^{{\diamond }}((q^{\prime }, P), s^{\prime }, (p^{\prime }, P) ) \neq \emptyset$$. It follows that $$s^{\prime }$$ induces a mapping g: PP which maps $$p^{\prime }$$ to $$q^{\prime }$$ if $$\text {Run}_{\mathcal {S}}^{{\diamond }}((q^{\prime }, P), s^{\prime }, (p^{\prime }, P) ) \neq \emptyset$$ and g satisfies pq. With an identical argumentation, we obtain that s induces a mapping h: PP which maps $$p^{\prime }$$ to $$q^{\prime }$$ if $$\text {Run}_{\mathcal {S}}^{{\diamond }}((q^{\prime }, P), s, (p^{\prime }, P) ) \neq \emptyset$$ and h satisfies pp and qq.
Let $$R^{\prime }$$ be the smallest set satisfying $$q \in R^{\prime }$$, $$g(R^{\prime }) \subseteq R^{\prime }$$, and $$h(R^{\prime }) \subseteq R^{\prime }$$, i.e., such that $$R^{\prime }$$ contains q and is closed under g and h. Then let $$R = \{p \} \cup R^{\prime }$$ and let p 1,…, p m be an enumeration of R. By pigeon hole principle, there exist integers 0 ≤ n 1 < n 2 such that $$(h^{n_{1}}(g(p_{1})), \ldots , h^{n_{1}}(g(p_{m}))) = (h^{n_{2}}(g(p_{1})), \ldots , h^{n_{2}}(g(p_{m})))$$. By definition of R and the fact that g( p) = q, we have $$h^{n_{1}}(g(p_{1})), \ldots , h^{n_{1}}(g(p_{m})) \in R$$. Thus, $$f = h^{n_{1}} \circ g$$ is a mapping f : RR and we can apply Lemma 7 to f with a = p. We obtain $$q^{\prime } \in R$$ and n ≥ 1 with $$f^{n}(p) = q^{\prime } = f^{n}(q^{\prime })$$. From the definitions of h and g, it follows that $$(s^{\prime }(s^{n_{1}}))^{n}$$ is a $$(q^{\prime }, P)$$-( p, P)-fork, and therefore also a $$q^{\prime }$$- p-fork. Since $$\mathcal {A}$$ does not satisfy the tree fork property, $$q^{\prime }$$ is therefore not a rival of p. Moreover, we have $$f^{n-1} \circ h^{n_{1}}(q) = f^{n}(p) = q^{\prime }$$, so we see that $$\text {Run}_{\mathcal {S}}^{{\diamond }}((q^{\prime },P), s^{n_{1}}((s^{\prime }(s^{n_{1}}))^{n-1} ), (q,P) ) \neq \emptyset$$ and therefore $$(q, P) \leq (q^{\prime }, P)$$.
Due to the fact that $$h^{n_{2} - n_{1}}(q^{\prime }) = q^{\prime }$$, we see from the definition of h that $$(q^{\prime }, P) \xrightarrow {s^{n_{2} - n_{1}} \mid z} (q^{\prime }, P)$$ for some $$z \in \mathbb {R}$$. Let k = n 2n 1. We know that $$(p, P) {{\xrightarrow {s \mid x}}} (p, P)$$ and $$(q, P) \xrightarrow {s \mid y} (q, P)$$ for some $$x,y \in \mathbb {R}$$ with xy. It follows that $$(p, P) {{\xrightarrow {s^{k} \mid kx}}} (p, P)$$ and $$(q, P) {{\xrightarrow {s^{k} \mid ky}}} (q, P)$$, so $$(q^{\prime }, P)$$ is either a rival of ( p, P) or of ( q, P) with witnesses u and s k. As $$(q^{\prime }, P)$$ and ( p, P) being rivals implies by Lemma 5(vii) that $$q^{\prime }$$ and p are rivals in $$\mathcal {A}$$ and we found that the latter is not the case, it must hold that $$(q^{\prime }, P)$$ and ( q, P) are rivals. □
Now assume that ( p, P) and $$(q, P) \in Q_{\mathcal {S}}$$ with ( p, P) ≤ ( q, P) are rivals in $$\mathcal {S}$$ with witnesses u and s. Furthermore, assume ( p 1, P) and ( p 2, P) may occur at prefix-independent positions, i.e., there is a tree tT Γ, prefix-independent positions w 1, w 2 ∈pos( t), and a run $$r \in \text {Run}_{\mathcal {S}}(t)$$ with r( w 1) = ( p 1, P) and r( w 2) = ( p 2, P). In the following, we want to analyze how ( p 1, P) may occur together with ( p, P) or ( q, P) in a run.
First, Theorems 6 and 8 tell us that ( p 1, P) may not occur prefix-independently from ( p, P) and ( q, P). Second, if ( p 1, P) ≤ ( p, P) or ( p 1, P) ≤ ( q, P), then by our assumption the state ( p 2, P) may occur prefix-independently from ( p, P) or ( q, P). This is impossible again by Theorems 6 and 8, so ( p 1, P) ≤ ( p, P) and ( p 1, P) ≤ ( q, P) both cannot hold. Third, we know that $$\text {Run}_{\mathcal {S}}(s^{|P|}(u), (p_{1}, P)) \neq \emptyset$$, from which follows that there is some $$\hat {p} \in P$$ and an integer k ≥ 1 with $$(p_{1}, P) \leq (\hat {p}, P)$$ and $$\text {Run}_{\mathcal {S}}^{{\diamond }}((\hat {p}, P), s^{k}, (\hat {p}, P) ) \neq \emptyset$$. Thus, $$(\hat {p}, P)$$ is a rival of either ( p, P) or ( q, P) and by our assumption, it may occur prefix-independently from ( p 2, P). Then if ( q, P) ≤ ( p 1, P) held, we would have $$(p, P) \leq (q, P) \leq (p_{1}, P) \leq (\hat {p}, P)$$. By applying Theorem 8 either to ( p, P) and $$(\hat {p}, P)$$ or to ( q, P) and $$(\hat {p}, P)$$, we see that ( p 2, P) may not occur prefix-independently from $$(\hat {p}, P)$$, which does not match our assumption. It follows that ( q, P) ≤ ( p 1, P) is also impossible. Finally, the only remaining possibility is ( p, P) ≤ ( p 1, P). This is in fact possible, as shown in Example 1, where we have $$(p^{\prime \prime }, P) \leq (q, P)$$, $$(p^{\prime \prime }, P) \leq (p^{\prime }, P)$$, and $$(p^{\prime }, P)$$ may occur at prefix-independent positions.
In conclusion, we obtain that if ( p, P) and ( q, P) are rivals in $$\mathcal {S}$$ with ( p, P) ≤ ( q, P), then all states with second entry P which can occur at prefix-independent positions can be trivially separated from ( q, P) as they may never occur in the same run. We decided not to employ this fact in Section  3.2 as doing so does not lead to a shorter proof or a significantly simpler construction.