Skip to main content
main-content

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Erschienen in: Theory of Computing Systems 4/2021

Open Access 26.03.2021

Finite Sequentiality of Unambiguous Max-Plus Tree Automata

verfasst von: Erik Paul

Erschienen in: Theory of Computing Systems | Ausgabe 4/2021

download
DOWNLOAD
share
TEILEN
print
DRUCKEN
insite
SUCHEN

Abstract

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.
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),labelt), where \(\text {pos}(t) \subset \mathbb {N}^{*}\) is a finite non-empty prefix-closed set of positions, labelt: pos(t) →Γ is a mapping, and for every w ∈pos(t) we have wi ∈pos(t) iff 1 ≤ i ≤rkΓ(labelt(w)). We write t(w) for labelt(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)∣vpw} 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)∣wpv}) ∪{wvv ∈pos(s)}. For v ∈pos(tsw〉), we let labeltsw(v) = s(u) if v = wu for some u ∈pos(s), and otherwise labeltsw(v) = t(v).
For aΓ(m) and trees t1,…, tmTΓ, we also write a(t1,…, tm) to denote the tree t with pos(t) = {ε}∪{iwi ∈{1,…, m}, w ∈pos(ti)}, labelt(ε) = a, and labelt(iw) = ti(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 w1,…, wn ∈pos(t) be a lexicographically ordered enumeration of all leaves of t labeled ◇. Then we call t an n-Γ-context and define ⋄i(t) = wi for i ∈{1,…, n}. For an n-Γ-context t and contexts \(t_{1}, \ldots , t_{n} \in T_{\varGamma _{{\diamond }}}\), we define t(t1,…, tn) = tt1 →⋄1(t)〉…〈tn →⋄n(t)〉 by substitution of t1,…, tn into the ◇-leaves of t. A 1-Γ-context is also called a Γ-word. For a Γ-word s, we define s0 = ◇ and sn+ 1 = s(sn) for n ≥ 0.
A commutative semiring is a tuple (K, ⊕, ⊙, https://static-content.springer.com/image/art%3A10.1007%2Fs00224-020-10021-w/MediaObjects/224_2020_10021_Figa_HTML.gif , https://static-content.springer.com/image/art%3A10.1007%2Fs00224-020-10021-w/MediaObjects/224_2020_10021_Figb_HTML.gif ), abbreviated by K, with operations sum ⊕ and product ⊙ and constants https://static-content.springer.com/image/art%3A10.1007%2Fs00224-020-10021-w/MediaObjects/224_2020_10021_Figc_HTML.gif and https://static-content.springer.com/image/art%3A10.1007%2Fs00224-020-10021-w/MediaObjects/224_2020_10021_Figd_HTML.gif such that (K, ⊕, https://static-content.springer.com/image/art%3A10.1007%2Fs00224-020-10021-w/MediaObjects/224_2020_10021_Fige_HTML.gif ) and (K, ⊙, https://static-content.springer.com/image/art%3A10.1007%2Fs00224-020-10021-w/MediaObjects/224_2020_10021_Figf_HTML.gif ) are commutative monoids, multiplication distributes over addition, and https://static-content.springer.com/image/art%3A10.1007%2Fs00224-020-10021-w/MediaObjects/224_2020_10021_Figg_HTML.gif 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 q0,…, qn, 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(ε) = q0 and r(⋄i(t)) = qi 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 rs(ε) = 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 rrsw〉(v) = rs(u) if v = wu for some u ∈pos(s), and rrsw〉(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 r0〈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 w1 = uv1 and w2 = uv2 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|(|v1| + |v2| + 2). This is clear since the unique runs of \(\mathcal {A}\) on w1 and w2 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 t1, t2TΓ be two trees with \({\llbracket }{\mathcal {A}}{\rrbracket }(t_{1}) \neq -\infty \) and \({\llbracket }{\mathcal {A}}{\rrbracket }(t_{2}) \neq -\infty \) and let w1pos(t1) and w2pos(t2) 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 w1 = usNvp and w2 = usNvq, where vp and vq 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 rp and rq; that is, we can find two positions w1 <pw2 in u with rp(w1) = rp(w2) and also rq(w1) = rq(w2). By removing everything between w1 and w2 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 rp and rq above ⋄1(s). More precisely, by pigeon hole principle we can find positions w1 <pw2pw3 <pw4 with \(w_{4} \leq _{p} w^{\prime } \leq _{p} {\Diamond }_1(s)\) in s for which (rp(w1), rq(w1)) = (rp(w2), rq(w2)) and (rp(w3), rq(w3)) = (rp(w4), rq(w4)). In the second case, there exist two disjoint simultaneous loops in rp and rq which are prefix-independent from ⋄1(s). That is, there exist positions w1 <pw2pw3 <pw4 with \(w^{\prime } <_{p} w_{1}\) and w4pw in s for which (rp(w1), rq(w1)) = (rp(w2), rq(w2)) and (rp(w3), rq(w3)) = (rp(w4), rq(w4)).
Let x12 and x34 be the weights of the loops in the run rp, and let y12 and y34 be the weights of the loops in the run rq. 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 xx12yy12, we remove the w1-w2 loop. Otherwise, if xx34yy34, we remove the w3-w4 loop. If we have both xx12 = yy12 and xx34 = yy34, we obtain that 2xx12x34 = 2yy12y34. From xy, it follows that xx12x34yy12y34, 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 rp and rq 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 w1 <pw2 in t with \(w_{2} \leq _{p} w^{\prime } \leq _{p} {\Diamond }_1(t)\) and (rp(w1), rq(w1)) = (rp(w2), rq(w2)). In the second case, there exist two positions w1 <pw2 in t with \(w^{\prime } <_{p} w_{1}\) and (rp(w1), rq(w1)) = (rp(w2), rq(w2)). By removing the part of t between w1 and w2, 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, qip, and qjq. □
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 (p1,…, pm, a, p0),(q1,…, qm, a, q0) ∈Δ, add (p0, q0) 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 (p1,…, pm, a, p0),(q1,…, qm, a, q0) ∈Δ, add (p0, q0) to \(R^{\prime }\) if \(\{ (p_{1},q_{1}), \ldots , (p_{m},q_{m})\} \subseteq S\) and R ∩{(p1, q1),…,(pm, qm)}≠. 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 Rp = {p}. Then we iterate the following operation.
Let \(R_{p}^{\prime } = R_{p}\). For every transition (p1,…, pm, a, p0) ∈Δ, add p0 to \(R_{p}^{\prime }\) if Rp ∩{p1,…, pm}≠. If \(R_{p}^{\prime } = R_{p}\), store Rp 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 Rq of all states reachable from q. This part of the algorithm runs in polynomial time and the sets Rp and Rq can thus be stored in polynomial space.
Next, we verify for every transition (p1,…, pm, a, p0) ∈Δ whether there exist indices i, j with 1 ≤ i < jm such that piRp and pjRq. 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 p0Q 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 p0Q 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 = {q1,…, qn} 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 xj = 0 if qj = p and \(x_{j} = -\infty \) otherwise, and let yj = 0 if qj = 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 = qi and q = qj. If b = 1 and xiyj, 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, zp, zq 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 qfQ 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 N0,…, Nn inductively as follows. We let Nn = 0 and if Nl+ 1,…, Nn are defined, then we define Nl 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 Nl. 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 ti, 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(sn(u), sn(u)) such that, by increasing n, the difference between the weights on the two subtrees sn(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(sn(u), sn(u)) and choose n large enough to ensure that in each of the deterministic automata, some sub-Γ-word sm of sn 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, v1 = ⋄1(t), and v2 = ⋄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 ≥|Qj|, we have \(r^{\prime }(v_{1}v^{n_{1}}) = r^{\prime }(v_{1}v^{n_{2}})\) for some n1, n2 ∈{0,…, N} with n1 < n2. 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 = n2n1 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(sN+m(u), sN(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(sN(u), sNm(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 = u1un 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 pn = p and qn = q.
We now show that the first occurrence of either p or q in the runs rp and rq serves as a “distinguisher” between the two runs. We let i be the smallest index with the property that pi ∈{p, q}. Similarly, we let j be the smallest index with the property that qj ∈{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 pi = qj, 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 = ui+ 1un, we see that we have valid runs \(p_{i} \xrightarrow {t} p\) and \(p_{i} \xrightarrow {t} q\), where pi ∈{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 piqj.
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 1p. 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 2p, since 1p 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 1p, as now no valid run on uaa exists to which the marker 1p 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 rp and rq 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 1p. 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 = w1w2, the state which \(\mathcal {D}\) is in after reading the prefix w1 is the set of all states which \({\mathscr{B}}\) could be in after reading w1. 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 π2r1=π2r2.
 
(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) = (pi, Pi) for i ∈{1,…, m}.
First, let qP, then there are states (q1,…, qm) ∈ P1 ×… × Pm 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 π2r1 = π2r2. 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) = Pi, 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, Pp), q = (q, Pq). 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 Pp = π2rp(ε) = π2rq(ε) = Pq. 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 w1, w2 ∈pos(t) with r(w1) = p and r(w2) = q. Then w1 and w2 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 w1 and w2 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 Q1 = Q ∖{p}, Q2 = 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 Qi. 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), f2(a),…, f|X|(a). By pigeon hole principle, there are numbers 0 ≤ m1 < m2 ≤|X| with \(f^{m_{1}}(a) = f^{m_{2}}(a)\). Then if we choose nm1 as a multiple of m2m1 and b = fn(a), we see that fn(a) = b = fn(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 fn(a) = b = fn(b). Here, fn is the n-th iterate of f, i.e., \(f^{0} = \text {id}_{X}\) and fm+ 1 = ffm.
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, wv1, and wv2 such that the second entry of r(w), r(wv1), and r(wv2) is P, then wv1 and wv2 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 w1 and w2 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 w1 and w2 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 w1 and w2. 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 r1,…, 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 sn below w2 which loops in all runs at the same time, i.e., where for some n1 we have \(r_{i}(w_{2}v^{n_{1}}) = r_{i}(w_{2}v^{n_{1} + n})\) for all runs ri. For each ri, we let \(q_{i} = r_{i}(w_{2}v^{n_{1}}) \in P\) be the state which ri loops in and let xi be the weight of this loop.
If xixj for some i and j, the states qi and qj are rivals in \(\mathcal {A}\) with witnesses u and sn. By Lemma 6, we may therefore assume qiqj. Again by pigeon hole principle, the run ri loops below w1 in sm for some m ≥ 1 with some state piP, say with weight yi. Due to xixj, we have mxinyi or mxjnyi. Since u can reach every state from P, the state pi is thus a rival of qi or qj with witnesses u and snm. From the existence of ri and the assumption that qiqj, we see that pi can occur prefix-independently both from qi and from qj. This is a contradiction to the assumption that \(\mathcal {A}\) does not satisfy the tree fork property. It must therefore hold that x1 = … = 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 nxx1 or nyx1, so the states qi are either all rivals of p or all rivals of q with witnesses u and sn. We assume all qi to be rivals of p and apply Lemma 7 to the mapping f : P →{q1,…, q|P|}, ri(ε)↦qi with a = p to obtain qjP and m ≥ 1 such that fm(p) = qj = fm(qj). Then with \(\tilde {s} = t \langle {\diamond } \to w_{2}v^{n_{1}} \rangle \), we see that the Γ-word \(\tilde {s}^{m}\) is a qj-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(w1vi) = P for 0 ≤ i ≤|P| and π2r(w2vi) = 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 {r1(ε),…, r|P|(ε)} = P. We have rj(w2vi) ∈ 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 n1 < n2 with \(\bar {q}_{n_{1}} = \bar {q}_{n_{2}}\) by pigeonhole principle. Let n = n2n1 and write \(\bar {q}_{n_{1}} = (q_{1}, \ldots , q_{|P|})\).
We now show that q1,…, 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 rp on u and Lemma 5(i), all states in P are siblings.
We show first that x1 = … = x|P|. We assume that by contradiction, xixj for some ij. Then qi and qj are rivals in \(\mathcal {A}\) with witnesses u and sn. By Lemma 6, we can therefore assume that qiqj or qjqi. We assume qiqj 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 m1, m2 ∈{0,…,|P|} with \(r_{i}(w_{1}v^{m_{1}}) = r_{i}(w_{2}v^{m_{2}})\) and m1 < m2. We let \(p_{i} = r_{i}(w_{1}v^{m_{1}})\) and m = m2m1 and show that pi is a rival of either qi or qj. We have \(p_{i} {{\xrightarrow { s^{m} \mid y_{i} }}} p_{i}\) for some weight \(y_{i} \in \mathbb {R}\). Since piP, we know that pi, qi, and qj 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 xixj, we have nyimxi or nyimxj, or both. Thus, pi is a rival of either qi or of qj.
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, x1 = … = x|P|.
To see that q1,…, 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 nxx1 or nyx1. Without loss of generality, we assume nxx1, thus all qi are rivals of p.
We now show that \(\mathcal {A}\) satisfies condition (i) of the tree fork property. We define a mapping f : P →{q1,…, q|P|} by ri(ε)↦qi for i ∈{1,…,|P|}; recall that \(\{q_{1}, \ldots , q_{|P|} \} \subseteq P\), {r1(ε),…, r|P|(ε)} = P, and ri(ε)≠rj(ε) for ij. By Lemma 7, there exists m ≥ 1 and i ∈{1,…,|P|} with fm(p) = qi = fm(qi). 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 qi 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 w1.
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 w1 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 w2. 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 w1 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 sn below w2 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 sn. From the fact that r(w1) = 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(w2vi) ∈ P for 0 ≤ i ≤|P|.
By pigeonhole principle, we can find n1, n2 ∈{0,…,|P|} with \(r(w_{2}v^{n_{1}}) = r(w_{2}v^{n_{2}})\) and n1 < n2. We let \(p^{\prime } = r(w_{1}v^{n_{1}})\) and n = n2n1 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 w1, w2pos(t) with π2r(w1) = π2r(w2) = P we have w1pw2 or w2pw1.
 
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 w1, w2 ∈pos(t) be two positions with π2r(w1) = π2r(w2) = P. By Lemma 9, we see that then w1 and w2 are prefix-dependent on w. From the definition of the prefix relation, we see that if either w1pw or w2pw, then all three positions are in prefix relation. We thus consider the case that wpw1 and wpw2. In this case, we see from Lemma 8 that w1 and w2 are prefix-dependent as follows. We write w1 = wv1 and w2 = wv2 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 v1 and v2 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 q0 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 Ri = {(pi, Pi),(qi, Pi)} such that (pi, Pi) and (qi, Pi) are rivals in \(\mathcal {S}\) and for every two rivals \((p, P), (q, P) \in Q_{\mathcal {S}}\), we have Ri = {(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 pi and qi are named such that piqi for all i ∈{1,…, n}.
For each pair of rivals Ri, we define a set of markers by Ii = {0,|Q| + 1}∪ ({1,…,|Q|}× Ri). The set of all combined records of markers is defined by I = I1 ×… × In. 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 |Ak|≤|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 |Ak|≤|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 |Ak| > |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 |Ak|≤|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 Ri, so we assign the dummy marker 0. Case 2 means our current position is a leaf and q is from Ri, 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 Ri, 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 Ri, and there is at most one subtree on which runs exist that obtained a marker for Ri. Then, we take the smallest number which is not already used in a marker for Ri 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 Ri, but we cannot apply case 4 as there are two distinct subtrees on which runs exist which obtained markers for Ri. 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 Bk[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 Ak 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 Ak with |Ak|≤|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)∣r1(v)≠r2(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 r1(wj) = r2(wj). From the definition of \(\tilde \pi {\mu }\), it is immediately clear that r1(w) = r2(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 Ri. 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 Pi 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 wpv 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 wpv 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 qRi 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, qRi 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 Ri are properly set in runs where states with Pi as a second entry occur only linearly. That is, we show that in these runs, a marker for Ri is only set when a rival from Ri 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 v1, v2pos(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 v1pv2 or v2pv1. 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 vpw 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 wpv, 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 wpv. 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 vpw 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 wpv. 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 Ri = {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 Ri = {p, q}. We may assume that p = (pi, Pi) and q = (qi, Pi).
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 rp(ε) = (pi, Pi) and we assumed piqi, so by Theorem 6 we obtain that for every two positions v1, v2 ∈pos(u) with π2rp(v1) = π2rp(v2) = Pi, we have v1pv2 or v2pv1. This also holds for rq since by by Lemma 5(ii) we have π2rp = π2rq.
Let wp ∈pos(u) be the prefix-largest position of u with rp(wp) ∈ Ri and wq ∈pos(u) be the prefix-largest position with rq(wq) ∈ Ri. That wp and wq exist is clear from the fact that rp(ε) ∈ Ri and rq(ε) ∈ Ri. 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 wp = wq we assume for contradiction that \(\bar {a}[i] = \bar {b}[i]\). Then we see that rp(wp) = rq(wq) ∈ Ri, and we also have rp(ε) = p and rq(ε) = q. It follows that with s = u〈◇→ wp〉, 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 wp = wq.
Now assume without loss of generality that wppwq with wpwq and write wq = wpjv 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 Ri 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|}× Ri.
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 v1, v2 ∈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 v1pv2 or v2pv1. We can therefore let wi ∈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 vpwi 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 wi 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 w1, w2pos(t) with π2r(w1) = π2r(w2) = P we have w1pw2 or w2pw1.
 
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 sn 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 p1,…, pm be an enumeration of R. By pigeon hole principle, there exist integers 0 ≤ n1 < n2 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 = n2n1. 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 sk. 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 (p1, P) and (p2, P) may occur at prefix-independent positions, i.e., there is a tree tTΓ, prefix-independent positions w1, w2 ∈pos(t), and a run \(r \in \text {Run}_{\mathcal {S}}(t)\) with r(w1) = (p1, P) and r(w2) = (p2, P). In the following, we want to analyze how (p1, P) may occur together with (p, P) or (q, P) in a run.
First, Theorems 6 and 8 tell us that (p1, P) may not occur prefix-independently from (p, P) and (q, P). Second, if (p1, P) ≤ (p, P) or (p1, P) ≤ (q, P), then by our assumption the state (p2, P) may occur prefix-independently from (p, P) or (q, P). This is impossible again by Theorems 6 and 8, so (p1, P) ≤ (p, P) and (p1, 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 (p2, P). Then if (q, P) ≤ (p1, 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 (p2, P) may not occur prefix-independently from \((\hat {p}, P)\), which does not match our assumption. It follows that (q, P) ≤ (p1, P) is also impossible. Finally, the only remaining possibility is (p, P) ≤ (p1, 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.
Open AccessThis 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://​creativecommons.​org/​licenses/​by/​4.​0/​.

Publisher’s Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Literatur
1.
Zurück zum Zitat Alexandrakis, A., Bozapalidis, S.: Weighted grammars and Kleene’s theorem. Inf. Process. Lett. 24(1), 1–4 (1987) MathSciNetCrossRef Alexandrakis, A., Bozapalidis, S.: Weighted grammars and Kleene’s theorem. Inf. Process. Lett. 24(1), 1–4 (1987) MathSciNetCrossRef
2.
Zurück zum Zitat Allauzen, C., Mohri, M.: Efficient algorithms for testing the twins property. J. Autom. Lang. Combin. 8(2), 117–144 (2003) MathSciNetMATH Allauzen, C., Mohri, M.: Efficient algorithms for testing the twins property. J. Autom. Lang. Combin. 8(2), 117–144 (2003) MathSciNetMATH
3.
Zurück zum Zitat Bala, S.: Which finitely ambiguous automata recognize finitely sequential functions? In: Chatterjee, K., Sgall, J. (eds.) 38th International Symposium on Mathematical Foundations of Computer Science (MFCS). Springer, Lecture Notes in Computer Science, vol. 8087, pp. 86–97 (2013) Bala, S.: Which finitely ambiguous automata recognize finitely sequential functions? In: Chatterjee, K., Sgall, J. (eds.) 38th International Symposium on Mathematical Foundations of Computer Science (MFCS). Springer, Lecture Notes in Computer Science, vol. 8087, pp. 86–97 (2013)
4.
Zurück zum Zitat Bala, S., Koniński, A., Martín-Vide, C., Truthe, B.: Unambiguous automata denoting finitely sequential functions. In: Dediu, A. (ed.) 7th International Conference on Language and Automata Theory and Applications (LATA), Springer, Lecture Notes in Computer Science, vol. 7810, pp. 104–115 (2013) Bala, S., Koniński, A., Martín-Vide, C., Truthe, B.: Unambiguous automata denoting finitely sequential functions. In: Dediu, A. (ed.) 7th International Conference on Language and Automata Theory and Applications (LATA), Springer, Lecture Notes in Computer Science, vol. 7810, pp. 104–115 (2013)
5.
Zurück zum Zitat Béal, M., Carton, O., Prieur, C., Sakarovitch, J.: Squaring transducers: an efficient procedure for deciding functionality and sequentiality. Theor. Comput. Sci. 292(1), 45–63 (2003) MathSciNetCrossRef Béal, M., Carton, O., Prieur, C., Sakarovitch, J.: Squaring transducers: an efficient procedure for deciding functionality and sequentiality. Theor. Comput. Sci. 292(1), 45–63 (2003) MathSciNetCrossRef
6.
Zurück zum Zitat Berstel, J., Reutenauer, C.: Recognizable formal power series on trees. Theor. Comput. Sci. 18, 115–148 (1982) MathSciNetCrossRef Berstel, J., Reutenauer, C.: Recognizable formal power series on trees. Theor. Comput. Sci. 18, 115–148 (1982) MathSciNetCrossRef
7.
Zurück zum Zitat Berstel, J., Reutenauer, C.: Rational Series and their Languages. EATCS Monographs in Theoretical Computer Science, vol. 12. Springer, Berlin (1988) Berstel, J., Reutenauer, C.: Rational Series and their Languages. EATCS Monographs in Theoretical Computer Science, vol. 12. Springer, Berlin (1988)
8.
Zurück zum Zitat Björklund, J., Drewes, F., Zechner, N., Martín-Vide, C., Truthe, B.: An efficient best-trees algorithm for weighted tree automata over the tropical semiring. In: Dediu, A., Formenti, E. (eds.) 9th International Conference on Language and Automata Theory and Applications (LATA), Springer, Lecture Notes in Computer Science, vol. 8977, pp. 97–108 (2015) Björklund, J., Drewes, F., Zechner, N., Martín-Vide, C., Truthe, B.: An efficient best-trees algorithm for weighted tree automata over the tropical semiring. In: Dediu, A., Formenti, E. (eds.) 9th International Conference on Language and Automata Theory and Applications (LATA), Springer, Lecture Notes in Computer Science, vol. 8977, pp. 97–108 (2015)
9.
Zurück zum Zitat Blattner, M., Head, T.: Automata that recognize intersections of free submonoids. Inf. Control 35(3), 173–176 (1977) MathSciNetCrossRef Blattner, M., Head, T.: Automata that recognize intersections of free submonoids. Inf. Control 35(3), 173–176 (1977) MathSciNetCrossRef
10.
Zurück zum Zitat Büchse, M., Fischer, A.: Deciding the twins property for weighted tree automata over extremal semifields. In: Drewes, F., Kuhlmann, M. (eds.) 2nd Workshop on Applications of Tree Automata Techniques in Natural Language Processing (ATANLP), The Association for Computer Linguistics, pp. 11–20 (2012) Büchse, M., Fischer, A.: Deciding the twins property for weighted tree automata over extremal semifields. In: Drewes, F., Kuhlmann, M. (eds.) 2nd Workshop on Applications of Tree Automata Techniques in Natural Language Processing (ATANLP), The Association for Computer Linguistics, pp. 11–20 (2012)
11.
Zurück zum Zitat Büchse, M., May, J., Vogler, H.: Determinization of weighted tree automata using factorizations. Journal of Automata. Lang. Comb. 15 (3/4), 229–254 (2010) MathSciNetMATH Büchse, M., May, J., Vogler, H.: Determinization of weighted tree automata using factorizations. Journal of Automata. Lang. Comb. 15 (3/4), 229–254 (2010) MathSciNetMATH
12.
Zurück zum Zitat Daviaud, L., Guillon, P., Merlet, G.: Comparison of max-plus automata and joint spectral radius of tropical matrices. In: [27], vol. 19, pp. 1–19:14 (2017) Daviaud, L., Guillon, P., Merlet, G.: Comparison of max-plus automata and joint spectral radius of tropical matrices. In: [27], vol. 19, pp. 1–19:14 (2017)
13.
Zurück zum Zitat Droste, M., Kuich, W., Vogler H. (eds.): Handbook of Weighted Automata. EATCS Monographs in Theoretical Computer Science. Springer, Berlin (2009) Droste, M., Kuich, W., Vogler H. (eds.): Handbook of Weighted Automata. EATCS Monographs in Theoretical Computer Science. Springer, Berlin (2009)
14.
15.
Zurück zum Zitat Filiot, E., Jecker, I., Lhote, N., Pérez, G.A., Raskin, J.: On delay and regret determinization of max-plus automata. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pp. 1–12. IEEE Computer Society (2017) Filiot, E., Jecker, I., Lhote, N., Pérez, G.A., Raskin, J.: On delay and regret determinization of max-plus automata. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pp. 1–12. IEEE Computer Society (2017)
16.
Zurück zum Zitat Fülöp, Z., Vogler, H.: Weighted tree automata and tree transducers. In: [13], chap 9, pp. 313–403 (2009) Fülöp, Z., Vogler, H.: Weighted tree automata and tree transducers. In: [13], chap 9, pp. 313–403 (2009)
17.
Zurück zum Zitat Hashiguchi, K.: Algorithms for determining relative star height and star height. Inf. Comput. 78(2), 124–169 (1988) MathSciNetCrossRef Hashiguchi, K.: Algorithms for determining relative star height and star height. Inf. Comput. 78(2), 124–169 (1988) MathSciNetCrossRef
18.
Zurück zum Zitat Hashiguchi, K., Ishiguro, K., Jimbo, S.: Decidability of the equivalence problem for finitely ambiguous finance automata. Int. J. Algebra Comput. 12(3), 445–461 (2002) MathSciNetCrossRef Hashiguchi, K., Ishiguro, K., Jimbo, S.: Decidability of the equivalence problem for finitely ambiguous finance automata. Int. J. Algebra Comput. 12(3), 445–461 (2002) MathSciNetCrossRef
19.
Zurück zum Zitat Kirsten, D.: A Burnside approach to the termination of Mohri’s algorithm for polynomially ambiguous min-plus-automata. Inf. Théor. Appl. 42(3), 553–581 (2008) MathSciNetCrossRef Kirsten, D.: A Burnside approach to the termination of Mohri’s algorithm for polynomially ambiguous min-plus-automata. Inf. Théor. Appl. 42(3), 553–581 (2008) MathSciNetCrossRef
20.
Zurück zum Zitat Kirsten, D.: Decidability, undecidability, and PSPACE-completeness of the twins property in the tropical semiring. Theor. Comput. Sci. 420, 56–63 (2012) MathSciNetCrossRef Kirsten, D.: Decidability, undecidability, and PSPACE-completeness of the twins property in the tropical semiring. Theor. Comput. Sci. 420, 56–63 (2012) MathSciNetCrossRef
21.
Zurück zum Zitat Kirsten, D., Lombardy, S.: Deciding unambiguity and sequentiality of polynomially ambiguous min-plus automata. In: Albers, S., Marion, J. (eds.) 26th International Symposium on Theoretical Aspects of Computer Science (STACS), Schloss Dagstuhl—Leibniz-Zentrum für Informatik, Leibniz International Proceedings in Informatics (LIPIcs), vol. 3, pp. 589–600 (2009) Kirsten, D., Lombardy, S.: Deciding unambiguity and sequentiality of polynomially ambiguous min-plus automata. In: Albers, S., Marion, J. (eds.) 26th International Symposium on Theoretical Aspects of Computer Science (STACS), Schloss Dagstuhl—Leibniz-Zentrum für Informatik, Leibniz International Proceedings in Informatics (LIPIcs), vol. 3, pp. 589–600 (2009)
22.
Zurück zum Zitat Klimann, I., Lombardy, S., Mairesse, J., Prieur, C.: Deciding unambiguity and sequentiality from a finitely ambiguous max-plus automaton. Theor. Comput. Sci. 327(3), 349–373 (2004) MathSciNetCrossRef Klimann, I., Lombardy, S., Mairesse, J., Prieur, C.: Deciding unambiguity and sequentiality from a finitely ambiguous max-plus automaton. Theor. Comput. Sci. 327(3), 349–373 (2004) MathSciNetCrossRef
23.
Zurück zum Zitat Komenda, J., Lahaye, S., Boimond, J., van den Boom, T.: Max-plus algebra in the history of discrete event systems. Ann. Rev. Control 45, 240–249 (2018) MathSciNetCrossRef Komenda, J., Lahaye, S., Boimond, J., van den Boom, T.: Max-plus algebra in the history of discrete event systems. Ann. Rev. Control 45, 240–249 (2018) MathSciNetCrossRef
24.
Zurück zum Zitat Koprowski, A., Waldmann, J.: Max/plus tree automata for termination of term rewriting. Acta Cybern. 19(2), 357–392 (2009) MathSciNetMATH Koprowski, A., Waldmann, J.: Max/plus tree automata for termination of term rewriting. Acta Cybern. 19(2), 357–392 (2009) MathSciNetMATH
25.
Zurück zum Zitat Krob, D.: The equality problem for rational series with multiplicities in the tropical semiring is undecidable. Int. J. Algebra Comput. 4(3), 405–426 (1994) MathSciNetCrossRef Krob, D.: The equality problem for rational series with multiplicities in the tropical semiring is undecidable. Int. J. Algebra Comput. 4(3), 405–426 (1994) MathSciNetCrossRef
26.
Zurück zum Zitat Kuich, W., Salomaa, A.: Semirings, Automata, Languages. EATCS Monographs in Theoretical Computer Science, vol. 5. Springer, Berlin (1986) Kuich, W., Salomaa, A.: Semirings, Automata, Languages. EATCS Monographs in Theoretical Computer Science, vol. 5. Springer, Berlin (1986)
27.
Zurück zum Zitat Larsen, K.G., Bodlaender, H.L., Raskin, J (eds.): 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS), Leibniz International Proceedings in Informatics (LIPIcs), vol. 83. Leibniz-Zentrum für Informatik, Schloss Dagstuhl (2017) Larsen, K.G., Bodlaender, H.L., Raskin, J (eds.): 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS), Leibniz International Proceedings in Informatics (LIPIcs), vol. 83. Leibniz-Zentrum für Informatik, Schloss Dagstuhl (2017)
28.
Zurück zum Zitat Mazowiecki, F., Riveros, C.: Pumping lemmas for weighted automata. In: Niedermeier R., Vallée B. (eds.) 35th Symposium on Theoretical Aspects of Computer Science (STACS), Schloss Dagstuhl—Leibniz-Zentrum für Informatik, Leibniz International Proceedings in Informatics (LIPIcs), vol. 96, pp. 50:1–50:14 (2018) Mazowiecki, F., Riveros, C.: Pumping lemmas for weighted automata. In: Niedermeier R., Vallée B. (eds.) 35th Symposium on Theoretical Aspects of Computer Science (STACS), Schloss Dagstuhl—Leibniz-Zentrum für Informatik, Leibniz International Proceedings in Informatics (LIPIcs), vol. 96, pp. 50:1–50:14 (2018)
29.
Zurück zum Zitat Mohri, M.: Finite-state transducers in language and speech processing. Comput. Linguist. 23(2), 269–311 (1997) MathSciNet Mohri, M.: Finite-state transducers in language and speech processing. Comput. Linguist. 23(2), 269–311 (1997) MathSciNet
30.
Zurück zum Zitat Mohri, M.: Weighted automata algorithms. In: [13], chap 6, pp. 213–254 (2009) Mohri, M.: Weighted automata algorithms. In: [13], chap 6, pp. 213–254 (2009)
31.
Zurück zum Zitat Paul, E.: The equivalence, unambiguity and sequentiality problems of finitely ambiguous max-plus tree automata are decidable. In: [27], vol. 53, pp. 1–53:13 (2017) Paul, E.: The equivalence, unambiguity and sequentiality problems of finitely ambiguous max-plus tree automata are decidable. In: [27], vol. 53, pp. 1–53:13 (2017)
32.
Zurück zum Zitat Paul, E.: Finite sequentiality of unambiguous max-plus tree automata. In: Niedermeier R., Paul C. (eds.) 36th International Symposium on Theoretical Aspects of Computer Science (STACS), Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Leibniz International Proceedings in Informatics (LIPIcs), vol. 126, pp. 55:1–55:17 (2019) Paul, E.: Finite sequentiality of unambiguous max-plus tree automata. In: Niedermeier R., Paul C. (eds.) 36th International Symposium on Theoretical Aspects of Computer Science (STACS), Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Leibniz International Proceedings in Informatics (LIPIcs), vol. 126, pp. 55:1–55:17 (2019)
33.
Zurück zum Zitat Petrov, S.: Latent variable grammars for natural language parsing. In: Coarse-to-Fine Natural Language Processing, Theory and Applications of Natural Language Processing, Springer, chap, vol. 2, pp. 7–46 (2012) Petrov, S.: Latent variable grammars for natural language parsing. In: Coarse-to-Fine Natural Language Processing, Theory and Applications of Natural Language Processing, Springer, chap, vol. 2, pp. 7–46 (2012)
34.
Zurück zum Zitat Rabin, M.O., Scott, D.S.: Finite automata and their decision problems. IBM J. Res. Dev. 3(2), 114–125 (1959) MathSciNetCrossRef Rabin, M.O., Scott, D.S.: Finite automata and their decision problems. IBM J. Res. Dev. 3(2), 114–125 (1959) MathSciNetCrossRef
35.
Zurück zum Zitat Sakarovitch, J.: A construction on finite automata that has remained hidden. Theor. Comput. Sci. 204(1–2), 205–231 (1998) MathSciNetCrossRef Sakarovitch, J.: A construction on finite automata that has remained hidden. Theor. Comput. Sci. 204(1–2), 205–231 (1998) MathSciNetCrossRef
36.
Zurück zum Zitat Sakarovitch, J.: Elements of Automata Theory. Cambridge University Press, Cambridge (2009) CrossRef Sakarovitch, J.: Elements of Automata Theory. Cambridge University Press, Cambridge (2009) CrossRef
37.
Zurück zum Zitat Salomaa, A., Soittola, M.: Automata-Theoretic Aspects of Formal Power Series. Texts and Monographs in Computer Science. Springer, Berlin (1978) CrossRef Salomaa, A., Soittola, M.: Automata-Theoretic Aspects of Formal Power Series. Texts and Monographs in Computer Science. Springer, Berlin (1978) CrossRef
38.
39.
Zurück zum Zitat Schützenberger, M.P.: Sur les relations rationnelles entre monoïdes libres. Theor. Comput. Sci. 3(2), 243–259 (1976) CrossRef Schützenberger, M.P.: Sur les relations rationnelles entre monoïdes libres. Theor. Comput. Sci. 3(2), 243–259 (1976) CrossRef
40.
41.
Zurück zum Zitat Simon, I.: Limited subsets of a free monoid. In: 19th Annual Symposium on Foundations of Computer Science (FOCS), pp. 143–150. IEEE Computer Society (1978) Simon, I.: Limited subsets of a free monoid. In: 19th Annual Symposium on Foundations of Computer Science (FOCS), pp. 143–150. IEEE Computer Society (1978)
42.
Zurück zum Zitat Simon, I.: Recognizable sets with multiplicities in the tropical semiring. In: Chytil, M.P., Janiga, L., Koubek, V. (eds.) 13th International Symposium on Mathematical Foundations of Computer Science (MFCS), Springer, Lecture Notes in Computer Science, vol. 324, pp. 107–120 (1988) Simon, I.: Recognizable sets with multiplicities in the tropical semiring. In: Chytil, M.P., Janiga, L., Koubek, V. (eds.) 13th International Symposium on Mathematical Foundations of Computer Science (MFCS), Springer, Lecture Notes in Computer Science, vol. 324, pp. 107–120 (1988)
43.
Zurück zum Zitat Waldmann, J.: Weighted automata for proving termination of string rewriting. Journal of Automata Lang. Comb. 12(4), 545–570 (2007) MathSciNetMATH Waldmann, J.: Weighted automata for proving termination of string rewriting. Journal of Automata Lang. Comb. 12(4), 545–570 (2007) MathSciNetMATH
44.
Zurück zum Zitat Weber, A., Seidl, H.: On the degree of ambiguity of finite automata. Theor. Comput. Sci. 88(2), 325–349 (1991) MathSciNetCrossRef Weber, A., Seidl, H.: On the degree of ambiguity of finite automata. Theor. Comput. Sci. 88(2), 325–349 (1991) MathSciNetCrossRef
Metadaten
Titel
Finite Sequentiality of Unambiguous Max-Plus Tree Automata
verfasst von
Erik Paul
Publikationsdatum
26.03.2021
Verlag
Springer US
Erschienen in
Theory of Computing Systems / Ausgabe 4/2021
Print ISSN: 1432-4350
Elektronische ISSN: 1433-0490
DOI
https://doi.org/10.1007/s00224-020-10021-w

Weitere Artikel der Ausgabe 4/2021

Theory of Computing Systems 4/2021 Zur Ausgabe

Premium Partner