Paul Gastin

Benjamin Monmege

Adding Pebbles to Weighted Automata Easy Specification & Efficient Evaluation

We extend weighted automata and weighted rational expressions with 2-way moves and (reusable) pebbles. We show with examples from natural language modeling and quantitative model-checking that weighted expressions and automata with pebbles are more expressive and allow much more natural and intuitive specifications than classical ones. We extend Kleene-Schützenberger theorem showing that weighted expressions and automata with pebbles have the same expressive power. We focus on an efficient translation from expressions to automata. We also prove that the evaluation problem for weighted automata can be done very efficiently if the number of (reusable) pebbles is low.

Introduction

Regular expressions have always been used to specify patterns. Popular because they propose a concise and intuitive way of denoting such patterns, they have also a long history in the formal language community. A seminal result, known as Kleene's theorem, establishes that the (denotational) regular expressions have the same expressive power as the (operational) finite state automata. Efficient translation algorithms of regular expressions into finite automata are crucial since expressions are convenient to denote patterns and automata are amenable to efficient algorithms. Regular expressions and finite automata have been extended in several directions, e.g., tree (walking) automata, (regular) XPath, etc.

Nowadays, quantitative models and analysis are intensively studied, resulting in a revision of the foundation of computer science where classical yes/no answers are replaced by quantities such as probability, energy consumption, reliability, cost, etc. In the 60s, Schützenberger provided a generic way of turning qualitative into quantitative systems, starting the theory of weighted automata [START_REF] Schützenberger | On the definition of a family of automata[END_REF] (see [START_REF] Ésik | Modern Automata Theory[END_REF][START_REF] Droste | Handbook of Weighted Automata[END_REF][START_REF] Berstel | Noncommutative rational series with applications[END_REF] for recent books on this theory). Indeed, probabilistic automata and word transducers appear as instances of that framework, which found its way into numerous application areas such as natural language processing, speech recognition or digital image compression. Schützenberger proved the equivalence between weighted automata and weighted regular expressions, extending Kleene's theorem. Various translation algorithms can be extended from the Boolean framework to the weighted case, see [START_REF] Sakarovitch | Elements of Automata Theory[END_REF][START_REF] Sakarovitch | Automata and expressions[END_REF] for surveys about Supported by LIA INFORMEL.

these methods, and [START_REF] Kuske | Schützenberger's theorem on formal power series follows from kleene's theorem[END_REF] which obtains Schützenberger's theorem as a corollary of Kleene's theorem.

In Sections 4 and 5, we extend weighted expressions and automata with 2way moves and pebbles. There are several motivations for these extensions. First, as shown in Section 2 for applications in natural language processing and quantitative model-checking, 2-way moves and pebbles allow more natural and more concise descriptions of the quantitative expressions we need to evaluate. Second, in the weighted case, 2-way and pebbles do increase the expressive power as already observed in [START_REF] Bollig | Pebble weighted automata and transitive closure logics[END_REF] in relation with weighted logics or in [START_REF] Ravikumar | On some variations of two-way probabilistic finite automata models[END_REF] in the probabilistic setting. This is indeed in contrast with the Boolean case where 2-way and pebbles do not add expressive power over words (see, e.g., [START_REF] Globerman | Complexity results for two-way and multi-pebble automata and their logics[END_REF]) even though they allow more succinct descriptions (see, e.g., [START_REF] Birget | State-complexity of finite-state devices, state compressibility and incompressibility[END_REF]). Our work is also inspired by pebble tree-walking automata and in particular their links with powerful logics, XPath formalisms and caterpillar expressions on trees [START_REF] Engelfriet | Tree-walking pebble automata[END_REF][START_REF] Brüggeman-Klein | Caterpillars: A context specification technique[END_REF][START_REF] Bojańczyk | Expressive power of pebble automata[END_REF][START_REF] Samuelides | Complexity of pebble tree-walking automata[END_REF][START_REF] Bojańczyk | Tree-walking automata[END_REF].

In Sections 6 and 7, we generalize Kleene and Schützenberger theorems to weighted expressions and automata with 2-way moves and pebbles. We establish their expressive power equivalence by providing effective translations in both directions. Showing how to transform an operational automaton into an equivalent denotational expression is indeed very interesting from a theoretical point of view, but is less useful in practice. On the other hand, we need highly efficient translations from the convenient denotational formalism of expressions to operational automata which, as stated above, are amenable to efficient algorithms. Efficiency is measured both with respect to the size of the resulting automaton, and the space and time complexities of the translation. We show that, Glushkov's [START_REF] Glushkov | The abstract theory of automata[END_REF] or Berry-Sethi [START_REF] Berry | From regular expressions to deterministic automata[END_REF] translations, which are among the best ones in the Boolean case, can be extended to weighted expressions with 2-may moves and pebbles. The constructions for the rational operations (sum, product, star) can be adapted easily to cope with 2-way moves, even though the correctness proofs are more involved and require new theoretical grounds such as series over a partial monoid as explained in Section 4.1. The main novelty in Sections 6 and 7 is indeed the treatment of pebbles in the translations between expressions and automata.

To complete the picture, we study in Section 8 the evaluation problem of a weighted automaton with 2-way moves and reusable pebbles over a given word. The algorithm is polynomial in the size of the word, where the degree is 1 plus the number of reusable pebbles. We can even decrease the degree by 1 for strongly layered automata. This applies when we only have one reusable pebble, and we obtain an algorithm which is linear in the size of the input word. This is in particular the case for automata derived from weighted LTL.

The paper includes intuitive explanations and examples for a better understanding of weighted expressions with 2-way moves and pebbles, and of the translations between automata and expressions. An extended abstract of this work appeared in [START_REF] Gastin | Adding pebbles to weighted automata[END_REF].

Motivations

We give in this section two motivating examples for studying weighted expressions and automata with 2-way moves and pebbles.

Language modeling

Since decades, weighted automata have been extensively used in Natural Language Processing (see [START_REF] Knight | Applications of weighted automata in natural language processing[END_REF]), in particular for automatic translation, speech recognition or transliteration. All these tasks have in common to split the problem into independent parts, certain directly related to the specific task and others related to the knowledge of the current language. For example, in the translation task from French sentences to English sentences, one splits the problem into first knowing translation of single words and then modeling English sentences (knowledge which is independent from the translation task). The second part, namely to know whether a sequence of words is a good English sentence, is known as language modeling. Often this knowledge is learned from a large corpus of English texts, and stored into a formal model, e.g., a weighted finite state automaton representing the probability distribution P of well-formed English sentences. The translation task is then resolved by first generating several English sentences from the original French one (due to ambiguity of the wordby-word translation task), and then choosing among this set of sentences the ones with highest probability.

One broadly used language model is the n-gram model, where the probability of a word in a sentence depends only on the previous n -1 words: for example in a 1-gram model, only the individual word frequencies are relevant to generate well-formed English sentences, whereas in a 2-gram model, the probability of a word depends on the very same frequency distribution and also the previous word. To formally describe these models, and further study them, let us define them using regular expressions. Let D denote the dictionary of words in the language. Suppose we are given the conditional probability distributions P(u n | u 1 , . . . , u n-1 ) in the n-gram model (with u i ∈ D for all i). The probability of a sentence (u i ) 1≤i≤m ∈ D m can be given by the following weighted regular expression in a 1-gram model and a 3-gram model:

E 1 = u∈D uP(u) * E 3 = →→ u,v,w∈D ←←uvwP(w | u, v) *
where symbols → and ← denote a right or left move, respectively, no matter what word it is reading. Expression E 1 is a classical weighted regular expression where the Kleene star iterates the computation of the inner expression, which here computes the probability of the current word u. Expression E 3 has the opportunity to move forward and backward: this allows to easily recover the context whereas a 1-way automaton would have to store the context in its states. Notice that expression E 3 is quite readable and intuitive. One could write an equivalent 1-way expression, but imagine how intricate it would be since positions would have to encode the context, i.e., the last two words. This is an important motivation for studying 2-way expressions and automata.

Actually, expression E 3 is not small since the sum hides the very big set D 3 : for a dictionary of size 1 million, this seems already unpracticable. But in practice, a much smaller expression could be sufficient. First, for many words, the frequency distribution of the word w is a sufficiently good approximation of the conditional probability P(w | u, v). Let us denote D 0 this set of words. For instance, the probability of observing the word the may not really depend on the previous words. Then, let D 1 be the set of words (disjoint from D 0 ) such that only the previous word is necessary to describe the probability. Finally, let D 2 be the rest of the dictionary. Now, we may replace expression E 3 by the following expression, whose size is much smaller if D 0 and D 1 contain enough words:

w∈D0 wP(w) + w∈D1,v∈D ←vwP(w | v) + w∈D2,u,v∈D ←←uvwP(w | u, v) *
To motivate the introduction of pebbles, let us add internationalization, which means that the user has the ability to write/speak alternately in two or more languages, e.g., English and French. All tasks such as automatic translation or speech recognition are now more complex since there is no a priori knowledge of the current language of the speaker. Again, splitting the problem into independent parts, we have to know the probability distributions P L for every involved language L, and, assuming a current language L, we should be able to solve the language processing task with a procedure Task L . Then, before processing the next word, we start a computation which re-reads the current prefix of the text in order to compute using P L the probability that the current language L is still valid. The next word is then processed with the current or the alternate language (see Figure 1). In order to compute the probability that the current language is still valid, we mark the current position with a pebble (↓ x ) and read the current prefix of the text with the automaton modeling the current language. Then we return to the marked position and lift the pebble (↑) in order to resume the top level computation. Details of these constructs will be developed in Section 5.

Weighted Linear Temporal Logic

Whereas weighted automata and weighted expressions have been extensively studied, logical formalisms adapted to the weighted case still need deeper understanding. This is especially true for weighted linear temporal logics [START_REF] Mandrali | Weighted LTL with discounting[END_REF], whereas weighted branching temporal logics have received more attention [START_REF] Ciesinski | On probabilistic computation tree logic[END_REF][START_REF] Buchholz | Model checking for a class of weighted automata[END_REF][START_REF] Meinecke | A weighted µ-calculus on words[END_REF][START_REF] Bollig | Weighted versus probabilistic logics[END_REF].

We would like to illustrate that using pebbles in weighted expressions or automata is a natural and powerful way to deal with nesting in LTL formulas. Temporal logics implicitely use a free variable to denote the position where the formula has to be evaluated. We will mark this position with a pebble, say x, in expressions E ϕ (x) or automata A ϕ (x) associated with an LTL formula ϕ.

English?

French?

OK KO OK KO Task En Task Fr ↓ x ↓ x ↑ ↑ ↑ ↑ → → → → Fig. 1.
Pebble automaton for the multi-language modeling task.

For this motivating example, we only consider finite words and the probabilistic setting. Given an LTL formula ϕ, a word u ∈ A + and a position i in u, the aim is to compute the probability P(ϕ, u, i) that ϕ holds on position i. Hence, the expression E ϕ (x) and the automaton A ϕ (x) associated with ϕ should compute this probability if pebble x marks position i of u.

For instance, the formula G ϕ (globally ϕ) means that ϕ should always hold in the future of the current position. Hence,

P(G( 1 3 a ∨ 3 4 b), aba, 0) = 1 3 • 3 4 • 1 3 and P(G( 1 3 a ∨ 3 4 b), aabb, 2) = 9 16
. More generally, P(G ϕ, u, i) = j≥i P(ϕ, u, j). Assume that we have already constructed an automaton A ϕ (y) with 2 designated terminal states {tt ϕ , ff ϕ }, such that runs ending in tt ϕ computes the probability that ϕ holds and those ending in ff ϕ computes the probability that ¬ϕ holds. Then, the automaton for G ϕ with the same property on terminal states tt G ϕ and ff G ϕ is depicted below:

A G ϕ = tt G ϕ ff G ϕ tt ϕ ff ϕ A ϕ (y) → x? ¬⊳?↓ y ⊳?↑ → ⊳? ⊳?↑

→

We can also give expressions for G ϕ and ¬ G ϕ:

E G ϕ (x) = ?→ * x? (y!E ϕ (y))→ * ? E ¬ G ϕ (x) = ?→ * x? (y!E ϕ (y))→ * (y!E ¬ϕ (y))→ * ? .
The expression E G ϕ (x) starts at the beginning of the word ( ?), moves right (→ * ) until it sees the marked position (x?). Then, it iterates the computation of ϕ with the current position marked with y (y!E ϕ (y)), moving right (→) between two computations. The iteration stops at the end of the word ( ?). The expression for ¬ G ϕ starts similarly, but it may exit the iteration at any point, computing the probability that ϕ does not hold (y!E ¬ϕ (y)).

The dual formula F ϕ (Finally ϕ) states that ϕ should eventually hold in the future of the current position. The semantics is obtained inductively with P(F ϕ, u, i) = P(ϕ, u, i) + P(¬ϕ, u, i) × P(F ϕ, u, i + 1): either ϕ holds immediately (P(ϕ, u, i)) or (+) it does not (P(¬ϕ, u, i)) and (×) it should be satisfied later (P(F ϕ, u, i + 1)). For instance, P(F( 1 3 a), abba, 0) = 1 3 + 2 3 (0 + 2 3 (0 + 2 3 • 1 3 )). The following dualities hold: F ϕ = ¬ G ¬ϕ and ¬ F ϕ = G ¬ϕ. Hence, we have

E F ϕ (x) = ?→ * x? (y!E ¬ϕ (y))→ * (y!E ϕ (y))→ * ? E ¬ F ϕ (x) = ?→ * x? (y!E ¬ϕ (y))→ * ? .
The automaton A F ϕ (x) is obtained from A G ϕ (x) by switching the terminal states:

A F ϕ = ff F ϕ tt F ϕ ff ϕ tt ϕ A ϕ (y) → x? ¬⊳?↓ y ⊳?↑ → ⊳? ⊳?↑ →
Using 2-way moves, it is not difficult to extend these constructions to cope with LTL including both future and past modalities.

Preliminaries

Words. The set of nonempty words over a finite alphabet A is denoted A + . We write u = u 0 • • • u n-1 ∈ A + a nonempty word of length |u| = n ≥ 1 with u i ∈ A for 0 ≤ i < |u|. The set of positions of u is pos(u) = {0, 1, . . . , |u|}. In particular, we include |u| in pos(u) even though the last letter is on position |u| -1.

Semirings. A semiring is a set S equipped with two binary internal operations denoted + and ×, and two neutral elements 0 and 1 such that (S, +, 0) is a commutative monoid, (S, ×, 1) is a monoid, × distributes over + and 0 × s = s × 0 = 0 for every s ∈ S. If the monoid (S, ×, 1) is commutative, the semiring itself is called commutative. See [START_REF] Droste | Semirings and formal power series[END_REF][START_REF] Sakarovitch | Elements of Automata Theory[END_REF] for more discussions about semirings, especially complete and continuous ones, as we describe now.

A semiring S is complete if every family (s i ) i∈I of elements of S over an arbitrary indexed set I is summable to some element in S denoted i∈I s i and called sum of the family, such that the following conditions are satisfied:

- i∈∅ s i = 0, i∈{1} s i = s 1 and i∈{1,2} s i = s 1 + s 2 ; -if I = j∈J I j is a partition, j∈J i∈Ij s i = i∈I s i ; - i∈I s i × j∈J t j = (i,j)∈I×J (s i × t j ).
Intuitively, this means that it is possible to define infinite sums that extends the binary addition and satisfies infinite versions of associativity and distributivity. In a complete semiring, for every s ∈ S, the element s * = i∈N s i exists (where s i is defined recursively by s 0 = 1 and s i+1 = s i × s). Here are some examples of complete semirings.

-The Boolean semiring ({0, 1}, ∨, ∧, 0, 1) with defined as an infinite disjunction.

-(R ≥0 ∪ {∞}, +, ×, 0, 1) with defined as usual for positive (not necessarily convergent) series: in particular,

s * = ∞ if s ≥ 1 and s * = 1/(1 -s) if 0 ≤ s < 1.
-(N ∪ {∞}, +, ×, 0, 1) as a complete subsemiring of the previous one.

-(R ∪ {-∞}, min, +, -∞, 0) with = inf and (R ∪ {∞}, max, +, ∞, 0) with = sup.

-Complete lattices such as ([0, 1], min, max, 0, 1).

-The semiring of languages over an alphabet A: (2 A * , ∪, +, ∅, {ε}) with defined as (infinite) union.

In this paper, we consider continuous semirings which are complete semirings in which infinite sums can be approximated by finite partial sums. Formally, a complete semiring S is continuous if the relation ≤ defined over S by a ≤ b if b = a + c for some c ∈ S is an order relation; and for every family (s i ) i∈I in S, the sum i∈I s i is the least upper bound of the finite sums i∈J s i for J ⊆ I finite. All the above complete semirings are also continuous.

Series and polynomials Let Z be a set. A series f over Z is a map f : Z → S. We denote by S Z the set of series over Z with coefficients in S. The support of a series f ∈ S Z is the set {z ∈ Z | f (z) = 0}. A series with a finite support is called a polynomial. We denote by S Z the set of polynomials over Z with coefficients in S.

We can lift addition from S to S Z pointwise by (f + g)(z) = f (z) + g(z) for all z ∈ Z. Then, (S Z , +, 0) is a commutative monoid where 0 is the series mapping every element z ∈ Z to 0. If Z is equipped with a structure of monoid and the semiring S is complete, we can also define the (Cauchy) product of two series by (f ×g)(z) = z=xy f (x)g(y) for all z ∈ Z. This sum may be infinite, but is well-defined since the semiring is complete. The Cauchy product is associative and admits as unit the characteristic function (denoted 1) of the neutral element of Z. Hence, (S Z , +, ×, 0, 1) is a semiring. When S is continuous, we can also lift infinite sums pointwise to S Z which becomes a continuous semiring.

Weighted Expressions with pebbles

The syntax of our weighted expressions is carefully chosen so that an efficient translation to weighted automata can be obtained, essentially based on Glushkov's construction as we will see in Section 7. Formally, for a (continuous) semiring S, an alphabet A and a set Peb of pebbles, the syntax is given by the grammar:

E ::= s | ϕ | → | ← | x!E | E + E | E • E | E + ϕ ::= a? | ? | ? | x? | ¬ϕ | ϕ ∧ ϕ | ϕ ∨ ϕ
with s ∈ S, a ∈ A, x ∈ Peb. We denote by Test the set of test formulas ϕ defined by the second line of the grammar above. For instance, one can check with ? and ? whether we are at the beginning or at the end of the word. This is indeed useful since we have 2-way expressions. We denote by pebWE the set of weighted expressions with pebbles. Below, we give the intuitive meaning of our weighted expressions. We start without pebbles (i.e., without x!E). Then, we introduce pebbles. The formal semantics is given in Table 1.

Notice that from the irreflexive iteration E + = n>0 E n , we get also the classical Kleene star: E * def = 1 + E + . Indeed, we also have E + = E • E * but if we apply Glushkov's construction (blindly) to E • E * we get an automaton with twice the number of states needed for E + . This is basically why we prefer to have E + as a primary construct.

We have chosen to distinguish between checking the current position with some test ϕ and moving to the right or left position with → and ←. This is in the spirit of XPath in trees. This allows to write concise expressions, e.g., E = → + a?← + b?→ + c?← + d?→ + to describe patterns consisting of an a having in its past a b, having in its future a c, having in its past a d. In the Boolean semantics, this expression defines words having this pattern. In the semiring N of natural numbers, the expression counts the number of occurrences of the pattern, e.g., [[E]](cabcdbadcbab) = 8. Indeed we may write an equivalent 1-way expression for this pattern but it would be less concise and harder to decipher (see e.g., [START_REF] Birget | State-complexity of finite-state devices, state compressibility and incompressibility[END_REF] for succinctness results in the Boolean case).

Let

u = u 0 u 1 • • • u |u|-1 ∈ A + .
A test ϕ will be evaluated at a position i ∈ pos(u): ? holds if i = 0, ? holds if i = |u| and a? holds if i < |u| and u i = a.

With the 2-way mechanism, a sub-expression such as a?← + b?→ + c?← + d? may start from position i, end in position j and still visit the whole word. In order to inductively define the semantics of expressions, we assign to triples

(u, i, j) a value [[E]](u, i, j) ∈ S.
It is also convenient to check-and-move so we introduce the macros a def = a?→ and a def = a?←. Then, we can write → * blue ← + ? → * black → * to define words having both blue and black as subwords. This allows to write classical (1-way) regular expressions such as (ab) + aa. In order to get the classical semantics for usual 1-way expressions, the evaluation of an expression on a whole word is defined as

[[E]](u) = [[E]](u, 0, |u|). For instance, [[a]](a) = [[a?→]](a, 0, 1) = 1, [[→ * a → * ]](baaba) = [[→ * a? → → * ]](baaba, 0, 5) = 3, and [[(2→) + ]](u) = 2 |u| .
Our 2-way expressions are uncomparable with expressions over the free group. Indeed, the expression aab always evaluates to 0 in our setting, whereas over the free group it would evaluate to 1 on b = aab.

Notice that with the 2-way mechanism we may write E = E 1 ? ← * ? E 2 to compute the product (intersection in the boolean semantics) of the values computed by E 1 and

E 2 : [[E]](u) = [[E 1 ]](u) × [[E 2 ]](u).
The 2-way mechanism together with iteration gives rise to infinite sums. This may be useful for probabilistic systems. For instance, in the continuous semiring (R ∞ ≥0 , +, ×, 0, 1), consider the expression E = (¬ ?(s →+(1-s)¬ ?←)) * ? with 0 < s < 1 some probability. Expression E describes a random walk1 and it will be used again in Section 5. Let F = ¬ ?(s → + (1 -s)¬ ?←) so that E = F * ?. Let u be a word of length m ≥ 2. We can easily see that for all i, j ∈ pos(u) and all n > |j -i|, the expression F n computes a positive value on (u, i, j). Therefore, the expression F * computes an infinite sum on (u, i, j). In the present case (0

< s < 1), the series n≥0 [[F n ]](u, i, j) converges and [[F * ]](u, i, j) ∈ R ≥0 .
On the other hand, for the expression G = ¬ ?→ + ¬ ?←, we can check that the series

n≥0 [[G n ]](u, i, j) diverges and we get [[G * ]](u, i, j) = ∞.
Since we are considering complete semirings, infinite sums exist and the semantics of an iteration E * or E + is always well-defined.

We explain now the pebble mechanism used in our expressions. The construct x!E marks with x the current position in u and evaluates E on the marked word, from beginning to end. Indeed, we can use x? in E to test whether the current position is marked. For instance, consider

E = → + a? x! (¬x?→) * b? (¬x?→) + c? ← + d? → + → *
which is a variant of our first example. Here the pattern consists of an a for which the corresponding prefix contains a b, having in its future a c, having in its past a d. In particular, the c must be on the left of the current a which is marked with x. Hence, we get [[E]](cabcdbadcbab) = 4.

As another example, on a word u, the expression (x!((2→) + ) →) + computes 2 |u|2 over the natural semiring 2 . Actually, the pebble is not tested in this expression: it is only used to restart the computation |u| times.

We give now the formal semantics of tests and of pebWE. For each word u ∈ A + , valuation σ : Peb → pos(u) and position i ∈ pos(u), the semantics u, σ, i |= ϕ of tests is defined inductively. The Boolean connectives are as usual. For the atoms, ? holds if i = 0, ? holds if i = |u|, a? holds if i < |u| and u i = a and x? holds if σ(x) = i < |u| (the last position |u| cannot be marked).

A marked word is a tuple (u, σ, i, j) where u ∈ A + is a word, σ : Peb → pos(u) is a valuation and i, j ∈ pos(u) are positions. We denote by Mk(A + ) the set of marked words (we will see below that it forms a partial monoid).

[[s]](u, σ, i, j) = s if j = i 0 otherwise [[ϕ]](u, σ, i, j) = 1 if j = i ∧ u, σ, i |= ϕ 0 otherwise [[→]](u, σ, i, j) = 1 if j = i + 1 0 otherwise [[←]](u, σ, i, j) = 1 if j = i -1 0 otherwise [[x!E]](u, σ, i, j) = [[E]](u, σ[x → i], 0, |u|) if j = i < |u| 0 otherwise [[E + F ]](u, σ, i, j) = [[E]](u, σ, i, j) + [[F ]](u, σ, i, j) [[E • F ]](u, σ, i, j) = k∈pos(u) [[E]](u, σ, i, k) × [[F ]](u, σ, k, j) [[E + ]](u, σ, i, j) = n>0 [[E n ]](u, σ, i, j)
Table 1. Semantics of weighted expressions

The semantics3 of a pebWE E is a map [[E]] : Mk(A + ) → S, i.e., a series over marked words: 1. Note that, since we are considering complete semirings, the infinite sum in the semantics of E + is always well-defined. If the expression has no free pebbles then we omit the valuation and simply write [[E]](u, i, j). For whole words we let

[[E]] ∈ S Mk(A + ) . It is is defined in Table
[[E]](u, σ) = [[E]](u, σ, 0, |u|) and [[E]](u) = [[E]](u, 0, |u|) as explained above.
Notice that for tests ϕ 1 and ϕ 2 , the expressions ϕ 1 ∧ ϕ 2 and ϕ 1 • ϕ 2 are equivalent, but ϕ 1 ∨ ϕ 2 and ϕ 1 + ϕ 2 are not equivalent in general. One can check that ϕ 1 + ¬ϕ 1 • ϕ 2 is equivalent to the disjunction ϕ 1 ∨ ϕ 2 . Hence, conjunctions and disjunctions in tests are not necessary for the expressive power of pebWE and they could have been defined as macros.

Similar to the star-height of an expression, we define the pebble-depth:

pebd(s) = pebd(ϕ) = pebd(←) = pebd(→) = 0 pebd(E + F ) = pebd(E • F ) = max(pebd(E), pebd(F )) pebd(E + ) = pebd(E) pebd(x!E) = 1 + pebd(E) .

Series over a partial monoid

We show in this subsection that the set of marked words can be endowed with a partial monoid structure which allows to define a Cauchy product on series in S Mk(A + ) . Since the sums can be lifted pointwise from S to series over S, we show that S Mk(A + ) is actually a continuous semiring. Indeed, the semantics defined for sum, product and iteration of pebWE in Table 1 corresponds to sum, Cauchy product and star in the continuous semiring S Mk(A + ) . This more formal view of the semantics of pebWE is especially useful for proofs, but since proofs are omitted in this paper this section may be skipped in a first reading.

Pebble weighted expressions and pebble weighted automata introduce two new difficulties. The first one comes from the 2-way navigation mechanism which prevents the computation of the behavior of an expression (or an automaton) using the concatenation of words in the underlying monoid, here the free monoid A + . The second one comes indeed from pebbles which allow to restart the computation. To address both problems, we had to fix the word when defining the semantics and we no more use the monoid structure of A + . Here, we define a partial monoid structure on the marked words and show how this allows us to reuse existing results from the classical theory of rational series.

A partial monoid is a triple (Z, •, Y ) where Z is the set of elements, • : Z 2 → Z is a partially defined associative concatenation 4 and Y ⊆ Z is a set of partial units satisfying:

∀x, z ∈ Z ∀y ∈ Y x • y = z =⇒ x = z ∀x, z ∈ Z ∀y ∈ Y y • x = z =⇒ x = z ∀z ∈ Z ∃!y ∈ Y y • z = z ∀z ∈ Z ∃!y ∈ Y z • y = z .
Indeed, a classical monoid is a partial monoid with the concatenation being totally defined and with the set of partial units being the singleton set consisting of the (real) unit.

We are especially interested in the partial monoid (Mk(A + ), •, Unit(A + )) of marked words over A + where

Mk(A + ) = {(u, σ, i, j) | u ∈ A + , σ : Peb → pos(u), i, j ∈ pos(u)} Unit(A + ) = {(u, σ, i, i) | u ∈ A + , σ : Peb → pos(u), i ∈ pos(u)}
and the partial concatenation is defined for all u ∈ A + , σ : Peb → pos(u) and i, j, k ∈ pos(u) by (u, σ, i, k) • (u, σ, k, j) = (u, σ, i, j) and it is undefined in all other cases. We can see that this partial concatenation is associative and that the above requirements for partial units are satisfied.

Note that a partial monoid needs not be graded and in particular, the partial monoid of marked words defined above is not graded. Hence, we cannot apply directly the theory of rational series over graded monoids as developped e.g. in [START_REF] Sakarovitch | Rational and recognisable power series[END_REF]. Instead, we will use the theory of rational series over a continuous semiring S (see e.g., [START_REF] Sakarovitch | Elements of Automata Theory[END_REF]III.5]). We first show that, even if the monoid Z, and more specifically Mk(A + ), is only partial, we can define (infinite) sums and (Cauchy) product on series over Z so that S Z forms a continuous semiring.

Let S be a continuous semiring and (Z, •, Y ) be a partial monoid. As described in Section 3, infinite sums may be lifted from S to series in S Z . We may also define the Cauchy product as usual. Note that, even though the concatenation in Z may be partially defined, the Cauchy product in S Z is always defined for f, g ∈ S Z and z ∈ Z by (f × g)(z) = x,y∈Z,z=x•y f (x) × g(y). The sum ranges over all pairs (x, y) for which the concatenation is defined and such that x • y = z. The sum may be finite or infinite but it is nonempty considering the left and right partial units of z. Finally, we let 1 Y be the characteristic function of the set Y of partial units of Z and we can easily check that it is a unit for the Cauchy product:

(f × 1 Y )(z) = x,y∈Z z=x•y f (x)1 Y (y) = x∈Z,y∈Y z=x•y f (x) = y∈Y z=z•y f (z) = f (z) .
Mimicking the proof for classical monoids, we can show the following. This allows to apply the theory of rational series over continuous semirings (see e.g., [START_REF] Sakarovitch | Elements of Automata Theory[END_REF]III.5]). In particular, a star operation may be defined.

We can check that the semantics of pebWE in the continuous semiring S Mk(A + ) as defined in Table 1 satisfies

[[E + F ]] = [[E]] + [[F ]] [[E * ]] = [[E]] * [[E • F ]] = [[E]] × [[F ]] [[E + ]] = [[E]] + . (1)

Weighted Automata with Pebbles

We fix a finite set Peb of pebbles and a (continuous) semiring S. We denote by Move = {←, →, ↑} ∪ {↓ x | x ∈ Peb} the set of possible moves of an automaton.

A pebble weighted automaton (pebWA) is a tuple A = (Q, A, I, M, T ) with Q a finite set of states, A a finite alphabet, I ∈ S Q a row vector assigning an initial weight to each state, T ∈ S Test Q a column vector assigning to each state a polynomial over tests, and M ∈ (S Test Move ) Q×Q the transition matrix.

We explain first the semantics of a pebWA on the automaton A 1 represented in Figure 2 with its matrix representation on the right.

Intuitively, we enter state 1 with weight 5. We can loop on state 1 if the current letter is either an a or a b, in which case we move right in the word. The weight of this loop is 2 or 3 depending on the current letter. If A 1 reads letter c while being in state 1, then it drops pebble x and restarts at the beginning of the word in state 2. There, it moves right in the word, either staying in state 2 with weight 1 (provided the current position does not carry the pebble), or going to state 3 with weight 7. Once we reach state 3, we must lift the pebble and go to state 4. Then, we move right coming back to state 1.

An accepting run of A 1 must start in state 1 and end in state 1. The weight of a run is the product of the weights of its transitions. Over the natural semiring (N ∞ , +, ×, 0, 1), each accepting run of A 1 has weight 5 ×

2 |u|a × 3 |u| b × 7 |u|c . 1 ⊳? 5 2 3 4 (2a? + 3b?)→ c? ↓ x ¬x? → 7→ ↑ → I = 5 0 0 0 M =     (2a? + 3b?)→ c? ↓ x 0 0 0 ¬x? → 7→ 0 0 0 0 ↑ → 0 0 0     T =     ? 0 0 0    
Fig. 2. A pebWA and its matrix representation. The non-deterministic choice in state 2 induces several runs. The semantics of the automaton is as usual the sum of the weights of all accepting runs. In our example,

A2 = s ¬⊳? → (1 -s) (¬⊲? ∧ ¬⊳?) ← ⊳? 0 1 2 n -2 n -1 n s 1 -s s 1 -s . . .
[[A 1 ]](u) = 5 × 2 |u|a × 3 |u| b × 7 |u|c × i∈pos(u) ui=c (i + 1) .
Consider also the 2-way automaton A 2 over the semiring (R ∞ ≥0 , +, ×, 0, 1), with 0 < s < 1. The matrix M of A 2 admits as unique coefficient the polynomial s ¬ ? → + (1 -s) (¬ ? ∧ ¬ ?) ←, which, for clarity, we preferred to draw with two loops in Figure 3. This is a compact and elegant way of representing a Markov chain describing a random walk, see Figure 3. The same example was described with a pebWE in Section 4.

Remark 2. Notice that 2-way weighted expressions/automata are strictly more expressive than their 1-way versions (where left moves are disabled). The automaton A 2 above for the random walk yields a counter-example. In fact, for s = 1 2 , the expression/automaton associates to a word u of length n the value 1 n+1 . This is not achievable by a 1-way weighted automaton over the semiring (R ∞ ≥0 , +, ×, 0, 1) with weights in Q. Intuitively, this is a consequence of the fact that the semantics of such an automaton is of the form a b c with a, b ∈ Z, b = 0 and c ∈ N: here b can be defined as the least common denominator of the weights appearing over transitions of the automaton. Hence, taking a word u of length p + 1 with p a prime number greater than b is sufficient to prove that such a 1-way weighted automaton cannot map word u to weight 1 p . Notice that this result strongly relies on the fact that we are dealing with infinite sums (because of the Kleene star, or the infinite number of runs). Indeed, it was shown in [START_REF] Bollig | Pebble weighted automata and transitive closure logics[END_REF] that 2-way WA are not more expressive than 1-way WA when the semantics is restricted to non-looping runs.

As for expressions, we allow macros in M and T : for a ∈ A, we use a def = a?•→ and a def = a? • ←, for d ∈ Move, we write d instead of tt? • d. For instance, the label of the loop on state 1 of A 1 could be written 2a + 3b.

For each p, q ∈ Q and d ∈ Move, we denote by M d p,q ∈ S Test the coefficient of move d in M p,q . For instance, M

↓ x 1,2 = c? in A 1 . We collect these coefficients in matrices M d = (M d p,q ) ∈ (S Test ) Q×Q .
We turn now to the formal definition of the semantics of pebWA. A configuration of A is a tuple (u, σ, q, i, π) with u ∈ A + a word, σ : Peb → pos(u) a valuation, q ∈ Q the current state, i ∈ pos(u) the current position, and π ∈ (Peb × pos(u)) * the stack of pebbles currently dropped. Since pebbles are reusable, the stack of pebbles may contain several occurrences of the same pebble dropped on different positions. In this case, only the last occurrence of each pebble is still visible for the automaton, older occurrences being hidden. This mechanism mimics the ability in pebWE to reuse the same pebble x in nested expressions x!E. We extract the visible pebbles from the stack π of dropped pebbles and the underlying valuation σ, hence defining a valuation σ π by induction over π by σ ε = σ and σ π(

x,i) = σ π [x → i].
We define the semantics of pebWA in terms of a weighted transition system TS(A) whose locations are the configurations of the automaton. The weight of (u, σ, p, i, π) ; (u, σ, q, j, π ) is defined by

[[M → p,q ]](u, σ π , i, i) if j = i + 1 and π = π (S1) [[M ← p,q ]](u, σ π , i, i) if j = i -1 and π = π (S2) [[M ↓ x p,q ]](u, σ π , i, i) if j = 0, i < |u| and π = π(x, i) (S3) [[M ↑ p,q ]](u, σ π , i, i) if π = π (y, j) for some y ∈ Peb (S4)
where [[M d p,q ]] is the semantics of M d p,q ∈ S Test , seen as a pebWE. Note from (S3) that a pebble cannot be dropped on position |u| in agreement with the convention adopted for weighted expressions.

The set of transitions of TS(A) consists of those (u, σ, p, i, π) ; (u, σ, q, j, π ) with a non-zero weight: hence TS(A) is a disjoint union of transition systems depending on the pair (u, σ) considered. A run of A is a path ρ in TS(A). Its weight is the product of the weights of its transitions from left to right.

Given a marked word (u, σ, i, j) ∈ Mk(A + ) and two states p, q ∈ Q, we define [[A p,q ]](u, σ, i, j) = ρ weight(ρ) where the sum ranges over all runs ρ from configuration (u, σ, p, i, ε) to configuration (u, σ, q, j, ε). This sum could be infinite, but is well defined since the semiring is complete. The semantics of A also use the initial and terminal weights:

[[A]](u, σ, i, j) = p,q∈Q I p × [[A p,q ]](u, σ, i, j) × [[T q ]](u, σ, j, j) .
When reading the whole word, we simply write [[A]](u, σ) for [[A]](u, σ, 0, |u|). Note that we can compute the set of free pebbles of an automaton, i.e., the set of pebbles x that may be tested with x? before being dropped with ↓ x . If the automaton has no free pebble, then the underlying valuation σ is not necessary and we simply write [[A]](u) for the semantics.

Layered automata. As observed in automaton A 1 , it is handy, if possible, to visualize a pebWA in terms of layers, where each layer contains subruns where no pebble is dropped or lifted. We will require in the following that there are a finite number of such layers: intuitively, this means that the depth of the current stack of pebbles is bounded by a fixed parameter K. Remark however that the stack may contain several occurrences of the same pebble. Also, due to the 2-way mechanism, runs may still be of unbounded size. More formally, we assume given a function : Q → {0, . . . , K} mapping each state to its layer. The top layer is K so (q) is the number of pebbles that can still be dropped on top of the stack. We want to start and end the computation at the top layer so we suppose that for all q ∈ Q, if I q = 0 or T q = 0 then (q) = K. To maintain syntactically the condition along every possible run, we also suppose for all p, q ∈ Q that if M ← p,q = 0 or M → p,q = 0 then (q) = (p); if M ↑ p,q = 0 then (q) = (p) + 1; and for all x ∈ Peb, if M ↓ x p,q = 0 then (q) = (p) -1. An automaton A verifying these conditions will be called K-layered in the following. If we order states by decreasing layers, a 2-layered automaton A = (Q, A, I, M, T ) is thus of the form

I = I (2) 0 0 , M =         N (2) D (2) 0 L (1) N (1) D (1) 0 L (0) N (0)         , T =         T (2) 0 0         (2)
where entries in N (i) are in S Test {←, →} , entries in L (i) are in S Test {↑} , and entries in

D (i) are in S Test {↓ x | x ∈ Peb} .
The entries of I (2) and T (2) are as usual in S and S Test respectively.

From Automata to Expressions

In this section, we prove that every K-layered pebble weighted automaton admits an equivalent pebble weighted expression. We first show that, for 2-way weighted automata (or 0-layered pebWA), we can use the classical constructions, e.g., the state elimination method of Brzozowski and McCluskey [START_REF] Brzozowski | Signal flow graph techniques for sequential circuit state diagrams[END_REF], the procedure of McNaughton and Yamada [START_REF] Mcnaughton | Regular expressions and state graphs for automata[END_REF] or the recursive algorithm [START_REF] Conway | Regular Algebra and Finite Machines[END_REF]. We refer to the 4. A pebWA and two equivalent generalized pebWA.

↓ x 2 → 2 → ⊳? ↑ → ↓ x (2 →) + ⊳? ↑ → x!(2 →) + → Fig.
survey of Sakarovitch [30, Section 6.2] where these methods are presented and compared for 1-way weighted automata.

In the state elimination method, states are progressively suppressed and transitions are labeled with (weighted) rational expressions. To deal with pebbles, we will also eliminate the lower layers and subsume their computations with expressions of the form x!E. Therefore, it is convenient to consider automata allowing pebWE in the labels of transitions.

We first introduce these generalized pebWA. Then, we show how to compute pebWE equivalent to the behaviors of 0-layered generalized pebWA. Finally, we explain how to deal with drop and lift moves of K-layered automata.

Generalized Pebble Automata

We start with an example presented in Figure 4. The loop of the left automaton gives rise to the iteration (2 →) + on the middle automaton. Moreover, the drop/lift process has even been replaced with the x!-feature of pebWE in the right automaton. This gives already the intuition of the construction of a pebWE equivalent to a pebWA. Note that the right automaton has a single layer whereas the left and middle ones have 2 layers.

Formally, a generalized pebWA (GpebWA) is a tuple A = (Q, A, I, M, T ) with I ∈ S Q , M ∈ (pebWE + S Test {↑} ∪ {↓ x | x ∈ Peb} ) Q×Q and T ∈ S Test Q . Intuitively, the entries M ← p,q • ← + M → p,q • → have been extended to arbitrary pebWE M pebWE p,q . The semantics of pebWA is easily extended to GpebWA. In fact, we only have to replace (S1-S2) by (G1-2) below:

[[M pebWE p,q ]](u, σ π , i, j) if π = π . (G1-2)
The definition of K-layered automata can easily be extended to GpebWA. Layered automata are still of the form given in (2), the only difference being that the entries of matrices N (i) are now pebWE instead of simple polynomials in S Test {←, →} . It is clear from the definition that every (K-layered) pebWA can be seen as a (K-layered) GpebWA.

Automata to expressions: 0-layered generalized pebWA

We deal in this section with GpebWA A = (Q, A, I, M, T ) with no drop or lift transitions, i.e., 0-layered GpebWA where the entries of the transition matrix are all pebWE: M ∈ pebWE Q×Q .

We first relate the semantics of the automaton with the star of the semantic matrix [[M ]]. For each p, q ∈ Q, the entry M p,q is a pebWE and its semantics [[M p,q ]] ∈ S Mk(A + ) is a series over marked words. Hence, the semantic matrix

[[M ]] = ([[M p,q ]]) (p,q)∈Q 2 ∈ S Mk(A + ) Q×Q .
Recall that K = S Mk(A + ) is a continuous semiring by Proposition 1. For each finite set Q, the semiring of matrices K Q×Q is also continuous. Hence, given a matrix H in K Q×Q , the star matrix H * = n≥0 H n ∈ K Q×Q is well-defined. Applying this to H = [[M ]] we can generalize the classical relation between the semantics of a 1-way WA and the star of a matrix of series. Theorem 3. Let A = (Q, A, I, M, T ) be a 0-layered GpebWA. For all states p, q ∈ Q, we have

[[A p,q ]] = ([[M ]] * ) p,q , i.e., [[A p,q ]](u, σ, i, j) = ([[M ]] * ) p,q (u, σ, i, j)
for all marked words (u, σ, i, j) ∈ Mk(A + ).

Proof. We show by induction on n ≥ 0 that for every (u, σ, i, j) ∈ Mk(A + ), ([[M ]] n ) p,q (u, σ, i, j) computes the sum of the weights of runs of length n from configuration (u, σ, p, i, ε) to configuration (u, σ, q, j, ε). This is true for n = 0, as 1 Unit(A + ) (u, σ, i, j) = 1 if and only if i = j. Then, assuming the property for n -1 ≥ 0, we prove it for n. A run of length n > 0 starts with a transition followed by a run of length n -1. Hence, the sum of the weights of runs of length n from configuration (u, σ, p, i, ε) to configuration (u, σ, q, j, ε) is computed by r∈Q,k∈pos(u)

[[M ]] p,r (u, σ, i, k) × ([[M ]] n-1 ) r,q (u, σ, k, j)
which is equal to ([[M ]] n ) p,q (u, σ, i, j) by definition of the matrix multiplication induced by the Cauchy product. Now, it is well known that the entries of the star of a matrix H are in the rational closure5 of the entries of H [START_REF] Conway | Regular Algebra and Finite Machines[END_REF]. Hence, we obtain: Theorem 4. Let A = (Q, A, I, M, T ) be a 0-layered GpebWA. We can construct a matrix Φ(M ) ∈ pebWE Q×Q which is equivalent to the automaton, i.e., such that [[Φ(M )]] = [[M ]] * . Moreover, the entries of Φ(M ) are in the rational closure of the entries of M .

The matrix Φ(M ) can be constructed from M using one of the classical algorithm, e.g., the recursive algorithm used in the proof below. We can also apply McNaughton-Yamada algorithm, or the state elimination method, or the system resolution method starting from any initial state p and final state q.

Proof. We use the recursive method, due to Conway, to construct a matrix

Φ(M ) of pebWE such that [[Φ(M )]] = [[M ]] * .
Let N ∈ K Q×Q be a matrix over a continuous semiring K.

Φ(M ) = E E F H H GE H + H GE F H . (4)

Dynamically Marked Words

In order to deal also with drop and lift moves of GpebWA, we first describe the semantics at a higher level, as we did in Section 4.1 for pebWE. If we only consider weighted automata with two-way navigation, marked words are suitable to define an equivalent semantics of pebWA. However, as soon as we introduce drop and lift moves, it is necessary to encode the contents of the stack of pebbles in the marked words, as it will change throughout the computation. Hence, we consider the partial monoid (DMk(A + ), •, DUnit(A + )) of dynamically marked words over A + where

DMk(A + ) = {(u, σ, i, π, i , π ) | u ∈ A + , σ : Peb → pos(u), i, i ∈ pos(u), π, π ∈ (Peb × pos(u)) * } DUnit(A + ) = {(u, σ, i, π, i, π) | u ∈ A + , σ : Peb → pos(u), i ∈ pos(u), π ∈ (Peb × pos(u)) * }
and the partial concatenation is defined for all u ∈ A + , σ :

Peb → pos(u), i, i , i ∈ pos(u), π, π , π ∈ (Peb × pos(u)) * by (u, σ, i, π, i , π ) • (u, σ, i , π , i , π ) = (u, σ, i, π, i , π )
and it is undefined in all other cases. We can check that this is indeed a partial monoid, so that, by Proposition 1, (S DMk(A + ) , +, ×, 0, 1 DUnit(A + ) ) is a continuous semiring.

6.4 Automata to expressions: K-layered generalized pebWA is now possible to give a natural semantics of drop and lift moves as series over DMk(A + ):

[[[↓ x ]]](u, σ, i, π, i , π ) = 1 if i < |u|, i = 0, π = π(x, i) 0 otherwise, [[[↑]]](u, σ, i, π, i , π ) = 1 if π = π (y, i ) for some y ∈ Peb 0 otherwise.
Actually, it is also possible to introduce dynamic pebble weighted expressions (DpebWE) simply by replacing the x!-construct by new atoms for drop and lift moves:

F ::= s | ϕ | → | ← | ↓ x | ↑ | F + F | F • F | F * .

The dynamic semantics [[[F ]]

] of a DpebWE is a series over DMk(A + ). The semantics of ↓ x and ↑ is already given above. For another atom F , it is inherited from the semantics of pebWE:

[[[E]]](u, σ, i, π, i , π ) = [[E]](u, σ π , i, i ) if π = π 0 otherwise.
Finally, since S DMk(A + ) is a continuous semiring, the semantics of sum, concatenation and star is obtained compositionnally:

[[[E + F ]]] = [[[E]]] + [[[F ]]] [[[E • F = [[[E]]] × [[[F ]]] [[[E * ]]] = [[[E]]] * .
We can now mimick Section 6.2 in order to translate automata into DpebWE. For instance, the DpebWE (↓ x (2→) + ?↑→) * is equivalent to the pebWA on the left of Figure 4.

Actually, we can deal with DpebWA which are automata A = (Q, A, I, M, T ) where transitions are labelled with DpebWE, i.e., M ∈ DpebWE Q×Q . The semantics is obtained as for pebWA via a weighted transition system TS(A): the weight of a transition (u, σ, p, i, π) ; (u, σ, q, i , π ) is now [[[M p,q ]]](u, σ, i, π, i , π ). Then, for (u, σ, i, π, i , π ) ∈ DMk(A + ), we define [[[A p,q ]]](u, σ, i, π, i , π ) as the sum of weights of the runs from configuration (u, σ, p, i, π) to configuration (u, σ, q, i , π ). Copying, mutatis mutandis, the proofs of Theorems 3 and 4 we obtain:

Proposition 5. Let A = (Q, A, I, M, T ) be a DpebWA. For all p, q ∈ Q, we have [[[A p,q ]]] = ([[[M ]]] * ) p,q . Moreover, the matrix Φ(M ) ∈ DpebWE Q×Q (whose entries are in the rational closure of the entries of M ) satisfies [[[Φ(M )]]] = [[[M ]]] * .
In particular, the semantics of a DpebWA verifies:

[[[A]]] = [[[I]]] × [[[M ]]] * × [[[T ]]].
Remark 6. The partial monoid Mk(A + ) is embedded in DMk(A + ) by identifying the marked word (u, σ, i, i ) with the dynamically marked word (u, σ, i, ε, i , ε). Also, any pebWA A = (Q, A, I, M, T ) is a DpebWA and the semantics over

Mk(A + ) coincide: [[A p,q ]](u, σ, i, i ) = [[[A p,q ]]](u, σ, i, ε, i , ε).
Hence, Proposition 5 constructs a DpebWE equivalent Mk(A + ) to the pebWA A. But our aim is to construct a pebWE which is equivalent to A. This is achieved below using as a tool the detour via DpebWE.

First, we show that pebWE can be seen as a fragment of DpebWE if we interpret x!E as a macro for ↓ x • E • ? • ↑. Indeed with this interpretation, the semantics coincide:

Lemma 7. Let E be a pebWE and let (u, σ, i, π, i , π ) ∈ DMk(A + ). Then, [[[E]]](u, σ, i, π, i , π ) = 0 implies π = π. Moreover, if π = π then [[[E]]](u, σ, i, π, i , π ) = [[E]](u, σ π , i, i ) .
Proof. We proceed by structural induction on the pebWE. For atoms of pebWE, the result is clear from the definition of [[ [-]]]. For sum, concatenation and star, the result is trivial since both semantics are compositional. The interesting case is x!E which is interpreted as

↓ x • E • ? • ↑ in DpebWE. By definition of [[[-]]
] and the Cauchy product in S DMk(A + ) we have

s = [[[↓ x • E • ? • ↑]]](u, σ, i, π, i , π ) = y∈Peb [[[E]]](u, σ, 0, π(x, i), |u|, π (y, i )) .
Since E ∈ pebWE, we obtain by induction that each term of the sum above is

null if π(x, i) = π (y, i ). Hence, s = 0 implies π = π. Moreover, if π = π then either i = i and s = 0 = [[x!E]](u, σ π , i, i ), or i = i and s = [[[E]]](u, σ, 0, π(x, i), |u|, π(x, i)) = [[E]](u, σ π(x,i) , 0, |u|) = [[x!E]](u, σ π , i, i)
where the second equality holds by induction and the third one follows from

σ π(x,i) = σ π [x → i].
We will extend Theorem 4 to any K-layered GpebWA A = (Q, A, I, M, T ). For i ≤ K, we let Q (i) = -1 (i) be the set of states in layer i. Note that a GpebWA is also a DpebWA hence we may apply the above results. Proposition 8. Let A = (Q, A, I, M, T ) be a 1-layered GpebWA. We can construct a 0-layered GpebWA A (1) = (Q (1) , A, I (1) , M (1) , T (1) ) which is equivalent to A:

[[A p,q ]] = [[A (1)
p,q ]] for all p, q ∈ Q (1) . We use the layered decomposition given in [START_REF] Berry | From regular expressions to deterministic automata[END_REF]. To simplify the notation, we write N = N (1) , D = D (1) , L = L (0) and P = N (0) so that M = N D L P .

Let p, q ∈ Q (1) be in layer 1 and p , q ∈ Q (0) be in layer 0. Then, D is a dropmatrix whose (p, p )-entry can be written x∈Peb d x p,p • ↓ x with d x p,p ∈ S Test . The (q , q)-entry of the lift-matrix L can be written e q ,q • ↑ with e q ,q ∈ S Test . Now, P is a Q (0) × Q (0) matrix of pebWE and we may apply Proposition 5 in order to get a matrix Φ(P ) of pebWE which is equivalent to the iteration of P :

[[[Φ(P )]]] = [[[P ]]] * . From (D, P, L), we define the Q (1) × Q (1) pebWE-matrix G by G p,q = p ,q x∈Peb d x p,p • x! Φ(P ) p ,q • e q ,q • → * .
The matrix G is also denoted C(D, P, L) below. Note that the maximal pebbledepth of the entries of G is at most 1 plus the maximal pebble-depth of the entries of P since the construction Φ(P ) does not increase the pebble-depth.

Lemma 9. We have [[[G]]] = [[[D]]] × [[[P ]]] * × [[[L]]].
Proof. Recall that when viewing pebWE as DpebWE we interpret the expression

x!E as ↓ x • E • ? • ↑. Now, it is easy to check that [[[→ * • ? • ↑]]] = [[[↑]]], hence the pebWE x! Φ(P ) p ,q • e q ,q • → * is equivalent to ↓ x • Φ(P ) p ,q • e q ,q • ↑. We deduce that [[[G p,q ]]] = p ,q [[[D p,p ]]] × [[[Φ(P ) p ,q ]]] × [[[L q ,q ]]] .

Since [[[Φ(P )]]] = [[[P ]

]] * by Proposition 5, the result follows.

To conclude the proof of Proposition 8, we simply set (1) ]]] * . Using again Proposition 5 we get for all p, q ∈ Q

M (1) = N + G. Now, for all p, q ∈ Q (1) , we have [[[A p,q ]]] = ([[[M ]]] * ) p,q by Proposition 5. Moreover, the upper-left of [[[M ]]] * is ([[[N ]]] + [[[D]]] × [[[P ]]] * × [[[L]]]) * which is, by Lemma 9, equal to ([[[N ]]] + [[[G]]]) * = [[[M
(1) that [[[A (1) p,q ]]] = ([[[M (1) ]]] * ) p,q = ([[[M ]]] * ) p,q = [[[A p,q ]]]. Using Remark 6, we deduce that [[A p,q ]] = [[A (1) p,q ]
]. Proposition 8 can then be generalized to an arbitrary number of layers.

Proposition 10. Let A = (Q, A, I, M, T ) be a K-layered GpebWA. We can construct a 0-layered GpebWA A (K) = (Q (K) , A, I (K) , M (K) , T (K) ) which is equivalent to A: [[A p,q ]] = [[A (K) p,q ]] for all p, q ∈ Q (K) .
Proof. We use again the notation of the layered decomposition. The proof is by induction on K. When K = 0 we simply have A (0) = A, i.e., M (0) = N (0) . For K > 0, we set M (K) = N (K) + C(D (K) , M (K-1) , L (K-1) ) where the matrix M (K-1) is obtained by induction. Correctness follows from Proposition 8.

Finally, from Theorem 4 and Proposition 10 we deduce:

Theorem 11. Let A = (Q, A, I, M, T ) be a K-layered GpebWA. The matrix H = Φ(M (K) ) of pebWE satisfies [[H p,q ]] = [[A p,q ]] for all p, q ∈ Q (K) . Therefore, the pebWE E(A) = I × H × T is equivalent to A: [[E(A)]] = [[A]]. Moreover, the pebble-depth of E(A) is at most K if A is a K-layered pebWA.

From Expressions to Automata

We describe in this section how to transform a weighted expression with pebbles to an equivalent weighted automaton with pebbles. Expressions are very convenient to denote in a rather clear and intuitive way the quantitative functions that we want to compute. On the other hand, automata are much more amenable to efficient algorithms, e.g., for evaluation as shown in Section 8. Hence, we need efficient translations from expressions to automata. Such translations have been well-studied both in the boolean and in the weighted (1-way) cases. Glushkov's translation (or Berry-Sethi) is acknowledged to be among the best ones. The good news is that this construction can be adapted to cope with 2-way moves and pebbles as we will show in this section. The construction is by structural induction on the expression. Theorem 12. For each pebWE E we can construct a layered pebWA

A(E) such that [[A(E)]] = [[E]], i.e., for all (u, σ, i, j) ∈ Mk(A + ) we have [[A(E)]](u, σ, i, j) = [[E]](u, σ, i, j) .
Moreover, the number of layers in A(E) is the pebble-depth of E.

We define the literal-length (E) of an expression as the number of occurrences of moves (← or →) plus twice the number of occurrences of ! (in x!-). We will see that the number of states of A(E) will be 1 + (E). For a 2-way expression E of pebble-depth 0 (2-way-WE) the literal-length is simply the number of moves, which are the positions to be marked for Glushkov's construction.

For the rational operations (+, •, * , and + ), we can still use the classical constructions even though we are working with pebWA. We recall these constructions below for the sake of completeness. The main novelty is indeed the treatment of pebbles.

We adopt the presentation of standard automata by Sakarovitch [START_REF] Sakarovitch | Automata and expressions[END_REF]. A standard automaton A = (Q, A, I, M, T ) has a single initial state ι with (initial) weight 1, all other states have initial weight 0. Moreover, the initial state ι has no ingoing transition. We use both the graphical representation and the matrix representation of an automaton:

A = ι c N J U A = 1 0    0 J 0 N      c U  
Since terminal weights allow polynomials over Test with the mapping T : Q → S Test , we will be able to cope with expressions of the form E • ϕ? and E • s without adding unnecessary states. For s ∈ S and ϕ ∈ Test, we simply write s for stt? and ϕ for 1ϕ, and also → for 1tt?→ and ← for 1tt?←. We start with atoms. Compared to the classical (1-way) translation, a slight difference is that we are using tests (ϕ) and moves (←,→) instead of letters (a = a?→) for the atoms. The automata for the atoms are defined as

A(s) = ι s A(→) = ι → 1 A(ϕ) = ι ϕ A(←) = ι ← 1
and we can easily see that they are equivalent to the corresponding atoms

: if E is an atom then [[E]](u, σ, i, j) = [[A(E)]](u, σ, i, j) for all (u, σ, i, j) ∈ Mk(A + ).
The constructions for sum and concatenation are as usual.

A 1 + A 2 = ι c 1 + c 2 N 1 J 1 U 1 N 2 J 2 U 2 A 1 • A 2 = ι c 1 c 2 N 1 J 1 U 1 c 2 N 2 c 1 J 2 U 2 U 1 J 2
In the concatenation, we are overloading the product notation as follows. The product of two monomials s 1 ϕ 1 and s 2 ϕ 2 from S Test should be understood as (s 1 s 2 )(ϕ 1 ∧ ϕ 2 ) to stay in S Test . Hence c 1 c 2 and the entries of

U 1 c 2 are in S Test . Similarly, in U 1 J 2 , the product of a monomial s 1 ϕ 1 ∈ S Test and a monomial s 2 ϕ 2 d (with d ∈ Move) is defined as (s 1 s 2 )(ϕ 1 ∧ ϕ 2 )d.
Hence, the entries of the matrices c 1 J 2 and U 1 J 2 are in S Test Move . The matrix representation is therefore:

A 1 • A 2 = 1 0 0        0 J 1 c 1 J 2 0 N 1 U 1 J 2 0 0 N 2               c 1 c 2 U 1 c 2 U 2       
For instance, the automaton for 2a = 2 • a? • → is computed as follows:

ι 2 • ι a? • ι → 1 = ι 2a 1
Similarly, for the expression E = (2a? + b?)→(2b? + 3c?) we compute the concatenation of 3 automata as follows:

ι 2a? + b? • ι → 1 • ι 2b? + 3c? = ι 2a + b 2b? + 3c?
Finally, the star is also computed as usual with the following construction.

A * = ι c ′ N + U c ′ J c ′ J U c ′ A * = 1 0    0 c J 0 N + U c J      c U c  
where c ∈ S Test is defined to be equivalent to c * as follows. Since c ∈ S Test and test formulas are closed under boolean connectives, we find an equivalent expression c ≡ i s i ϕ i with (ϕ i ) i pairwise incompatible test formulas (i = j implies ϕ i ∧ ϕ j unsatisfiable). Then we can easily check that [

[c]] * = [[c ]] with c = i s * i ϕ i .
Notice that s * i ∈ S is well-defined since the semiring is complete. As for the concatenation, we can check that the entries of U c are in S Test and the entries of U c J are in S Test Move . The strict iteration A + is computed similarly by simply changing the final weight of ι to c = i s + i ϕ i (note that 0 + = 0), but keeping the other occurrences of c in c J, U c J and U c .

For instance, for expression E = → + a?← + b?→ + c?← + d?→ + introduced in Section 4, we can compute the automaton as follows:

A(→ + ) = ι → → 1 A(→ + • a?) = ι → → a? A(E) = ι → → ← a?← → b?→ ← c?← → d?→ 1
Finally, we give the construction for x!E which should drop the pebble on the current position, evaluate E from beginning to end ( ?) of the word and finally lift the pebble. From a standard automaton A equivalent to E, we construct the following standard automaton x!A :

x!A = ι ′ ι ↓ x τ ′ N J U ⊳?↑ x!A = 1 0 0 0        0 0 ↓ x 0 0 0 0 0 0 0 0 J 0 U ?↑ 0 N               0 1 0 0        (5)
For instance, consider again expression E below used in Section 4:

E = → + a? x! (¬x?→) * b? (¬x?→) + c? ← + d? → + → * .
The construction applied to E gives the following pebWA. Let us briefly discuss the complexity of our translation. Clearly, the number of states of the automaton A(E) is 1 plus the literal-length (E) of expression E. The time complexity is cubic in the length of E. It should be possible to get a quadratic algorithm by generalizing the notion of star normal form introduced in [START_REF] Brüggeman-Klein | Regular expressions into finite automata[END_REF] for word languages or the algorithm presented in [START_REF] Allauzen | A unified construction of the Glushkov, Follow, and Antimirov automata[END_REF] for classical weighted expressions and automata.

To conclude this section, we prove the correctness of the constructions. This correctness is trivial for the atoms. For sum, product and star, the proof is similar to the case of classical (1-way) weighted expressions and automata. For the sake of completeness, we give below the arguments for product and star, then we deal with the x!-construction.

From Proposition 5, we know that [

[[A]]] = [[[I]]] × [[[M ]]] * × [[[T ]]].
Using the special form of standard automata and (3), we have

[[[M ]]] =    0 [[[J]]] 0 [[[N ]]]    [[[M ]]] * =    1 [[[J]]][[[N ]]] * 0 [[[N ]]] *    and we get [[[A]]] = [[[c]]] + [[[J]]][[[N ]]] * [[[U ]]].
For the concatenation, the matrix

N of A = A 1 • A 2 satisfies (applying (3)): [[[N ]]] =    [[[N 1 ]]] [[[U 1 J 2 ]]] 0 [[[N 2 ]]]    [[[N ]]] * =    [[[N 1 ]]] * [[[N 1 ]]] * [[[U 1 J 2 ]]][[[N 2 ]]] * 0 [[[N 2 ]]] *    .
Hence we obtain

[[[A]]] = [[[c]]] + [[[J]]][[[N ]]] * [[[U ]]] = [[[c 1 c 2 ]]] + [[[J 1 ]]][[[N 1 ]]] * [[[U 1 c 2 ]]] + [[[J 1 ]]][[[N 1 ]]] * [[[U 1 J 2 ]]][[[N 2 ]]] * [[[U 2 ]]] + [[[c 1 J 2 ]]][[[N 2 ]]] * [[[U 2 ]]] = ([[[c 1 ]]] + [[[J 1 ]]][[[N 1 ]]] * [[[U 1 ]]])([[[c 2 ]]] + [[[J 2 ]]][[[N 2 ]]] * [[[U 2 ]]]) = [[[A 1 ]]][[[A 2 ]]]
For the star construction, the correctness is obtained as follows using classical rational identities and [

[[c]]] * = [[[c ]]]: [[[A]]] * = ([[[c]]] + [[[J]]][[[N ]]] * [[[U ]]]) * = ([[[c]]] * [[[J]]][[[N ]]] * [[[U ]]]) * [[[c]]] * = ([[[c ]]][[[J]]][[[N ]]] * [[[U ]]]) * [[[c ]]] = [[[c ]]] + [[[c ]]][[[J]]]([[[N ]]] * [[[U ]]][[[c ]]][[[J]]]) * [[[N ]]] * [[[U ]]][[[c ]]] = [[[c ]]] + [[[c ]]][[[J]]]([[[N ]]] + [[[U ]]][[[c ]]][[[J]]]) * [[[U ]]][[[c ]]] = [[[c ]]] + [[[c J]]]([[[N + U c J]]]) * [[[U c ]]] = [[[A * ]]]
It remains to prove the correctness of the new construction for the x!-operation. Assume for simplicity that A is a 0-layered automaton, then A = x!A is a 1-layered automaton and its layered decomposition is shown in [START_REF] Bojańczyk | Tree-walking automata[END_REF]. We the single computation in the automaton labeled by u, from left to right: at every position of the word, we only have to keep one memory cell containing the state reached after the current prefix of u. This memory cell can be updated with each letter in constant time using the transition function. On the overall, this leads to a complexity O(|u|) (in particular, independent of the automaton size). For a non-deterministic finite-state automaton, this complexity is not achievable anymore. A first solution consists of determinizing the automaton and then applying previous method: we obtain a complexity O(2 n + |u|) where n is the number of states of the NFA. This method cannot be extended to weighted automata, as they are not necessarily determinizable. Hence, we would rather use a dynamic programming method. We will pay the price of non-determinism by using more memory cells during the left-to-right computation of the runs of the automaton over the word. We use one memory cell s q for every state q of the automaton. Cell s q is a boolean which is true after reading a word u if and only if there exists a run labeled u leading from an initial state to state q. Cells are initially true for initial states and false otherwise. The update of the cells when reading a letter a is done by the multiplication of the row vector of cells (of dimension 1 × |Q|) with the adjacency matrix of the transitions of the automaton labeled with letter a. Hence, each update requires a number of operations O(n 2 ), leading to an overall complexity of O(n 2 |u|). This method can naturally be extended to the weighted setting using memory cells containing values in S. More precisely, cell s q holds the sum of weights of runs starting in an initial state and ending in state q. The update now use the weighted transition matrix and can be done with the same complexity.

We now explain how to evaluate layered pebWA with similar methods. Let A = (Q, A, I, M, T ) be a K-layered pebWA. As in Section 6.4, for k ≤ K, we let Q (k) = -1 (k) be the set of states in layer k. For each layer k we let n k = |Q (k) |. The total number of states is then n = |Q| = K k=0 n k . Theorem 14. Given a K-layered pebWA with p ≥ 0 reusable pebbles and a word u ∈ A + , we can compute with O((p + 1)|Q| 3 |u| p+1 ) scalar operations (sum, product, star) the values [[A q,q ]](u, σ) for all layers k ≤ K, states q, q ∈ Q (k) and valuations σ : Peb → pos(u).

Proof. We follow the same basic idea, recalled previously, used to evaluate classical weighted automata: memory cells are associated with each state computing weights of the runs from left to right. The 2-way navigation is then resolved by adding more memory cells (a quadratic number with respect to n), namely those that compute weights of the back and forth loops. Finally, we deal with layers inductively. In the whole proof, we fix a word u ∈ A + .

Recall that, for all valuations σ : Peb → pos(u), layers k ∈ {0, . . . , K} and states q, q ∈ Q (k) , the value [[A q,q ]](u, σ) is the sum of weights of the runs from configurations (u, σ, q, 0, ε) to (u, σ, q , |u|, ε): observe that the stack of pebbles is empty at the beginning of these runs, hence they stay in layers k, k -1, . . . , 0. In the following, these values (and others that will be defined later) will be (u, σ) (u, σ) q q ′ q q ′ Fig. 5. Runs of a 2-way automaton grouped into matrices indexed by subsets of states. In particular, we let

B (k) σ = ([[A q,q ]](u, σ)) q,q ∈Q (k) be such a matrix indexed by Q (k) × Q (k) .
Let k ∈ {0, . . . , K} be a layer of the automaton. If k > 0, we assume by induction that for all valuations σ : Peb → pos(u) we have already computed the matrices B (k-1) σ . For each valuation σ : Peb → pos(u), we will compute the matrix B (k) σ reading the word u from left to right. Formally, for 0 ≤ i ≤ |u|, we define the matrix B →i σ = (B →i σ,q,q ) q,q ∈Q (k) where B →i σ,q,q is the sum of weights of the runs from configuration (u, σ, q, 0, ε) to (u, σ, q , i, ε) with intermediary configurations of the form (u, σ, r, j, π) with π = ε or j ≤ i (See left of Figure 5). These are the runs which move from the beginning of the word to position i, staying on the left of position i, unless some pebbles are currently dropped (if a pebble is dropped, then automaton can read the whole word). In order to compute inductively B →i σ using B →i-1 σ , we also define the matrices B i σ = (B i σ,q,q ) q,q ∈Q (k) where B i σ,q,q is the sum of weights of the runs from configuration (u, σ, q, i, ε) to (u, σ, q , i, ε) with intermediary configurations of the form (u, σ, r, j, π) with π = ε or j ≤ i (See right of Figure 5). Again, these runs stay on the left of their starting position except when they drop pebbles.

By definition we have B →0 σ = B 0 σ . Moreover, for 0 < i ≤ |u|, a run from position 0 to position i can be decomposed as a run from position 0 to position i -1 followed by a right move, followed by a loop over position i:

B →i σ = B →i-1 σ × M →,(k) σ,i-1 × B i σ .
Here and in the following, we will denote by

M d,(k) σ,i the Q (k) × Q (k)
-matrix with (q, q )-coefficient given by [[M d q,q ]](u, σ, i, i) for d ∈ {→, ←}: this coefficient denotes the weight of taking a transition with move d from state q to state q on position i with current valuation σ. We will also need similar matrices for drop and lift moves. We denote by M

↓ x ,(k) σ,i the Q (k) × Q (k-1) -matrix with (q, q )- coefficient given by [[M ↓ x q,q
]](u, σ, i, i). Without loss of generality, we assume that lift moves only occur on position |u| of the word u, hence we do not need to give position and valuation (as no pebble can be dropped on this position) to define similar matrix for lift: let M ↑,(k) be the Q (k-1) × Q (k) -matrix with (q, q )coefficient given by [[M ↑ q,q ]](u, σ, |u|, |u|) for any valuation σ.

We now explain how to compute the matrices B i σ inductively from left to right. At the bottom level (k = 0) no pebble can be dropped and we get

B 0 σ = Id B i σ = M ←,(k) σ,i × B i-1 σ × M →,(k) σ,i-1 * if 0 < i ≤ |u| .
If k > 0, the run may immediately drop some pebble x ∈ Peb on position 0 ≤ i < |u| resulting in the nested computation of

N (k) σ,i = x∈Peb M ↓ x ,(k) σ,i × B (k-1) σ[x →i] × M ↑,(k) .
If i > 0, the run may also start by moving left, hence we obtain

B 0 σ = N (k) σ,0 * B i σ = N (k) σ,i + M ←,(k) σ,i × B i-1 σ × M →,(k) σ,i-1 * if 0 < i < |u| B |u| σ = M ←,(k) σ,|u| × B |u|-1 σ × M →,(k) σ,|u|-1 *
using the hypotheses ensuring that no pebble is dropped on the last position.

Finally, once all these matrices obtained, we can compute the behavior of layer k with the formula

B (k) σ = B →|u| σ .
To conclude this proof, it remains to count the number of scalar operations in the whole computation. For this, we first count the number of matrix operations (sum, product and star) and then infer the number of scalar operations assuming standard algorithms on matrices (quadratic for sum, cubic for product and cubic for star using Lemma 13).

Fix a layer k. For all valuations σ (there are |u| p such valuations), matrices B →i σ , B i σ must be computed for every 0 ≤ i ≤ |u|. When k = 0, the total number of matrix operations (sum, product, star) is O(|u| p × |u|), which corresponds to O(n 3 0 × |u| p+1 ) scalar operations. For k > 0, the computation of

N (k) σ,i takes O(p(n k n 2 k-1 + n 2 k n k-1
)) scalar sum and products for each σ and i. Hence, the total number of scalar operations for computing all matrices

B →i σ , B i σ of layer k is now O(p(n k n 2 k-1 + n 2 k n k-1 + n 3 k )|u| p+1 ). Summing over all k ≤ K, we get a total number of O((p + 1)n 3 |u| p+1 ) scalar operations since n 3 0 + K k=1 n k n 2 k-1 + n 2 k n k-1 + n 3 k ≤ n 3 .
It is important to notice that the complexity with respect to the pebWA does not depend on the number K of layers but only on the total number of states. The number of pebbles occurs in the exponent but since we allow reusable pebbles, this number may be rather small. This is in the same vein as restricting the number of variable names, e.g., in first-order logic, without restricting the quantifier depth. Restricting the number of variable names often results in much lower complexity. For instance, the complexity of the evaluation (model-checking) problem of first-order logic over relational structures drops from PSPACE to PTIME when the number of variable names is bounded [START_REF] Vardi | The complexity of relational query languages[END_REF][START_REF] Vardi | On the complexity of bounded-variable queries[END_REF].

We have seen in Section 2.2 that weighted LTL formulas can be described with pebWE using two pebbles x and y. Actually, the same constructions are valid if we reuse pebble x instead of y. For instance, until may be described with E ϕUψ (x) = ?→ * x? (x!(E ¬ψ (x)← * E ϕ (x)))→ * (x!E ψ (x))→ * ? .

Therefore, any weighted LTL formula ϕ may be described with a pebWE E ϕ using a single pebble x. The pebble-depth of E ϕ being the nesting depth of modalities in ϕ. Using Theorem 12 we obtain a layered pebWA A ϕ equivalent to E ϕ . The number K of layers in A ϕ is the pebble-depth of E ϕ , i.e., the nesting depth of ϕ. Moreover, A ϕ uses only one pebble. The number of states of A ϕ is linear in the size of ϕ. Hence, Theorem 14 yields an evaluation algorithms using O(|ϕ| 3 |u| 2 ) scalar operations. We see below that there is an algorithm which is also linear in |u|.

We say that a K-layered pebWA A = (Q, A, I, M, T ) is strongly K-layered if in each layer only a fixed pebble may be dropped: for all i ≤ K, there is a pebble x i ∈ Peb such that for all q, q ∈ Q and x ∈ Peb, if (q) = i and x = x i then M ↓ x q,q = 0.

Theorem 15. Given a strongly K-layered pebWA with p > 0 reusable pebbles and a word u ∈ A + , we can compute with O(|Q| 3 |u| p ) scalar operations (sum, product, star) the values [[A q,q ]](u, σ) for all layers k ≤ K, states q, q ∈ Q (k) and valuations σ : Peb → pos(u).

Proof. The idea is to decrease by 1 the exponent in the complexity by reducing the total number of valuations σ for which we must compute the matrices used in the proof of Theorem 14. Indeed, knowing the unique pebble that may be dropped in a given layer permits to forget the precise position of this pebble when computing the matrices of this layer.

Let 0 ≤ k ≤ K be a layer of A. In addition to matrices defined in the proof of Theorem 14, we introduce new matrices B i σ and B i→ σ in order to compute the sum of weights of runs which stay on the right of their starting position (except when they drop pebbles). For every states q, q ∈ Q (k) and 0 ≤ i ≤ |u|, we denote by B i σ,q,q the sum of weights of the runs from configuration (u, σ, q, i, ε) to (u, σ, q , i, ε) with intermediary configurations of the form (u, σ, r, j, π) with π = ε or j ≥ i. Finally, we denote by B i→ σ,q,q the sum of weights of the runs from configuration (u, σ, q, i, ε) to (u, σ, q , |u|, ε) with intermediary configurations of the form (u, σ, r, j, π) with π = ε or j ≥ i.

Apparently, it seems that we will compute twice as many matrices, however we will gain in complexity by replacing the usual valuation σ by its restriction σ to the pebbles in Peb\{x k }. Indeed, with j = σ(x k ), we can compute the matrix B We let N (0) σ ,i = 0. Then, it is easy to verify that for 0 < i < |u|: The computation of the four types of matrices, for all valid positions i and all partial valuations σ , requires globally O(|u| p-1 × |u|) matrix operations. Hence, this improves the overall complexity as announced.

B 0 σ = N
Notice that if p ≤ 1 then any K-layered pebWA is strongly K-layered. In this case, we get an evaluation algorithm using O(|Q| 3 |u|) scalar operations. This is in particular the case for pebWA arising from weighted LTL formulas.

Discussion

To conclude, let us briefly mention some interesting topics that could be studied in the future. As already stated in Section 7, one should try to obtain a quadratic algorithm for the translation of pebWE to pebWA. Next, as in Section 8 for the evaluation problem, one should develop efficient algorithms for quantitative model-checking, emptiness, containment, etc.

We have no restriction over the syntax of expressions or automata. In particular, 2-way moves may give rise to unbounded loops which is why we considered continuous semirings. We believe that continuous semirings are suitable for most applications. But in case one needs to work without this hypothesis, it is possible to put restrictions on the syntax of expressions and automata in order to rule out unbounded loops and have a well-defined semantics in arbitrary semirings. For instance, one may restrict iterations to forward proper or backward proper expressions.

The correctness of our translations between pebWE and pebWA relies on the partial monoid structure of marked words, which does not use concatenation of words. We can also endow marked trees with such a partial monoid structure. Therefore, pebWE can be extended to trees with a semantics in the continuous semiring of series over marked trees. We obtain in this way a weighted extension of caterpillar expressions or Regular XPath. Similarly, one may define tree-walking pebWA. We believe that the translations presented in this paper also apply to pebWE over trees and tree-walking pebWA.

A more prospective problem is to replace the x!-construction of pebWE with a chop product E ; F which evaluates E on the current prefix and F on the current suffix. We can easily simulate this relativization mechanism using a pebble to mark the current position. The converse is an interesting problem which needs to be investigated: is it possible to simulate pebbles with chop products?

Proposition 1 .

 1 If S is a continuous semiring and (Z, •, Y ) is a partial monoid then the series S Z forms a continuous semiring (S Z , +, ×, 0, 1 Y ).

Fig. 3 .

 3 Fig. 3. Markov Chain obtained by synchronizing A2 with a word of length n

  A and D square matrices, we have [14] D = D * and A = (A + BD C) * . Following (3) we define Φ(M ) inductively. If |Q| = 1, i.e., when M ∈ pebWE, then we simply let Φ(M ) = M * . From the compositionality of the semantics of pebWE (1), we obtain [[Φ(M )]] = [[M ]] * . Next, if |Q| > 1 we consider the block decomposition M = E F G H with H of size 1. Then, we let

  with H = H * and E = Φ(E + F H G). We apply[START_REF] Berstel | Noncommutative rational series with applications[END_REF] with K = S Mk(A + ) , N = [[M ]] and the block decomposition with D of size 1. Hence, we have[[E]] = A, [[F ]] = B, [[G]] = C and [[H]] = D.From the compositionality of the semantics of pebWE (1), we obtain [[H ]] = [[H]] * = D * = D . By induction we get [[E ]] = [[Φ(E + F H G)]] = [[E + F H G]] * . Using again the compositionality (1), we get [[E ]] = [[E +F H G]] * = A , as well as [[E F H ]] = A BD and [[H GE ]] = D CA . From (3-4) we deduce [[Φ(M )]] = [[M ]] * .

σ.

  by splitting the word u into three parts: positions appearing before j, position j and positions appearing after j. Hence, for 0< j = σ(x k ) < |u|, we can compute B (k) σ with (notice that σ [x k → j] = σ) B (k) σ = B →j-1This formula can easily be adapted when j = 0. It remains to compute the matrices B →i σ and B i σ for 0 ≤ i < |u|, and the matrices B i σ and B i→ σ for 0 < i ≤ |u|. First, if k > 0 then pebble x k ∈ Peb may be dropped on position 0 ≤ i < |u| (with i = σ(x k )) resulting in the nested computation ofN (k) σ ,i = M ↓ x k ,(k) σ ,i × B (k-1) σ [x k →i] × M ↑,(k) .

With α = 1-s s , one can show that [[E]](u, 0, |u|) = 1 1+α+...+α |u| .

This function cannot be computed without pebble by a classical 1-way weighted expression. We can see this using Schützenberger's theorem since weighted automata only compute values in 2O(|u|) .

We may also define the semantics [[E]]V of an expression E using valuations over a subset V ⊆ Peb, provided it contains the free pebbles of E.

for all x, y, z ∈ Z, (x • y) • z is defined iff x • (y • z) is defined, and in this case (x • y) • z = x • (y • z)

The rational closure is the closure under sum (+) concatenation (•) and star ( * ).

Acknowledgements The authors would like to thank Benedikt Bollig and Jacques Sakarovitch for helpful discussions.

write the corresponding block decomposition of the transition matrix of A as

where M is the transition matrix of A, D is the drop matrix with only non-zero entry being D ι ,ι = ↓ x , and L is the lift matrix with non-zero entries in the column U ?↑. By (3), the upper-left block of

where G = C(D, M, L) (see Lemma 9). Let Q be the set of non-initial states of A. We have,

We conclude using

and x!(c + F ) ≡ x!F when c ∈ S Test and F ∈ pebWE since we only consider nonempty words and the x!-construct requires to read the whole word.

Evaluation of pebble weighted automata

In this section, we study the evaluation problem of a K-layered pebWA A with reusable pebbles: given a word u and a valuation σ : Peb → pos(u), compute [[A]](u, σ). The challenge is important since, even if the word is fixed, the number of accepting runs may be infinite. We will prove in particular that the complexity of the evaluation problem is only linear in the size of the input word when the number p of reusable pebbles is at most 1.

The computations are done with matrix operations sum, product and star. But it is important to know the cost in scalar operations. This is well-known for sum and product of matrices. We show below that computing the star of a square matrix has the same complexity as computing the product of matrices. Indeed, we can improve the cubic complexity of product and star by using a better algorithm for computing the product of matrices. Lemma 13. Let K be a continuous semiring and N ∈ K n×n be a square matrix of dimension n. We can compute N * with O(n) scalar star operations and O(n 3 ) scalar sum and product operations.

Proof. We use (3) with a block decomposition of N such that D is a scalar, i.e., a block of size 1. Assuming that A is already computed, (3) allows to compute N * with one scalar star operation and a quadratic number of scalar sum and product operations. The result follows by induction.

Before explaining, how to evaluate efficiently pebWA, let us recall how this can be done for classical finite-state automata. In case of a deterministic finitestate automaton, we can easily check whether a word u is accepted by following