Finite Sequentiality of Unambiguous Max-Plus Tree Automata

We show the decidability of the finite sequentiality problem for unambiguous max-plus tree automata. A max-plus tree automaton is called unambiguous if there is at most one accepting run on every tree. The finite sequentiality problem asks whether for a given max-plus tree automaton, there exist finitely many deterministic max-plus tree automata whose pointwise maximum is equivalent to the given automaton.


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 maxplus 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.

Preliminaries
For a set X, we denote the power set of X by P(X) and the cardinality of X by |X|. For two sets X and Y and a mapping f : X → Y , 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 ⊆ X, we call the set f (X ) = {y ∈ Y | ∃x ∈ X : f (x) = y} the image or range of X under f . The restriction of f to X , denoted by f X , is the mapping f X : X → Y defined by f X (x) = f (x) for every x ∈ X . For an element y ∈ Y , we call the set f −1 (y) = {x ∈ X | f (x) = y} the preimage of y under f . For a second mapping g : X → Y , we write f = g if for all x ∈ X we have f (x) = g (x).
Let N = {0, 1, 2, . . .}. By N * we denote the set of all finite words over N. The empty word is denoted by ε, and the length of a word w ∈ N * by |w|. The set N * is partially ordered by the prefix relation ≤ p and totally ordered with respect to the lexicographic ordering ≤ l . Two words from 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 rk Γ : Γ → N a mapping which assigns a rank to every symbol. For every The set of (finite, labeled, and ordered) Γ -trees, denoted by T Γ , is the set of all pairs t = (pos(t), label t ), where pos(t) ⊂ 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 height(t) = max w∈pos(t) |w|. For a leaf w ∈ pos(t), the set {v ∈ pos(t) | v ≤ p w} is called a branch of t. Now let s, t ∈ T Γ and w ∈ pos(t). The subtree of t at w, denoted by t w , is a Γ -tree defined as follows. We let pos(t w ) = {v ∈ N * | wv ∈ pos(t)} and for v ∈ pos(t w ), we let label t w (v) = t (wv).
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 maxplus semiring R max = (R ∪ {−∞}, max, +, −∞, 0) where the sum and the product operations are max and +, respectively, extended to R ∪ {−∞} in the usual way.
A max-plus weighted bottom-up finite state tree automaton (short: max-plus-WTA) over Γ is a tuple A = (Q, Γ, μ, ν) where Q is a finite set (of states), Γ is a ranked alphabet (of input symbols), μ : the function of transition weights), and ν : Q → R max (the function of final weights). We define For a tree t ∈ T Γ , a mapping r : pos(t) → Q is called a quasi-run of A on t. For a quasi-run r on t and a position w ∈ pos(t) with t (w) = a ∈ Γ (m) , the tuple t(t, r, w) = (r(w1), . . . , r(wm), a, r(w)) is called the transition at w. The quasi-run r is called a (valid) run if for every w ∈ pos(t) the transition t(t, r, w) is valid with respect to A. We call a run r accepting if r(ε) is final. By Run A (t) and Acc A (t) we denote the sets of all runs and all accepting runs of A on t, respectively. For a state q ∈ Q, we denote by Run A (t, q) the set of all runs r ∈ Run A (t) such that r(ε) = q.
For a run r ∈ Run A (t), the weight of r is defined by μ(t(t, r, w)).
The behavior of A, denoted by A , is the mapping defined for every t ∈ T Γ by where the maximum over the empty set is −∞ by convention. For a max-plus-WTA A = (Q, Γ, μ, ν), a run of A on a Γ -context t is a run of the max-plus- For an n-Γ -context t ∈ T Γ and states q 0 , . . . , q n , we denote by Run A (q 1 , . . . , q n , t, q 0 ) the set of all runs r ∈ Run A (t) such that r(ε) = q 0 and r(♦ i (t)) = q i for every i ∈ {1, . . . , n}. For a Γ -word s, we write p s|x − → q if there exists a run r ∈ Run A (p, s, q) with wt A (s, r) = x. In this case, r is said to realize p s|x − →q. Note that r ∈ Run A (s) implies x = −∞. Similar to trees, we define restrictions, substitutions, and powers of runs as follows. Let t, s ∈ T Γ , r ∈ Run A (t), w ∈ pos(t), and r s ∈ Run A (s) with r s (ε) = r(w). Then we define r w ∈ Run A (t w ) by r w (v) = r(wv) for every v ∈ pos(t w ). We define r r s → w ∈ Run A (t s → w ) by r r s → w (v) = r s (u) if v = wu for some u ∈ pos(s), and r r s → w (v) = r(v) otherwise. For a Γ -word s and a run For a max-plus-WTA A, we define a relation ≤ on Q by p ≤ q iff there exists a Γ -word s ∈ T Γ such that Run A (q, s, p) = ∅. We call A trim if for every p ∈ Q there exists t ∈ T Γ , r ∈ Acc A (t), and w ∈ pos(t) with r(w) = p. The trim part of A is the automaton obtained from A by removing all states p ∈ Q for which no such t, r, and w exist. This process obviously has no influence on A .
A max-plus-WTA A is called deterministic or sequential if for every m ≥ 0, a ∈ Γ (m) , andp ∈ Q m , there exists at most one q ∈ Q with μ(p, a, q) = −∞. We call A unambiguous if |Acc A (t)| ≤ 1 for every t ∈ T Γ . We call the behavior A of A finitely sequential if there exist finitely many deterministic max-plus-WTA where the maximum is taken pointwise.

Main Result
We will show that for an unambiguous max-plus-WTA A, it is decidable whether its behavior A is finitely sequential. Moreover, if it is finitely sequential, we will obtain that the deterministic max-plus-WTA A 1 , . . . , 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 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 A is not finitely sequential if A satisfies the tree fork property. On the other hand, if A does not satisfy the tree fork property, we show how to construct finitely many unambiguous max-plus-WTA whose pointwise maximum is A , 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 A , 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 A be a deterministic maxplus word automaton and let L be the largest weight, in terms of absolute value, occurring in A (excluding −∞). Then for two words w 1 = uv 1 and w 2 = uv 2 which have an accepting run in A, the difference between A (w 1 ) and A (w 2 ) can be at most |L|(|v 1 | + |v 2 | + 2). This is clear since the unique runs of 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 A = (Q, Γ, μ, ν) be a deterministic max-plus-WTA, let X = (μ(Δ A ) ∪ ν(Q)) \ {−∞}, and let L = max x∈X |x|. Furthermore, let t 1 , t 2 ∈ T Γ be two trees with A (t 1 ) = −∞ and A (t 2 ) = −∞ and let w 1 ∈ pos(t 1 ) and w 2 ∈ pos(t 2 ) be two positions such that Proof Since A is deterministic, there exists exactly one run r 1 ∈ Acc A (t 1 ) and exactly one run r 2 ∈ Acc A (t 2 ). Likewise, there exists exactly one run r ∈ Run A (t). Due to t 1 w 1 = t 2 w 2 = t, we thus have r 1 w 1 = r 2 w 2 = r. It follows that 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 A = (Q, Γ, μ, ν) be a max-plus-WTA. Two states p, q ∈ Q are called siblings if there exists a tree u ∈ T Γ such that Run A (u, p) = ∅ and Run A (u, q) = ∅. We recall that Run A (u, p) and Run A (u, q) contain only valid runs.
Two siblings p, q are called twins if for every Γ -word s and weights we have x = y whenever x = −∞ and y = −∞ holds. Here, the maximum over the empty set is −∞ 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. 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 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 ∈ R, we can choose N sufficiently large to ensure that | A (w 1 ) − A (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 A if it does not satisfy the twins property. For trees, we can proceed in the same way. Proof We follow the idea for the proof of [29,Theorem 9]. Let A = (Q, Γ, μ, ν) be a trim unambiguous max-plus-WTA and let p, q ∈ Q be siblings, i.e., there exists a tree u ∈ T Γ and runs r p ∈ Run A (u, p) and r q ∈ Run A (u, q). Let s ∈ T Γ be a Γ -word such that p s|x − →p and q s|y − →q for weights x, y ∈ R. Since A is trim, there exist Γ -wordsû p ,û q ∈ T Γ such that pû p |z p − −− →p and qû q |z q − −− →q for two final states p , q ∈ Q and weights z p , z q ∈ R. We let κ p = wt A (u, r p ) + z p + ν(p ) and κ q = wt A (u, r q ) + z q + ν(q ) and for n ≥ 1 define the trees t (n) p =û p (s n (u)) and t (n) q =û q (s n (u)). Due to the unambiguity of A, we see that for every n ≥ 1 we have

Lemma 2 Let
Assume that there exists a deterministic max-plus-WTA A with A = A . Then by Lemma 1, there exists L ∈ R such that for all n ≥ 1 we have From the equations above we thus obtain that for every n ≥ 1 we have This can only hold if x = y. It follows that 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 A it is decidable whether there exists a deterministic max-plus-WTA
If such an automaton A 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 PSPACEhard, 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 cycleunambiguous 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 A = (Q, Γ, μ, ν) is called cycle-unambiguous if for every Γ -word s ∈ T Γ and every state q ∈ Q, there is at most one run which loops s in q, i.e., the set Run A (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. Proof Let p, q ∈ Q 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 u ∈ T Γ and two runs r p ∈ Run A (t, p) and r q ∈ Run 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 u w 2 → w 1 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 ∈ Run A (p, s, p) be the run on s which loops in p with weight x = wt A (s, r p ) and let r q ∈ Run A (q, s, q) be the run on s which loops in q with weight y = wt A (s, r q ). Furthermore, let w ∈ pos(s) with |w| = height(s) and let w ∈ pos(s) be the longest common prefix of w and ♦ 1 (s). Then either |w | > 2|Q| 2 or |w| − |w | > 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 2 ≤ p w 3 < p w 4 with w 4 ≤ p w ≤ p ♦ 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 2 ≤ p w 3 < p w 4 with w < p w 1 and w 4 ≤ p 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 and runs r p and r q of distinct weights which loop in p and q, respectively, by removing either one of the two loops or both loops as follows. If x − x 12 = y − y 12 , we remove the w 1 -w 2 loop. Otherwise, if x − x 34 = y − y 34 , we remove the w 3 -w 4 loop. If we have both x − x 12 = y − y 12 and x − x 34 = y − y 34 , we obtain that 2x − x 12 − x 34 = 2y − y 12 − y 34 . From x = y, it follows that x − x 12 − x 34 = y − y 12 − y 34 , so we remove both loops. From the cycle-unambiguity of 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.
Run A (u, q) = ∅ and a Γ -word s such that p s|x − →p and q s|y − →q with x = y. In this case, u and s are also said to be witnesses for the fact that p and q are rivals.
If 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 Run A (s), we have x = −∞ and y = −∞ 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. Fig. 1 A max-plus word automaton A over the alphabet {a} which is unambiguous, whose behavior is finitely sequential, but which does not satisfy the twins property as p and q are siblings but not twins. The behavior A of A assigns 0 to all words of odd length and |w| to all words w of even length Definition 3 Let A = (Q, Γ, μ, ν) be a max-plus-WTA. We say that A satisfies the tree fork property if at least one of the following two conditions is satisfied.
(i) There exist rivals p, q ∈ Q and a Γ -word t with p t|z p − − →p and p t|z q − − →q for some weights z p , z q ∈ R. In this case, t is also called a p-q-fork.
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
and only if A does not satisfy the tree fork property. If such automata A 1 , . . . , A n exist, they can be effectively constructed. Furthermore, there is a PSPACE-algorithm to decide whether 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 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 A is finitely sequential if and only if A does not satisfy the tree fork property.
To decide whether A satisfies condition (i), we first show that if there exists a pq-fork t for two rivals p and q, then there exists a p-q-fork t of height at most 2|Q| 2 . The argumentation for this is similar to the proof of Lemma 3 that the property of With u = a and s = b, we see that p and q are rivals, and a is a p-q-fork. All b's after the last a in a word are treated differently from the b's before the last a. A deterministic automaton cannot "guess" which a is the last in the word, and since there may be arbitrarily many a's in a word, even finitely many deterministic automata cannot compensate this inability to guess 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 t|z p − − →p and p t|z q − − →q for some weights z p , z q ∈ R. We let w ∈ pos(t) be a position with |w| = height(t) and let w be the longest common prefix of w and ♦ 1 (t). Then either |w | > |Q| 2 or |w| − |w | > |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 ≤ p w ≤ p ♦ 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 < 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 = t t w 2 → w 1 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, A does not satisfy condition (i).
In order to decide whether 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 μ(q 1 , . . . , q m , a, q 0 ) = −∞ → q 0 ≤ q i for all transitions (q 1 , . . . , q m , a, q 0 ) ∈ Δ A and i ∈ {1, . . . , m}. Then, by the trimness of A, condition (ii) is satisfied if and only if there exist two rivals p and q, a tran- Let A = (Q, Γ, μ, ν) 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 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 |A| of A as the size of its representation, i.e., 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 A = (Q, Γ, μ, ν) be a cycle-unambiguous max-plus-WTA and let Δ = {d ∈ Δ A | μ(d) = −∞} be the set of all valid transitions of 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 A satisfies the tree fork property.

Enumerating All Pairs of Siblings
We enumerate all siblings of A using the following reachability algorithm. We initialize the set of all pairs S ⊆ Q×Q which are siblings with S = ∅. Then we iterate the following operation.
Let S = 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 if {(p 1 , q 1 ), . . . , (p m , q m )} ⊆ S. If S = S, store S as the set of all siblings and terminate. If S S , let S = S 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 there exists a p-q-fork and the algorithm continues to "Test for rivals". If (p, q) / ∈ R and R R , the algorithm sets R = R and continues the iteration in search for a p-q-fork. If (p, q) / ∈ R and R = R , 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 = R p . For every transition (p 1 , . . . , p m , a, p 0 ) ∈ Δ, add p 0 to R p if R p ∩ {p 1 , . . . , p m } = ∅. If R p = R p , store R p as the set of all states reachable from p. If R p R p , let R p = R p 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 < j ≤ m such that p i ∈ R p and p j ∈ R 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 s|x − →p and q s|y − →q with x = y. 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 s|x − →p and q s|y − →q with x = y.
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 w contains a leaf , the tuple contains for each state p 0 ∈ Q an entry with the weight of the unique run from Run A (p, s w , p 0 ). If s does not contain a leaf , the tuple contains for each state p 0 ∈ Q an entry with the weight of the unique run from Run A (s 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 Run A (p, s, p) and Run A (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 "+ 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 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 = rk Γ (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 tuplesx (i) ,ȳ (i) ∈ R n max for wi. If a = , then for each j ∈ {1, . . . , n}, let x j = 0 if q j = p and x j = −∞ otherwise, and let y j = 0 if q j = q and y j = −∞ otherwise. If a = , compute for every j ∈ {1, . . . , n} the weights Store the tuplesx = (x 1 , . . . , x n ) andȳ = (y 1 , . . . , y n ) for w and discard the tuples x (i) ,ȳ (i) for all positions w1, . . . , wm and discard all tuples of the form (wi, a ). Then choose the next position to process as follows. If w = ε, continue to "Part 3". Otherwise, we can write w = vi with i ∈ N. Let a be the label we guessed for v. If i = rk Γ (a ), redefine w = v as the next position to process and continue to "Part 2".
If i < rk Γ (a ), 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 weightsx,ȳ ∈ R n max for ε. Let i, j be the indices such that p = q i and q = q j . If b = 1 and x i = y j , the algorithm terminates successfully. Otherwise, the algorithm is not successful.
The following two sections are dedicated to completing the proof of Theorem 3.

Necessity
In this section, we show that if an unambiguous max-plus-WTA A satisfies either condition (i) or condition (ii) of the tree fork property, then A 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 A be a trim unambiguous max-plus-WTA over Γ . If A satisfies condition (i) of the tree fork property, then there do not exist deterministic max-plus-WTA
Proof For contradiction, assume that A satisfies condition (i) of the tree fork property and that there exist deterministic max-plus- 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 ∈ Run A (u, p) and define z u = wt A (u, r p ). Furthermore, by trimness there exists a Γ -wordû with qû |zû − − →q f for some weight zû ∈ R and some state q f ∈ Q with ν(q f ) = −∞.
We define the constant L ∈ R to be the largest weight, in terms of absolute value, which occurs in the automata A 1 , . . . , A n as follows. We let X = n i=1 μ i (Δ A i ) ∪ ν i (Q i ) and define L = max x∈X\{−∞} |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 We define trees t 0 , . . . , t n inductively by t 0 = s N 0 (t (u)) and t k+1 = s N k+1 (t (t k )); for clarity, in the word case we would have t k = uts N 0 ts N 1 · · · ts N k . Then for k ∈ {1, . . . , n}, we let t k =û(t k ). Due to the unambiguity of A, we see that for every k ∈ {1, . . . , n} we have Thus, for k > l, we have 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 A j is deterministic, we have by Lemma 1 that In conclusion, we have n + 1 trees t i , and n automata A i , so by pigeonhole principle and the assumption that 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 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 A be a trim unambiguous max-plus-WTA over Γ . If A satisfies condition (ii) of the tree fork property, then there do not exist deterministic max-plus- Proof For contradiction, we assume that A satisfies condition (ii) of the tree fork property and that there exist deterministic max-plus- 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 ∈ Run A (u, p), r q u ∈ Run A (u, q), r p s ∈ Run A (p, s, p), and r q s ∈ Run A (q, s, q). Furthermore, we write A i = (Q i , Γ, μ i , ν i ) and let N = max n i=1 |Q i |. By the following argument, we may assume that ν(r(ε)) = −∞. By trimness, there exists a Γ -word s and a run r ∈ Run A (s ) with r (♦ 1 (s )) = r(ε) and ν(r (ε)) = −∞. Thus, if ν(r(ε)) = −∞, we can consider the 2-Γ -context s (t) with the run r r → ♦ 1 (s ) instead of t and r.
We now consider the tree t = t (s N (u), s N (u)) together with the run Since r ∈ Run A (t ) and ν(r (ε)) = −∞, we have In particular, x = y. We may assume that x < y. We consider two cases.
First, if z ≥ m 2 (x + y), then for the tree t + = t (s N+m (u), s N (u)) we obtain Note that this follows because A and 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 ≤ m 2 (x + y), we see that for the tree t − = t (s N (u), s N−m (u)) we obtain In both cases, we see that A = max n i=1 A i 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.

Sufficiency
In this section, we show that the behavior of an unambiguous max-plus-WTA 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 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 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 A. Furthermore, let u = u 1 · · · u n be a word for which there exist valid runs r p = p 0 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 u i+1 ···u n − −−−− →p and q j u j +1 ···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+1 · · · u n , we see that we have valid runs p i t − → p and p i t − → q, where p i ∈ {p, q}. Thus, A would satisfy the fork property. Since our assumption is that A does not satisfy the fork property, we have either i = j or p i = q 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 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 A, we can thus make a copy of 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 A is unambiguous, the number of valid runs on every given word is bounded by the number of states in 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 A could be constructed. In particular, the number of markers assigned at any given "time" is bounded by the number of states of 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 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 A, but the runs of its Schützenberger covering. The Schützenberger covering of a max-plus automaton A is a max-plus automaton which possesses the same behavior as A. It has already been employed in a number of decidability results for max-plus automata [3,4,22,31]. Its Fig. 3 On the left, an unambiguous max-plus word automaton over the alphabet {a, b} which does not satisfy the twins property but whose behavior is finitely sequential. On the right, an illustration of the runs of the automaton on the words ε, a, aa, and aaa together with appropriate markers. Arrows indicate a transition. The states p and q are rivals with witnesses u = ε and s = b  (2) , a, b ∈ Γ (1) , and d ∈ Γ (0) . All unspecified weights are assumed to be −∞. The states p and q are rivals 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 D is the result of applying the powerset construction to an NFA B. Then we might say that for a word w = w 1 w 2 , the state which D is in after reading the prefix w 1 is the set of all states which B could be in after reading w 1 . Similarly, the Schützenberger covering of a max-plus automaton A annotates to every state of a run of A on a word w the set of all states which "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 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 A = (Q, Γ, μ, ν) be a trim unambiguous max-plus-WTA which does not satisfy the tree fork property. We let π 1 : Q×P(Q) → Q, (p, P ) → p and π 2 : Q×P(Q) → P(Q), (p, P ) → P be the projections.
It is elementary to show that for a run of S on a tree t, the second entry of the state at a position w consists of all states of A which can be reached by a valid run of A on t w . In particular, every two runs on the same tree coincide on their second entries. Furthermore, projecting all states of a run of S to their first coordinate yields a run of A, and the weights of these runs coincide. It follows that S is unambiguous and satisfies S = A . Also, S is trim by definition.
We can also make the following observation about the rivals of S. Let p and q be rivals of S and let u and s be as in the definition of rivals. Since all runs of 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 S on u and s to their first entries yields runs of A on u and s, respectively, we additionally see that the first entries of p and q are rivals in A. Thus, if two states p, q ∈ Q S are rivals in S, then p = (p, P ) and q = (q, P ) for some set P ⊆ Q and two states p, q ∈ Q which are rivals in 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 S.
(vi) For every Γ -word s and two states p, q ∈ Q S with p s|x − →q, we have (vii) If two states p, q ∈ Q S are rivals in S, then p = (p, P ) and q = (q, P ) for some set P ⊆ Q and two states p, q ∈ Q which are rivals in A.
Proof (i) Let t ∈ T Γ and r ∈ Run 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 q ∈ P , then there are states (q 1 , . . . , q m ) ∈ P 1 × . . . × P m with μ(q 1 , . . . , q m , a, q) = −∞. By assumption, for every i ∈ {1, . . . , m} we find a run r i ∈ Run A (t wi , q i ). Then the quasi-run r : pos(t w ) → Q defined by r (ε) = q and r (iv) = r i (v) is a run of A on t w with r (ε) = q.
On the other hand, let r ∈ Run A (t w ) and let q = r (ε). Then for every i ∈ {1, . . . , m} we have that r i ∈ Run A (t wi ), so by assumption, r (i) ∈ P i . Moreover, μ(r (1), . . . , r (m), a, q) = −∞, so q ∈ P . Thus, (i) holds for w, which is a contradiction, so w does not exist. (ii) follows from (i). (iii) Let t ∈ T Γ . By definition of μ S , it is clear that for r ∈ Run S (t) we have π 1 • r ∈ Run A (t). The injectivity of π 1 : Run S (t) → Run A (t) follows from (ii) since for every two runs r 1 , r 2 ∈ Run S (t) we have π 2 • r 1 = π 2 • r 2 .
(vi) Let s be a Γ -word and p, q ∈ Q S be two states with p s|x − → q, then there exists a run r ∈ Run S (p, s, q) with wt S (s, r) = x. By definition of μ S , we have π 1 • r ∈ Run A (s) and wt S (s, r) = wt A (s, π 1 • r), so π 1 (p) s|x − → π 1 (q). (vii) Let p, q ∈ Q S be rivals in S and write p = (p, P p ), q = (q, P q ). Let u ∈ T Γ and s ∈ T Γ be as in the definition of rivals and let r p ∈ Run S (u, p) and r q ∈ Run S (u, q). By (ii), we have P p = π 2 • r p (ε) = π 2 • r q (ε) = P q . By (iii), we have π 1 • r p ∈ Run A (u, p) and π 1 • r q ∈ Run A (u, q), so p and q are siblings. Finally, from (p, P p ) s|x − → (p, P p ) and (q, P q ) s|y − → (q, P q ), we obtain by (vi) that p s|x − → p and q s|y − → q. Since x = y, p and q are rivals in 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 S, we need two preparatory lemmata. As a first simplification, we show that we may assume that two rivals p and q of 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 A. Thus, we can create two copies of 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 A.

Lemma 6
We may assume that for all rivals p, q ∈ Q we have either p ≤ q or q ≤ p, or both.
Proof Let p, q ∈ Q be rivals for which neither p ≤ q nor q ≤ p. Then we can show that p and q never occur together in the same run as follows. Assume we have a tree t ∈ T Γ , a run r ∈ Run 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 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 p ≤ q or q ≤ p. This is a contradiction, and thus r as chosen does not exist.
We let Q 1 = Q \ {p}, Q 2 = Q \ {q}, and let A i = (Q i , Γ, μ i , ν 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 A, every run of A is also a run of at least one of the automata A 1 , A 2 . Thus, we have A = max 2 i=1 A i and both A 1 and 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 A 1 , . . . , A n , all of which do not satisfy the tree fork property, such that A = max n i=1 A i and all rivals in an automaton A i are pairwise in ≤-relation.
Next, we note an elementary statement about self-maps f : X → X. Namely, if X is a finite set and f : X → X a mapping, then for every a ∈ X there exists some element b ∈ X 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) We now identify the first important property which all rivals of S satisfy. Namely, if P ⊆ Q is the second entry of some rival, then it cannot occur in the form of a "triangle" in any valid run of 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. (p, P ), (q, P ) ∈ Q S be rivals in S. Furthermore, let t ∈ T Γ be a tree, r ∈ Run S (t ) a run of S on t , and w 1 , w 2 ∈ pos(t ) be positions in t . If π 2 • r (ε) = π 2 • r (w 1 ) = π 2 • r (w 2 ) = P , then w 1 and w 2 are prefix-dependent.

Lemma 8 Let
Proof We proceed by contradiction and assume that t , r , 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, 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 S, this means both of these trees can also reach the states of r at w 1 and w 2 . In particular, there exists a run of S on the tree t = t s |P | (u) → w 1 s |P | |P | (u) → w 2 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 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 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 ) ∈ P be the state which r i loops in and let x i be the weight of this loop.
If x i = x j for some i and j , the states q i and q j are rivals in A with witnesses u and s n . By Lemma 6, we may therefore assume q i ≤ q 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 i ∈ P , say with weight y i . Due to x i = x j , we have mx i = ny i or mx j = ny 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 i ≤ q 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 A does not satisfy the tree fork property. It must therefore hold that We let x and y be the weights such that A loops s in p with weight x and in q with weight y. Then from x = y it follows that nx = x 1 or ny = x 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 j ∈ P and m ≥ 1 such that f m (p) = q j = f m (q j ). Then withs = t → w 2 v n 1 , we see that the Γ -words m is a q j -p-fork, i.e., 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 s |P | (u) → w 1 s |P | |P | (u) → w 2 and construct a run r ∈ Run S (t) of S on t as follows. By assumption, there exists a run r p ∈ Run S (u, (p, P )) and a run r s ∈ Run S ((p, P ), s, (p, P )). We let r 1 = r (p, P )) and r 2 ∈ Run S (s |P | |P | (u), (p, 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 s n |x j − −− → q j for all j ∈ {1, . . . , |P |} with weights x 1 , . . . , x |P | ∈ 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 i = x j for some i = j . Then q i and q j are rivals in A with witnesses u and s n . By Lemma 6, we can therefore assume that q i ≤ q j or q j ≤ q i . We assume q i ≤ q j and let s i j be a Γword such that there exists a run r i j ∈ Run 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 2 − m 1 and show that p i is a rival of either q i or q j . We have p i s m |y i − −− →p i for some weight y i ∈ R. Since p i ∈ P , we know that p i , q i , and q j are all siblings. Also, we have p i we have ny i = mx i or ny i = mx j , or both. Thus, p i is a rival of either q i or of q j .
Under these assumptions, we see that A satisfies condition (ii) of the tree fork property as follows. Either the 2-Γ -context t 1 = t → w 1 v m 1 → w 2 v n 1 together with the run r i pos(t 1 ) or the 2-Γ -context t 2 = t 1 ( , s i j ) together with the run r i pos(t 1 ) r i j → ♦ 2 (t 1 ) is a witness for condition (ii) to be satisfied. Since our assumption for this section is that A does not satisfy the tree fork property, this is a contradiction. In conclusion, 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 ∈ Run A (u, q i ). Furthermore, we have p From this, we obtain that withs = t → w 2 v n 1 we have q is m |z − − →q i and q is m |z − −− →p for weights z, z ∈ R. As p and q i are rivals, this means that 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 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 p ≤ q, then all occurrences of P as a second entry are prefix-dependent on (p, P ).

Lemma 9
Let (p, P ), (q, P ) ∈ Q S be rivals in S with p ≤ q. Furthermore, let t ∈ T Γ be a tree, r ∈ Run S (t ) a run of S on t , and w 1 ∈ pos(t ) a position in t with r (w 1 ) = (p, P ). Then all positions w 2 ∈ pos(t ) with π 2 • r (w 2 ) = P are prefix-dependent on w 1 .
Proof We proceed by contradiction and take (p, P ), (q, P ), t , r , w 1 as in the statement of the lemma and assume that there exists a position w 2 ∈ pos(t ) which is prefix-independent from w 1 and for which π 2 • r (w 2 ) = P . We show that under these assumptions, 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 S, it can also reach the state of r at w 2 . Thus, there exists a run of S on the tree t = t s |P | (u) → w 2 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 ∈ P . Let z be the weight of this loop and let x and y be the weights such that A loops s in p with weight x and in q with weight y. Due to x = y, we have nx = z or ny = z. Since u can reach every state from P , the state p 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 p ≤ q, we see that p can occur prefix-independently both from p and from q. This is a contradiction to the assumption that A does not satisfy the tree fork property.
In more detail, the proof is as follows. We define the tree t = t s |P | (u) → w 2 and construct a run r ∈ Run A (t) of A on t as follows. By assumption, there exists a run r p ∈ Run S (u, (p, P )) and a run r s ∈ Run S ((p, P ), s, (p, P )). We let r 2 = r |P | v s r p → v |P | . Then r 2 ∈ Run S (s |P | (u), (p, P )). By Lemma 5(iv), we have π 1 • r (w 2 ) ∈ P , so by Lemma 5(i) we can find r 2 ∈ Run A (s |P | (u)) with r 2 (ε) = π 1 • r (w 2 ). Then r = π 1 (r ) r 2 → w 2 ∈ Run A (t) is a run of 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 = r(w 1 v n 1 ) and n = n 2 − n 1 and show that p is a rival of either p or q. We know that p s n |z − − → p for some weight z ∈ R. Since p ∈ P , we can also find a run r p ∈ Run A (u, p ) which means that p is a sibling of both p and q. We now have p We see that A satisfies condition (ii) of the tree fork property as follows. Since we assumed p ≤ q, there exists a Γ -word s p q and a run r p q ∈ Run A (q, s p q , p). Therefore, either the 2-Γ -context t 1 = t → w 1 → w 2 v n 1 together with the run r pos(t 1 ) or the 2-Γ -context t 2 = t 1 (s p q , ) together with the run r pos(t 1 ) r p q → ♦ 1 (t 1 ) is a witness for condition (ii) to be satisfied. Since our assumption for this section is that A does not satisfy the tree fork property, this is a contradiction.
We can now prove that every run of S satisfies at least one of the following two conditions. If (p, P ) and (q, P ) are rivals in S with p ≤ q, then for every run r of 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 S on u. This is true in particular for the two rivals (p, P ) and (q, P ). Theorem 6 Let (p, P ), (q, P ) ∈ Q S be rivals in S with p ≤ q. Then for every tree t ∈ T Γ and every run r ∈ Run S (t) of 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 w ∈ pos(t).
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 π 2 • r(w 1 ) = π 2 • r(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 1 ≤ p w or w 2 ≤ p w, then all three positions are in prefix relation. We thus consider the case that w ≤ p w 1 and w ≤ p 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 = t w and r = r w . Then we have r ∈ Run S (t ), r (ε) = (p, P ), and π 2 • r (v 1 ) = π 2 • r (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 A = ({q 0 , p, p , p , q}, Γ, μ, ν) 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 , p , q} and let S be the Schützenberger covering of A. We construct A such that it satisfies the following conditions.
(i) A is unambiguous and does not satisfy the tree fork property. We achieve unambiguity simply by making 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 , and p . (iv) We have p ≤ q ≤ p ≤ q ≤ p . In particular, we cannot trivially separate these states to different automata. (v) In S, the state (q, P ) is a rival of all of (p, P ), (p , P ), and (p , P ). (vi) In S, we have (p , P ) ≤ (q, P ) ≤ (p, P ) ≤ (q, P ), i.e., these three states cannot be trivially separated, and we have (p , P ) ≤ (p , P ). (vii) In S, the state (p , P ) may occur at arbitrarily many pairwise prefixindependent 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 , P ) occurs in a run, then all states with second entry P occur at pairwise prefix-dependent positions, (2) both (p , P ) and (p , P ) may occur together in the same run, and (3) the state (p , P ) may occur at two prefix-independent positions in the same run. We define μ and ν as follows. , q 0 , c, p) = μ(q 0 , p, c, q) = μ(p , q 0 , c, p ) = μ(p , q 0 , c, p (p, a, q) = μ(q, a, p) = μ(p , a, p ) = μ(q, a,  − −− →(p , P ), we see that condition (vi) is also satisfied. Let P 0 = {q 0 , p, p }, then the tree in Fig. 9 together with the run of S on it illustrates that (p , P ) may occur nonlinearly, i.e., condition (vii) is satisfied as well.
This scenario does not violate Theorem 6 since (p , P ) can occur nonlinearly only "below" an f . By construction of A, there is a prefix-minimal position labeled f in every tree which both contains an f and possesses a valid run of A. Below this prefix-minimal f , only q 0 and p may occur, and all occurrences of p, q, p are between the root and the prefix-minimal f . In S, one can check that P cannot occur We note that the states p and p are also rivals in A with witnesses u = d and s = a(b(a( ))). Furthermore, S contains many more rivals than the ones men-  (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 , . . . , R n ⊆ Q S be an enumeration of all (unordered) pairs of rivals of 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 S and for every two rivals (p, P ), (q, P ) ∈ Q 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 A are in ≤-relation, we assume in the following that p i and q i are named such that p i ≤ q 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ā ∈ I , we denote byā[i] the i-th entry ofā.
Intuitively, the states of our new automaton will consist of a state from 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 S × I × P(Q S × 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 q ∈ Q S , we have m subtrees below our current position in the tree, the runs we consider on these subtrees have obtained markersā 1 , . . . ,ā m ∈ I , and the sets of states we could be in on these trees, together with their markers, are given by A 1 , . . . , A m ⊆ Q S × I .
Every pair (p,ā) ∈ A k corresponds to exactly one run of S on the k-th subtree together with its markers. Since S is unambiguous, we can therefore assume that |A k | ≤ |Q|. Also, sinceā k is the marker of a run on the k-th subtree, we may assume that (Q S × {ā k }) ∩ A k = ∅. Then if for all k ∈ {1, . . . , m} we have |A k | ≤ |Q| and (Q S × {ā k }) ∩ A k = ∅, we define the record of markersb for our current position by (explanations below) 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 I it will not actually occur.
We define our "run-marking" max-plus-WTA B = (Q, Γ,μ,ν) as follows. We letQ = Q S × I × P(Q S × I ) and let B be the trim part of the automaton B = (Q , Γ,μ ,ν ) defined for a ∈ Γ with rk Γ (a) = m and (p 0 ,ā 0 , A 0 ), . . . , ((p 1 ,ā 1 , A 1 ), . . . , (p m ,ā m , A m ), a, (p 0 ,ā 0 , A 0 ) . . . , p m , a, p 0 ā 1 , . . . ,ā m , A 1 , . . . , A m ) and For the rest of this section, we show that the automaton B "does what we want": We show that B is unambiguous, that it has the same behavior as 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.
We prove the following basic observations about B.
Lemma 10 Let t ∈ T Γ be a tree. Then the following statements hold.
(i) For every run r ∈ Run B (t) we have (π 1 • r(w),π 2 • r(w)) ∈π 3 • r(w). In particular, in the construction above the operator I is only applied to sets A k and tuplesā k with (Q S × {ā k }) ∩ A k = ∅. (ii) For every two runs r 1 , r 2 ∈ Run B (t) and every position w ∈ pos(t) we havẽ π 3 • r 1 (w) =π 3 • r 2 (w). (iii) For every run r ∈ Run B (t) and position w ∈ pos(t) we haveπ 3
In particular, in the construction above the operator I is only applied to sets A k with |A k | ≤ |Q|.
Proof (i) Let t ∈ T Γ and r ∈ Run 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) = (p,ā, A) and r(wj ) = (p j ,ā j , A j ) for j ∈ {1, . . . , m}.
Next, we prove two basic statements about how B sets markers. Assume we have some run in which a state (p,ā, A) occurs. First, we show that ifā[i] = 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 (q,b) withb[i] = 0 for some i, then we must have visited some state with second entry P i in the past.

Lemma 11
Let t ∈ T Γ be a tree, r ∈ Run B (t) be a run of B on t, let w ∈ pos(t) be a position in t, assume that r(w) = (p,ā, A), and let i ∈ {1, . . . , n}. Then the following statements hold.
. This set is not empty since it contains w. We write r(v) = (q,b, B). If q / ∈ R i would hold, we see from the definition ofμ, the definition of the operator I, and the fact that we chose v prefix-maximal from above set, that either case 1 or case 3 of the definition of I would apply in the definition ofb[i]. Thus,b[i] = 0 would hold, which is not the case. Therefore, q ∈ R i holds. (ii) Assume there is (q,b) ∈ A withb[i] = 0. By Lemma 10(iii), there is a run r ∈ Run B (t w ) with r (ε) = (q,b, A). Then by (i), there exists v ∈ pos(t w ) withπ 1 • r (v) ∈ R i . Furthermore, we have r w ∈ Run B (t w ). Combining Lemma 10(iv) and Lemma 5(ii), we have P i = π 2 •π 1 •r (v) = π 2 •π 1 •r w (v). Thus, we see that π 2 •π 1 • 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.
. 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 w ≤ p v. Then from Lemma 11(i) and our assumption on r we immediately obtaiñ In the next lemma, we show that if two states are rivals in 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. If (p,ā, A) and (q,b, B)  Proof Letp = (p,ā, A) andq = (q,b, B) be rivals in B. Let u and s be as in the definition of rivals and let rp ∈ Run B (u,p) and rq ∈ Run B (u,q). Then by Lemma 10(iv), we haveπ 1 (rp) ∈ Run S (u, p) andπ 1 (rq ) ∈ Run S (u, q). By Lemma 10(vii), we also have p s|x − → p and q s|y − →q with x = y, thus p and q are rivals in 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 ).

Lemma 13
We show thatā[i],b[i] / ∈ {0, |Q| + 1}. We let r p =π 1 • rp and r q =π 1 • rq . We have r p (ε) = (p i , P i ) and we assumed p i ≤ q i , so by Theorem 6 we obtain that for every two positions v 1 , v 2 ∈ pos(u) with This also holds for r q since by by Lemma 5(ii) we have π 2 • r p = π 2 • r 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  . 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 π 1 • r p (w p ) s|z 1 − − →p i and π 1 • r p (w p ) s|z 2 − − → q i for weights z 1 , z 2 ∈ R. Thus, A satisfies condition (i) of the tree fork property, which is a contradiction. Therefore, a[i] =b[i] cannot hold when w p = w q . Now assume without loss of generality that w p ≤ p w q with w p = w q and write w q = w p jv and rπ q (w p j) = (q ,b , A j ). By Lemma 10(i) and Lemma 10(ii), we then have (q ,b ) ∈ A j =π 3 • rp(w p j). By Lemma 12(i), we know that π 2 • rp(w p )[i] is defined using case 4 of the definition of I, soā[i] =b[i] must hold.
We turn to our final construction where we distribute the runs of B across multiple automata. For every record of markersc ∈ I , we construct one automaton Bc which for each pair of rivals R i admits only runs using the markers 0 andc[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 . Finally, we formally prove that the automata Bc are unambiguous, that their pointwise maximum is equivalent to the behavior of A, and that they all satisfy the twins property, which means that they can be determinized. We note that the construction of the automata Bc is optimized for provability, so we omit analyzing their size and the complexity of their construction.

Theorem 7
We have A = maxc ∈I Bc and for everyc ∈ I , the automaton Bc is unambiguous and satisfies the twins property.
Proof The unambiguity of Bc follows from the unambiguity of B. To see that Bc satisfies the twins property, let (p,ā, A), (q,b, B) ∈Qc be rivals in Bc. Then (p,ā, A)  and (q,b, B) ,ā, A), (q,b, B) ∈Qc is impossible, so there are no rivals in Bc and Bc satisfies the twins property.
To show that A = maxc ∈I Bc , we show that for every tree t ∈ T Γ we have Run B (t) = c∈I Run Bc (t). From this, it follows that maxc ∈I Bc = B = A . The inclusion "⊇" is clear.
Let t ∈ T Γ , r ∈ Run B (t), and let O = {i ∈ {1, . . . , n} | there is a position w ∈ pos(t) withπ 1 • r(w) = (p i , P i )}. Let i ∈ O and assume we have two positions v 1 , v 2 ∈ pos(t) such that π 2 •π 1 • r(v 1 ) = π 2 •π 1 • r(v 2 ) = P i . Then, sincẽ π 1 (r) ∈ Run S (t) by Lemma 10(iv), we obtain by Theorem 6 that v 1 ≤ p v 2 or v 2 ≤ p v 1 . We can therefore let w i ∈ pos(t) be the prefix-largest position in t with π 1 • r(w i ) ∈ R i . Then from Lemma 12(ii) and Lemma 12(iii), we obtain that for all positions v ∈ pos(t) with v ≤ p w i we haveπ 2  We now obtain a finitely sequential representation of A by applying Theorem 1 to the automata Bc. 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.

Further Insights
In this section, we show some additional properties of the rivals of the Schützenberger covering 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 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 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 ) ∈ Q S be rivals in S with p ≤ q. Then for every tree t ∈ T Γ and every run r ∈ Run S (t) of 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 w ∈ pos(t).
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 , P ) of (q, P ) with (q, P ) ≤ (q , P ). Thus, Theorem 8 follows by applying Theorem 6 to the rivals (q, P ) and (q , 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 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 ) ∈ Q S be rivals in S with witnesses u and s such that (p, P ) ≤ (q, P ). Then there exists a state q ∈ P with (q, P ) ≤ (q , P ) such that (q , P ) and (q, P ) are rivals in 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 be a Γ -word such that Run S ((q, P ), s , (p, P )) = ∅, which exists due to (p, P ) ≤ (q, P ) By construction of S and our assumption on s , there exists for every p ∈ P at least one q ∈ P with Run S ((q , P ), s , (p , P )) = ∅. On the other hand, we obtain from the unambiguity of S that for every p ∈ P , there can be at most one q ∈ P with Run S ((q , P ), s , (p , P )) = ∅. It follows that s induces a mapping g : P → P which maps p to q if Run S ((q , P ), s , (p , P )) = ∅ and g satisfies p → q. With an identical argumentation, we obtain that s induces a mapping h : P → P which maps p to q if Run S ((q , P ), s, (p , P )) = ∅ and h satisfies p → p and q → q.
Let R be the smallest set satisfying q ∈ R , g(R ) ⊆ R , and h(R ) ⊆ R , i.e., such that R contains q and is closed under g and h. Then let R = {p} ∪ R 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 )), . . . , h n 1 (g(p m ))) = (h n 2 (g(p 1 )), . . . , 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 )), . . . , h n 1 (g(p m )) ∈ R. Thus, f = h n 1 • g is a mapping f : R → R and we can apply Lemma 7 to f with a = p. We obtain q ∈ R and n ≥ 1 with f n (p) = q = f n (q ). From the definitions of h and g, it follows that (s (s n 1 )) n is a (q , P )-(p, P )-fork, and therefore also a q -p-fork. Since A does not satisfy the tree fork property, q is therefore not a rival of p. Moreover, we have f n−1 • h n 1 (q) = f n (p) = q , so we see that Run S ((q , P ), s n 1 ((s (s n 1 )) n−1 ), (q, P )) = ∅ and therefore (q, P ) ≤ (q , P ).
Due to the fact that h n 2 −n 1 (q ) = q , we see from the definition of h that , so (q , P ) is either a rival of (p, P ) or of (q, P ) with witnesses u and s k . As (q , P ) and (p, P ) being rivals implies by Lemma 5(vii) that q and p are rivals in A and we found that the latter is not the case, it must hold that (q , P ) and (q, P ) are rivals. Now assume that (p, P ) and (q, P ) ∈ Q S with (p, P ) ≤ (q, P ) are rivals in 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 t ∈ T Γ , prefix-independent positions w 1 , w 2 ∈ pos(t), and a run r ∈ Run 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.
By applying Theorem 8 either to (p, P ) and (p, P ) or to (q, P ) and (p, P ), we see that (p 2 , P ) may not occur prefix-independently from (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 , P ) ≤ (q, P ), (p , P ) ≤ (p , P ), and (p , P ) may occur at prefix-independent positions.
In conclusion, we obtain that if (p, P ) and (q, P ) are rivals in 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.
Funding Open Access funding enabled and organized by Projekt DEAL.
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommonshorg/licenses/by/4. 0/.