Mathieu Caralp

Pierre-Alain Reynier

Jean-Marc Talbot

Visibly Pushdown Automata with Multiplicities: Finiteness and K-Boundedness

We propose an extension of visibly pushdown automata by means of weights (represented as positive integers) associated with transitions, called visibly pushdown automata with multiplicities. The multiplicity of a computation is the product of the multiplicities of the transitions used along this computation. The multiplicity of an input is the sum of the ones of all its successful computations. Finally, the multiplicity of such an automaton is the supremum of multiplicities over all possible inputs. We prove the problem of deciding whether the multiplicity of an automaton is finite to be in PTIME. We also consider the K-boundedness problem, i.e. deciding whether the multiplicity is bounded by K: we prove this problem to be EXPTIMEcomplete when K is part of the input and in PTIME when K is fixed. As visibly pushdown automata are closely related to tree automata, we discuss deeply the relationship of our extension with weighted tree automata.

Introduction

Visibly pushdown automata (VPA for short) have been proposed in [START_REF] Alur | Visibly pushdown languages[END_REF] as an interesting subclass of pushdown automata, strictly more expressive that finite state automata, but still enjoying good closure and decidability properties. They are pushdown automata such that the behavior of the stack, i.e. whether it pushes or pops, is visible in the input word. Technically, the input alphabet is partitioned into call, return and internal symbols. When reading a call the automaton must push a symbol onto the stack, when reading a return it must pop and when reading an internal it cannot touch the stack. The partitioning of the alphabet induces a nesting structure of the input word. Calls and returns can be viewed as opening/closing brackets, and well-nested words are words where every call symbol (resp. return symbol) has a matching return (resp. call).

The original motivation for their introduction was for verification purposes, the stack being used for the modelization of call/returns of functions. Another application domain is the processing of XML documents. Indeed, unranked trees in their linear form can be viewed as well-nested words. Actually, the model of visibly pushdown automata is expressively equivalent to that of finite tree automata, see [START_REF] Alur | Visibly pushdown languages[END_REF].

It is quite standard to extend a class of automata with weights, by adding a labeling function assigning a weight to each transition. In this work, we consider VPA with multiplicities (N-VPA for short) where weights are positive integers (multiplicities). The multiplicity of a run is the product of the multiplicities of the transitions used along it. The multiplicity of a word is the sum of the ones of all its accepting runs. Finally, the multiplicity of the automaton is the supremum of the multiplicities of the words it accepts. This model extends the model of finite state automata with multiplicities [START_REF] Sakarovitch | Elements of Automata Theory[END_REF].

A special case of multiplicity is the degree of ambiguity of a word, i.e. the number of accepting runs (obtained when every transition has weight 1). The class of finitely ambiguous automata has been investigated for both automata on words and on trees [START_REF] Chan | On the finite-valuedness problem for sequential machines[END_REF][START_REF] Weber | On the degree of ambiguity of finite automata[END_REF][START_REF] Seidl | On the finite degree of ambiguity of finite tree automata[END_REF][START_REF] Seidl | Deciding equivalence of finite tree automata[END_REF]. The interest in this class arised from the fact that it allows an efficient (polynomial) equivalence check. An analogy can be drawn with the context of transducers where the equivalence problem is decidable for finite-valued transducers (and undecidable in general). In [START_REF] Sakarovitch | On the decidability of bounded valuedness for transducers[END_REF], the characterization of automata whose multiplicity is finite is used to build a characterization of finite-valued word transducers. The present work is thus a first step towards the characterization of finite-valued visibly pushdown transducers, which is a relevant issue as this model is incomparable with bottom-up tree transducers (see [START_REF] Filiot | Properties of visibly pushdown transducers[END_REF]).

The first problem we consider is the finiteness of the multiplicity of an automaton, i.e. does there exist K ∈ N such that the multiplicity is bounded by K. To solve this problem, we extend a characterization of finite state automata based on patterns to visibly pushdown automata. We also provide an algorithm to decide the presence of these patterns in polynomial time. The second class of problems asks whether the multiplicity of an automaton is bounded by K, where K is given. This problem can be considered under the hypothesis that K is part of the input, or is fixed. We show that the problem is EXPTIME-complete in the first case, and can be solved in polynomial time in the second one. Finally, we make a comparison of our results with existing results for the equivalent model of tree automata with weights on the semiring (N, +, •). As this equivalence is effective, we discuss the consequences of our results in this context.

Definitions are given in Section 2. Comparisons with existing results for tree automata with multiplicities are drawn in Section 3. In Section 4, we give the characterization of N-VPA with infinite multiplicity based on original patterns and the decision procedure associated. We study K-boundedness problems in Section 5, and conclude with an application of our results to tree automata in Section 6. Details of proofs and definitions about tree automata are omitted, and can be found in the appendix.

Definitions

Preliminaries

All over this paper, Σ denotes a finite alphabet partitioned into three disjoint sets Σ c , Σ r and Σ ι , denoting respectively the call, return and internal alphabets. We denote by Σ * the set of (finite) words over Σ and by ǫ the empty word. The length of a word u is denoted by |u|. The set of well-nested words Σ * wn is the smallest subset of Σ * such that Σ * ι ⊆ Σ * wn and for all c ∈ Σ c , all r ∈ Σ r , all u, v ∈ Σ * wn , cur ∈ Σ * wn and uv ∈ Σ * wn . Let u = α 0 α 1 • • • α k-1 ∈ Σ * be a word with α i ∈ Σ, for 0 ≤ i ≤ k -1. Let 0 ≤ i ≤ j ≤ |u|, then u i,j denotes the word α i • • • α j-1 if i < j, and the empty word

if i = j. A position i < |u| is a pending call if α i ∈ Σ c and for all i < j ≤ |u|, u i,j ∈ Σ *
wn . The height of u at position i, denoted by h u (i), is the number of pending calls of u 0,i , i.e. h u (i) = |{j | 0 ≤ j < i and α j is a pending call of u 0,i }|. The height of u is the maximal height of all the positions of u:

h u = max 0≤i≤|u| h u (i). For instance, h (crcrcc) = h (ccrcrr) = 2.

Visibly Pushdown Automata with Multiplicities

Visibly pushdown automata [START_REF] Alur | Visibly pushdown languages[END_REF] are a restriction of pushdown automata in which the stack behavior is imposed by the input word. On a call symbol, the VPA pushes a symbol onto the stack, on a return symbol, it must pop the top symbol of the stack and on an internal symbol, the stack remains unchanged.

Definition 1 (Visibly pushdown automata [1]). A visibly pushdown automaton

(VPA) over Σ is a tuple A = (Q, Γ, δ, Q in , Q f ) where Q is a finite set of states, Q in ⊆ Q is the set of initial states, Q f ⊆ Q is the set of final states, Γ is a finite stack alphabet, δ = δ c ⊎δ r ⊎δ ι is the set of transitions, with δ c ⊆ Q×Σ c ×Γ ×Q, δ r ⊆ Q×Σ r ×Γ ×Q, and δ ι ⊆ Q × Σ ι × Q.
Configuration -Run -Degree of ambiguity. A configuration of a VPA is a pair (q, σ) ∈ Q × Γ * (where Γ * denotes the set of finite words over Γ ). We denote by ⊥ the empty word on Γ . Initial (resp. final) configurations are configurations of the form (q, ⊥), with q ∈ Q in (resp. q ∈ Q f ).

A run of A on a sequence of transitions η = {t i } 1≤i≤k from a configuration (q, σ) to a configuration (q ′ , σ ′ ) over a word u = α 0 . . . α k-1 ∈ Σ * is a finite non-empty sequence ρ = {(q i , σ i )} 0≤i≤k such that q 0 = q, σ 0 = σ, q k = q ′ , σ k = σ ′ and for each

1 ≤ i ≤ k, t i = (q i-1 , α i-1 , γ i , q i ) ∈ δ c and σ i = σ i-1 γ i or t i = (q i-1 , α i , γ i , q i ) ∈ δ r and σ i-1 = σ i γ i , or t i = (q i-1 , α i , q i ) ∈ δ ι and σ i = σ i-1 .
We say that the run is labeled by the word u and denote this run by (q, σ) u -→ (q ′ , σ ′ ). A run is accepting if it starts in an initial configuration and ends in a final configuration. The degree of ambiguity of A, denoted by da(A), is the maximal number of accepting runs for any possible input word.

Language. A word u is accepted by A if there exists an accepting run of A on u. The language of A, denoted by L(A), is the set of words accepted by A. Note that we require here to end up with an empty stack, this restriction implies that all accepted words are well-nested. Unlike [START_REF] Alur | Visibly pushdown languages[END_REF], we do not consider returns on empty stack and unmatched calls. This assumption is done to avoid technical details but the general framework could be handled 1 .

Trimmed. A configuration (q, σ) is reachable (resp. co-reachable) if there exists u ∈ Σ * and q 0 ∈ Q in (resp. q f ∈ Q f ) such that (q 0 , ⊥) u -→ (q, σ) (resp. such that (q, σ) u -→ (q f , ⊥)). A VPA A is trimmed if
every reachable configuration is co-reachable, every co-reachable configuration is reachable and if every state of A belongs to a reachable configuration. In [START_REF] Caralp | A polynomial procedure for trimming visibly pushdown automata[END_REF], we present a procedure which allows to trim a VPA and which preserves the set of accepting runs. We also prove that this procedure can be applied to the model of N-VPA (see below).

Path. A path over a word u ∈ Σ * is a sequence of transitions η = {t i } 1≤i≤k such that there exists a run on η labeled by the word u. Note that there may be different runs on the same path, differing in their initial configurations. The empty path (on the empty word ǫ) is denoted by η ǫ . A path is said to be accepting whenever there exists an accepting run over it. Let η be a path over a word u = ǫ, then there exist states p and q such that any run over η goes from a configuration (p, σ) to a configuration (q, σ ′ ) for some σ, σ ′ ∈ Γ * . We then say that η goes from p to q, and write η :

p u -→ q. Lemma 1. a. Let u i ∈ Σ * \ {ǫ} and η i : p i ui -→ q i a path over u i for i ∈ {1, 2, 3} such that u 1 u 3 , u 2 ∈ Σ *
wn , and η 1 η 2 η 3 is a path. Then:

-for all η ′ 2 : p 2 u ′ 2 -→ q 2 such that u ′ 2 ∈ Σ * wn \ {ǫ}, η 1 η ′ 2 η 3 is a path, -if p 1 = q 1 and p 3 = q 3 , then η 2 1 η 2 η 2
3 is a path. b. Assume A is trimmed. For any family (η i ) i∈I of paths going from p to q on some well-nested word u = ǫ, there exist two paths η ′ , η ′′ such that for any i ∈ I, η ′ η i η ′′ is an accepting path.

We introduce the model of VPA with multiplicities in N (N-VPA for short), where transitions are labeled by positive integers:

Definition 2 (N-VPA). An N-VPA is a pair T = (A, λ) composed of a VPA A = (Q, Γ, δ, Q in , Q f ) and a labeling function λ : δ → N >0 .
The notions of configurations, runs and paths are lifted from VPA to N-VPA. We define the language of an N-VPA T = (A, λ) as the language of A. Multiplicity. For each transition t ∈ δ, λ(t) is called the multiplicity of t. Let η = {t i } 1≤i≤k be a path of A over the word u and let m i = λ(t i ) for 1 ≤ i ≤ k. The multiplicity of η denoted by η is 1≤i≤k m i . Let a word u = ǫ, we write p u|m --→ q when there exists a path over u from p to q with multiplicity m. The multiplicity of the empty path η ǫ is 1.

We define the multiplicity of a run ρ, denoted by ρ , as the one of its underlying path η. Let u ∈ L(T ) be a word. The multiplicity of u, denoted by u is the sum of the multiplicities of the accepting runs for the word u. The multiplicity of an N-VPA T , denoted by T , is defined as T = sup{ u | u ∈ L(T )}. Let K ∈ N. We say that T is bounded by K if T ≤ K. We say that T is finite if we have T < +∞, and infinite otherwise. Note that the degree of ambiguity of a VPA is equal to the multiplicity of the corresponding N-VPA where all the multiplicities of transitions are set to 1.

Relating Tree Automata and VPA

There is a strong relationship between words written over a partitioned alphabet and (un)ranked trees. This relationship extends to recognizers with VPA on one side and tree automata on the other side. A polynomial time construction from VPA to tree automata is presented in [START_REF] Alur | Visibly pushdown languages[END_REF]. This latter construction preserves the language but not the computations; however, the construction can be slightly modified to guarantee the isomorphism of accepting computations [START_REF] Caralp | Automates à pile visible : ambiguité et valuation[END_REF]. Conversely, it is easy to encode ranked trees as well-nested visible words, and to build from a tree automaton a VPA accepting the encodings and preserving the accepting computations as well.

Note that preserving (accepting) computations implies that the degree of ambiguity of the encoded VPA and of the target tree automaton are the same.

Hence, one may now wonder whether this relationship extends to models with weights and what are the results known for weighted tree automata that carry over N-VPA: this question is crucial as in one direction, it may be the case that problems we want to address could be solved thanks to this relationship and on the other direction, new results for N-VPA may carry over weighted tree automata almost for free. Weighted tree automata [START_REF] Fülöp | Handbook of Weighted Automata, chapter Weighted Tree Automata and Tree Transducers[END_REF] over the semiring (N, +, .) allow to encode N-VPA: the weight of a node in a run is the product of the weight of its children multiplied by the one associated with the transition rule applied at this node, the weight of a tree being the sum of the weights of its accepting runs. Thanks to one-to-one isomorphism between the transitions of the N-VPA and the ones of the tree automaton recognizing stack trees, weights are preserved by this translation. Conversely, when a (ranked) tree automaton is translated into a VPA, a transition rule for some symbol a of the tree automaton is encoded as two rules in the VPA (one for a call symbol a, one for a return symbol a ), the weight of the rule in the tree automaton being associated with one of the twos, the other one having multiplicity 1 (see Appendix C).

Let us briefly recap some known results for tree automata with weights/costs. In [START_REF] Seidl | Finite tree automata with cost functions[END_REF], (ranked) tree automata with polynomial costs are considered over several semirings. The main ingredient of these automata is that a polynomial over a semiring is attached to transitions : computing the cost of a node amounts to apply the polynomial with each variable x i instanciated with the cost of the ith child. However, the result of the computation is the set of costs computed for each accepted run (no combination is made with the accepting computations over the same input tree). Finiteness and K-boundedness problems whose decidability issues are addressed relate to the finiteness and to the K-boundedness of this set of costs (shown to be in PTIME for many semirings and in particular, (N, +, .)) and is thus different from the problems we consider here. These results are extended in [START_REF] Borchardt | Bounds for tree automata with polynomial costs[END_REF] by considering more general semirings but without addressing complexity issues.

As already mentioned, the degree of ambiguity and the multiplicity of automata are related. In particular, finiteness or K-boundedness problems of the degree of ambiguity of tree automata provide lower bounds for the corresponding problems for N-VPA.

However, the algorithms for finiteness of the degree of ambiguity [START_REF] Seidl | On the finite degree of ambiguity of finite tree automata[END_REF] (deciding DA = da(A) < +∞) in PTIME and of the cost of some tree automaton with costs [START_REF] Seidl | Finite tree automata with cost functions[END_REF] (deciding MM = sup{ ρ | ρ an accepting computation} < +∞) in PTIME can be combined to get a PTIME algorithm for finiteness of weighted tree automata, thanks to the following statement : max(DA, MM) ≤ A ≤ DA * MM. Thanks to the PTIME encoding of N-VPA into weighted tree automata preserving the degree of ambiguity and the multiplicities of encoded computations, we obtain a PTIME algorithm for finiteness of N-VPA. However, our approach provides a direct method based on VPA and a rather intuitive algorithm compared to [START_REF] Seidl | On the finite degree of ambiguity of finite tree automata[END_REF][START_REF] Seidl | Finite tree automata with cost functions[END_REF]. Moreover, we will see in Section 6 that conversely, our approach leads to a new vision and a new and rather simple PTIME algorithm for finiteness of weighted tree automata over (N, +, .).

[14] also relates the degree of ambiguity and costs provided the use of multi dimensional cost automata. We believe that this may be extended to the computation of multiplicities. As pointed out in [START_REF] Seidl | Finite tree automata with cost functions[END_REF], this would yield an exponential time-complexity method to test K-boundedness, the algorithm being exponential in the dimension which is in this case the number of states of the tree automaton (we will show that this problem with the binary encoding of K being part of the input, for VPA and for tree automata is EXPTIME-hard). However, we will present a much simpler approach based on [START_REF] Chan | On the finite-valuedness problem for sequential machines[END_REF] to tackle this problem.

Characterization and decision of infinite N-VPA

In this section, we give a characterization on N-VPA ensuring their infiniteness by means of patterns. Then, based on this characterization, we devise a PTIME algorithm to solve the finiteness problem. All over this section, we assume a trimmed N-VPA

T = (A, λ), with A = (Q, Γ, δ, Q in , Q f ).
We denote by n the cardinality of Q, and by L the value max{λ(t) | t ∈ δ}.

Characterization

We introduce the criteria depicted on Figures 1(a) and 1(b) which characterize infinite N-VPA. Pattern of Figure 1(a) coincides with patterns for finite-state automata with multiplicities (see [START_REF] Weber | On the degree of ambiguity of finite automata[END_REF][START_REF] Souza | Étude structurelle des transducteurs de norme bornée[END_REF]). Pattern of Figure 1(b) is specific to the model of VPA. Intuitively, the loop over a well-nested word is splitted into two loops on words u 1 and u 2 , such that the concatenation u 1 u 2 is a well-nested word but u 1 is not well-nested. We say that T contains a pattern whenever there exist words in Σ * , states of T and paths in T that fulfill all the conditions of the pattern. For instance, if we consider the pattern (S1), we should find a word u ∈ Σ * wn , two states p, q ∈ Q (which may be equal), three paths η 1 :

p u|m1 ---→ p, η 2 : p u|m2 ---→ q, η 3 : q u|m3 ---→ q such that η 1 η 2 η 3 is a path, and m 1 > 1 or η 1 = η 2 .
In these patterns, all words except w are necessarily non-empty. Note that these patterns also yield a characterization of infinite ambiguity by removing the disjunctions on multiplicities (conditions m > 1). We will show in this section that these criteria characterize infinite N-VPA:

p q η2 : u | m2 η1 : u | m1 η3 : u | m3 (a) (S1) Well-nested case: u ∈ Σ * wn . η1η2η3 is a path and m1 > 1 or η1 = η2. p q q ′ p ′ η2 : u1|m2 η : w|m η ′ 2 : u2|m ′ 2 η1 : u1|m1 η3 : u1|m3 η ′ 3 : u2|m ′ 2 η ′ 1 : u2|m ′ 1 (b) (S2) Matched loops case: w ∈ Σ * wn , u1u2 ∈ Σ * wn , and u1 ∈ Σ * wn . η1η2η3ηη ′ 3 η ′ 2 η ′ 1 is a path, and either (m1 > 1 or m ′ 1 > 1), or (η1 = η2 or η ′ 1 = η ′ 2 ).
Theorem 1. Let T be an N-VPA. T

is infinite if and only if T complies with one of the criteria (S1) and (S2).

To prove this result, we first show that if we have one of the criteria then the multiplicity is infinite. In a second part we show that if the multiplicity is infinite, then the N-VPA complies with one of the criteria. Lemma 2. Let T be an N-VPA. If T complies with (S1) or (S2), then T is infinite.

Proof (Sketch). We sketch the proof for criterion (S1), the case of (S2) being similar. Let u ∈ Σ * wn and η 1 , η 2 , η 3 be paths selected according to pattern (S1). We first suppose that condition m 1 > 1 holds. As η 1 is a path going from p to p and u ∈ Σ * wn , η 2 1 is also a path from p to p. By applying iteratively Lemma 1.a, we can consider path η i 1 whose multiplicity η i 1 = m i 1 grows to infinity when i tends to +∞. As T is trimmed, by Lemma 1.b, this gives accepting paths with multiplicity growing to infinity. Consider now the case where the condition η 1 = η 2 holds. Let k ∈ N >0 , and i, j ∈ N such that i + j = k -1. As η 1 η 2 η 3 is a path and u ∈ Σ * wn , by Lemma 1.a, the path η i 1 η 2 η j 3 is a path over the word u k . Moreover, as η 1 = η 2 , all these paths are different when i, j range over the set of integers such that i + j = k -1. When k tends to infinity, we obtain an arbitrarily large number of paths over u k going from p to q. As T is trimmed, by Lemma 1.b, this gives arbitrarily many accepting paths over a same word.

⊓ ⊔

The proof of the converse (an infinite multiplicity implies the presence of one of the criteria) relies on the two technical Lemmas 4 and 5 which we present intuitively. To state these lemmas, we define the constant N = (n 2 L) 2 |Γ | and the function ψ : N → N as ψ(z) = n(N z) 2 n . Pattern (S1) allows to increase the multiplicity along a well-nested word. Lemma 4 states that if T does not comply with (S1), then a well-nested word u whose multiplicity is greater than ψ(l) has a well-nested subword v whose multiplicity is greater than l, and such that h u > h v . Then, Lemma 5 applies iteratively Lemma 4 to prove that a word with large multiplicity has a large height, and hence allows to find pattern (S2), using a vertical pumping.

Let u ∈ Σ * wn and k = |u|. Given two positions i, j such that 0 ≤ i ≤ j ≤ k and u i,j ∈ Σ * wn , we define a matrix, denoted by induced u i,j , representing intuitively how the multiplicities of runs are modified by the subword u i,j . Formally, induced u i,j is an element of N Q×Q , and for p, q ∈ Q, we let induced u i,j (p, q) be the sum of the multiplicities of the paths η : p ui,j --→ q of T for which there exist η 1 path on u 0,i , η 2 path on u j,k such that η 1 ηη 2 is an accepting path on u.

Finally, we also define s u i,j ∈ N as s u i,j = p,q∈Q induced u i,j (p, q). We have:

Lemma 3. Let u ∈ Σ * wn and three positions i, j, k such that 0 ≤ i ≤ j ≤ k ≤ |u| and u i,j , u j,k , u i,k ∈ Σ * wn . Then we have induced u i,k = induced u i,j × induced u j,k , s u i,j ≤ s u i,k , and s u i,k ≤ s u i,j .s u j,k .
Lemma 4. We suppose that T is infinite but T does not comply with (S1). Let u ∈ L(T ), l ∈ N >0 and x, y be two positions such that 0 ≤ x ≤ y ≤ |u|, u x,y ∈ Σ * wn and s u

x,y ≥ ψ(l). Then there exist two positions

x < x ′ ≤ y ′ < y such that u x ′ ,y ′ ∈ Σ * wn , h u (x ′ ) = h u (x) + 1 and s u x ′ ,y ′ ≥ l.
Proof (Sketch). The proof is based on a pumping on positions in the set

P = {i ∈ N >0 | x ≤ i ≤ y ∧ u x,i ∈ Σ * wn }.
This approach is similar to that used in [START_REF] Souza | Étude structurelle des transducteurs de norme bornée[END_REF] for automata on words. For each i ∈ P , we define r i = s u x,i and

X i = {q ∈ Q | induced u
x,i (p, q) > 0 for some p}. Intuitively, r i corresponds to the multiplicity associated with the wellnested subword u x,i and X i is the set of states that can be reached after this subword (along an accepting path over u). For any i < j, i, j ∈ P , we have thanks to Lemma 3, r i ≤ r j and r j ≤ r i × s u i,j . Suppose, for the sake of contradiction, that for any two consecutive indices i < j in P , we have s u i,j < N l. Using the hypothesis r y = s u x,y ≥ ψ(l) and the definition of ψ, we can prove that this entails that there exist two positions i < j in the set P such that r i < r j and X i = X j . Let v = u i,j and X = X i . We define a multigraph X = (X, E) where E ⊆ X × X × N is defined as follows: ∀p, q ∈ X, m ∈ N, for each path η : p v|m --→ q such that η ′ ηη ′′ is an accepting path on u for some paths η ′ on word u 0,i and η ′′ on word u j,|u| , we construct an edge p m -→ q ∈ E. Thanks to property r i < r j , we show that either there is a vertex with two outgoing edges, or X is composed of disjoint loops and contains an edge with label m > 1. In the former case, we prove that T contains pattern (S1) with property η 1 = η 2 while in the latter case, we prove it contains (S1) with property m 1 > 1. This contradicts our hypothesis on T .

Hence, we have proven that there exist two indices i < j in P such that s u i,j ≥ N l. Then, we can extract from i and j the two expected indices x ′ and y ′ .

⊓ ⊔ Lemma 5. Let T be an N-VPA. If T is infinite, then T complies with one of the two criteria (S1) and (S2).

Proof (Sketch). Suppose that T is infinite but does not comply with (S1), and prove it complies with (S2). Let u ∈ L(T ) be a word such that u ≥ ψ H (1) where H = 2 n 2 and ψ h+1 = ψ • ψ h , for h ∈ N. By applying Lemma 4 iteratively, we define a sequence of length greater than H of couples of positions χ i = (x i , y i ) of u. These couples represent well-nested subwords of u, which are recursively embedded. In addition, their multiplicities s u χi are strictly decreasing. We then proceed with a pumping argument similar to the one done in the proof of Lemma 4, and exhibit the pattern (S2).

⊓ ⊔

Decidability of finiteness

We show in this part how to decide in PTIME the presence of one of the patterns. The algorithm (Figure 2) uses four bunches of inference rules applied as a saturation procedure: the first bunch builds a set S 0 of pairs (p, q) such that there exists a path over a well-nested word from p to q. The second bunch builds a set S 1 of tuples composed of 6 states and a Boolean, which allows to decide the presence of the pattern (S1). The 6 states represent the source and the target of 3 paths over the same well-nested word and the Boolean retains an information about a multiplicity greater than 1 or the fact that different paths are considered. The third bunch builds a set S 2 of tuples composed of 12 states and a Boolean which allows to decide the presence of pattern (S2). This construction is based on S 1 : the states aim to identify two sets of 3 paths over two words u 1 and u 2 , such that the second set pops the stack pushed by the first set, ensuring that u 1 u 2 ∈ Σ * wn . The information stored in the Boolean depends on one of the sets. Finally, the last bunch builds a set S 3 which ensures that some tuple built in S 1 forms the pattern (S1) in the rule 4.1, or that some tuple built in S 2 represents the pattern (S2), which in addition are connected through a well-nested word (condition over S 0 ) in the rule 4.2.

Proposition 1. For any N-VPA T , (⊤) ∈ S 3 iff T is infinite.

Theorem 2. Finiteness for N-VPA is in PTIME. p ∈ Q (1.1) (p, p) ∈ S0 (p, a, q) ∈ δι (1.2) (p, q) ∈ S0 (p, q) ∈ S0, (q, q ′ ) ∈ S0 (1.3) (p, q ′ ) ∈ S0 (p, q) ∈ S0, (p ′ , c, γ, p) ∈ δc, (q, r, γ, q ′ ) ∈ δr (1.4) (p ′ , q ′ ) ∈ S0 pi ∈ Q for all i ∈ {1, 2, 3} (2.1) (p1, p1, p2, p2, p3, p3, ⊥) ∈ S1 ti = (pi, a, p ′ i ) ∈ δι for all i ∈ {1, 2, 3} (2.2) (p1, p ′ 1 , p2, p ′ 2 , p3, p ′ 3 , (t1 = t2 ∨ ϕ1)) ∈ S1 (p1, q1, p2, q2, p3, q3, B) ∈ S1, (q1, q ′ 1 , q2, q ′ 2 , q3, q ′ 3 , B ′ ) ∈ S1 (2.3) (p1, q ′ 1 , p2, q ′ 2 , p3, q ′ 3 , B ∨ B ′ ) ∈ S1 (p1, q1, p2, q2, p3, q3, B) ∈ S1, ti = (p ′ i , c, γi, pi) ∈ δc, t ′ i = (qi, r, γi, q ′ i ) ∈ δr for all i ∈ {1, 2, 3} (2.4)
(p ′ 1 , q ′ 1 , p ′ 2 , q ′ 2 , p ′ 3 , q ′ 3 , B ∨ (t1 = t2 ∨ t ′ 1 = t ′ 2 ∨ ϕ ′ 1 ∨ ϕ1)) ∈ S1 (p1, q1, p2, q2, p3, q3, B) ∈ S1, (q ′ 3 , p ′ 3 , q ′ 2 , p ′ 2 , q ′ 1 , p ′ 1 , B ′ ) ∈ S1 (3.1) (p1, q1, p2, q2, p3, q3, q ′ 3 , p ′ 3 , q ′ 2 , p ′ 2 , q ′ 1 , p ′ 1 , B ∨ B ′ ) ∈ S2 ti = (p ′ i , c, γi, pi) ∈ δc, t ′ i = (qi, r, γi, q ′ i ) ∈ δr, for all i ∈ {1, 2, 3} (3.2)
(p ′ 1 , p1, p ′ 2 , p2, p ′ 3 , p3, q3, q ′ 3 , q2, q ′ 2 , q1, q ′ 1 , t1 = t2 ∨ t ′ 1 = t ′ 2 ∨ ϕ1 ∨ ϕ ′ 1 ) ∈ S2 (p1, p ′ 1 , p2, p ′ 2 , p3, p ′ 3 , q ′ 3 , q3, q ′ 2 , q2, q ′ 1 , q1, B) ∈ S2, (p ′′ 1 , p1, p ′′ 2 , p2, p ′′ 3 , p3, q3, q ′′ 3 , q2, q ′′ 2 , q1, q ′′ 1 , B ′ ) ∈ S2 (3.3) (p ′′ 1 , p ′ 1 , p ′′ 2 , p ′ 2 , p ′′ 3 , p ′ 3 , q ′ 3 , q ′′ 3 , q ′ 2 , q ′′ 2 , q ′ 1 , q ′′ 1 , B ∨ B ′ ) ∈ S2
(p, p, p, q, q, q, ⊤) ∈ S1 (4.1) (⊤) ∈ S3 (q, q ′ ) ∈ S0, (p, p, p, q, q, q, q ′ , q ′ , q ′ , p ′ , p We consider a trimmed N-VPA T = (A, λ), with A = (Q, Γ, δ, Q in , Q f ) and an integer K ∈ N >0 represented in binary and describe an algorithm to decide whether T < K.

′ , p ′ , ⊤) ∈ S2 (4.2) (⊤) ∈ S3 with ϕ1 = λ(t1) > 1 and ϕ ′ 1 = λ(t ′ 1 ) > 1
The procedure we describe builds a set M of n × n integer matrices by saturation, where rows and columns of matrices are indexed by states of A. The semantics of a matrix M ∈ M can be understood as follows: there exists a word u ∈ Σ * wn such that, for any p, q ∈ Q, the entry M (p, q) is equal to the sum of the multiplicities of paths p u -→ q. We have then u = qi∈Qin,q f ∈Q f M (q i , q f ). For an n × n integer matrix M , we denote by M the value qi∈Qin,q f ∈Q f M (q i , q f ).

The algorithm proceeds by building such matrices for well-nested words of increasing lengths. It starts with internal words of length 1, and then extends words either by concatenation, or by adding a matching pair of call/return symbols.

We introduce the following notations: let M ǫ be the identity matrix. Let a ∈ Σ ι , then M a is the matrix defined by M a (p, q) = λ(t) if there exists t = (p, a, q) ∈ δ ι , and M a (p, q) = 0 otherwise. Let γ ∈ Γ and let c ∈ Σ c (resp. r ∈ Σ r ), then M c,γ (resp. M r,γ ) is the matrix defined by M c,γ (p, q) = λ(t) if there exists t = (p, c, γ, q) ∈ δ c , and M c,γ (p, q) = 0 otherwise (and similarly for matrix M r,γ ).

Finally, we introduce the operator Extra K : N → N defined by Extra K (z) = z if z ≤ K, and Extra K (z) = K otherwise. This operator is naturally extended to integer matrices. Our algorithm is presented as Algorithm 1.

Algorithm 1 Decision of the K-boundedness of an N-VPA

Require: An N-VPA T and K ∈ N>0

1: M {ExtraK (Ma) | a ∈ Σι} ∪ {Mǫ} 2: M ′ ∅ 3: repeat 4: M M ∪ M ′ 5: if ∃M ∈ M such that M ≥ K then 6:
return false 7:

end if This complexity should be compared with that of determining whether the ambiguity of a finite state automaton is less than K which is known to be PSPACE-complete [START_REF] Chan | On the finite-valuedness problem for sequential machines[END_REF].

8: M ′ {ExtraK (M1.M2) | M1, M2 ∈ M} ∪ {ExtraK ( γ∈Γ Mc,γ .M.Mr,γ ) | M ∈ M, c ∈ Σc,
Proof (Sketch). The EXPTIME membership follows from the fact that all the matrices built are n × n matrices whose entries are bounded by K. For the hardness, we can proceed to a reduction from the emptiness of the intersection of K deterministic bottomup tree automata [START_REF] Comon | Tree automata techniques and applications[END_REF]. One can first consider the tree automaton obtained as the disjoint union of these K automata. Then one can turn this tree automaton into a VPA accepting the encodings of the trees as well-nested words, and with an isomorphic set of accepting runs. Considering this VPA as an N-VPA T (each multiplicity is set to 1), one can show that the intersection of the K deterministic tree automata is empty iff T < K.

⊓ ⊔

Computing the multiplicity of a finite N-VPA Consider now, given a finite N-VPA, the problem consisting in computing its multiplicity. We derive from the previous algorithm a procedure solving this problem. The procedure simply explores as before the set of matrices, without using the operator Extra K , until saturation of the set of matrices. The termination of the algorithm relies on the fact that T is finite and trimmed. Indeed, this entails that coefficients computed are all bounded by T . In particular, this proves that the number of matrices built is bounded by T n 2 , and:

Theorem 4. For all finite N-VPA T , the value of T can be computed in time T O(n 2 ) .

Deciding K-bounded multiplicity (for a fixed K)

As a final result in this section, we investigate the K-bounded multiplicity problem for which the input is only an N-VPA T and we ask whether T < K. The algorithm from Section 5.1 shows that this problem for a fixed K can be solved in exponential time; however, by adapting the approach used in [START_REF] Seidl | Deciding equivalence of finite tree automata[END_REF] for ambiguity of tree automata, Theorem 5. Fix K ∈ N >0 . For an N-VPA T , deciding whether T < K is in PTIME.

Proof. We consider the family of VPA's (A i ) 1≤i≤K such that A i accepts words from L(T ) having a multiplicity greater than K. More precisely, A i is a VPA that accepts words u such that there are i different accepting runs ρ 1 , . . . , ρ i of T over u verifying 1≤j≤i ρ j ≥ K. Therefore, A i simulates in parallel i runs of T over the same word, and for each of them keeps track of the current multiplicity in its states by computing up to K. More precisely, for

T = (A, λ), with A = (Q, Γ, δ, Q in , Q f ), we define A i as (Q i , Γ i , δ i , Q i in , Q i f ) where Q i = (Q × [1..K]) i × B i×i , Γ i = (Γ ) i , Q i in = (Q in × {1}) i × {0 B i×i }, Q i f = {((q 1 , m 1 ), . . . , (q i , m i )) × {Id B i×i } | (q 1 , . . . , q i ) ∈ (Q f ) i , ( 1≤j≤i m j ) ≥ K}.
The element of B i×i , which is the set of the i × i square matrices of Booleans, is used to store whether the runs are distinct. 0 B i×i (resp. Id B i×i ) is the matrix containing only false values (resp. only true values except on the diagonal which is set to false), i.e. all runs are equal (resp. distinct). Let δ i = δ c i ⊎ δ ι i ⊎ δ r i where

δ c i =       
(((q 1 , m 1 ), . . . , (q i , m i ), M ), c, (γ 1 , . . . , γ i ), ((q ′ 1 , m ′ 1 ), . . . , (q ′ i , m ′ i ), M ′ ))

c ∈ Σ c , for all 1 ≤ j, l ≤ i, t j = (q j , c, γ j , q ′ j ), t l = (q l , c, γ l , q ′ l ) ∈ δ c m ′ j = Extra K (λ((q j , c, γ j , q ′ j )) * m j ) and

M ′ (j, l) = M (j, l) ∨ (t j = t l )        δ ι
i and δ r i are defined similarly. It is obvious that each A i can be built in polynomial time in |T |. Finally, we test in polynomial time for emptiness each of the K VPA A i .

⊓ ⊔

Back to Trees

Considering the polynomial encoding of (weighted) tree automata into VPA (with multiplicities), we can deduce the two following results:

1. Determining whether the ambiguity of a tree automaton A is less than K, when A and the binary encoding of K are part of the input, is EXPTIME-complete. 2. We exhibit a simple pattern characterizing infinite weighted tree automata over N, which can be decided in PTIME. Moreover, it turns out to be the disjunction of a pattern for infinite ambiguity, and one for infinite cost (in the sense of [START_REF] Seidl | Finite tree automata with cost functions[END_REF]).

Point 1 should be compared with the PTIME complexity of this problem when K is fixed (see [START_REF] Seidl | Deciding equivalence of finite tree automata[END_REF]). Regarding point 2, we claim (see Figure 3): a weighted tree automaton T over N is infinite iff there exists a one-hole context C and computations ϕ i for i ∈ {1, 2, 3} of T over C such that ϕ 1 : p We can then derive a PTIME algorithm for weighted tree automata rather similar to the one we proposed for N-VPA (see Appendix C.3).

C -→ p, ϕ 2 : p C -→ q, ϕ 3 : q C -→ q for some p, q ∈ Q verifying ϕ 1 > 1 or ϕ 1 = ϕ 2 .

A Proofs of Section 4 A.1 Equivalent patterns

We present in an equivalent way the two patterns (S1) and (S2).

p q q ′ p ′ η2 : u1 η : w η ′ 2 : u2 η1 : u1 η3 : u1 η ′ 3 : u2 η ′ 1 : u2 (b) Dumbbell: η1η2η3ηη ′ 3 η ′ 2 η ′ 1 is a path and (η1 = η2 or η ′ 1 = η ′ 2 )
. Multiplicities have been omitted for readability.

A.2 Proof of Lemma 1

Proof. a. Let u i ∈ Σ * \ {ǫ} and η i = p i ui -→ q i be a path of T for i ∈ {1, 2, 3} such that u 1 u 3 , u 2 ∈ Σ * wn and η 1 η 2 η 3 is a path of T . By definition of paths and since u 1 u 3 , u 2 ∈ Σ * wn , there exist three runs

ρ 1 = (p 1 , ⊥) u1 -→ (q 1 , σ), ρ 2 = (p 2 , ⊥) u2 -→ (q 2 , ⊥) and ρ 3 = (p 3 , σ ′ ) u3 -→ (q 3 , ⊥) in T for σ, σ ′ ∈ Γ * . Since η 1 η 2 η 3 is a path, there exists some σ ′′ ∈ Γ * such that (p 1 , σ ′′ ) u1 -→ (q 1 , σ ′′ σ) u2 -→ (q 2 , σ ′′ σ ′ ) u3 -→ (q 3 , σ ′′ ) is a run of T . Observe that u 2 ∈ Σ *
wn , thus we have σ ′′ σ = σ ′′ σ ′ and thus σ = σ ′ . It follows that for any path η

′ 2 = p 2 u ′ 2 -→ q 2 with u ′ 2 ∈ Σ * wn , there exists a run ρ ′ 2 = (p 2 , ⊥) u ′ 2 -→ (q 2 , ⊥) in T over η ′ 2 .
Thus, there is the run

(p 1 , σ ′′ ) u1 -→ (q 1 , σ ′′ σ) u ′ 2 -→ (q 2 , σ ′′ σ) u3 -→ (q 3 , σ ′′ ) in T over η 1 η ′ 2 η
3 which is then a path of T . We consider now that p 1 = q 1 and p 3 = q 3 . Observe that since

ρ 1 = (p 1 , ⊥) u1 -→ (p 1 , σ) and ρ 3 = (p 3 , σ) u3 -→ (p 3 , ⊥) are runs of T with u 1 u 3 ∈ Σ * wn , ρ 2 1 and ρ 2 3 are runs of T . Since u 2 ∈ Σ * wn , there is a run ρ 2 = (p 2 , ⊥) u2 -→ (q 2 , ⊥) in T , and thus ρ ′ 2 = (p 2 , σσ) u2 -→ (q 2 , σσ) is also a run in T . Then η 2 1 η 2 η 2 3 is a path of T .
b. Let (η i ) i∈I be a family of paths going from p to q on some well-nested word u = ǫ. Since T is trimmed, there exists σ ∈ Σ * such that (p, σ) is reachable. Let i ∈ I, and a run (p, ⊥) u -→ (q, ⊥) over the well-nested word u. Then, configuration (q, σ) is reachable and thus, as T is trimmed, also co-reachable. Let ρ be a run which leads from a configuration (q in , ⊥) (with q in ∈ Q in ) to the configuration (p, σ) and ρ ′ a run which leads from the configuration (q, σ) to a configuration (q f , ⊥) (with q f ∈ Q f ). Let η (resp. η ′ ) be the path underlying run ρ (resp. ρ ′ ). Then, for any i ∈ I, the concatenation ηη i η ′ is an accepting path of T . ⊓ ⊔

A.3 Proof of Lemma 2

Proof. Case 1 T complies with (S1.a) Let u ∈ Σ * wn and η be a path selected according to pattern (S1.a). As η is a path going from p to p and u ∈ Σ * wn , η 2 is also a path from p to p. By applying iteratively Lemma 1.a, we can consider path η i whose multiplicity η i = m i grows to infinity when i tends to +∞. As T is trimmed, by Lemma 1.b, this gives accepting paths with multiplicity growing to infinity.

Case 2 T complies with (S1.b)

Let u ∈ Σ * wn and η 1 , η 2 , η 3 be paths selected according to pattern (S1.b). Let k ∈ N >0 , and i, j ∈ N such that i + j = k -1. As η 1 η 2 η 3 is a path and u ∈ Σ * wn , by Lemma 1.a, the path η i 1 η 2 η j 3 is a path over the word u k . Moreover, as η 1 = η 2 , all these paths are different when i, j range over the set of integers such that i + j = k -1. When k tends to infinity, we obtain an arbitrarily large number of paths over u k going from p to q. As T is trimmed, by Lemma 1.b, this gives arbitrarily many accepting paths over a same word.

Case 3 T complies with (S2.a)

Let u 1 u 2 , w ∈ Σ * wn and η 1 , η, η 2 be paths selected according to the criterion (S2.a). By applying iteratively Lemma 1.a, we can consider path η i 1 ηη i 2 whose multiplicity m i 1 mm i 2 grows to infinity when i tends to +∞. As T is trimmed, by Lemma 1.b, this gives accepting paths with multiplicity growing to infinity.

Case 4 T complies with (S2.b)

Let u 1 u 2 , w ∈ Σ * wn and η 1 , η 2 , η 3 , η, η ′ 3 , η ′ 2 , η ′ 1 be paths selected according to the criterion (S2.b). By applying iteratively Lemma 1.a, we can consider path η j 3 ηη ′j 3 for any j ∈ N >0 . As path η j 3 ηη ′j 3 goes from q to q ′ , Lemma 1.a entails that η 2 η j 3 ηη ′j 3 η ′ 2 is a path. Then, the second point of Lemma 1.a entails that η i 1 η 2 η j 3 ηη ′j 3 η ′ 2 η ′i 1 is a path for any i ∈ N >0 . Let k ∈ N >0 , one can observe that for any i, j such that i

+ j = k -1, the path η i 1 η 2 η j 3 ηη ′j 3 η ′ 2 η ′i 1 is over word u k 1 wu k 2
, and goes from p to p ′ . As T is trimmed, by Lemma 1.b, this gives arbitrarily many accepting paths over a same word.

⊓ ⊔

A.4 Proof of Lemma 4

Proof. We first define the following set of positions in u:

P = {i ∈ N >0 | x ≤ i ≤ y ∧ u x,i ∈ Σ * wn }.
Then for each i ∈ P , we define r i = s u x,i and

X i = {q ∈ Q | induced u
x,i (p, q) > 0 for some p}. Intuitively, r i corresponds to the multiplicity associated with the well-nested subword u x,i and X i is the set of states that can be reached after this subword (along an accepting path over u). Note that we have x ∈ P , as we have u x,x = ǫ ∈ Σ * wn , and X x is the set of states that accepting paths of T on u can go through at position x. In particular, this entails r x = s u x,x ≤ n. For all i, j ∈ P , such that i < j, we have:

1. ∀p ∈ X i , ∃q ∈ X j such that there is a path p ui+1,j ----→ q in T 2. ∀q ∈ X j , ∃p ∈ X i such that there is a path p uj,i+1 ----→ q in T 3. r i ≤ r j 4. r j ≤ r i × s u i,j
Properties (3) and (4) follow Lemma 3. Let C be the set defined as C = {i ∈ P | ∀j ∈ P, j < i ⇒ r j < r i }. We note the elements of C in ascending order as i 1 , i 2 , • • • , i c , with c = |C|. Then we have r ij < r i j ′ for any 1 ≤ j < j ′ ≤ c.

We will now prove that there exists 1 ≤ j < c such that s u ij ,ij+1 ≥ N l. By contradiction, we suppose that this property does not hold, i.e.: Property ( †) combined with property (4) implies r ij+1 < r ij × N l for any 1 ≤ j < c.

∀1 ≤ j < c, s u ij ,ij+1 < N l ( †) ψ(l)
We thus obtain r ic < r i1 × (N l) c-1 . By definition, we have r i1 = r x ≤ n, and r ic = s u x,y ≥ ψ(l) = n(N l) 2 n . We thus obtain c -1 > 2 n , which entails that there exist two indices j = j ′ such that

X ij = X i j ′ . We note X = X ij . Let v = u ij ,i j ′ . By construction v ∈ Σ *
wn . Now we construct the multigraph X v = (X, E v ) with E v ⊆ X × X × N defined as follows: ∀p, q ∈ Q, m ∈ N, for each path η = p v|m --→ q such that η ′ ηη ′′ is an accepting path on u for some path η ′ on word u 0,i , and η ′′ on word u j,|u| , we construct an edge p m -→ q ∈ E v . Note in particular that if there are two different paths on word v with the same multiplicity m going from state p to state q, then the edge p m -→ q occurs twice in the multiset E v . Because of ( 1) and ( 2) and the fact that X ij = X i j ′ , each vertex from X has both an in-degree and an out-degree greater or equal than 1. Suppose for the sake of contradiction that the two following properties hold simultaneously: (a) each arc of E v has a multiplicity equal to 1, (b) each node of X v has an in-degree and an out-degree equal to 1.

In this case, one can observe that X v is a simple graph (not a multigraph), and then that induced u ij ,i j ′ is exactly the incidence matrix of this graph. Moreover, the graph is functional, and thus this matrix is a permutation matrix M . As a consequence of Lemma 3, we obtain induced u

x,ij = induced u x,i j ′ × M and then r ij = r i j ′ , which is a contradiction.

We now distinguish two cases whether assertion (a) or assertion (b) does not hold. We first suppose that (b) holds and (a) does not hold. Consider the arc of E v that has a multiplicity m > 1. Thanks to property (b), this arc belongs to a cycle in graph X v . This cycle then corresponds to a "heavy cycle" in T , in the sense of pattern (S1.a).

Consider now that the assertion (b) is false. W.l.o.g., this entails that there exists a vertex p ∈ X whose out-degree is at least two. By definition, there are two different paths η, η ′ in T of the form:

η : p v -→ q and η ′ : p v -→ q ′
Note that the paths are distinct but q and q ′ could be equal. Since each vertex of X has at least one successor, q and q ′ allow to reach a cycle along the word v l for some l ∈ N >0 . Moreover, since each vertex of X has at least one predecessor, p is accessible from a cycle. The overall situation is depicted on Figure 7, where ϕ i denote the state around which are the cycles. If ϕ 1 = ϕ 2 , then the pattern (S1.b) can be exhibited in T using states ϕ 1 to ϕ 2 and a well-chosen iteration of the two cycles (in such a way that the powers of word v are matching). The situation is similar if ϕ 1 = ϕ 3 . If ϕ 1 = ϕ 2 = ϕ 3 , then pattern (S1.b) is present in T using the two different paths η and η ′ . There are two different cycles around state p, one using η going through locations q, ϕ 2 = ϕ 1 and p, and another one using η ′ going through locations q ′ , ϕ 3 = ϕ 1 and p. These two cycles are different (as η = η ′ ), and can be iterated so that they are on the same word v l for some l > 0. This yields the expected dumbbell.

ϕ1 p q q ′ ϕ2 ϕ3 v l 2 η : v η ′ : v v l 4 v l 3 v l 1 v l 5 v l 6
Finally, we have proven that if Property ( †) holds, then T contains pattern (S1), which contradicts our hypothesis. Thus there exists 1 ≤ j < c such that s u ij ,ij+1 ≥ N l. Let two positions x ′′ and y ′′ defined by y ′′ = i j+1 and x ′′ = max{i ∈ P | i < y ′′ }. By definition of C, we have r ij = r x ′′ . This means that s u

x,ij = s u x,x ′′ , i.e. the sums of multiplicities of accepting paths over u between positions x and i j on one side, and between x and x ′′ on the other side, are equal. This entails that when considering the same sums between positions larger than i j , the equality will also hold. In other terms, we can deduce s u ij ,ij+1 = s u x ′′ ,ij+1 . Moreover, by our choice of x ′′ and y ′′ , there is no position z ∈ P such that x ′′ < z < y ′′ . Two cases are possible, either u x ′′ ,y ′′ ∈ Σ ι , or u x ′′ ,y ′′ = cwr, with c ∈ Σ c , r ∈ Σ r and w ∈ Σ * wn . The property s u x ′′ ,y ′′ ≥ N l excludes the first case. We can thus consider positions x ′ = x ′′ + 1 and y ′ = y ′′ -1 which fulfill the conditions x ≤ x ′ ≤ y ′ ≤ y, u x ′ ,y ′ ∈ Σ * wn and h u (x ′ ) = h u (x) + 1. Finally, s u

x ′′ ,y ′′ ≥ N l = (n 2 L)

A.5 Proof of Lemma 5

Proof. To prove this result, we assume that T is infinite but does not comply with (S1), and prove it complies with (S2).

Let a word u ∈ L(T ) such that u ≥ ψ H (1) where H = 2 n 2 , and let k = |u|. First, we define a partial function Φ u : N × N → N × N. The domain of Φ u is the set of couple of positions (x, y) such that 0 ≤ x ≤ y ≤ k, u x,y ∈ Σ * wn and s u x,y ≥ ψ(1).Let (x, y) be a couple of positions in Dom(Φ u ) and l max be the largest l ∈ N >0 such that s u x,y ≥ ψ(l max ), Then by Lemma 4 there exist two positions x ′ and y ′ such that x < x ′ ≤ y ′ < y, u x ′ ,y ′ ∈ Σ * wn , h u (x ′ ) = h u (x)+1 and s u x ′ ,y ′ ≥ l max . We pick (x ′ , y ′ ) minimal in lexicographical order, and then define Φ u (x, y) = (x ′ , y ′ ). We consider the (finite) sequence (χ i ) i ∈ (N × N) N defined by χ 0 = (0, k) and, for i ≥ 1, χ i is defined iff χ i-1 ∈ Dom(Φ u ), and then defined as χ i = Φ u (χ i-1 ). By definition of mapping Φ u , we have for any i ≥ 1, h u (χ i ) = h u (χ i-1 ) + 1. Since h u is finite this entails that sequence (χ i ) i is finite, and we represent it as (χ i ) 0≤i≤L . Note that the sequence stops iff the last term does not belong to Dom(Φ u ), which means that s u χL < ψ(1) (the other conditions are fulfilled). For each index 0 ≤ i ≤ L we define a value r i ∈ N >0 and a set of pairs of states X i ⊆ Q×Q as follows: (we let χ i = (x, y))

-r i = s u χi -X i = {(p 1 , p 2 ) ∈ Q × Q | there exist a path η = p 1 ux,y
---→ p 2 , a path η ′ on word u 0,x and a path η ′′ on word u y,k such that η ′ ηη ′′ is an accepting path of T } Note that by definition of s u χi , we have r i-1 ≥ r i for any 1 ≤ i ≤ L. Let C be the set defined as C = {i ∈ [0, L] ∩ N | ∀j ∈ N, j < i ⇒ r j > r i }. We note the elements of C in ascending order as i 0 , i 1 , . . . , i c with c = |C| -1. Note that r ij > r i j ′ , for 0 ≤ j < j ′ ≤ c. We have r i0 = r 0 = s u χ0 = u ≥ ψ H (1). By Lemma 4 this implies r i h ≥ ψ H-h (1) for 0 ≤ h ≤ min{H, c}. As we have r ic = r L = s u χL < ψ(1), this entails c ≥ H. As there are c + 1 elements in C, this implies that there exist two distinct indices j and j ′ such that X ij = X i j ′ .

The rest of the proof follows the same lines as proof of Lemma 4, but to identify pattern (S2), we consider a graph where vertices are pairs of states. We let X = X ij , (x, y) = χ ij , (x ′ , y ′ ) = χ i j ′ , u 1 = u x,x ′ be the "call loop" word, u 2 = u y ′ ,y be the "return loop" word, and w = u x ′ ,y ′ be the well-nested word between the "call loop" and the "return loop" (see pattern (S2)). Now we construct the multigraph X = (X, E) where E ⊆ X × X × N >0 × N >0 is defined as follows: for each pair of paths

η 1 : p 1 v1|m1 ----→ q 1 , q 2 v2|m2
----→ p 2 such that η ′ η 1 ηη 2 η ′′ is an accepting path on u, for some paths η ′ , η and η ′′ on words u 0,x1 , w and u x2,k respectively, we add the edge

(p 1 , q 1 ) (m1,m2)
-----→ (p 2 , q 2 ) in E. Note that X is a multigraph, thus the same edge can occur more than once in E.

Note that a path in X corresponds to a path in T in the following sense: let (p 0 , q 0 )

(m 0 1 ,m 0 2 ) -----→ (p 1 , q 1 ) • • • (p µ-1 , q µ-1 ) (m µ 1 ,m µ 2 )
------→ (p µ , q µ ) be a path of X , then p 0

u1|m 0 1 ----→ p 1 • • • p µ-1 u1|m µ 1 ----→ p µ w|m ---→ q µ u2|m µ 2 ----→ q µ-1 • • • q 1 u2|m 0 1
----→ q 0 is a path of T that can be extended to an accepting path, for some m ∈ N >0 .

Note that because X ij = X i j ′ , each vertex from X has both an in-degree and an out-degree greater or equal than 1. Suppose for the sake of contradiction that the two following properties hold simultaneously: (a) each arc of E has a multiplicity equal to (1, 1), (b) each node of X has an in-degree and an out-degree equal to 1.

In this case, one can observe that X is a simple graph (not a multigraph), and then that r ij = r i j ′ , which is a contradiction.

We now distinguish two cases whether assertion (a) or assertion (b) does not hold. We first suppose that (b) holds and (a) does not hold. Consider the arc of E v that has a multiplicity m > 1. Thanks to property (b), this arc belongs to a cycle in graph X . One can verify that this cycle corresponds to a "heavy cycle" in T , in the sense of pattern (S2.a). Now we consider that assertion (b) does not hold. W.l.o.g., this entails that there exists (p, q) ∈ X with at least two successors: there are two distinct edges

(p, q) (m 1 1 ,m 1 2 )
-----→ (p 1 , q 1 ) and (p, q)

(m 2 1 ,m 2 2 ) -----→ (p 2 , q 2 )
We let ϕ 1 = (p 1 , q 1 ), ϕ 2 = (p 2 , q 2 ) and consider the four paths of T :

η 1 = p u1|m 1 1 ----→ p 1 , η 2 = p u1|m 2 1 ----→ p 2 , η ′ 1 = q u2|u 1 2 ---→ q 1 and η ′ 2 = q u2|u 2 2
---→ q 2 . By construction ϕ 1 and ϕ 2 can be equal but we have (η 1 , η ′ 1 ) = (η 2 , η ′ 2 ). rule 1.2 Let (p, q) be a couple added to S 0 by rule 1.2. So there exists t = (p, a, q) ∈ δ ι .

Observe that a ∈ Σ * wn and p a -→ q is a path of T because of t. Then (p, q) satisfies (1). rule 1.3 Let (p, q ′ ) be a couple added to S 0 by rule 1.3. So there exist (p, q), (q, q ′ ) ∈ S 0 . By induction there exist two words u, u ′ ∈ Σ * wn such that p u -→ q and q u ′ -→ q ′ are paths of T . Observe that uu ′ ∈ Σ * wn and p uu ′ --→ q ′ is a path of T . Then (p, q ′ ) satisfies (1). rule 1.4 Let (p ′ , q ′ ) be a couple added to S 0 by rule 1.4. So there exist (p, q) ∈ S 0 , (p ′ , c, γ, p) ∈ δ c and (q, r, γ, q ′ ) ∈ δ r . By induction there exists a word u ∈ Σ * wn such that p u -→ q is a path of T . Observe that cur ∈ Σ * wn , p ′ cur --→ q ′ is a path of T . Then (p, q) satisfies (1).

Then the backward direction. By contradiction suppose that there exist u ∈ Σ * wn and two states p, q ∈ Q such that p u -→ q is a path of T but (p, q) / ∈ S 0 . We choose u such that |u| is minimal. If |u| ≤ 1, then by rule 1.1 and 1.2, (p, q) ∈ S 0 , contradiction. Otherwise we can decompose u in two ways: either u = u 1 u 2 such that u 1 , u 2 ∈ Σ * wn \ {ǫ}, or u = cu ′ r such that c ∈ Σ c , r ∈ Σ r and u ′ ∈ Σ * wn . We consider the first case. u 1 = ǫ and u 2 = ǫ, so we can decompose p u -→ q as p u1 -→ p ′ u2 -→ q. Since u is minimal we have |u| > |u 1 | and |u| > |u 2 |, this entails (p, p ′ ) ∈ S 0 and (p ′ , q) ∈ S 0 . Then by rule 1.3, (p, q) ∈ S 0 , contradiction. Now we consider the second case. We

can decompose p u -→ q as p c -→ p ′ u ′ -→ q ′ r -→ q.
Since u is minimal and |u| > |u ′ |, (p ′ , q ′ ) ∈ S 0 . Then by rule 1.4, (p, q) ∈ S 0 , contradiction.

We prove that for all tuple c = (p 1 , q 1 , p 2 , q 2 , p 2 , q 3 , B), c ∈ S 1 if and only if the following property holds: ∃u ∈ Σ * wn and three paths η i :

p i u -→ q i of T for i ∈ {1, 2, 3} such that B = (η 1 = η 2 = η ǫ ∨ η 1 > 1) (2)
First the forward direction. We show that every rule preserves [START_REF] Borchardt | Bounds for tree automata with polynomial costs[END_REF]. We proceed by induction. We show that any tuple in S 1 satisfies (2

i = (p i , a, q i ) ∈ δ ι for i ∈ {1, 2, 3} such that B = λ(t 1 ) > 1 ∨ (t 1 = t 2 ).
Observe that a ∈ Σ * wn and η i = p i a -→ q i is a path of T because of t i . Then we have η 1 = λ(t 1 ) and η 1 = η 2 iff t 1 = t 2 . Then (p 1 , q 1 , p 2 , q 2 , p 3 , q 3 , B) satisfies (2). rule 2.3 Let (p 1 , q ′ 1 , p 2 , q ′ 2 , p 3 , q ′ 3 , B ′′ ) be a tuple added to S 1 by rule 2.3. So there exist (p 1 , q 1 , p 2 , q 2 , p 3 , q 3 , B), (q 1 , q ′ 1 , q 2 , q ′ 2 , q 3 , q ′ 3 , B ′ ) ∈ S 1 such that B ′′ = B ∨ B ′ . By induction there exist two words u, u ′ ∈ Σ * wn such that η i = p i u -→ q i and

η ′ i = q i u ′ -→ q ′ i are paths of T for i ∈ {1, 2, 3}, with B = η 1 > 1 ∨ η ǫ = η 1 = η 2 and B ′ = η ′ 1 > 1 ∨ η ǫ = η ′ 1 = η ′ 2 . Observe that uu ′ ∈ Σ * wn and η ′′ i = p i uu ′
--→ q i trees, i.e. T Σ is the smallest set T satisfying (i) Σ 0 ⊆ T , and (ii), if a ∈ Σ m and t 0 , . . . , t m-1 ∈ T , then a(t 0 , . . . , t m-1 ) ∈ T . Note that (i) can be viewed as a subcase of (ii) if we allow m to equal 0. Let t = a(t 0 , . . . , t m-1 ) ∈ T Σ for some a ∈ Σ m with m ≥ 0. The set of nodes of t, S(t) is the subset of N * defined by S(t) = {ǫ} ∪ m-1 j=0 j • S(t j ). t defines a map α t : S(t) → Σ mapping the nodes of t to their labels. We have:

α t (r) = a if r = ǫ α tj (r ′ ) if r = j • r ′
Tree automata A finite tree automaton over Σ is a triple A = (Q, I, δ) where:

-Q is a finite set of states -I ⊆ Q is the set of initial states -δ ⊆ L m=0 Q × Σ m × Q m is
the set of transitions. Given a transition τ = (q, a, q 0 . . . q m-1 ) ∈ δ, we denote by rk(τ ) the value rk(a).

Let t = a(t 0 , . . . , t m-1 ) ∈ T Σ and q ∈ Q. A q-computation of A for t consists of a transition (q, a, q 0 . . . q m-1 ) ∈ δ for the root and q j -computations of A for the subtrees t j , j ∈ {0 . . . m -1}. Formally, a computation ϕ of A for t can be viewed as a map ϕ : S(t) → δ satisfying for any r ∈ S(t), if α t (r) = a ∈ Σ m , then ϕ(r) = (q, a, q 0 . . . q m-1 ) and for any 0 ≤ j ≤ m -1, ϕ(r • j) = (q j , a j , q j 0 . . . q j mj -1 ) where a j = α t (r • j) and m j = rk(a j ). ϕ is a q-computation of A for t whenever ϕ(ǫ) is of the form (q, a, q 0 . . . q m-1 ). A q-computation is accepting iff q ∈ I. A tree t is accepted by A iff there is an accepting computation of A for t. The language of A is the set of trees accepted by A and is denoted by L(A).

Weighted tree automata A weighted tree automaton over the alphabet Σ and the semiring (N, +, •) is a pair T = (A, λ) where A = (Q, I, δ) is a tree automaton and λ : δ → N >0 is a mapping assigning a multiplicity to each transition of A. Notions of computations, accepted computations and languages are lifted from tree automata to weighted tree automata. Let t ∈ L(A). The multiplicity of a computation ϕ of A for t, denoted by ϕ , is the product of the multiplicities composing it, i.e. ϕ = Π r∈S(t) λ(ϕ(r)). The multiplicity of t ∈ L(A), denoted by t , is defined as t = { ϕ | ϕ accepting computation for t}.

C.2 From tree automata (with multiplicities) to VPA (with multiplicities)

From trees to well-nested words Let Σ = Σ 0 ∪ . . . ∪ Σ L be a ranked alphabet. We defined the structured alphabet Σ = Σ c ∪ Σ r as follows:

Σ c = { a | a ∈ Σ} Σ r = {a | a ∈ Σ}
The encoding of a tree t ∈ T Σ is a well-nested word over Σ, denoted by enc(t), and defined inductively as follows: if t = a(t 0 , . . . , t m-1 ) ∈ T Σ , then enc(t) = a enc(t 0 ) . . . enc(t m-1 ) a . One can easily verify that for any t ∈ T Σ , we have enc(t) ∈ Σ * wn .

Automata translation Let T = (A, λ) where A = (Q, I, δ) be a tree automaton with multiplicities over Σ. We define an N-VPA T ′ = (A ′ , λ ′ ) such that:2 L(T ′ ) = {enc(t) | t ∈ L(T )} and ∀t ∈ L(T ), t T = enc(t) T ′ (4)

We first define the VPA A ′ = (Q ′ , Γ ′ , δ ′ , Q ′ in , Q ′ f ) over the alphabet Σ as follows:

-Q ′ = {(q, i) | q ∈ I, 0 ≤ i ≤ 1} ∪ {(τ, i) | τ ∈ δ, 0 ≤ i ≤ rk(τ )} -Q ′ in = {(q, 0) | q ∈ I} -Q ′ f = {(q, 1) | q ∈ I} -Γ ′ = Q ′ × Σ
We now define δ ′ by its restrictions δ ′ c and δ ′ r on call and return symbols respectively: s a,(s,a)

-----→ s ′ ∈ δ ′ c iff one of the following cases holds: 1. s = (q, 0) and s ′ = (τ ′ , 0) where q ∈ I and τ ′ = (q, a, q ′ 0 . . . q ′ m ′ -1 ) ∈ δ 2. s = (τ, i) and s ′ = (τ ′ , 0) where τ = (q, b, q 0 . . . q m-1 ) ∈ δ, i < rk(τ ), and τ ′ = (q i , a, q ′ 0 . . . q ′ m ′ -1 ) ∈ δ Intuitively, the state s gives the rule that is applied, and at which position in the rule we are. In the first case, this is an initialization rule, for some state q. We require that the new rule τ ′ starts from a root in state q. In the second case, we were applying rule τ , at position i. Thus the current state was q i . We thus require that the new rule we apply (τ ′ ) starts from a root in state q i . s a ,(s ′′ ,a)

------→ s ′ ∈ δ ′ r iff one of the following cases holds: 1. s ′′ = (q, 0), s ′ = (q, 1) and s = (τ ′ , rk(τ ′ )) where q ∈ I and τ ′ = (q, a, q ′ 0 . . . q ′ m ′ -1 ) ∈ δ 2. s ′′ = (τ, i), s ′ = (τ, i + 1) and s = (τ ′ , rk(τ ′ )) where τ = (q, b, q 0 . . . q m-1 ) ∈ δ, i < rk(τ ), and τ ′ = (q i , a, q ′ 0 . . . q ′ m ′ -1 ) ∈ δ To read a return symbol, we should have finished the rule we were applying. This is what is required with condition s = (τ ′ , rk(τ ′ )) in both cases. Then, we recover from the stack symbol s ′′ what is the rule we were applying on the root, and we move one position forward in this rule. For instance, in the second case, we go from (τ, i) to (τ, i + 1). We also check that the rule that is finished was on the good state, i.e. q in the first case, and q i in the second case.

Last, we define the multiplicity mapping λ ′ as follows: for any transition d ∈ δ ′ r , we let λ ′ (d) = 1, and for any transition d = s a,(s,a)

-----→ s ′ ∈ δ ′ c where s ′ = (τ ′ , 0), we let λ ′ (d) = λ(τ ′ ). Intuitively, a transition in the tree automaton is applied twice in the VPA, once when the call symbol is read, and once when the return symbol is read. We thus report its multiplicity only in the case of the call symbol.

We claim:

Proposition 2. Let T = (A, λ) be a tree automaton with multiplicities, and T ′ = (A ′ , λ ′ ) be the N-VPA defined before. The set of accepting computations of T is in bijection with the set of accepting paths of T ′ , and T ′ verifies property (4).

Fig. 1 .

 1 Fig. 1. Patterns characterizing infinite multiplicity.

Fig. 2 . 5 Finite bounds for N-VPA 5 . 1

 2551 Fig. 2. Inference rules for deciding finiteness

r ∈ Σr} 9 : 3 .

 93 until M ′ ∪ M = M 10: return true Theorem Given an N-VPA T and K ∈ N >0 , the problem of determining whether T < K is EXPTIME-complete.

Fig. 3 .

 3 Fig. 3. Patterns for infinite weighted tree automata

  It is not difficult to verify that (S1) (resp. (S2)) is equivalent to (S1.a) or (S1.b) (resp. (S2.a) or (S2.b)).

pη

  : u | m (a) Heavy cycle: m > 1. p q η2 : u | m2 η1 : u | m1 η3 : u | m3 (b) Dumbbell: η1η2η3 is a path and η1 = η2.

Fig. 4 .

 4 Fig. 4. (S1) Well-nested case: u ∈ Σ * wn .

Fig. 5 .

 5 Fig. 5. (S2) Matched loops case: w ∈ Σ * wn , u1u2 ∈ Σ * wn , and u1 ∈ Σ * wn .

Fig. 6 .

 6 Fig. 6. s u i j ,i j+1 < N l

Fig. 7 .

 7 Fig. 7. Finding the dumbbell using graph Xv.

Fig. 9 .

 9 Fig. 9. s ux,y ≥ ψ(lmax)

  2 |Γ |l implies that s u x ′ ,y ′ ≥ l as expected.

					⊓ ⊔
	height
	r Xi j	r x ′	r	r r y ′ Xi j+1	length
		Fig. 8. s u x ′′ ,y ′′ ≥ Ll

rule 2.2

  Let (p 1 , p ′ 1 , p 2 , p ′ 2 , p 3 , p ′ 3 , B) be a tuple added to S 1 by rule 2.2. So there exist t

). A tuple can be added to S 1 in four different ways: rule 2.1 Let (p 1 , p 1 , p 2 , p 2 , p 3 , p 3 , B) be a tuple added to S 1 by rule 2.1. So there exist p i ∈ Q for i ∈ {1, 2, 3}. Observe that η ǫ is a path of T . Then (p 1 , p 1 , p 2 , p 2 , p 3 , p 3 , B) satisfies (2) with B = ⊥.

More precisely, given a general VPA A, one can build a VPA A ′ according to Definition 1 such that accepting runs of A ′ are in bijection with those of A. This can be achieved by adding self-loops on initial states that allow to push a special symbol (for the returns on empty stack) and self-loops on final states that allow to pop any symbols.

We use indexes to explicit whether the multiplicity is computed within T or within T ′ .

Since each vertex of X has at least one successor, ϕ 1 and ϕ 2 allow to reach cycles in X . Moreover, since each vertex of X has at least one predecessor, (p, q) is reachable from a cycle in X . The overall situation is depicted on Figure 10. (u1, u2) l 3 (u1, u2) l 1 (u1, u2) l 5 (u1, u2) l 6 Fig. 10. Finding the dumbbell using graph X .

We let ϕ 3 = (p 3 , q 3 ), ϕ 4 = (p 4 , q 4 ) and ϕ 5 = (p 5 , q 5 ) and distinguish three cases. If ϕ 3 = ϕ 4 , then we can identify patter (S2.b) using the path in X going from ϕ 3 to ϕ 4 (the construction is similar to that done on X v in the proof of Lemma 4). The same reasoning holds if ϕ 3 = ϕ 5 . If ϕ 3 = ϕ 4 = ϕ 5 , then pattern (S2.b) can be exhibited using the two different edges outgoing from (p, q). The constructions are similar to that done on X v in the proof of Lemma 4. This concludes the proof.

⊓ ⊔ Proof. We proceed successively with S 0 , S 1 , S 2 and S 3 . We prove that for all couple c = (p, q), c ∈ S 0 if and only if the following property holds:

∃u ∈ Σ * wn and a path η :

First the forward direction. We proceed by induction. We show that any couple in S 0 satisfies [START_REF] Alur | Visibly pushdown languages[END_REF]. A couple can be added to S 0 in four different ways:

In addition, one also has

) be a tuple added to S 1 by rule 2.3. So there exist (p 1 , q 1 , p 2 , q 2 , p 3 , q 3 , B) ∈ S 1 ,

. By induction there exists a word u ∈ Σ * wn such that

. Then (p 1 , q 1 , p 2 , q 2 , p 3 , q 3 , B ′ ) satisfies (2). Then the backward direction. By contradiction suppose that there exist u ∈ Σ * wn and states

We choose u such that |u| is minimal. If |u| ≤ 1, then by rule 2.1 and 2.2, (p 1 , q 1 , p 2 , q 2 , p 3 , q 3 , B) ∈ S 1 , contradiction. Otherwise we can decompose u in two ways: either u = u 1 u 2 such that u 1 , u 2 ∈ Σ * wn \ {ǫ}, or u = cu ′ r such that c ∈ Σ c , r ∈ Σ r and u ′ ∈ Σ * wn . We consider the first case. u 1 = ǫ and u 2 = ǫ, so we can decompose η i as

Contradiction. Now we consider the second case. We can

For the end of the proof we define the following notation: let u, u ′ be two words such that uu ′ ∈ Σ * wn and η 1 :

Then we write that η 1 and η 2 are matching paths iff σ = σ ′ .

We prove that for all tuple c = (p 1 , q 1 , p 2 , q 2 , p 3 , q 3 , q

and only if the following property holds:

wn and paths η i :

First the forward direction. We show that every rule preserves (3). We proceed by induction. We show that any tuple in S 2 satisfies (3). A tuple can be added to S 2 in three different ways:

) be a tuple added to S 2 by rule 3.1. So there exist (p 1 , q 1 , p 2 , q 2 , p 3 , q 3 , B),

Then by (2) there exist u, u ′ ∈ Σ * wn and paths

Observe that uu ′ ∈ Σ * wn and η i and η ′ i for any i ∈ {1, 2, 3} are trivially matching paths as u and u ′ are well-nested. Then (p 1 , q 1 , p 2 , q 2 , p 3 , q 3 , q

) be a tuple added to S 2 by rule 3.2. So there exist

wn , η i and η ′ i are matching paths of T and (η

By induction there exist four words u, u ′ , ũ′ and ũ such that uũ ∈ Σ * wn , u ′ ũ′ ∈ Σ * wn , matching paths η i = p ′′ i u -→ p i and ηi = q i ũ -→ q ′′ i and matching paths

Then the backward direction. By contradiction suppose that there exist two words u, u ′ and p i , q i , q ′ i , p

We choose u and u ′ such that h u (|u|) (the number of pending calls of u) is minimal. There exists a unique decomposition of u (resp. u ′ ) as u = w 1 cw 2 (resp. as u ′ = w ′ 2 rw ′ 1 ) with w 1 , w ′ 1 , w 2 w ′ 2 ∈ Σ * wn , c ∈ Σ c and r ∈ Σ r . We can thus decompose path η i as

--→ q i and similarly for path ηi with paths η′′′

. By rule 3.2 applied on matching paths η ′′ i and η′′ i , we have

By applying twice the rule 3.3, we obtain

We can verify that B is logically equivalent with B c , contradiction.

22

We now prove that ⊤ ∈ S 3 iff T is infinite. First the forward direction. There are two possibilities of the presence of ⊤ in S 3 : rule 4.1 There exists (p, p, p, q, q, q, ⊤) ∈ S 1 by rule 4.1. By property (2) of S 1 , there exist u ∈ Σ * wn and paths

This corresponds to the definition of pattern S1, then T is infinite. rule 4.2 There exist (q, q ′ ) ∈ S 0 and (p, p, p, q, q, q, q ′ , q ′ , q ′ , p ′ , p ′ , p ′ , ⊤) ∈ S 2 by rule 4.2. By property (1) of S 0 and property (3) of S 2 , there exist three words u, u ′ , w, such that uu ′ , w ∈ Σ * wn , and paths η = q

This corresponds to the definition of pattern S2, then T is infinite.

Then the backward direction. Since T is infinite, we are able to find pattern S1 or pattern S2 in T . If pattern S1 is present in T , then there exist u ∈ Σ * wn and paths η 1 = p u -→ p, η 2 = p u -→ q and η 3 = q u -→ q of T with η 1 > 1 or η 1 = η 2 . By property (2) of S 1 , (p, p, p, q, q, q, ⊤) ∈ S 1 . Then by rule 4.1, ⊤ ∈ S 3 . If pattern S2 is present in T , then there exist three words u, u ′ , w, such that uu ′ , w ∈ Σ * wn , and paths η = q w -→ q ′ ,

that η i and η ′ i are matching paths of T and with

By property (1) of S 0 and property (3) of S 2 , (q, q ′ ) ∈ S 0 and (p, p, p, q, q, q, q ′ , q ′ , q ′ , p ′ , p ′ , p ′ , ⊤) ∈ S 2 . Then by rule 4.

C.3 A New Algorithm for Finiteness of Weighted Tree Automata

We consider a trimmed weighted tree automaton B = (Ξ, Q, I, ∆, λ) where Ξ is a ranked alphabet (with symbols of arity at most m, Ξ i being symbols of arity i), Q is a finite set of states, I ⊆ Q the set of initial states, ∆ is a transition relation (∆ ⊆ m i=0 Q i × Ξ i × Q) and λ associates with each transition rule a positive integer.

We construct by saturation three sets S 0 , S 1 and S 2 of tuples built from states and a Boolean respectively of the form (q 1 , q ′ 1 , q ′′ 1 , b), (q 1 , q ′ 1 , q 2 , q ′ 2 , q 3 , q ′ 3 , b), (b) where q i , q ′ i ∈ Q and b ∈ B using the following inference rules from Figure 13.

the arity of f is k, (pj, qj , p ′ j , q ′ j , p ′′ j , q ′′ j , bj) ∈ S1 for some 1 ≤ j ≤ k for all 1 ≤ ℓ ≤ k, ℓ = j, (q ℓ , q ′ ℓ , q ′′ ℓ , b ℓ ) ∈ S0 τ = f (q1, . . . , q k ) → q, τ ′ = f (q ′ 1 , . . . , q ′ k ) → q ′ , τ ′′ = f (q ′′ 1 , . . . , q ′′ k ) → q ′′ ∈ ∆ (2.2) (pj, q, p ′ j , q ′ , p ′′ j , q ′′ , j|j =ℓ bj ∨ τ = τ ′ ∨ λ(τ ) > 1) ∈ S1 (p, p, p, q, q, q, ⊤) ∈ S1 (3.1) (⊤) ∈ S2 Intuitively, a triple (q, q ′ , q ′′ , b) belongs to S 0 if there exists a tree having three runs which label the root respectively by q, q ′ and q ′′ and b is true if the first one has used a transition whose multiplicity is strictly greater than 1 or the first two runs differ at some position in the transition rules they use. A tuple (q 1 , q 2 , q ′ 1 , q ′ 2 , , q ′′ 1 , q ′′ 2 , b) belongs to S 1 if there exists a context having three runs which label the hole of the context by q 1 , q ′ 1 and q ′′ 1 respectively and the root by q 2 , q ′ 2 and q ′′ 2 respectively and b is true if the first one has used a transition whose multiplicity is strictly greater than 1 or the first two runs differ at some position in the transition rules they use. Finally, the last rule is used to identify the presence of the required pattern.

Obviously, this algorithm is in PTIME.


 P G Conaghan

D J Hunter

J F Maillefert

W M Reichmann

E Losina

Summary and recommendations of the OARSI FDA osteoarthritis Assessment of Structural Change Working Group

Keywords:  Osteoarthritis,  Conventional radiography,  Magnetic resonance imaging,  Validity,  Responsiveness,  Reliability

The Osteoarthritis Research Society International initiated a number of working groups to address a call from the US Food and Drug Administration (FDA) on updating draft guidance on conduct of osteoarthritis (OA) clinical trials. The development of disease-modifying osteoarthritis drugs (DMOADs) remains challenging. The Assessment of Structural Change (ASC) Working Group aimed to provide a state-of-the-art critical update on imaging tools for OA clinical trials.

Methods

The Group focussed on the performance metrics of conventional radiographs (CR) and magnetic resonance imaging (MRI), performing systematic literature reviews for these modalities. After acquiring these reviews, summary and research recommendations were developed through a consensus process.

Results

For CR, there is some evidence for construct and predictive validity, with good evidence for reliability and responsiveness of metric measurement of joint space width (JSW). Trials off at least 1 and probably 2 years duration will be required. Although there is much less evidence for hip JSW, it may provide greater responsiveness than knee JSW. For MRI cartilage morphometry in knee OA, there is some evidence for construct and predictive validity, with good evidence for reliability and responsiveness. The responsiveness of semi-quantitative MRI assessment of cartilage morphology, bone marrow lesions and synovitis was also good in knee OA.

Conclusions

Radiographic JSW is still a recommended option for trials of structure modification, with the understanding that the construct represents a number of pathologies and trial duration may be long.

MRI is now recommended for clinical trials in terms of cartilage morphology assessment. It is important to study all the joint tissues of the OA joint and the literature is growing on MRI quantification (and its responsiveness) of non-cartilage features. The research recommendations provided will focus researchers on important issues such as determining how structural change within the relatively short duration of a trial reflects long-term change in patient-centred outcomes.

Introduction

Current status of guidance for assessing osteoarthritis (OA) disease modification

The development of disease-modifying osteoarthritis drugs (DMOADs) is faced with many challenges.

There remains an inadequate understanding of the primary endpoint for demonstrating DMOAD efficacy. The actual result of clinical OA symptomatic progression, arthroplasty, is associated with multiple problems as an endpoint in clinical trials including the variability in rates of surgery, in part related to socioeconomic disparities, different healthcare environments and the relatively low incidence rate of arthroplasties compared with the total OA burden [1] and [2] . Alternative clinical endpoints for DMOAD clinical trials have therefore been considered and the Food and Drug Administration (FDA) previously provided regulatory draft guidelines for use in DMOAD development 3 . The FDA Clinical Development Programs for Drugs, Devices and Biological Products Intended for the Treatment of OA draft guidelines defined the current acceptable structural endpoint for DMOAD clinical trials as a slowing in the loss of knee or hip joint space narrowing (JSN) using conventional radiographs (CR); depending on the structural change this would need to be accompanied by symptom improvement.

Similar recommendations were adopted by the European Medicines Agency (EMEA) in Europe 4 (also adopted by the Therapeutic Goods Administration (TGA) in Australia) and remain in their recently revised Guideline 5 .

The current hierarchy of claims for structural outcome as defined by the FDA Clinical Development Programs for Drugs, Devices and Biological Products Intended for the Treatment of OA draft guidance is as follows:

1.

Normalise the X-ray (reverse progression).

2.

Improve the X-ray (halt progression).

3.

Slow JSN by at least a pre-specified amount (slow the rate of progression).

CR have traditionally been the method of choice in clinical trials because of their relative feasibility.

Until recently, it was widely accepted that alteration in progression of JSN implies preservation of hyaline cartilage and consequently clinical benefit; measurement of joint space width (JSW) by X-ray was determined as the most appropriate structural endpoint measure [6] and [7] . However it was recognized that the nature and magnitude of structural changes that are likely to be clinically relevant remain uncertain. Whether parallel clinical outcomes should be included in the claim depends on what JSW outcome is achieved, but collection of these data (including measurement of pain, a patient global assessment, a self-administered questionnaire and the time to the need for total joint replacement surgery) was strongly recommended regardless of the anticipated outcome since their assessment is critical for analysis of the overall risks and benefit of a product 3 . Since the concept of structural improvement connotes an element of durability, trials to demonstrate structure improvement were recommended to last at least 1 year 3 .

As well, owing to the rapid growth of magnetic resonance imaging (MRI) studies in the last decade, there has been an increased awareness that symptomatic OA represents a process involving all the tissues in the OA joint, not just cartilage [8] and [9] . MRI has evolved substantially over the last decade and its strengths include its ability to visualise individual tissue pathologies, as well as the interrelationship between tissue pathologies.

Limitations of JSN as an outcome

Although a product showing a slowing of JSN would be expected to also affect symptoms, it is possible that certain products may affect structural progression without associated symptomatic evidence 10 . It is also possible that slowing of structural progression may occur at an earlier time-point with later reduction in symptoms (acknowledged in the recent EMEA Guideline 5 ). A claim of structural improvement (i.e., slowing of JSN) might conceivably be dissociated from other claims when the mechanism of action of the product, and/or the size of the effect on slowing of JSN, are suggestive of future clinical benefits. If products are not anticipated to have different effects on these parameters or show only small improvements in JSN without demonstrated effects in symptoms they will not generally be considered for approval or for separate claims. In other words, as long as an observed delay in JSN progression is correlated to an improvement of clinical outcomes it is considered as an appropriate primary endpoint and as a surrogate endpoint for total joint replacement, the critical event characteristic of medical treatment failure for OA. It is assumed that a delay in JSN will consequently delay the need for total joint surgery, and can hence be interpreted as a treatment success for DMOADs.

The use of JSN measured by CR as a structural endpoint is associated with some concerns. Since disease progression is generally slow, minimal and variable within and between subjects [10] and [11] , the use of JSW as an endpoint measurement requires long-term treatment periods (>1 year) and inclusions of large patient numbers. Moreover, the inability of radiographs to visualise cartilage leads to lack of sensitivity to detect early and small changes in this tissue 12 . There is difficulty in obtaining high quality reproducible images of OA joints, despite state-of-the-art standardisation of radiographic protocols to reduce the variability related to joint repositioning 13 . MRI studies have demonstrated that JSN represents a complex of hyaline cartilage loss, meniscal extrusion and meniscal degeneration 14 .

Although structure is a critical component of OA assessment, the relationships between structure and pain and/or function and between structure and future outcomes (e.g., arthroplasty) are not well developed and the definition of a clinically relevant change in JSN has not been established.

The use of JSW alone may not be entirely relevant as an outcome measure for DMOAD efficacy since it fails to capture the multi-tissue nature of OA [9] and [15] . As such, potential early beneficial changes in other components of the joint are missed by the use of JSN alone as the structural endpoint.

Moreover, the insensitivity of JSN to early changes in cartilage and meniscus means that even "moderate" OA knees (Kellgren-Lawrence ≥ 2) may already represent a stage of the disease too molecularly and biochemically advanced for alteration of disease course by pharmacological intervention. Previous attempts at OA disease modification using JSN as an endpoint have provided important lessons about the design and conduct of such trials, including issues on radiographic positioning, measurement methods, and study "enrichment" for progressors in order to ensure progression in the placebo group; this has been previously well reviewed [7] and [16] . Despite the limitations as a measure for DMOAD efficacy, delay in JSN has been reported for a small number of potential DMOADs to date [7] and [16] . However the lack of associated symptomatic benefit in these studies has prevented any of these agents from being successfully registered.

Methods

In the last decade since the FDA produced its draft guidance for industry, much evidence has been accumulated on the assessment of structural change in OA. The Osteoarthritis Research Society International (OARSI) FDA OA Assessment of Structural Change (ASC) Working Group comprised a wide range of expertise including clinical trialists, methodologists, academics, imaging experts and pharmaceutical company representatives with relevant trials experience; the Group was tasked with:

1.

Examining a number of key issues about the performance metrics (including predictive validity for relevant clinical outcomes and responsiveness) of the commonest imaging tools used to assess structural change in OA, focussing predominantly on CR and MRI, while briefly examining the information on other modalities especially the growing field of ultrasound. This was performed by conducting systematic literature reviews for CR and MRI. The draft strategy for the literature review was written in December 2008, sent to all members of the ASC Working Group, underwent iterative revision, and a final version of the protocol was approved in February 2009. Details of the protocol and the search terms are published separately [17], [18], [19] and [20] . The literature search was conducted using articles published up to the time of the search in April 2009. For examining the role of ultrasound, where it was acknowledged there was a much smaller literature base, we used a recently published systematic literature review on ultrasound in OA 21 .

2.

Producing state-of-the-art recommendations in assessing OA structural change for the purposes of optimising utilisation in OA clinical trials, based on the findings of the systematic literature reviews and via a consensus approach.

3.

To also develop research recommendations again based on the literature reviews and through a consensus process of the ASC Working Group.

The following summary and derived recommendations attempts to overview the large amount of literature reviewed during this process. Much of the work summarised below is detailed in the more detailed accompanying systematic reviews of both radiography and MRI [17], [18], [19] and [20] ; for this reason, individual references supporting each statement are not provided in this summary.

Summary and recommendations

The underlying assumption of these recommendations is that the manifestations of joint pain and disability currently associated with OA are strongly related to the pathophysiology of OA seen in joint structures. This postulate is to some extent supported by epidemiological evidence of the association between radiographic OA, joint pain and disability in the general population.

Much of the published evidence on imaging ASC relates to OA of the knee, with much less evidence (especially for modern imaging modalities) relating to OA of the hip and very limited information available for hand OA. This summary must therefore be seen as largely related to trials for OA of the knee and to a lesser extent, the hip. Importantly most of the therapeutic studies on OA have included symptomatic and radiographically moderate to severe OA, so there is an absence of literature and definitions for "early" OA, especially studies entering people before the currently recognized clinical syndrome is apparent and when structural pathology is presumably minimal. So the literature on the performance of existing imaging modalities at this important stage of the OA process is sparse.

When mentioned, the term 'therapies' refers to drugs, devices and biological products entered into the treatment of OA and regulated by the FDA; this could also include interventions such as weight loss.

Conventional radiography

• CR presents an image of the joint space of a diarthrodial joint, the width of which represents the thickness of articular cartilage. In some joints, notably the knee, JSW also reflects the presence, location and condition of other structures (e.g., meniscus), and JSW is a composite measure of the combined thickness of those structures. This should be considered when defining a relevant knee trial outcome.

•

Much is now known of the performance metrics of CR JSW in the knee and to a lesser extent in the hip. There is some evidence for construct and predictive validity, with good evidence for reliability and responsiveness of metric measurement of JSW. In terms of correlations with concurrent symptoms, there is a weak association between progression in JSN and progression of symptoms. There is little information on how progression in JSN during the course of a study reflects post-study (long-term) change in symptoms. JSN progression is associated with increased rate of subsequent total joint replacement, but these may not be truly independent events as radiographic JSN is one of the features used to select people for joint replacement surgery.

•

In the knee, the use of fluoroscopic positioning and semi-flexed views improve responsiveness, although it is acknowledged that access to fluoroscopic facilities is restricted. Studies will generally need to be at least 12 and more likely 24 months duration.

• It is possible and therefore advisable to 'enrich' a knee OA study population to increase the rate of joint space loss, for example, by including higher Kellgren Lawrence (KL) grade.

• Automated methods for assessing parameters of JSW offer promise of improved precision and therefore improved responsiveness.

•

The natural history of hip OA appears different to that of knee OA and although the literature concerning the hip is much less extensive, there is some evidence for better responsiveness for JSW measurement at the hip. Hip JSW as a construct does not include a meniscus. There is little evidence on enriching cohorts for purposes of increasing rate of JSN progression.

•

We support the continued use of CR JSW as one option for assessing structural OA change, taking all the previous points into account when deciding on study endpoint.

Research recommendations

To further understand the relationship between JSN and symptoms, future studies should focus on the following areas:

• Cross-sectional studies in which the patients are their own controls (such as one recently published 22 ) to better evaluate the potential correlation.

• Longitudinal studies evaluating the relationship between changes in symptoms and changes in joint space.

•

Predictive validity studies, i.e., does joint space predict subsequent pain and disability and subsequent joint replacement? For example, does JSN between month 0 and month 12 correlates with joint replacement by month 60? • Construct validity studies, i.e., correlation between JSN and mean pain or function. For example, is JSW between month 0 and month 12 correlated with mean pain and function evaluated every 6 months between month 0 and month 12, or between month 12 and month 24?

For Knee OA:

• Studies of the relationship between symptoms and radiographic joint space evaluated on semi-flexed X-rays with fluoroscopy.

• Studies on predictors of joint loss evaluated on semi-flexed X-rays with fluoroscopy and optimal serial tibial plateau alignment.

•

Studies on the effect of rate of joint space loss on treatment effect.

For Hand OA:

• Studies comparing the metrological properties of hand OA scoring systems.

MRI

• For assessing MRI cartilage morphometry in knee OA, there is some evidence for construct and predictive validity, with good evidence for reliability and responsiveness. Using MRI it is possible to accurately and feasibly measure change in cartilage morphology over 12 months for knee OA and we recommend the use of MRI for assessing cartilage morphology in trials of OA structure modification.

•

It is possible to 'enrich' a knee OA study population with MRI outcomes in order to increase the rate of cartilage loss, for example, by including higher KL grade.

•

In terms of correlations with concurrent symptoms, there is a weak association between progression of cartilage loss and increasing symptoms. There is little information on how change in cartilage parameters during the course of a study reflects post-study change in symptoms. There is some predictive validity with progression of cartilage loss predicting subsequent total joint replacement.

• More information is required on the performance metrics of MRI semi-quantitative and compositional measures of cartilage morphology. There may be a role for semi-quantitative assessments for assessing focal cartilage defects.

• Structure modification should be considered in a broader context than that of cartilage alone. Since MRI has the capacity to image the other tissues, further work is needed on the quantification and predictive validity of non-cartilage MRI pathologies. The performance metrics of non-cartilage MRI features have not been extensively studied but there is a rapidly emerging literature in this field.

Research recommendations

As well as the areas recommended above, including research into 'whole organ' or multi-tissue assessment (currently via semi-quantitative scores) and improving the quantification of non-cartilage pathologies, the MRI OA field needs:

• Studies to define more responsive measures of structural change.

• Studies that measure change at an earlier stage of disease when it may be more suitable for DMOAD intervention.

• Studies to improve predictive validity of current structural measures for important clinical outcomes (e.g., total joint replacement (TJR), virtual TJR).

• Studies to improve assessment precision of structural measures more closely related to symptom change (e.g., bone marrow lesions, synovitis).

Other imaging modalities

The potential for non-CR or MRI modalities to assess relevant non-cartilage tissues should be considered. Ultrasound is currently the other recent imaging modality with most information available, and at this stage it appears it is most promising as a tool for evaluating OA synovitis. Ultrasounddetected pathologies have been associated with current OA symptoms. Further work is required to better understand the performance metrics of ultrasonographic quantification of pathology, with such work requiring improved pathology definitions.

Conclusions

The amount of publications assessing OA structural change has dramatically increased over recent years, related to the availability of large cohort studies. Though we now understand CR JSW represents a complex of pathologies, gaps still remain in our understanding of both construct and predictive validity. The growth of MRI as an OA imaging biomarker has evolved to a point where it can be recommended for clinical trials in terms of cartilage morphology assessment. Much still needs to be understood about compositional cartilage measures and just as importantly, quantification of non-cartilage features. The literature reviews performed by the ASC Working Group, together with attention to the research recommendations listed here, should ensure that the current gaps in our knowledge regarding the performance metrics and clinical importance of existing tools will be filled.