Stéphane Demri

Diego Figueira

M Praveen

Reasoning about Data Repetitions with Counter Systems

We study linear-time temporal logics interpreted over data words with multiple attributes. We restrict the atomic formulas to equalities of attribute values in successive positions and to repetitions of attribute values in the future or past. We demonstrate correspondences between satisfiability problems for logics and reachability-like decision problems for counter systems. We show that allowing/disallowing atomic formulas expressing repetitions of values in the past corresponds to the reachability/coverability problem in Petri nets. This gives us 2EXPSPACE upper bounds for several satisfiability problems. We prove matching lower bounds by reduction from a reachability problem for a newly introduced class of counter systems. This new class is a succinct version of vector addition systems with states in which counters are accessed via pointers, a potentially useful feature in other contexts. We strengthen further the correspondences between data logics and counter systems by characterizing the complexity of fragments, extensions and variants of the logic. For instance, we precisely characterize the relationship between the number of attributes allowed in the logic and the number of counters needed in the counter system.

I. INTRODUCTION

Words with multiple data: Finite data words [START_REF] Bouyer | A logical characterization of data languages[END_REF] are ubiquitous structures that include timed words, runs of counter automata or runs of concurrent programs with an unbounded number of processes. These are finite words in which every position carries a label from a finite alphabet and a data value from some infinite alphabet. More generally, structures over an infinite alphabet provide an adequate abstraction for objects from several domains: for example, infinite runs of counter automata can be viewed as infinite data words, finite data trees model XML documents with attribute values [START_REF] Figueira | Reasoning on words and trees with data[END_REF] and so on. A wealth of specification formalisms for data words (or slight variants) has been introduced stemming from automata, see e.g. [START_REF] Neven | Finite state machines for strings over infinite alphabets[END_REF], [START_REF] Segoufin | Automata and logics for words and trees over an infinite alphabet[END_REF], to adequate logical languages such as firstorder logic [START_REF] Bojańczyk | Two-variable logic on data words[END_REF], [START_REF] David | Analyse de XML avec données non-bornées[END_REF] or temporal logics [START_REF] Lisitsa | Temporal logic with predicate λ-abstraction[END_REF], [START_REF] Kupferman | Memoryful Branching-Time Logic[END_REF], [START_REF] Figueira | Reasoning on words and trees with data[END_REF], [START_REF] Kara | Temporal logics on words with multiple data values[END_REF], [START_REF] Figueira | A decidable two-way logic on data words[END_REF] (see also a related formalism in [START_REF] Fitting | Modal logic between propositional and first-order[END_REF]). Depending on the type of structures, other formalisms have been considered such as XPath [START_REF] Figueira | Reasoning on words and trees with data[END_REF] or monadic second-order logic [START_REF] Bollig | Model checking languages of data words[END_REF]. In full generality, most formalisms lead to undecidable decision problems and a well-known research trend consists of finding a good trade-off between expressiveness and decidability. Restrictions to regain decidability are protean: bounding the models (from trees to words for instance), restricting the number of variables, see e.g. [START_REF] Bojańczyk | Two-variable logic on data words[END_REF], limiting the set of the temporal operators or the use Work supported by project REACHARD ANR-11-BS02-001, and FET-Open Project FoX, grant agreement 233599. M. Praveen was supported by the ERCIM "Alain Bensoussan" Fellowship Programme.

of the data manipulating operator, see e.g. [START_REF] Figueira | Future-looking logics on data words and trees[END_REF], [START_REF] Demri | Temporal logics of repeating values[END_REF]. Moreover, interesting and surprising results have been exhibited about relationships between logics for data words and counter automata [START_REF] Bojańczyk | Two-variable logic on data words[END_REF], [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF], [START_REF] Bojańczyk | An extension of data automata that captures XPath[END_REF], leading to a first classification of automata on data words [START_REF] Bojańczyk | An extension of data automata that captures XPath[END_REF]. This is why logics for data words are not only interesting for their own sake but also for their deep relationships with data automata or with counter automata. Herein, we pursue further this line of work and we work with words in which every position contains a vector of data values.

Motivations: In [START_REF] Demri | Temporal logics of repeating values[END_REF], a decidable logic interpreted over (finite or infinite) sequences of variable valuations (understood as words with multiple data) is introduced in which the atomic formulae are of the form either x ≈ X i y or x ≈ ? y. The formula x ≈ X i y states that the current value of variable x is the same as the value of y i steps ahead (local constraint) whereas x ≈ ? y states that the current value of x is repeated in a future value of y (future obligation). Such atomic properties can be naturally expressed with a freeze operator that stores a data value for later comparison, and in [START_REF] Demri | Temporal logics of repeating values[END_REF], it is shown that the satisfiability problem is decidable with the temporal operators in {X, X -1 , U, S}. The freeze operator allows to store a data value in a register and then to test later equality between the value in the register and a data value at some other position. This is a powerful mechanism but the logic in [START_REF] Demri | Temporal logics of repeating values[END_REF] uses it in a limited way: only repetitions of data values can be expressed and it restricts very naturally the use of the freeze operator. The decidability result is robust since, for instance, it holds with the addition of atomic formulas of the form x ≈ ? -1 y stating that the current value of x is repeated in a past value of y (past obligation). Decidability can be shown either by reduction into FO 2 (∼, <, +ω), a first-order logic over data words introduced in [START_REF] Bojańczyk | Two-variable logic on data words[END_REF] or by reduction into the verification of fairness properties in Petri nets, shown decidable in [START_REF] Jančar | Undecidability of bisimilarity for Petri Nets and some related problems[END_REF]. In both cases, an essential use of the decidability of the reachability problem for Petri nets is made, for which no primitive recursive algorithm is known, see e.g. [START_REF] Leroux | Vector addition system reachability problem: a short selfcontained proof[END_REF]. Hence, even though the logics shown decidable in [START_REF] Demri | Temporal logics of repeating values[END_REF] poorly use the freeze operator (the only properties about data are related to controlled repetitions), the complexity of their satisfiability problems is unknown. Moreover, it is unclear whether the reductions into the reachability problem for Petri nets are really needed; this would be the case if reductions in the other direction exist. Note that in [START_REF] Kara | Temporal logics on words with multiple data values[END_REF], a richer logic has been introduced and it has been shown that satisfiability is equivalent to the reachability problem for Petri nets.

Our main motivation is to investigate logics that express repetitions of values, revealing the correspondence between expressivity of the logic and reachability problems for counter machines, including well-known problems for Petri nets. This work can be seen as a study of the precision with which counting needs to be done as a consequence of having a mechanism for demanding "the current data value is repeated in the future/past" in a logic. Hence, this is not the study of yet another logic, but of a natural feature shared by most studied logics on data words [START_REF] Demri | Temporal logics of repeating values[END_REF], [START_REF] Bojańczyk | Two-variable logic on data words[END_REF], [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF], [START_REF] Figueira | Future-looking logics on data words and trees[END_REF], [START_REF] Kara | Temporal logics on words with multiple data values[END_REF], [START_REF] Figueira | Reasoning on words and trees with data[END_REF], [START_REF] Figueira | A decidable two-way logic on data words[END_REF]: the property of demanding that a data value be repeated. We consider different ways in which one can demand the repetition of a value, and study the repercussion in terms of the "precision" with which we need to count in order to solve the satisfiability problem. Our measurement of precision here distinguishes the reachability versus the coverability problem for Petri nets and the number of counters needed as a function of the number of variables used in the logic.

Our contribution: We introduce the logic LRV ("Logic of Repeating Values") interpreted over finite words with multiple data, equipped with atomic formulas of the form either x ≈ X i y or x ≈ φ? y [resp. x ≈ φ? y], where x ≈ φ? y [resp.

x ≈ φ? y] states that the current value of x is repeated [resp. is not repeated] in some future value of y in a position where φ holds true. When we impose φ = , the logic introduced in [START_REF] Demri | Temporal logics of repeating values[END_REF] is obtained and it is denoted by LRV . The syntax for future obligations is freely inspired from PDL with its test operator '?'. Even though LRV contains the past-time temporal operators X -1 and S, it has no past obligations. We write PLRV to denote the extension of LRV with past obligations of the form x ≈ φ? -1 y or x ≈ φ? -1 y. Below, we illustrate how LRV and variants are compared to existing data logics. BD-LTL [START_REF] Kara | Temporal logics on words with multiple data values[END_REF] (≡ Reach(VASS))

LTL ↓ 1 (X, X -1 , U, S) [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] (undec.)

PLRV LRV PLRV = CLTL XF,XF -1 [START_REF] Demri | Temporal logics of repeating values[END_REF] LRV = CLTL XF [START_REF] Demri | Temporal logics of repeating values[END_REF] (1 attribute)

Our main results are listed below. 1. We begin where [START_REF] Demri | Temporal logics of repeating values[END_REF] stopped: the reachability problem for Petri nets is reduced to the satisfiability problem of PLRV (i.e., the logic with past obligations). 2. Without past obligations, the satisfiability problem is much easier: we reduce the satisfiability problem of LRV and LRV to the control-state reachability problem for VASS, via a detour to a reachability problem on gainy VASS. But the number of counters in the VASS is exponential in the number of variables used in the formula. This gives us a 2EXPSPACE upper bound. 3. The exponential blow up mentioned above is unavoidable: we show a polynomial-time reduction in the converse direction, starting from a linear sized counter machine (without zero tests) that can access exponentially many counters.

This gives us a matching 2EXPSPACE lower bound. 4. Several augmentations to the logic do not alter the complexity: we show that complexity is preserved when MSOdefinable temporal operators are added or when infinite words with multiple data are considered. 5. The power of nested testing formulas: we show that the complexity of the satisfiability problem for LRV reduces to PSPACE-complete when the number of variables in the logic is bounded by a constant, while the complexity of the satisfiability of LRV does not reduce even when only one variable is allowed. Recall that the difference between LRV and LRV is that the later allows any φ in x ≈ φ? y while the former restricts φ to just . 6. The power of pairs of repeating values: we show that the satisfiability problem of LRV augmented with x, y ≈ ? x , y (repetitions of pairs of data values) is undecidable, even when x, y ≈ ? -1 x , y is not allowed (i.e., even when past obligations are not allowed). 7. Implications for classical logics: we show a 3EXPSPACE upper bound for the satisfiability problem for forward-EMSO 2 (+1, <, ∼) over data words, using results on LRV. For proving the result mentioned in point 3 above, we introduce a new class of counter machines that we call chain systems and show a key hardness result for them. This class is interesting for its own sake and could be used in situations where the power of binary encoding needs to be used. We prove the (k + 1)EXPSPACE-completeness of the control state reachability problem for chain systems of level k (we only use k = 1 in this paper but the proof for arbitrary k is no more complex than the proof for the particular case of k = 1). In chain systems, the number of counters is equal to an exponential tower of height k but we cannot access the counters directly in the transitions. Instead, we have a pointer that we can move along a chain of counters. The (k + 1)EXPSPACE lower bound is obtained by a non-trivial extension of the EXPSPACE-hardness result from [START_REF] Lipton | The reachability problem requires exponential space[END_REF], [START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF]. Then we show that the control state reachability problem for the class of chain systems with k = 1 can be reduced to the satisfiability problem for LRV (see Section V). It was known that data logics are strongly related to classes of counter automata, see e.g. [START_REF] Bojańczyk | Two-variable logic on data words[END_REF], [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF], [START_REF] Bojańczyk | An extension of data automata that captures XPath[END_REF] but herein, we show how varying the expressive power of logics leads to correspondence with different reachability problems for counter machines.

II. PRELIMINARIES

We write N [resp. Z] to denote the set of non-negative integers [resp. integers] and [i, j] to denote {k ∈ Z : i ≤ k and k ≤ j}. For v ∈ Z n , v(i) denotes the i th element of v for every i ∈ [1, n]. We write v v whenever for every i ∈ [1, n], we have v(i) ≤ v (i). For a (possibly infinite) alphabet Σ, Σ * represents the set of finite words over Σ, Σ + the set of finite non-empty words over Σ. For a finite word or sequence u = a 1 . . . a k over Σ, we write |u| to denote its length k. For 0 ≤ i < |u|, u(i) represents the (i + 1)-th letter of the word, here a i+1 .

Logics of Repeating Values: Let VAR = {x 1 , x 2 , . . .} be a countably infinite set of variables. We denote by LRV the logic whose formulas are defined as follows, where x, y ∈ VAR, i ∈ N.

φ ::= x ≈ X i y | x ≈ φ? y | x ≈ φ? y | φ ∧ φ | ¬φ | Xφ | φUφ | X -1 φ | φSφ
A valuation is a map from VAR to N, and a model is a finite non-empty sequence σ of valuations. For every model σ and 0 ≤ i < |σ|, the satisfaction relation |= is defined:

• σ, i |= x ≈ X j y iff i + j < |σ| and σ(i)(x) = σ(i + j)(y),

• σ, i |= x ≈ φ? y iff there exists j such that i < j < |σ|, σ(i)(x) = σ(j)(y) and σ, j |= φ. The semantics x ≈ φ? y is defined similarly but asking for a different data value. The temporal operators next (X), previous (X -1 ), until (U) and since (S) and Boolean connectives are defined in the usual way. We also use the standard derived temporal operators (G, F, F -1 , . . . ) and constants , ⊥. We write σ |= φ if σ, 0 |= φ. Given a set of temporal operators O, we write LRV(O) to denote the fragment of LRV restricted to formulas with operators from O. The satisfiability problem for LRV (written SAT(LRV)) is to check for an LRV formula φ, whether there is σ such that σ |= φ. Let PLRV be the extension of LRV with additional atomic formulas of the form x ≈ φ? -1 y and x ≈ φ? -1 y. The satisfaction relation is extended as expected: σ, i |= x ≈ φ? -1 y iff there is 0 ≤ j < i such that σ(i)(x) = σ(j)(y) and σ, j |= φ, and similarly for x ≈ φ? -1 y. We write LRV [resp. PLRV ] to denote the fragment of LRV [resp. PLRV] in which atomic formulas are restricted to x ≈ X i y and x ≈ ? y [resp. to x ≈ X i y, x ≈ ? y and x ≈ ? -1 y]. In [START_REF] Demri | Temporal logics of repeating values[END_REF], LRV and PLRV were shown to be decidable by reduction into the reachability problem for Petri nets. However, the characterization of their complexity remained open.

Properties: In the table below, we justify our choices for atomic formulae by presenting several abbreviations (with their obvious semantics). By contrast, we include in LRV both x ≈ φ? y and x ≈ φ? y when φ is an arbitrary formula since there is no obvious way to express one with the other.

Abbreviation Definition

x

≈ X i y ¬(x ≈ X i y) ∧ i times X • • • X x ≈ X -i y i times X -1 • • • X -1 (X i x ≈ y) x ≈ X -i y ¬(x ≈ X -i y) ∧ i times X -1 • • • X -1 x ≈ ? y (x ≈ Xy) ∨ X((y ≈ Xy)U(y ≈ Xy)) x ≈ ? -1 y (x ≈ X -1 y) ∨ X -1 ((y ≈ X -1 y)S(y ≈ X -1 y))
Models for LRV can be viewed as finite data words in (Σ × D) * , where Σ is a finite alphabet and D is an infinite domain. E.g., equalities between dedicated variables can simulate that a position is labelled by a letter from Σ; moreover, we may assume that the data values are encoded with the variable x. Let us express that whenever there are i < j s.t. i and j [resp. i + 1 and j + 1, i + 2 and j + 2] are labelled by a [resp. a , a ], σ(i + 1)(x) = σ(j + 1)(x). This can be stated in LRV by: G(a ∧ X(a ∧ Xa ) ⇒ X¬(x ≈ X -1 a ∧ a ∧ Xa ? x)). This is an example of key constraints, see e.g. [START_REF] Niewerth | Two-variable logic and key constraints on data words[END_REF]Definition 2.1] and the paper contains also numerous examples of properties that can be captured by LRV.

Basics on VASS: A vector addition system with states

(VASS) is a tuple A = Q, C, δ where Q is a finite set of control states, C is a finite set of counters and δ is a finite set of transitions in Q × Z C × Q. A configuration of A is a pair q, v ∈ Q × N C . We write q, v - → q , v if there is (q, u, q ) ∈ δ such that v = v + u.
The reachability problem for VASS (written Reach(VASS)) consists in checking whether q 0 , v 0 * -→ q f , v f , given two configurations q 0 , v 0 and q f , v f . The reachability problem for VASS is decidable with non-primitive recursive complexity algorithms [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF], [START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF], [START_REF] Leroux | Vector addition system reachability problem: a short selfcontained proof[END_REF], but the best known lower bound is only EXPSPACE [START_REF] Lipton | The reachability problem requires exponential space[END_REF], [START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF]. The control state reachability problem is the following EXPSPACE-complete problem [START_REF] Lipton | The reachability problem requires exponential space[END_REF], [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]: given a configuration q 0 , v 0 and a control state q f , check whether q 0 , v 0 * -→ q f , v for some v ∈ N C . We also use two other kinds of computations: with gains (-→ gainy ) or losses (-→ lossy ). We write q, v -→ gainy q , v [resp. q, v -→ lossy q , v ] if there is a transition (q, u, q ) ∈ δ and w ∈ N C such that v w and w + u v [resp. w v and v w + u].

III. THE POWER OF PAST: FROM REACH(VASS) TO SAT(PLRV)

While [START_REF] Demri | Temporal logics of repeating values[END_REF] concentrated on decidability results, here we begin with a hardness result. When past obligations are allowed as in PLRV, SAT(PLRV) is equivalent to the very difficult problem of reachability in VASS. Combined with the result of the next section where we prove that removing past obligations leads to a reduction into the control state reachability problem for VASS, this means that reasoning with past obligations is much more complicated.

Theorem 1. There is a polynomial-space reduction from Reach(VASS) into SAT(PLRV).

The proof of Theorem 1 is analogous to the proof of [START_REF] Bojańczyk | Two-variable logic on data words[END_REF]Theorem 16] except that properties are expressed in PLRV instead of being expressed in FO 2 (∼, <, +1). In Section IV-A, we show how to eliminate test formulas φ from x ≈ φ? y and x ≈ φ? -1 y. Combining this with the decidability proof for PLRV satisfiability from [START_REF] Demri | Temporal logics of repeating values[END_REF], we get that SAT(PLRV) [resp. for SAT(PLRV )] is equivalent to Reach(VASS) modulo polynomial-space reductions.

IV. LEAVING THE PAST BEHIND SIMPLIFIES THINGS: FROM SAT(LRV) TO CONTROL STATE REACHABILITY

In this section, we show the reduction from SAT(LRV) to the control state reachability problem in VASS. We obtain a 2EXPSPACE upper bound for SAT(LRV) as a consequence. This is done in two steps: [START_REF] Bojańczyk | Two-variable logic on data words[END_REF] simplifying formulas of the form x ≈ φ? y to remove the test formula φ (i.e., a reduction from SAT(LRV) into SAT(LRV )); and (2) reducing from SAT(LRV ) into the control state reachability pb. in VASS.

A. Elimination of Test Formulas

We give a polynomial-time algorithm that for every ϕ ∈ LRV computes a formula ϕ ∈ LRV that preserves satisfiability: there is a model σ s.t. σ |= ϕ iff there is a model σ s.t. σ |= ϕ . We give the reduction in two steps. First, we eliminate formulas with inequality tests of the form x ≈ ϕ? y using only positive tests of the form x ≈ ϕ? y. We then eliminate formulas of the form x ≈ ϕ? y, using only formulas of the form x ≈ ? y. Let LRV ≈ be the logic LRV where there are no appearances of formulas of the form x ≈ ϕ? y; and let PLRV ≈ be PLRV without x ≈ ϕ? y or x ≈ ϕ? -1 y.

Proposition 2 (from LRV to LRV ≈ ). There is a polynomialtime reduction from SAT(LRV) into SAT(LRV ≈ ); and from SAT(PLRV) into SAT(PLRV ≈ ).

Proof sketch: For every ϕ ∈ LRV, we compute ϕ ∈ LRV ≈ in polynomial time, which preserves satisfiability. Besides all the variables from ϕ, ϕ uses a distinguished variable k (which will have a constant value, different from all the values of the variables of ϕ) and variables v ≈ y,ψ , v x ≈ ψ? y for every subformula ψ of ϕ and variables x, y of ϕ.

Each subformula x ≈ ψ? y is replaced by x ≈ v x ≈ ψ? y ∧ v x ≈ ψ? y ≈ ψ? y, where v x ≈ ψ? y is a fresh variable. On the other hand, for each subformula ¬(x ≈ ψ? y), we use the variable v ≈ y,ψ in conjunction with k as shown below.

k v ≈ y,ψ x ≈ k v ≈ y,ψ x ≈ |= ¬(x ≈ ψ? y) k v ≈ y,ψ |= ¬ψ ≈ ≈ y v ≈ y,ψ |= ψ ≈ y v ≈ y,ψ |= ¬ψ ≈ y v ≈ y,ψ |= ψ

≈

In the beginning, v ≈ y,ψ ≈ k, which is broken at the first position where all future positions where ψ holds have the same value for y. At this position (say i + 1), v ≈ y,ψ ≈ k and v ≈ y,ψ maintains the same value (say n) at all future positions, illustrated as a dashed box above. In all positions after i that satisfy ψ, y ≈ v ≈ y,ψ . These conditions can be enforced without using ¬(x ≈ ψ? y). Suppose x also has value n at position i as shown above. Now in any position after i that satisfies ψ, y has the value n, which is the value of x in position i. This is exactly the semantics of ¬(x ≈ ψ? y). Hence, ¬(x ≈ ψ? y) can be replaced by ¬XFψ ∨ x ≈ Xv ≈ y,ψ . Past obligations are treated in a symmetrical way.

Proposition 3 (from LRV ≈ to LRV ). There is a polynomialtime reduction from SAT(LRV ≈ ) into SAT(LRV ); and from SAT(PLRV ≈ ) into SAT(PLRV ).

Proof sketch: For every ϕ ∈ LRV ≈ , we compute in polynomial time ϕ ∈ LRV that preserves satisfiability. Besides all the variables from ϕ, ϕ uses a new distinguished variable k, and a variable v y,ψ for every subformula ψ of ϕ and every variable y of ϕ. We enforce k to have a constant value different from all values of variables of ϕ. At every

k v ≈ y,ψ x ≈ ≈ k v ≈ y,ψ x ≈ ≈ k v ≈ y,ψ x ≈ ≈ |= ¬(x ≈ ψ?y) y v ≈ y,ψ ψ ≈ y v ≈ y,ψ ¬ψ y v ≈ y,ψ ψ ≈ k ψ k ≈ ≈ v y,ψ v y,ψ y y k v ≈ y,ψ x ≈ ≈ k v ≈ y,ψ x ≈ ≈ k v ≈ y,ψ x ≈ ≈ |= ¬(x ≈ ψ?y) y v ≈ y,ψ ψ ≈ y v ≈ y,ψ ¬ψ y v ≈ y,ψ ψ ≈ k ψ k ≈ ≈ v y,ψ v y,ψ
y y position, we enforce ψ to hold if v y,ψ ≈ y, and ψ not to hold if v y,ψ ≈ k as shown above. Then x ≈ ψ? y is replaced by x ≈ ? v y,ψ .

Corollary 4. There is a polynomial-time reduction from SAT(LRV) into SAT(LRV ).

Since SAT(PLRV ) is decidable [START_REF] Demri | Temporal logics of repeating values[END_REF], we obtain the decidability of SAT(PLRV).

Corollary 5. SAT(PLRV) is decidable.

B. From LRV Satisfiability to Control State Reachability

In [START_REF] Demri | Temporal logics of repeating values[END_REF], SAT(LRV ) is reduced to the reachability problem for a subclass of VASS. Herein, this is refined by introducing incremental errors in order to improve the complexity.

In [START_REF] Demri | Temporal logics of repeating values[END_REF], the standard concept of atoms from the Vardi-Wolper construction of automaton for LTL is used. Refer to the diagram at the top of Figure 1. The formula x ≈ ? y in the left atom creates an obligation for the current value of to appear some time in the future in y. This obligation cannot be satisfied in the second atom, since y has to satisfy some other constraint there (y ≈ z). To remember this unsatisfied obligation about y while taking the transition from the first atom to the second, the counter X {y} is incremented. The counter can be decremented later in transitions that allow the repetition in y. If several transitions allow such a repetition, only one of them needs to decrement the counter (since there was only one obligation at the beginning). The other transitions which should not decrement the counter can take the alternative labelled "no change" in the right part of Figure 1.

x x ≈ Xz x ≈ ? y y ≈ z X ++ {y} X -- {y} no change X -- {y} no change x ≈ Xz x ≈ ? y y ≈ z X ++ {y} X -- {y} + ∆ X -- {y} + ∆
The idea here is to replace the combination of the decrementing transition and the "no change" transition in the top of Figure 1 with a single transition with incremental errors as shown in the bottom. After Lemma 6 below that formalises ideas from [6, Section 7], we prove that the transition with incremental errors is sufficient. Lemma 6 ([6]). For a LRV formula φ that uses the variables {x 1 , . . . , x k }, a VASS A φ = Q, C, δ can be defined, along with sets Q 0 , Q f ⊆ Q of initial and final states resp., s.t.

• the set of counters C consists of all nonempty subsets of {x 1 , . . . ,

x k }. • For all q, q ∈ Q, either {u | (q, u, q ) ∈ δ} = [n 1 , m 1 ] × • • • × [n |C| , m |C| ] for some n 1 , m 1 , . . . , n |C| , m |C| ∈ [-k, k], or {u | (q, u, q ) ∈ δ} = ∅. (We call this property closure under component-wise interpolation.) • If δ ∩({q}×[-k, k] C ×{q })
is not empty, then for every X ∈ C there is (q, u, q ) ∈ δ so that u(X) ≥ 0. (We call this property optional decrement.)

• Let 0 be the counter valuation that assigns 0 to all counters. Then φ is satisfiable iff q 0 , 0 * -→ q f , 0 for some q 0 ∈ Q 0 and q f ∈ Q f . At the top of Figure 1, only one counter X {y} is shown and is decremented by 1 for simplicity. In general, multiple counters can be changed and they can be incremented/decremented by any number up to k, depending on the initial and target atoms of the transition. If a counter can be incremented by k 1 and can be decremented by k 2 , then there will also be transitions between the same pair of atoms allowing changes of k 1 -1, . . . , 1, 0, -1, . . . -(k 2 -1). This corresponds to the closure under component-wise interpolation mentioned in the lemma above. The optional decrement property corresponds to the fact that there will always be a "no change" transition that does not decrement any counter. Now, we show that a single transition that decrements all counters by the maximal possible number can simulate the set of all transitions between two atoms, using incremental errors.

Let A inc = Q, C, δ min and Q 0 , Q f ⊆ Q, where Q, Q 0 , Q f
and C are same as those of A φ and δ min is defined as follows: (q, minup q,q , q ) ∈ δ min iff δ ∩ ({q} × [-k, k] C × {q }) is not empty and minup q,q (X) = min u:(q,u,q )∈δ {u(X)} for all X ∈ C.

Lemma 7. If q, v - → q , v in A φ , then q, v - → gainy q , v in A inc .
Proof sketch: If A φ takes one of the transitions in the top of Figure 1, A inc takes the corresponding transition at the bottom, adjusting the incremental error ∆ accordingly.

Lemma 8. If q 1 , v 1 * - → gainy q 2 , 0 in A inc and v 1 v 1 , then q 1 , v 1 * - → q 2 , 0 in A φ .
Proof sketch: If A inc takes a transition at the bottom of Figure 1, A φ takes the corresponding decrementing transition at the top, ignoring any incremental errors. This may result in A φ reaching 0 earlier in the run, in which case "no change" transitions are used in the rest of the run.

Theorem 9. SAT(LRV ) is in 2EXPSPACE.

Proof sketch: The proof is in four steps (standard arguments are used for 3. and 4.).

1 From [START_REF] Demri | Temporal logics of repeating values[END_REF], a LRV formula φ is satisfiable iff q 0 , 0 * -→ q f , 0 in A φ for some q 0 ∈ Q 0 and q f ∈ Q f . 2 This is the step that requires new insight. From Lemmas 7 and 8, q 0 , 0

* - → q f , 0 in A φ iff q 0 , 0 * - → gainy q f , 0 in A inc .
3 Let A dec be the VASS obtained from A inc by "reversing" each transition. By replacing each gainy transition of A inc by the reverse lossy transtion of A dec , we infer that

q 0 , 0 * - → gainy q f , 0 in A inc iff q f , 0 * - → lossy q 0 , 0 in A dec . 4 q f , 0 * - → lossy q 0 , 0 iff q f , 0 * - → q 0 , v for some v.
Checking the latter condition is precisely the control state reachability problem for VASS.

The number of control states and counters in A φ and in A dec is exponential in |φ| (size of φ). Each control state and transition function of A dec can be represented in space polynomial in |φ|. Given a control state, testing if it is an initial or a final state can be done in linear time in the size of the state. The automaton A dec can be constructed in exponential time in |φ|. Hence, the EXPSPACE upper bound for the control state reachability problem in VASS [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF] gives the 2EXPSPACE upper bound for SAT(LRV ).

Corollary 10. SAT(LRV) is in 2EXPSPACE.

V. SIMULATING EXPONENTIALLY MANY COUNTERS

In Section IV, the reduction from SAT(LRV) to control state reachability involves an exponential blow up, since we use one counter for each subset of variables. The question of whether this can be avoided depends on whether LRV is powerful enough to reason about subsets of variables or whether there is a smarter reduction without a blow-up. Similar questions are open in other related areas [START_REF] Manuel | Counting multiplicity over infinite alphabets[END_REF].

Here we prove that LRV is indeed powerful enough to reason about subsets of variables. We establish a 2EXPSPACE lower bound, which leverages the power of LRV to access exponentially many counters through binary encoding. Consider the variables and their values shown in the table below. The conditions in the third row are about the equality of variable values in a single position.

≈ z x 2 ≈ z x 3 ≈ z inc ≈ z dec ≈ z Encodes 1 0 1 decrement
The combination of all the conditions can be thought of as encoding "decrement 101 th counter", considering 101 as the binary encoding of 5, where the i-th bit is 1 if x i ≈ z. A total of 8 counters can be manipulated with x 1 , x 2 and x 3 . Using the power of LRV to reason about values that repeat in the future, we can encode the condition "for every counter, an increment is followed by a decrement in the future", which then ensures control state reachability.

The rest of this section is divided into three parts. The first part defines chain systems, which are like VASS where transition rules like "increment counter X" are replaced by "increment 101 th counter". The second part shows lower bounds for the control state reachability problem for chain systems. The third part shows that LRV can reason about chain systems of level 1.

A. Chain Systems

We introduce a new class of counter systems that is instrumental to show that SAT(LRV ) is 2EXPSPACE-hard. This is an intermediate formalism between counter automata with zero-tests with counters bounded by triple exponential values (having 2EXPSPACE-hard control state reachability problem) and properties expressed in LRV . Systems with chained counters have no zero-tests and the only updates are increments and decrements. However, the systems are equipped with a finite family of counters, each family having an exponential number of counters. Let exp(0, n)

def = n and exp(k + 1, n) def = 2 exp(k,n) for every k ≥ 0.
Definition 11. A counter system with chained counters (herein called a chain system) is a tuple

A = Q, f, k, Q 0 , Q F , δ
where (1) f : [1, n] → N where n ≥ 1 is the number of chains and exp(k, f (α)) is the number of counters for the chain α where k ≥ 0, (2) Q is a non-empty finite set of states, (3) Q 0 ⊆ Q is the set of initial states and Q F ⊆ Q is the set of final states, (4) δ is the set of transitions in Q × I × Q where I = {inc(α), dec(α), next(α), prev(α), first(α)?, first(α)?, last(α)?, last(α)? : α ∈ [1, n]}.

The system A = Q, f, k, Q 0 , Q F , δ is said to be at level k. In order to encode the natural numbers from f and the value k, we use a unary representation. We say that a transition containing inc(α) is α-incrementing, and a transition containing dec(α) is α-decrementing. The idea is that for each chain α ∈ [1, n], we have exp(k, f (α)) counters, but we cannot access them directly in the transitions like we do in VASS. Instead, we have a pointer to a counter that we can move. We can ask if we are pointing to the first counter (first(α)?) or not (first(α)?), or the last counter (last(α)?) or not (last(α)?), and we can change the pointer to the next (next(α)) or previous (prev(α)) counter.

A run is a finite sequence ρ in δ * such that 1) for every two ρ(i) = q instr --→ r and ρ(i + 1) = q instr --→ r we have r = q , 2) for every chain α ∈ [1, n], for every i ∈ [1, |ρ|], we have

0 ≤ c α i < exp(k, f (α))
where

c α i = card({i < i | ρ(i ) = q next(α) ----→ r}) - card({i < i | ρ(i ) = q prev(α) ----→ r}), (1)
3) for every i ∈ [1, |ρ|] and for every chain α ∈ [1, n],

(a) if ρ(i) = q first(α)? ----→ q , then c α i = 0; (b) if ρ(i) = q first(α)? ----→ q , then c α i = 0; (c) if ρ(i) = q last(α)? ----→ q , then c α i = exp(k, f (α)) -1; (d) if ρ(i) = q last(α)? ----→ q , then c α i = exp(k, f (α)) -1.
A run is accepting whenever ρ(1) starts with an initial state from Q 0 and ρ(|ρ|) ends with a final state from Q F . A run is perfect iff for every α ∈ [1, n], there is some injective function

γ : {i | ρ(i) is α-decrementing} → {i | ρ(i) is α-incrementing}
such that for every γ(i) = j we have that j < i and c α i = c α j . A run is gainy and ends at zero iff for every chain α ∈ [1, n], there is some injective function

γ : {i | ρ(i) is α-incrementing} → {i | ρ(i) is α-decrementing}
such that for every γ(i) = j we have that j > i and c α i = c α j . In the sequel, we shall simply say that the run is gainy. Below, we define two problems for which we shall characterize the computational complexity. The proof of Lemma 13 consists of simulating perfect runs by the runs of a VASS in which the control states record the positions of the pointers in the chains.

B. Hardness Results for Chain Systems

We show that Per(k) is (k + 1)EXPSPACE-hard. The implication is that replacing direct access to counters by a pointer that can move along a chain of counters does not decrease the power of VASS, while providing access to more counters. To demonstrate this, we extend Lipton's EXPSPACE-hardness proof for the control state reachability problem in VASS [START_REF] Lipton | The reachability problem requires exponential space[END_REF] (see also its exposition in [START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF]). Since our pointers can be moved only one step at a time, this extension involves new insights into the control flow of algorithms used in Lipton's proof, allowing us to implement it even with the limitations imposed by step-wise pointer movements.

Lipton's proof starts from the standard result in computability theory that a Turing Machine using space 2 n γ can be simulated by a counter automaton equipped with 4 counters whose values are bounded by 2 2 n γ . Lipton's proof shows that such a counter automaton can be simulated with a VASS. Unlike counter automata, VASS does not have zero-test transitions. Each counter c of the automaton is complemented with an extra counter c in the VASS. The VASS is designed such that the sum of the values in c and c is 2 2 n γ in any reachable configuration. Now testing c for zero is equivalent to testing that c is 2 2 n γ . This later test is implemented in a VASS as explained next.

Figure 2 illustrates how a counter s i is decremented 2 2 i times. There are two nested loops indexed by y i-1 and z i-1 , initialised to 2 2 i-1 . When all the iterations are finished, we would have decremented s i exactly 2 2 i-1 × 2 2 i-1 = 2 2 i times. Testing y i-1 and z i-1 for zero is done by a similar gadget, where i, i -1 are replaced by i -1, i -2. The resulting VASS is composed of n γ constant sized VASS, each one implementing the nested loops for an i between 1 and n γ . The idea behind our (k + 1)EXPSPACE lower bound is to replace the VASS with a chain system and n γ with exp(k, n γ ). This will not work as it is, since a chain system composed of exp(k, n γ ) constant sized portions will not give a polynomialtime reduction. We reduce the size of the chain system by observing that the decrementing algorithm for i-1 is the same as the one for i, except that i, i-1 are replaced by i -1, i -2 respectively. We can write a single sequence of instructions for the decrementing algorithm and invoke it for any i by placing the pointers at the appropriate counters. Roughly speaking, exp(k, n γ ) copies of the code for large decrements is replaced by one copy of the code plus a chain of implicit length exp(k, n γ ) equipped with a pointer to refer to a specific copy.

y i-1 = z i-1 = 2 2 i-1 y -- i-1 , y i-1 ++ z -- i-1 , z i-1 ++ s -- i , s i ++ z i-1 = 0?
The main difficulty in the implementation is to ensure that the multiple invocations of the algorithm return to the correct point. Unlike Lipton's proof that uses VASS, we have to work with chain systems and this introduces some more constructions, the technical details of which are rather tedious. Theorem 14. Per(k) is (k + 1)EXPSPACE-hard.

C. Reasoning About Chain Systems with LRV Given a chain system A of level 1, we construct a formula in LRV that is satisfiable iff A has a gainy accepting run. Hence, we get a 2EXPSPACE lower bound for SAT(LRV). The main idea is to encode runs of chain systems with LRV formulas that access the counters using binary encoding, so that the formulas can handle exponentially many counters.

Lemma 15. There is a polynomial-time reduction from Gainy(1) into SAT(LRV(X, F)).

Proof sketch: Let

A = Q, f, 1, Q 0 , Q F , δ be a chain system of level 1 with f : [1, n] → N, having thus n chains of counters, of respective size 2 f (1) , . . . , 2 f (n) .
We encode a word ρ ∈ δ * that represents an accepting run. For this, we use the alphabet δ of transitions. We can simulate the labels δ = {t 1 , . . . , t m } with variables t 0 , . . . , t m , where a node has an encoding of the label t i iff the formula t i = t 0 ≈ t i holds true. We build an LRV formula ϕ so that there is an accepting gainy run ρ ∈ δ * of A if, and only if, there is a model σ so that σ |= ϕ and σ encodes ρ.

The counter-blind conditions to check are: (a) Every position satisfies t for some t ∈ δ; (b) the first position satisfies (q 0 , instr, q) for some q 0 ∈ Q 0 , instr ∈ I, q ∈ Q; (c) the last position satisfies (q, instr, q ) for some q ∈ Q, instr ∈ I, q ∈ Q F ; (d) no two consecutive positions i and i + 1 satisfy (q, u, q ) and (p, u , p ) respectively, with q = p. The difficulty is then in checking that the values of the counters encode indeed a correct gainy run.

We say that a position i is α-incrementing [resp. αdecrementing] if it satisfies (q, u, q ) for some q, q ∈ Q and u = inc(α) [resp. u = dec(α)]. We use a label (α, i) and variables x α inc , x α dec for every α ∈ [1, n] and i ∈ [1, f (α)]. We say that a position i operates on the α-counter c, if (α, j) holds (i.e., position i encodes the label (α, j)) for every position j of the representation of c in base 2 containing a '1', and ¬ (α, j) for every position j containing a '0'. Note that we can encode every value 0 ≤ c < 2 f (α) .

For every chain α, let us consider the following properties:

• Every two positions of σ have different values of x α inc [resp. of x α dec ]. • For every position i of σ operating on an α-counter c with an instruction 'first(α)?' [resp. 'first(α)?', 'last(α)?', 'last(α)?'] , we have

c = 0 [resp. c = 0, c = 2 f (α) -1, c = 2 f (α) -1].
• For every position i of σ operating on an α-counter c, if the position contains an instruction 'next(α)' [resp. 'prev(α)'], then the next position i + 1 operates on the α-counter c+1 [resp. c-1]; otherwise, the position i+1 operates on the α-counter c.

• For every α-incrementing position i of σ operating on an α-counter c there is a future α-decrementing position j > i on the same α-counter, so that σ(i)(x α inc ) = σ(j)(x α dec ). In fact, these properties together with (a)-(d) are sufficient and necessary to encode a gainy and accepting run of A, and they can be all expressed in LRV. Then, we obtain a polynomialtime reduction from Gainy(1) into the satisfiability problem for LRV(X, F).

VI. A ROBUST EQUIVALENCE

We have seen that the satisfiability problem for LRV is equivalent to the control state reachability problem in an exponentially larger VASS. In this section we evaluate how robust is this result with LRV variants or fragments.

A. Infinite Words with Multiple Data

So far, we have considered only finite words with multiple data. It is also natural to consider the variant with infinite words, but it is known that this sometimes leads to undecidability. However, in this case the decidability and complexity results are preserved. Let LRV ω be the variant of LRV in which infinite models of length ω are taken into account instead of finite ones. The logics PLRV ω , LRV ω , etc. are defined accordingly.

Proposition 16. (I) SAT(PLRV ω ) is decidable. (II) SAT(LRV ω ) is 2EXPSPACE-complete.

B. Adding MSO-Definable Temporal Operators

It is standard to extend LTL with MSO-definable temporal operators (see e.g. [START_REF] Wolper | Temporal logic can be more expressive[END_REF], [START_REF] Gastin | Satisfiability and model checking for MSOdefinable temporal logics are in PSPACE[END_REF]), and the same can be done with LRV. A temporal operator ⊕ of arity n is MSO-definable whenever there is a formula φ(x, P 1 , . . . , P n ) from monadic second-order logic with a unique free position variable x and with n free unary predicates such that σ, i |= ⊕(φ 1 , . . . , φ n ) iff σ |= φ(i, X 1 , . . . , X n ) in MSO where each set X j is equal to the set of positions from σ satisfying the formula φ j , see e.g. [START_REF] Gastin | Satisfiability and model checking for MSOdefinable temporal logics are in PSPACE[END_REF]. The 2EXPSPACE upper bound is preserved with a fixed finite set of MSO-definable operators.

Theorem 17. Let {⊕ 1 , . . . , ⊕ N } be a finite set of MSOdefinable temporal operators. Satisfiability problem for LRV extended with {⊕ 1 , . . . ,

⊕ N } is 2EXPSPACE-complete.
Note that PLRV augmented with MSO-definable temporal operators is decidable too.

C. The Now Operator or the Effects of Moving the Origin

The satisfiability problem for Past LTL with the temporal operator Now is known to be EXPSPACE-complete [START_REF] Laroussinie | Temporal logic with forgettable past[END_REF]. The satisfaction relation is parameterized by the current position of the origin and past-time temporal operators use that position. For instance, σ, i

|= o Now φ def ⇔ σ, i |= i φ and σ, i |= o φ 1 Sφ 2 def ⇔ there is j ∈ [o, i] such that σ, j |= o φ 2 and for all j ∈ [j -1, i],
we have σ, j |= o φ 1 . The powerful operator Now can be obviously defined in MSO but not with the above definition since it requires two free position variables, one of which refers to the current position of the origin.

Theorem 18. SAT(LRV + Now) is 2EXPSPACE-complete.
This contrasts with the undecidability results from [START_REF] Kara | Temporal logics on words with multiple data values[END_REF]Theorem 5] in presence of the operator Now.

D. Bounding the Number of Variables

Given the relationship between the number of variables in a formula and the number of counters needed in the corresponding VASS, we investigate the consequences of fixing the number of variables. Interestingly, this classical restriction has an effect only for LRV , i.e., when test formulas φ are restricted to in x ≈ φ? y. Let LRV k [resp. LRV k , PLRV k ] be the restriction to formulas with at most k variables. In [START_REF] Demri | Temporal logics of repeating values[END_REF]Theorem 5], it is shown that SAT(LRV 1 ) is PSPACE-complete by establishing a reduction into the reachability problem for VASS when counter values are linearly bounded. Below, we generalize this result for any k ≥ 1 by using the proof of Theorem 9 and the fact that the control state reachability problem for VASS with at most k counters is in PSPACE.

Proposition 19. For every

k ≥ 1, SAT(LRV k ) is PSPACE- complete.
This does not imply that LRV k is in PSPACE, since the reduction from LRV into LRV in Section IV-A introduces new variables. In fact, it introduces a number of variables that depends on the size of the formula. It turns out that this is unavoidable, and that its satisfiability problem is 2EXPSPACEhard, by the following reduction.

Lemma 20. There is a polynomial-time reduction from SAT(LRV ) into SAT(LRV 1 ) [resp. SAT(PLRV ) and SAT(PLRV 1 )].

Proof sketch: Let ϕ ∈ LRV using k variables x 1 , . . . , x k so that σ |= ϕ. We will encode σ restricted to x 1 , . . . , x k inside a model σ ϕ with only one variable, say x. To this end, σ ϕ is divided into N segments s 1 • • • s N of equal length, where N = |σ|. A special data value d not used in σ plays the role of delimiter between segments and between positions that code values from σ. Suppose that d is a data value that is not in σ. Then, each segment s i has length k = 2k + 1, and is defined as the data values "d d 1 d d 2 . . . d d k d", where d j = σ(i)(x j ). Figure 3 contains an example. We can force that the model has this shape with LRV 1 . With this coding, we can tell that we are between two segments if there are two consecutive equal data values. In fact, we are at a position corresponding to x i (for i ∈ [1, k]) inside a segment if we are standing at the 2i-th element of a segment, and we can test this with the formula

γ i = X k -2i x ≈ X k -2i+1 x ∨ (X k -2i ∧ ¬X k -2i+1 ).
Using the γ i 's, we translate x i ≈ ? x j in ϕ into a formula that: moves to the position 2i of the segment (the one corresponding to x i ), and tests x ≈ γ j ? x. We can do this similarly with all formulas.

Corollary 21. For all k ≥ 1, SAT(LRV k ) is 2EXPSPACE- complete.
Corollary 22. For all k ≥ 1, SAT(PLRV k ) is as hard as Reach(VASS).

E. The Power of Pairs of Repeating Values

Let us consider an LRV variant so that repetition of tuples of values is possible: we add formulas of the form (x 1 , . . . , x k ) ≈ φ? (y 1 , . . . , y k ) where x 1 , . . . , x k , y 1 , . . . , y k ∈ VAR. This extends x ≈ ϕ? y by testing whether the vector of data values from the variables (x 1 , . . . , x k ) of the current position coincides with that of (y 1 , . . . , y k ) in a future position.

We call this extension LRV vec . Unfortunately, we can show that SAT(LRV vec ) is undecidable, even when only tuples of dimension 2 are allowed. This is proved by reduction from a variant of Post's Correspondence Problem (PCP). In order to code solutions of PCP instances, we adapt a proof technique used in [START_REF] Bojańczyk | Two-variable logic on data words[END_REF] for first-order logic with two variables and two equivalence relations on words. However, our proof uses only future modalities (unlike the proof of [1, Proposition 27]) and no past obligations (unlike the proof of [START_REF] Kara | Temporal logics on words with multiple data values[END_REF]Theorem 4]). To prove this result, we work with a variant of the PCP problem in which solutions Theorem 23. SAT(LRV vec (X, U)) is undecidable.

u i1 • • • u in = v i1 • • • v in have to satisfy |u i1 • • • u ij | ≤ |v i1 • • • v ij | for every j.
Furthermore, our proof can be adapted to show that SAT(LRV vec ) is also undecidable.

VII. IMPLICATIONS FOR LOGICS ON DATA WORDS

A data word is an element of (Σ × D) * , where Σ is a finite alphabet and D is an infinite domain. We focus here on firstorder logic with two variables, and on a temporal logic.

Two-variable Logics:

We study a fragment of EMSO2 (+1, <, ∼) on data words, and we show that it has a satisfiability problem in 3EXPSPACE, as a consequence of our results on the satisfiability for LRV. The satisfiability problem for EMSO 2 (+1, <, ∼) is known to be decidable, equivalent to the reachability problem for VASS [START_REF] Bojańczyk | Two-variable logic on data words[END_REF], with no known primitive-recursive algorithm. Here we show a large fragment with elementary complexity.

Consider the fragment of EMSO 2 (+1, <, ∼) -that is, firstorder logic with two variables, with a prefix of existential quantification over monadic relations-where all formulas are of the form ∃X 1 , . . . , X n ϕ with

ϕ ::= atom | ¬ϕ | ϕ ∧ ϕ | ϕ ∨ ϕ | ∃x∃y ϕ | ∀x∀y ϕ | ∀x∃y (x ≤ y ∧ ϕ),
where

atom ::= ζ = ζ | ζ = ζ | ζ ∼ ζ | ζ < ζ | ζ ≤ ζ | + 1(ζ, ζ ) | X i (ζ) | a(ζ)
for any a ∈ Σ, i ∈ [1, n], and ζ, ζ ∈ {x, y}. The relation x < y tests that the position y appears after x in the word; +1(x, y) tests that y is the next position to x; and x ∼ y tests that positions x and y have the same data value. We call this fragment forward-EMSO 2 (+1, <, ∼). In fact, forward-EMSO 2 (+1, <, ∼) captures EMSO 2 (+1, <) (i.e., all regular languages on the finite labeling of the data word). 1 However, it seems to be strictly less expressive than EMSO 2 (+1, <, ∼), since it does not appear to be able to express, for example, there are exactly two occurrences of every data value. Yet, it can express there are at most two occurrences of every data value (with ∃X ∀x∀y. x ∼ y ∧ x < y → X(x) ∧ ¬X(y)), and there is exactly one occurrence of every data value. For the same reason, it would neither capture EMSO 2 (+1, ∼).

By an exponential reduction into SAT(LRV), we obtain that forward-EMSO 2 (+1, <, ∼) is decidable in elementary time.

Proposition 24. The satisfiability problem for forward-EMSO 2 (+1, <, ∼) is in 3EXPSPACE.

Proof sketch: Through a standard translation we can bring any formula of forward-EMSO 2 (+1, <, ∼) into a formula of the form

ϕ = ∃X 1 , . . . , X n ∀x∀y χ ∧ k ∀x∃y (x ≤ y ∧ ψ k )
that preserves satisfiability, where χ and all ψ k 's are quantifierfree formulas, and there are no tests for labels. Furthermore, this is a polynomial-time translation. This translation is just the Scott normal form of EMSO 2 (+1, <, ∼) [START_REF] Bojańczyk | Two-variable logic on data words[END_REF] adapted to forward-EMSO 2 (+1, <, ∼), and can be done in the same way.

We now give an exponential-time translation tr : forward-EMSO 2 (+1, <, ∼) → LRV. For any formula ϕ of forward-EMSO 2 (+1, <, ∼), tr(ϕ) is an equivalent (in the sense of satisfiability) LRV formula.

The translation makes use of: a distinguished variable x that encodes the data values of any data word satisfying ϕ; variables x 0 , . . . , x n that are used to encode the monadic relations X 1 , . . . , X n ; and a variable x prev whose purpose will be explained later on. We give now the translation. To translate ∀x∀y χ, we first bring the formula to a form

m∈M ¬∃x∃y x ≤ y ∧ χ m ∧ χ x m ∧ χ y m , ( )
where every χ x m (resp. χ y m ) is a conjunction of (negations of) atoms of monadic relations on x (resp. y); and χ m = µ ∧ ν where µ ∈ {x=y, +1(x, y), ¬(+1(x, y) ∨ x=y)} and ν ∈ {x ∼ y, ¬(x ∼ y)}. As an example, if χ = ¬(x ∼ y) ∨ X(x) ∨ X(y), then the corresponding formula would be

µ,χ x ,χ y (¬∃x∃y x ≤ y ∧ µ ∧ ¬X(x) ∧ χ y ) ∧ (¬∃x∃y x ≤ y ∧ µ ∧ χ x ∧ ¬X(y))
for all µ ∈ {x=y, +1(x, y), ¬(+1(x, y) ∨ x=y)}, χ x ∈ {X(x), ¬X(x)}, χ y ∈ {X(y), ¬X(y)}. We can bring the formula into this normal form in exponential time. We define tr(χ x m ) as the conjunction of all the formulas x 0 ≈ x i so that X i (x) is a conjunct of χ x m , and all the formulas ¬(x 0 ≈ x i ) so that ¬X i (x) is a conjunct of χ x m ; we do similarly for tr(χ y m ). If µ = +1(x, y) and ν = x ∼ y we define tr ∃y

x ≤ y ∧ χ m ∧ χ x m ∧ χ y m as x ≈ Xx∧tr(χ x m )∧ Xtr(χ y m ). If µ = (x = y) and ν = x ∼ y we translate tr ∃y x ≤ y ∧ χ m ∧ χ x m ∧ χ y m = tr(χ x m ) ∧ tr(χ y m ).
We proceed similarly for µ = +1(x, y), ν = ¬(x ∼ y); and the translation is of course ⊥ (false) if µ = (x=y), ν = ¬(x∼y). The difficult cases are the remaining ones. Suppose µ = ¬(+1(x, y) ∨ x=y), ν = x∼y. In other words, x is at least two positions before y, and they have the same data value. Observe that the formula tr(χ x m ) ∧ x ≈ tr(χ y m )? x does not encode precisely this case, as it would correspond to a weaker condition x < y ∧ x ∼ y. In order to properly translate this case we make use of the variable x prev , ensuring that it always has the data value of the variable x in the previous position

prev = G X ⇒ x ≈ Xx prev .
We then define tr ∃y

x ≤ y ∧ χ m ∧ χ x m ∧ χ y m as tr(χ x m ) ∧ x ≈ x prev ≈ tr(χ y m )? x?
x prev . Note that by nesting twice the future obligation we ensure that the target position where tr(χ y m ) must hold is at a distance of at least two positions. For ν = ¬(x∼y) we produce a similar formula, replacing the innermost appearance of ≈ with ≈ in the formula above. We then define tr(∀x∀y χ) as

prev ∧ m∈M ¬ F tr ∃y (x ≤ y ∧ χ m ∧ χ x m ∧ χ y m ) .
To translate ∀x∃y (x ≤ y ∧ ψ k ) we proceed in a similar way. One can show that tr preserves satisfiability. By Corollary 10 we can decide the satisfiability of the translation in 2EXPSPACE, and since the translation is exponential, this gives us a 3EXPSPACE bound for the satisfiability of forward-EMSO 2 (+1, <, ∼).

Temporal Logics: Our results have also implications for a fragment of the logic LTL extended with one register for storing and comparing data values (called the freeze operator), noted LTL ↓ 1 . Its satisfiability problem was shown to be decidable, but with non-primitive-recursive complexity [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF].

Our results yield a fragment of LTL ↓ 1 with elementary 2EXPSPACE upper bound.

VIII. CONCLUSION

We introduced the logic LRV and variants by allowing data value repetitions thanks to formulas of the form x ≈ φ? y. LRV extends the main logic from [START_REF] Demri | Temporal logics of repeating values[END_REF] but it is also a fragment of BD-LTL from [START_REF] Kara | Temporal logics on words with multiple data values[END_REF] whose satisfiability is equivalent to Reach(VASS). We showed that SAT(LRV) is 2EXPSPACEcomplete by reduction into the control-state reachability problem for VASS (via a detour to gainy VASS) and by introducing a new class of counter machines (the chain systems) in order to get the complexity lower bound. This new class of counter machines is interesting for its own sake and could be used to establish other hardness results thanks to our results that extend non-trivially the proof from [START_REF] Lipton | The reachability problem requires exponential space[END_REF], [START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF]. Correspondences between extensions of LRV (such as PLRV, PLRV and PLRV 1 ) and reachability problem for VASS are also established, strengthening further the relationships between data logics and reachability problems for counter machines. Other results for variants are presented in the paper and a summary can be found below.

LRV k : PSPACE-complete LRV ≡ LRV ≡ LRV 1 ≡ LRV + {⊕ 1 , . . . , ⊕ k } : 2EXPSPACE-complete PLRV ≡ PLRV ≡ PLRV 1 ≡ Reach(VASS) LRV vec : undecidable APPENDIX A. Proof of Theorem 1
Proof: First, the reachability problem for VASS can be reduced in polynomial-space to its restriction such that the initial and final configurations have all the counters equal to zero and each transition can only increment or decrement a unique counter. In the sequel, we consider an instance of this subproblem: A = Q, C, δ is a VASS, the initial configuration is q i , 0 and the final configuration is q f , 0 . Now, we build a formula φ in PLRV such that q f , 0 is reachable from q i , 0 iff φ is satisfiable. To do so, we encode runs of A by data words following exactly the proof of [1, Theorem 16] except that the properties are expressed in PLRV instead of FO2(∼, <, +1).

The objective is to encode a word ρ ∈ δ * that represents an accepting run from q i , 0 to q f , 0 . We use the alphabet δ of transitions, that we code using a logarithmic number of variables. One can simulate m different labels in PLRV, by using log(m) + 1 variables and its equivalence classes. In order to simulate the alphabet δ, we use the variables x 0 , . . . , x N , with N = log(card(δ)) . For any t ∈ δ, let t ∈ PLRV be the formula that tests for label t at the current position. More precisely, for any fixed injective function λ : δ → 2 [1,N ] we define

t = i∈λ(t) x 0 = x i ∧ 1≤i≤N,i ∈λ(t) x 0 = x i .
Note that t uses exclusively variables x 0 , . . . , x N , that is of size logarithmic in card(δ), and that t holds at a position for at most one t ∈ δ. We build a PLRV formula φ so that any word from δ * corresponding to a model of φ is an accepting run for A from q i , 0 to q f , 0 . And conversely, for any accepting run of A from q i , 0 to q f , 0 there is a model of φ corresponding to the run. The following are standard counter-blind conditions to check. 1) Every position satisfies t for some t ∈ δ.

2) The first position satisfies q i , instr, q for some q ∈ Q.

3) The last position satisfies q, instr, q f for some q ∈ Q. 4) There are no two consecutive positions i and i + 1 satisfying q 1 , instr, q 2 and q 1 , instr , q 2 respectively, with q 2 = q 1 . In the formula φ, we use the variable x to relate increments and decrements. Here are the main properties to satisfy. 1) For every counter c ∈ C, there are no two positions labelled by a transition with instruction inc(c) having the same same value for x:

G(inc(c) ⇒ ¬(x ≈ inc(c)? x))
where inc(c) is a shortcut for q,inc(c),q ∈δ t . A similar constraint can be expressed with dec(c). 2) For every counter c ∈ C, for every position labelled by a transition with instruction inc(c), there is a future position labelled by a transition with instruction dec(c) with the same value for x:

G(inc(c) ⇒ x ≈ dec(c)? x)
where dec(c) is a shortcut for q,dec(c),q ∈δ t . This will guarantee that the final configuration ends with all counters equal to zero. 3) Similarly, for every counter c ∈ C, for every position labelled by a transition with instruction dec(c), there is a past position labelled by a transition with instruction inc(c) with the same value for x:

G(dec(c) ⇒ x ≈ inc(c)? -1 x)
This will guarantee that every decrement follows a corresponding increment, satisfying that counter values are never negative. Let φ be the conjunction of all the formulas defined above. Since all the properties considered herein are those used in the proof of [START_REF] Bojańczyk | Two-variable logic on data words[END_REF]Theorem 16] (but herein they are expressed in PLRV instead of FO2(∼, <, +1)), it follows that φ is satisfiable in PLRV iff there is an accepting run of A from q i , 0 to q f , 0 .

B. Proofs of Propositions 2 and 3

Henceforward, vars(ϕ) denotes the set of all variables in ϕ, and sub (ϕ) the set of all subformulas ψ such that x ≈ ψ? y or x ≈ ψ? y appears in ϕ for some x, y ∈ vars(ϕ).

In both reductions we make use of the following easy lemma. Lemma 25. There is a polynomial-time satisfiability-preserving translation t : LRV → LRV [resp. t : LRV ≈ → LRV ≈ ] such that for every ϕ and ψ ∈ sub (t(ϕ)), we have sub (ψ) = ∅.

Proof: This is a standard reduction. Indeed, given a formula ϕ with subformula x ≈ ψ?

y, ϕ is satisfiable iff G(ψ ⇔ x new ≈ y new ) ∧ ϕ[x ≈ ψ? y ← x ≈ x new ≈ y new ? y]
is satisfiable, where x new , y new ∈ vars(ϕ), and ϕ[x ≈ ψ? y ← x ≈ x new ≈ y new ? y] is the result of replacing every occurrence of x ≈ ψ? y by x ≈ x new ≈ y new ? y in ϕ.

Proof of Proposition 2:

We show how to compute in polynomial time, for every ϕ ∈ LRV, a formula ϕ ∈ LRV ≈ that preserves satisfiability. The formula ϕ uses, besides all the variables from ϕ, a distinguished variable k ∈ vars(ϕ), and variables v ≈

x,ψ , v x ≈ ψ? y for every subformula ψ of ϕ and variables x, y ∈ vars(ϕ).

The idea behind the coding is the following. Any positive test x ≈ ψ? y can be always converted to a test x ≈ v x ≈ ψ? y ∧ v x ≈ ψ? y ≈ ψ? y, where v x ≈ ψ? y is a fresh variable. At any given position, we only need at most as many fresh variables as there are subformulas ψ and source and target variables x, y ∈ vars(ϕ), and we hence index these fresh variables by x, y and ψ. On the other hand, when a negative test ¬(x ≈ ψ? y) holds at a position i, it means that all positions satisfying ψ to the right of i have the same data value in the variable y. Since this data value is determined for every ψ, y, there is only boundedly many data values to remember, one for every subformula and variable. We use separate variables v ≈

x,ψ to remember this data value for every x, ψ. This variable is used in conjunction with k.

Whenever v ≈ x,ψ ≈ k at a position i, it means that ¬(v ≈ x,ψ ≈ ψ?
x), and we can make sure of this without using ≈. Indeed, we can do this by letting v ≈

x,ψ maintain the same value from position i onwards -until the last element verifying ψ-, we can test that whenever ψ holds, we have x ≈ v ≈ x,ψ . For any model σ, let σ ϕ be so that • if for some j ≥ i, σ, j |= ψ and for every i ≤ j < |σ| such that σ, j |= ψ we have σ(j

)(x) = σ(j )(x), then σ ϕ (i)(v ≈ x,ψ ) = σ(j)(x), • otherwise, σ ϕ (i)(v ≈ x,ψ ) = σ ϕ (i)(k); (
e) for every 0 ≤ i < |σ|, x, y ∈ vars(ϕ), and ψ ∈ sub (ϕ),

• if for some j > i, σ(j)(y) = σ(i)(x) and σ, j |= ψ, then let j 0 be the first such j, and

σ ϕ (i)(v x ≈ ψ? y ) = σ(j 0 )(y), • otherwise, σ ϕ (i)(v x ≈ ψ? y ) = σ ϕ (i)(k).
For every other unmentioned variable, σ and σ ϕ coincide. It is evident that for every ϕ and σ, a model σ ϕ with the aforementioned properties exists. Next, we define ϕ ∈ LRV ≈ so that σ |= ϕ if, and only if, σ ϕ |= ϕ .

( †)

We assume that for every ψ ∈ sub (ϕ), we have that sub (ψ) = ∅; this is without any loss of generality due to Lemma 25. We will also assume that ϕ is in negation normal form, that is, negation appears only in subformulas of the type ¬(x ≈ X y) or ¬(x ≈ ψ? y) [resp. ≈]. In particular, this means that we introduce a dual operator for each temporal operator.

• First, the variable k will act as a constant; it will always have the same data value at any position of the model, which must be different from those of all variables of ϕ.

const = G   (k ≈ Xk ∨ ¬X ) ∧ x∈vars(ϕ) (k ≈ x)  
• Second, for every position we ensure that if v ≈ x,ψ is different from k, then it preserves its value until the last element verifying ψ; and if ψ holds at any of these positions then v ≈

x,ψ contains the value of x.

val-v ≈ x,ψ = G k ≈ v ≈ x,ψ ⇒ v ≈ x,ψ ≈ Xv ≈ x,ψ ∨ ¬XFψ ∧ k ≈ v ≈ x,ψ ∧ ψ ⇒ v ≈ x,ψ ≈ x
• Finally, let ϕ ≈ be the result of replacing (a) every appearance of ¬(x ≈ ψ? y) by ¬XFψ ∨ x ≈ Xv ≈ y,ψ , and (b) every positive appearance of x ≈ ψ? y by x ≈ v x ≈ ψ? y ∧ v x ≈ ψ? y ≈ ψ? y in ϕ. We then define the translation ϕ as follows.

ϕ = ϕ ≈ ∧ const ∧ ψ∈sub (φ), x∈vars(ϕ) val-v ≈ x,ψ
Notice that ϕ can be computed from ϕ in polynomial time.

Claim 26. ϕ is satisfiable if, and only if, ϕ is satisfiable.

Proof: [⇒] Note that one direction would follow from ( †): if ϕ is satisfiable by some σ, then ϕ is satisfiable in σ ϕ . In order to establish ( †), we show that for every subformula γ of ϕ and

0 ≤ i < |σ ϕ |, we have σ, i |= γ iff σ ϕ , i |= γ ≈ . ( ‡)
Since σ ϕ |= const by condition (c), and

σ ϕ |= val-v ≈ x,ψ for every ψ due to (d), this is sufficient to conclude that σ |= ϕ iff σ ϕ |= ϕ .
We show ( ‡) by structural induction. If γ = x ≈ ψ? y, then σ, i |= γ if there is some j > i where σ(j)(y) = σ(i)(x) and σ, j |= ψ. Let j 0 be the first such j. Then, by condition (e), σ(i

)(x) = σ ϕ (i)(v x ≈ ψ? y ) = σ(j 0 )(y). Hence, σ ϕ , i |= v x ≈ ψ? y ≈ ψ? y and σ ϕ , i |= x ≈ v x ≈ ψ? y and thus σ ϕ , i |= γ ≈ .
If, on the other hand, γ = ¬(x ≈ ψ? y) then either

• there is no j > i so that σ, j |= ψ, or, otherwise,

• for every j ≥ i + 1 so that σ, j |= ψ we have σ(j )(y) = σ(i)(x). In the first case we have that σ ϕ , i |= ¬XFψ, and in the second case we have that, by (d), σ ϕ (i )(v ≈ y,ψ ) = σ ϕ (i)(x) for every i > i, and in particular for i = i + 1. Hence, σ ϕ , i |= ¬XFψ ∨ x ≈ Xv ≈ y,ψ and thus

σ ϕ , i |= γ ≈ .
Finally, the proof for the base case of the form γ = x ≈ X y [resp. ≈] and for all boolean and temporal operators are by an easy verification, since (•) ≈ is homomorphic for these. Hence, ( ‡) holds.

[⇐] Now suppose that σ |= ϕ . Since σ |= const, we have that σ verifies condition (c). And since σ |= val-v ≈

x,ψ for every ψ ∈ sub (ϕ), x ∈ vars(ϕ), we have that σ verifies (d). We prove by structural induction that for every subformula γ of ϕ, if σ, i |= γ ≈ then σ, i |= γ.

• If γ = x ≈ y [resp. x ≈ y, x ≈ X y, x ≈ X y] it is immediate since γ ≈ = γ. • If γ = x ≈ ψ? y and thus γ ≈ = x ≈ v x ≈ ψ? y ∧ x ≈ y,ψ ≈ ψ? y. Then, σ(i)(x) = σ(i)(v x ≈ ψ? y ) = σ(j)(y) for some j > i where σ, j |= ψ. Hence, σ, i |= x ≈ ψ? y. • If γ = ¬(x ≈ ψ? y), and thus γ ≈ = ¬XFψ ∨ x ≈ Xv ≈ y,ψ
. This means that either there is no j > i so that σ, j |= ψ and hence σ, i |= ¬(x ≈ ψ? y), or σ, j |= ψ for some j > i and σ(i)(x) = σ(i + 1)(v ≈ y,ψ ). By condition (d), we have that for all i < j , so that σ, j |= ψ, we have σ(j )(v ≈ y,ψ ) = σ(j )(y). Then, σ, i |= ¬(x ≈ ψ? y). • If γ = Fψ and γ ≈ = Fψ ≈ , there must be some position i ≥ i so that σ, i |= ψ ≈ . By inductive hypothesis, σ, i |= ψ and hence σ, i |= Fψ. We proceed similarly for all temporal operators and their dual, as well as for the boolean operators ∧, ∨. This is because (•) ≈ is homomorphic for all temporal and positive boolean operators.

We can easily extend this coding allowing for past obligations. We only need to use some extra variables v -1,≈

x,ψ , v -1

x ≈ ψ? -1 y that behave in the same way as the previously defined, but with past obligations. That is, we also define a val-v -1,≈

x,ψ as val-v ≈ x,ψ , but making use of v -1,≈ x,ψ , X -1 and F -1 . And finally, we have to further replace (c) every appearance of ¬(x ≈ ψ? -1 y) by ¬X -1 F -1 ψ ∨ x ≈ Xv -1,≈ y,ψ , and (d) every positive appearance of x ≈ ψ? -1 y by x ≈ v -1

x ≈ ψ? -1 y ∧ v -1

x ≈ ψ? -1 y ≈ ψ? -1 y in ϕ to obtain ϕ ≈ .

Proof of Proposition 3: We show how to compute in polynomial time, for every ϕ ∈ LRV ≈ , a formula ϕ ∈ LRV that preserves satisfiability. The formula ϕ uses, besides all the variables from ϕ, a distinguished variable k that does not appear in ϕ, and a variable v x,ψ for every subformula ψ of ϕ and every variable x appearing in ϕ.

The idea is that k acts as a constant, it preserves the same data value throughtout the model, and we enforce, for every subformula ψ and variable x of ϕ, that: ψ holds at a position if v x,ψ ≈ x, and ψ does not hold at a position if v x,ψ ≈ k. Now, instead of testing x ≈ ψ? y, one can simply test x ≈ ? v y,ψ .

Let ϕ ∈ LRV ≈ . We define vars(ϕ) as the set of all variables in ϕ, and sub (ϕ) as the set of all subformulas ψ such that x ≈ ψ? y appears in ϕ for some x, y. We show how to build a formula ϕ ∈ LRV which preserves satisfiability. For any model σ, let σ ϕ be so that (a

) |σ| = |σ ϕ |, (b) for every 0 ≤ i < |σ| and x ∈ vars(ϕ), σ(i)(x) = σ ϕ (i)(x), (c) there is some data value d ∈ {σ ϕ (i)(x) | x ∈ vars(ϕ), 0 ≤ i < |σ|} such that for every 0 ≤ i < |σ|, σ ϕ (i)(k) = d, and (d) for every 0 ≤ i < |σ|, σ ϕ (i)(v x,ψ ) = σ ϕ (i)(x) if σ, i |= ψ, and σ ϕ (i)(v x,ψ ) = σ ϕ (i)(k) otherwise.
For every other unmentioned variable, σ and σ ϕ coincide. It is evident that for every ϕ and σ, a model σ ϕ with the aforementioned properties exists. Next, we define ϕ ∈ LRV so that

σ |= ϕ if, and only if, σ ϕ |= ϕ . ( †)
We assume that for every ψ ∈ sub (ϕ), we have that sub (ψ) = ∅. This is without any loss of generality by Lemma 25.

• First, the variable k will act as a constant; it will always have the same data value at any position of the model, which must be different from those of all variables of ϕ.

const = G   (k ≈ Xk ∨ ¬X ) ∧ x∈vars(ϕ) (k ≈ x)  
• Second, any variable v x,ψ has either the value of k or that of x. Further, the latter holds if, and only if, ψ is true.

val-v x,ψ = G(v x,ψ ≈ k ∨ v x,ψ ≈ x) ∧ G(v x,ψ ≈ x ⇔ ψ)
• Finally, let ϕ be the result of replacing every appearance of x ≈ ψ? y by x ≈ ? v y,ψ in ϕ. We then define ϕ as follows.

ϕ = ϕ ∧ const ∧ ψ∈sub (ϕ) val-v x,ψ
Notice that ϕ can be computed from ϕ in polynomial time.

Claim 27. ϕ is satisfiable if, and only if, ϕ is satisfiable.

Proof: [⇒] Note that one direction would follow from ( †): if ϕ is satisfiable by some σ, then ϕ is satisfiable in σ ϕ . In order to establish ( †), we show that for every subformula γ of ϕ and

0 ≤ i < |σ ϕ |, we have σ, i |= γ iff σ ϕ , i |= γ ≈ . ( ‡)
Since σ ϕ |= const by condition (c) and σ ϕ |= val-v x,ψ for every ψ due to (d), this is sufficient to conclude then σ |= ϕ iff σ ϕ |= ϕ . We show it by structural induction. If σ, i |= x ≈ ψ? y then there is some j > i where σ(j)(y) = σ(i)(x) and σ, j |= ψ. Then, by condition (d), σ ϕ (j)(v y,ψ ) = σ ϕ (j)(y) and thus σ ϕ , i |= x ≈ ? v y,ψ . Conversely, if σ ϕ , i |= x ≈ ? v y,ψ this means that there is some j > i such that σ ϕ (i)(x) = σ ϕ (j)(v y,ψ ). By (c), we have that σ ϕ (j)(v y,ψ ) = σ ϕ (j)(k), and by (d) this means that σ ϕ (j)(v y,ψ ) = σ ϕ (j)(y) and σ ϕ , j |= ψ. Therefore, σ, i |= x ≈ ψ? y. The proof for the base case of the form ψ = x ≈ X i y and for all the cases of the induction step are by an easy verification since (•) is homomorphic. Hence, ( ‡) holds.

[⇐] Suppose that σ |= ϕ . Note that due to const condition (c) holds in σ, and due to val-v x,ψ , condition (d) holds. We show that for every position i and subformula γ of ϕ, if σ, i |= γ , then σ, i |= γ.

The only interesting case is when γ = x ≈ ψ? y, and γ = x ≈ ? v y,ψ , since for all boolean and temporal operators (•) is homomorphic. If σ, i |= x ≈ ? v y,ψ there must be some j > i so that σ(j)(v y,ψ ) = σ(i)(x). By condition (c), σ(j)(k) = σ(j)(v y,ψ ) = σ(i)(x), and by condition (d), this means that σ, j |= ψ and σ(j)(v y,ψ ) = σ(j)(y). Hence, σ, i |= x ≈ ψ? y. The remaining cases are straightforward since (•) is homomorphic on temporal and boolean operators.

Finally, note that we can extend this coding to treat past obligations in the obvious way.

C. Proofs of Lemmas 7, 8 and Theorem 9

We define the VASS A inc as Q, C, δ min and Q 0 , Q f ⊆ Q, where Q, Q 0 , Q f and C are same as those of A φ and δ min is defined as follows: (q, minup q,q , q

) ∈ δ min iff δ ∩ ({q} × [-k, k] C × {q })
is not empty and minup q,q (X) = min u:(q,u,q )∈δ {u(X)} for all X ∈ C.

We also use the "maximal" transition in some lemmas: maxup q,q (X) = max u:(q,u,q )∈δ {u(X)}.

Proof of Lemma 7: Since q, v -→ q , v , there is a transition (q, u, q ) ∈ δ such that u + v = v . By definition of A inc , there is a transition (q, minup q,q , q ) ∈ δ min where uminup q,q 0. Let incer = uminup q,q (this will be the incremental error used in A inc ). Now we have q, v +

incer minup q,q -----→ q , v + u = q , v in A inc . Hence, q, v - → gainy q , v in A inc .
Proof of Lemma 8: By induction on the length n of the run q 1 , v 1 * -→ gainy q 2 , 0 . The base case n = 0 is trivial since there is no change in the configuration.

Induction step: the idea is to simulate the first gainy transition by a normal transition that decreases each counter as much as possible while ensuring that (1) the resulting value is non-negative and (2) we can apply the induction hypothesis to the resulting valuation. We calculate the update required for each counter individually and by closure under component-wise interpolation, there will always be a transition with the required update function. Let q 1 , v 1 -→ gainy q 3 , v 3 * -→ gainy q 2 , 0 and v 1 v 1 . We will define an update function u such that q 1 , v 1 -→ q 3 , v 3 , v 3 (X) = v 1 (X) + u (X) for each X ∈ C and v 3 v 3 . For each counter X ∈ C, u (X) is defined as follows:

Case 1:

v 1 (X) + minup q1,q3 (X) ≥ 0. Let u (X) = minup q1,q3 (X). v 3 (X) ≥ v 1 (X) + minup q1,q3 (X) [From the semantics of A inc ] ≥ v 1 (X) + minup q1,q3 (X) [Since v 1 v 1 ] = v 1 (X) + u (X) [By definition of u (X)] = v 3 (X)
Case 2: v 1 (X) + minup q1,q3 (X) < 0. Therefore, minup q1,q3 (X) < -v 1 (X). Moreover, since maxup q1,q3 (X) ≥ 0 (due to the optional decrement property) and

v 1 (X) ≥ 0, -v 1 (X) ≤ maxup q1,q3 (X). Let u (X) = -v 1 (X). Now, v 3 (X) = v 1 (X) + u (X) = 0 v 3 (X).
By definition of minup q1,q3 and the closure of the set of transitions δ of A φ under component-wise interpolation, we have (q 1 , u , q 3 ) ∈ δ and hence q 1 , v 1 -→ q 3 , v 3 . Since v 3 v 3 and q 3 , v 3 * -→ gainy q 2 , 0 , we can use the induction hypothesis to conclude that q 3 , v 3 * -→ q 2 , 0 . So we conclude that

q 1 , v 1 - → q 3 , v 3 * - → q 2 , 0 .
Proof of Theorem 9: The proof is in four steps.

Step 1: From [START_REF] Demri | Temporal logics of repeating values[END_REF], a LRV formula φ is satisfiable iff q 0 , 0 * -→ q f , 0 in A φ for some q 0 ∈ Q 0 and

q f ∈ Q f .
Step 2: This is the step that requires new insight. From Lemmas 7 and 8, q 0 , 0 * -→ q f , 0 in A φ iff q 0 , 0 * -→ gainy q f , 0 in A inc .

Step 3: This is a standard trick. Let A dec = Q, C, δ rev be a VASS such that for every transition (q, u, q ) ∈ δ min of A inc , A dec has a transition (q , -u, q) ∈ δ rev , where -u : C → Z is the function such that -u(X) = -1 × u(X) for all X ∈ C. We infer that q 0 , 0 * -→ gainy q f , 0 in A inc iff q f , 0 * -→ lossy q 0 , 0 in A dec (we can simply reverse every transition in the run of A inc to get a run of A dec and vice-versa).

Step 4: This is another standard trick. Since A dec does not have zero-tests, we can remove all decrementing errors from a run of A dec from q f , 0 to q 0 , 0 , to get another run from q f , 0 to q 0 , v , where v is some counter valuation (possibly different from 0). Using decremental errors at the last configuration, A dec can then reach the configuration q 0 , 0 . In other words, q f , 0 * -→ lossy q 0 , 0 iff q f , 0 * -→ q 0 , v for some counter valuation v. Checking the latter condition is precisely the control state reachability problem for VASS.

If the control state in the above instance is reachable, then Rackoff gives a bound on the length of a shortest run reaching it [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]. The bound is doubly exponential in the size of the VASS. Since in our case, the size of the VASS is exponential in the size of the LRV formula φ, the bound is triply exponential. A non-deterministic Turing machine can maintain a binary counter to count up to this bound, using doubly exponential space. The machine can start by guessing some initial state q 0 and a counter valuation set to 0. (this can be done in polynomial space). In one step, the machine guesses a transition to be applied next and updates the current configuration accordingly, while incrementing the binary counter. At any step, the space required to store the current configuration is at most doubly exponential. By the time the binary counter reaches its triply exponential bound, if a final control state is not reached, the machine rejects its input. Otherwise, it accepts. Since this non-deterministic machine operates in doubly exponential space, an application of Savitch's Theorem gives us the required 2EXPSPACE upper bound for the satisfiability problem of LRV .

D. Proofs of Lemmas 12 and 13

Let A = Q, f, k, Q 0 , Q F , δ be a chain automaton of level k. A run ρ ends in zero whenever for every chain α ∈ [1, n], c α L = 0 with L = |ρ|. We write Per zero (k) and Gainy zero (k) to denote the variant problems of Per(k) and Gainy(k), respectively, in which runs that end in zero are considered. First, note that Per zero (k) and Per(k) are interreducible in logarithmic space since it is always possible to add adequately self-loops when a final state is reached in order to guarantee that c α L = 0 for every chain α ∈ [1, n]. Similarly, Gainy zero (k) and Gainy(k) are interreducible in logarithmic space.

Proof of Lemma 12: Below, we show that Per zero (k) and Gainy zero (k) are interreducible in logarithmic space, which allows us to get the proof of the lemma since logarithmic-space reductions are closed under composition. From A, let us define a reverse counter automaton A of level k, where the reverse operation • is defined on instructions, transitions, sets of transitions and automata as follows:

• inc(α) def = dec(α); dec(α) def = inc(α); next(α) def = prev(α); prev(α) def = next(α), • first(α)? def = last(α)?; last(α)? def = first(α)?; first(α)? def = last(α)?; last(α)? def = first(α)?, • q instr --→ q def = q instr --→ q, • A def = Q, f, k, Q F , Q 0 , δ with δ def = { q instr --→ q : q instr --→ q ∈ δ}. Note that Q 0 and Q F have been swapped.
The reverse operation can be extended to sequences of transitions as follows:

ε def = ε and t • u def = u • t.
Note that • extends the reverse operation defined in the proof of Theorem 9 (step 3).

One can show the following implications, for any run ρ fo A that ends in zero:

1) ρ is perfect and accepting for A implies ρ is gainy and accepting for A.

2) ρ is gainy and accepting for A implies ρ is perfect and accepting for A.

3) ρ is gainy and accepting for A implies ρ is perfect and accepting for A. 4) ρ is perfect and accepting for A implies ρ is gainy and accepting for A.

(1) and (4) [resp. ( 2) and ( 3)] have very similar proofs because • -1 is actually equal to •. (1)-( 4) are sufficient to establish that Per zero (k) and Gainy zero (k) are interreducible in logarithmic space.

Proof of Lemma 13: It is sufficient to show that Per zero (k) is in (k + 1)EXPSPACE. Let A = Q, f, k, Q 0 , Q F , δ be a chain automaton with f : [1, n] → N. We reduce this instance of Per zero (k) into several instances of the control state reachability problem for VASS such that the number of instances is bounded by O(|A| 2 ) and the size of each instance is in O(exp(k, |A|) |A| ), which provides the (k + 1)EXPSPACE upper bound by [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]. The only instructions in the VASS A defined below are: increment a counter, decrement a counter or the skip action, which just changes the control state without modifying the counter values (which can be obviously simulated by an increment followed by a decrement).

Let us define a VASS A = Q , C , δ with

C = {c 1 0 , . . . , c 1 exp(k,f (1)
)-1 , . . . , c n 0 , . . . , c n exp(k,f (n))-1 } In A it will be possible to access the counters directly by encoding the positions of the pointers in the states.

Let Q = Q × [0, exp(k, f (1)) -1] × • • • × [0, exp(k, f (n)) -1]
. It remains to define the transition relation δ :

• Whenever q inc(α) ---→ q ∈ δ, we have q, β 1 , . . . , β n inc(c α βα )
----→ q , β 1 , . . . , β n ∈ δ (and similarly with decrements),

• Whenever q next(α) ----→ q ∈ δ, we have q, β 1 , . . . , β α , . . . , β n skip --→ q , β 1 , . . . , β α + 1, . . . , β n ∈ δ if β α + 1 < exp(k, f (α)) (and similarly with prev(α)),

• When q first(α)? ----→ q ∈ δ, q, β 1 , . . . , β n skip --→ q , β 1 , . . . , β n ∈ δ if β α = 0 (and similarly with first(α)?, last(α)? and last(α)?). It is easy to show that there is a perfect accepting run that ends in zero iff there are q 0 ∈ Q 0 × {0} n and q F ∈ Q F × {0} n such that there is a run from the configuration q 0 , 0 to the configuration q F , x for some x.

In order to prove the above equivalence, we can use the transformations (I) and (II) stated below. (I) Let ρ = t 1 • • • t L be a run of A such that for every i ∈ [1, L -1], t i = q i-1 instri --→ q i and the values c α i are defined as before [START_REF] Bojańczyk | Two-variable logic on data words[END_REF]. One can show that ρ = t 1 • • • t n with t i = q i-1 , x i-1 instr i --→ q i , x i for every i, is a run of A where

• x 0 = 0 and for every i ∈ [1, L], x i = c 1 i , . . . , c n i , • for every i ∈ [1, L],
if instr i = inc(α) then instr i = inc(c α c α i ) (a similar clause holds for decrements), -otherwise (i.e., if instr i is not inc(α) nor dec(α) for any α), instr i = skip.

(II) Similarly, let ρ = t 1 • • • t L be a run of A where t i = (q i-1 , x i-1 ) instr i --→ (q i , x i ) for every i, with

x 0 = 0. One can show that ρ = t 1 • • • t L with t i = q i-1 instri --→ q i for
every i, is a perfect accepting run of A such that for every i ∈ [1, L],

• if instr i = inc(c α j ) then instr i = inc(α) (a similar clause holds for decrements), • otherwise, if x i+1 (α) = x i (α) + 1 for some α, then instr i = next(α) (a similar clause holds for previous),

• otherwise, if x i (α) = 0 and q i first(α)?

----→ q i+1 ∈ δ for some α, then instr i = first(α)? (a similar clause holds for first(α)?),

• otherwise, if x i (α) = exp(k, f (α)) -1 and q i last(α)? ----→ q i+1 ∈ δ for some α, then instr i = last(α)? (a similar clause holds for last(α)?).

E. Details of the Hardness Result for Chain Automata

This section is dedicated to prove Theorem 14 by extending Lipton's proof [START_REF] Lipton | The reachability problem requires exponential space[END_REF] (see also its presentation in [START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF]) that shows that control state reachability problem for VASS is EXPSPACE-hard. In Sub-section E1, we recall principles of Lipton's proof without entering into the implementation details; indeed when dealing with chain automata the coding has to be refined. In Sub-section E2, we explain how large decrements can be encoded with chain automata (a key point in the proof). Sub-section E3 is dedicated to the initialization of the counter values (another key point in the proof). In Lipton's proof, initialization amounts to performing a series of large increments using principles analogous to those for encoding decrements. When chain automata are used as a low level programming language, we need to maintain additional data structures (in chain automata, this means chains of counters). Unlike [START_REF] Lipton | The reachability problem requires exponential space[END_REF], [START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF], we do not use a return mechanism and we simulate directly the call/return stack. Hence, our construction is more general but at the cost of a more careful analysis. Sub-section E4 contains the statements and proofs of the main lemmas to conclude the correctness of our simulation. Finally, Sub-section E5 summarizes the different steps of the proof and concludes this section.

The proof below is complicated and sometimes we may repeat arguments for the sake of clarity and to present arguments from different viewpoints. We believe this might help the reader to grasp the present simulation.

1) Principles of Lipton's Proof: In this section, we present the principles behind the proof showing that the control state reachability problem for VASS is EXPSPACE-hard [START_REF] Lipton | The reachability problem requires exponential space[END_REF], [START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF].

Lipton's proof starts from the standard result in computability theory that a Turing Machine using space 2 n γ can be simulated by a counter automaton equipped with 4 counters whose values are bounded by 2 2 n γ . Lipton's proof shows that such a counter automaton can be simulated with a VASS. Unlike counter automata, VASS does not have zero-test transitions. Each counter c of the automaton is complemented with an extra counter c in the VASS. The VASS is designed such that the sum of the values in c and c is 2 2 n γ in any reachable configuration. Now testing c for zero is equivalent to testing that c is 2 2 n γ . This later test is performed as explained next.

Testing that c is 2 2 n γ is done by decrementing c by 2 2 n γ . To do so, the value of c is transferred to another counter s and then s is decremented by 2 2 n γ . This whole operation results in the values of c and c getting swapped, while all other counters retain their original values. To rectify the swapping between c and c, we repeat the operation except that the value of c is transferred to s and then s is decremented by 2 2 n γ .

Decrementing s by 2 2 n γ is done by having a series of counters s i , s i for each i between 1 and n γ . For each i, the sum of values in s i and s i is maintained at 2 2 i . Below, we illustrate how a counter s i is decremented 2 2 i times. There are two nested loops indexed by y i-1 and z i-1 , initialised to 2 2 i-1 . When all the iterations are finished, we would have decremented s i exactly 2 2 i-1 × 2 2 i-1 = 2 2 i times. Testing y i-1 and z i-1 for zero is done by a similar gadget, where i, i -1 are replaced by i -1, i -2. The resulting VASS is composed of n γ constant sized VASS, each one implementing the nested loops for an i between 1 and n γ .

y i-1 = z i-1 = 2 2 i-1 y -- i-1 , y i-1 ++ z -- i-1 , z i-1 ++ s -- i , s i ++ z i-1 = 0?
In the above explanation of the decrementing algorithm, we have assumed that the counters y i-1 and z i-1 have the exact value 2 2 i-1 in the beginning. This can be achieved if we first inductively initialize all counters y j and z j to have the value 2 2 j for each j between 1 and i -2. Assuming this initialization has been done, the algorithm shown in Fig. 5 initializes y i-1 and z i-1 to 2 2 i-1 . The algorithm shown in Fig. 5 is based on the same principle as the one in Fig. 4, except that i, i -1 are replaced by i -1, i -2 and that instead of decrementing s i inside the nested loops, y i-1 , z i-1 are incremented. Now that we know how zero-tests are implemented in a VASS, let us see how a VASS simulates counter automata with bounded counter values. For every transition q, c ← c + 1, q of the counter automaton, the VASS will have the transition q, (inc(c); dec(c)), q . Thus, for every incrementing transition of the counter automaton, the VASS can execute a corresponding incrementing transition. Conversely, for every incrementing transition executed by the VASS, the counter automaton can execute the corresponding incrementing transition.

y i-2 = z i-2 = 2 2 i-2 y -- i-2 , y i-2 ++ z -- i-2 , z i-2 ++ y ++ i-1 , z ++ i-1 z i-2 = 0?
For every transition q : if c = 0 goto q 1 else c ← c-1 goto q 2 of the counter automaton, the VASS will have transitions corresponding to the following program. q: goto nonzero or zero nonzero: dec(c); inc(c); goto q 2 zero: transfer(c, s); goto Dec zerorep zerorep: transfer(c, s); goto Dec q1 The macro transfer(c, s) is intended to be a shortcut for "s := s + c; c := 0" but its actual implementation is described in the next section. Its code guarantees that at least one of its executions performs the sequence "s := s + c; c := 0". The macro transfer(c, s) is defined analogously.

In the above, the control state Dec zerorep launches a program that decrements s by 2 2 n γ and then transfers the control to zerorep. Similarly, Dec q1 launches a program that decrements s by 2 2 n γ and then transfers the control to q 1 . The idea behind our (k+1)EXPSPACE lower bound is that a Turing Machine using space exp(k+1, n γ ) can be simulated by a counter automaton equipped with 4 counters whose values are bounded by exp(k + 2, n γ ). We shall show that such a counter automaton can be simulated with a chain automaton of level k with a map f such that for each chain α, f (α) = n γ . Each chain α of the chain automaton will be complemented with another chain α. We will denote the counters in these chains by α 1 , α 1 , . . . , α exp(k,n γ ) , α exp(k,n γ ) . The chain automaton will be designed such that the sum of the values in α i and α i is 2 2 i in any reachable configuration and for any i between 1 and exp(k, n γ ). Now testing α i for zero is equivalent to testing that α i is 2 2 i . This later test will not work directly as explained above, since a chain automaton composed of exp(k, n γ ) constant sized portions will not give a polynomial-time reduction. We reduce the size of the chain automaton by observing that the decrementing algorithm for i -1 is the same as the one for i, except that i, i -1 are replaced by i -1, i -2 respectively. We can write a single sequence of instructions for the decrementing algorithm and invoke it for any i by placing the pointers at the appropriate counters. The main difficulty in the implementation is to ensure that the multiple invocations of the algorithm return to the correct point, which is handled in the next section.

2) Encoding Large Decrements with Chain Automata: In the ideas explained in the previous section, we assumed that a call to a procedure will return to the correct program point. In Lipton's proof [START_REF] Lipton | The reachability problem requires exponential space[END_REF] and its exposition contained in [START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF], the decrementing algorithms are described as subroutines, and a return mechanism (which involves remembering return addresses) is implemented in a VASS. Since we do not have direct access to counters in chain automata, it is cumbersome to implement a general purpose return mechanism. In this section, we explain how decrements can be implemented with a chain automaton without using a return mechanism.

Recall the following high-level algorithm used in Lipton's proof.

outerloop: Decrement y i-1 . innerloop: Decrement z i-1 . decrement: Decrement s i . innerexit: If z i-1 = 0, go to innerloop. Otherwise, set z i-1 back to 2 2 i-1 and go to outerexit. outerexit: If y i-1 = 0, go to outerloop. Otherwise, set y i-1 back to 2 2 i-1 and return. Whenever we have to return from the decrementing algorithm for stage i -1, we have to return to the step labeled either innerexit or outerexit of stage i, in the high-level algorithm described above. To remember which one, we maintain a pair of chains stack and stack, each having exp(k, n γ ) counters, so that the sum of the values of stack i and stack i is 1. For convenience, we will use N = exp(k, n γ ) from here onwards. We follow the convention that if at stage i, the counter in the chain stack has value 1, then it is the step labeled innerexit that invoked the decrementing algorithm for stage i -1. A stack value of 0 at stage i implies that the step labeled outerexit invoked the decrementing algorithm for stage i -1. In addition, we have six chains y, y, z, z, s and s, each with N counters. Recall that for the decrementing algorithm to work properly at stage i, y i-1 and z i-1 both should have the value 2 2 i-1 and s i-1 should have the value 0 (so s i-1 should have the value 2 2 i-1 ). We also need to have stack i-1 to have the value 0 (so stack i-1 should have the value 1).

To understand our implementation of the decrementing algorithm, it will be helpful to think of the counters in the chains arranged as follows.

Chain\Stage

N N -1 N -2 . . . i i -1 • • • 1 y 2 2 i-1 z 2 2 i-1 s 2 2 i 0 stack 0 0 1 • • • 1 • • • 0 Pointer Nextstage ← ↑ → Prevstage
The fact that all chains have their pointers at stage i is shown by the arrow ↑ in the last row of the above table. We will frequently move the pointers. The macro Nextstage is short for the sequence of transitions next(y); next(y); . . . ; next(stack); next(stack), which moves all the pointers one stage up as shown above. The macro Prevstage similarly moves all the pointers one stage down. The macro transfer(z, s) is short for the following sequence of transitions. transfer(z, s) Next control state { zero: inc(z); dec(z); inc(s); dec(s); goto zero or fin fin: goto Next control state } In the above description, Next control state represents the control state that immediately follows the macro transfer(z, s) in a listing. The macro transfer(y, s) is similar to the above, with y and y replacing z and z respectively. The macro inc(next(z)) moves the pointer of the chain z one stage up, increments z once and moves the pointer back one stage down: next(z); inc(z); prev(z). The macros inc(next(y)) and inc(next(s)) are similar to inc(next(z)) with y and s replacing z respectively. The macro dec(next(s)) is similarly defined to decrement the next counter in the chain s. The macro stack == 1 tests if the counter in the current stage in the chain stack is greather than 0: dec(stack); inc(stack).

Our returning mechanism is specific to the decrementing algorithm. There will be one copy for every zero testing transition in the counter automaton that we simulate (the size of the chain automaton will be linear in the size of the automaton even after creating these copies). The listing below is written in the form of a program in a low level programming language for readability. It can be easily translated into a set of transitions of a chain automaton. There is a control state between every two consecutive instructions below, but only the important ones are given names like "outerloop2". A line such as "innernonzero2: dec(z); inc(z); goto innerloop2" actually represents the set of transitions { innernonzero2, dec(z), q , q, inc(z), innerloop2 }. The instruction "q: if first(α)? then {program 1} else {program 2}" represents the set of transitions { q, first(α)?, q 1 , q, first(α)?, q 2 } ∪ {transitions for program 1 from q 1 } ∪ {transitions for program 2 from q 2 }. An instruction of the form "q : inc(stack); goto outernonzero2 or outerzero2" represents the set of transitions { q, inc(stack), outernonzero2 , q, inc(stack), outerzero2 }. Depending on the non-deterministic choices made at control states that have multiple transitions enabled, there will be several different runs. We prove later that there is one run which has the intended effect and the other runs will never reach the final state. To understand the flow of the algorithm below, whenever the pointer is at stage i and the instruction "goto Dec" is executed, the reader can assume that s is decremented 2 2 i times and the control is magically transferred to the instruction immediately following the "goto Dec". We later prove formally that this actually happens. Referring to the tabular arrangement of the counters shown above would also help understand the following implementation and proofs of correctness. As can be seen from the listing, there are two recursive calls to "Dec" from inside "Dec". The first one is from "innerzero2", which should return to "outertest2". The second one is from "outerzero2", which should return to "outerexit2". As seen in the listing and also in the diagram above, the call from "innerzero2" is made just after incrementing stack. When the recursive call to "Dec" finishes (after possibly moving the pointers to previous stage and moving them back to current stage multiple times) and comes to backtrack, it will check if stack == 1. Since this is the case, the control goes to "outertest2", where the stack is set back to 0 and rest of the computation continues.

On the other hand, when a recursive call to "Dec" is made from "outerzero2", stack will be set to 0. Hence, when the recursive call to "Dec" returns and checks whether stack == 1, the answer will be no and the control goes to "outerexit2".

3) Initialisation Phase: In this section, we explain how to get counters to their required initial values (at the beginning of the runs all the values are equal to zero). We briefly recall what are these values after initialization: 1) each counter c has value zero, 2) for every i ∈ [1, N ], y i , z i and s i are equal to zero, 3) for every i ∈ [1, N ], stack i is equal to zero and stack i is equal to one, 4) each complement counter c has value 2 2 N , 5) for every i ∈ [1, N ], y i , z i and s i have the value 2 2 i . Initialization for the points 1)-3) is easy to perform and below we focus on the initialization for the point 5). Initialization of the complement counter in point 4) will be dealt with in Section E5 by simply adjusting what is done below.

To help achieve these initial values for 5), we have another chain init, with N counters. We follow the convention that if at stage i, the counter in the chain init has value 1, then all the counters in all the chains at stage i or below have been properly initialized. By convention, the condition last(init)? is true if the pointer in the chain init is at stage N .

To understand our implementation of the decrementing algorithm, again, it will be helpful to think of the counters in the chains arranged as follows (this time we added the chain init)

Chain\Level N N -1 N -2 • • • i i -1 . . . 1
y 2 2 i-1 z 2 2 i-1 s 2 2 i 0 stack 0 0 1 • • • 1 • • • 0 init 0 0 1 • • • 1 • • • 1 Pointer Nextstage ← ↑ → Prevstage The macro
Nextstage is short for the sequence of transitions next(y); next(y); . . . ; next(init); next(init), which moves all the pointers one stage up as shown above. The macro Prevstage similarly moves all the pointers one stage down. The macro next(init) == 1 tests if the value of the counter one stage up in the chain init is greater than 0: next(init); dec(init); inc(init); prev(init).

We give below the code used to initialize y, z, s and stack to the required values, assuming that all counters are initially set to 0 and all the pointers in all the chains are pointing to stage 0. To ease the reading, we have reproduced the code for Dec from Section E2.

As explained in Section E1, the principle for initialization is again nested loops. Below, the outer loop is implemented between the states "outerinit" and "outernonzero1", while the inner loop is between "innerinit" and "innernonzero1". Inside these loops, we have "inc(next(y)); inc(next(z));inc(next(s))", which will increment counters in the next stage. This will work properly provided the counters in the current stage and below have already been initialized. We will prove later that initialization of counters at some stage will start only after all stages below have been initialized. We will also need to test counters at lower stages for zero, for which we will use the Dec algorithm from the previous section. Apart from the recursive calls to Dec from inside Dec itself, now there are also calls to Dec from "innerzero1" and "outerzero1" below. To handle these additional return locations, "backtrack" part of the code below has been updated that also checks if the call has been made from initialization code. begininit: (inc(y)) 4 ; (inc(z)) 4 ; (inc(s)) 4 ; inc(init); inc(stack) initialise: If last(init)? goto beginsim else goto outerinit outerinit: dec(y); inc(y) /* y is the index for outer loop */ innerinit: dec(z); inc(z) In the figure we simplify some of the instructions, for example instead of dec(s); inc(s) we just put s--, instead of dec(z); inc(z) we just put z > 0?, etc.

4) Proof of Correctness:

In the following lemmas, we refer to "a configuration of the chain automaton", by which we mean a configuration of the VASS A defined in the proof of Lemma 13. A configuration has the pointer in chain α at stage i if the control state of A is q, β 1 , . . . , β α , . . . for some q ∈ Q and β α = i. A configuration has the value x in the counter in the chain α at stage i if the counter c α i has the value x. Lemma 28. Suppose in a configuration of the chain automaton, all the pointers in all the chains are at stage i, the counters in the chains init and s at stage i have values 1 and 2 2 i respectively and all the counters in all the chains at or below stage i -1 have been initialised. If the control state is at "Dec", then there is a run ρ i ending at the control state "DecFinished" (just before "backtrack" in the above listing) with the pointers at stage i in all the chains and no change to any counter at any stage, except that the counter at stage i in the chain s has the value 0 (intuitively, there is a run which decreases s by 2 2 i and does nothing else).

Proof: By induction on i. For the base case i = 1, we note that the test first(init)? is true. So ρ 1 is the run that decrements s four times, increments s four times and goes to "DecFinished".

Assuming the lemma is true up to value i, we prove it for i + 1. The run ρ i+1 does not perform the test first(init)? at the beginning of "Dec" but instead goes to the "else" branch. Following is the run ρ i+1 . Prevstage; (outerloop2; (innerloop2; dec(next(s)); inc(next(s)); innertest2) 2 2 i innerzero2; transfer(z, s); ρ i ; DecFinished; backtrack; outertest2) 2 2 i outerzero2; transfer(y, s); ρ i ; DecFinished; backtrack; outerexit2; Nextstage; DecFinished Note that in the above run, we have omitted some instructions and program points but we have kept those that are the most essential for our reasoning.

The first transition is to move all pointers one stage down to i. Since all counters at stage i or below have been initialised, y and z both have the value 2 2 i . The first execution of outerloop2 results in y decreasing and y increasing. The first execution of innerloop2 results in z decreasing and z increasing. Then dec(next(s)); inc(next(s)) results in the counter at stage i + 1 in the chain s decreasing and s increasing (recall that the pointer is now at stage i). Then our run chooses to go to innernonzero2, decreases and increases z and goes back to innerloop2. This inner loop is repeated 2 2 i times, at the end of which the counter at stage i in the chain z has value 0, z has value 2 2 i and the counter at stage i + 1 in the chain s has been decremented 2 2 i times. Now our run chooses to go to innerzero2, where the first macro transfers the value of z into s at stage i. So, the counters at stage i in the chains s and z both have the value 2 2 i . Then inc(stack); dec(stack); sets stack to 1 at stage i and the control is transferred to "Dec". Since all the counters at or below stage i -1 have been initialised (they were initialised in the beginning and we did not touch any counter at or below stage i -1 so far) and the counter at stage i in the chain init is 1 (recall that all counters at stage i were initialised at the beginning and we have not touched init so far), we can apply the induction So our run now goes to "DecFinished" with s at stage i set to 0 and no other changes, and all the pointers in all the chains at stage i. At DecFinished, the control is transferred to "backtrack". Here the test (next(init) == 1) passes (since the counter at stage i + 1 in the chain init has the value 1) and so does (stack == 1) (since we increased stack at stage i before going to Dec) and so the control is transferred to outertest2. At outertest2, our run sets stack back to 0 and chooses to go to outernonzero2. Here, y is increased, then decreased and the control is transferred back to outerloop2. Here y is decreased and the whole innerloop is again executed to decrease s stage i + 1 2 2 i times. This way, the inner loop is executed 2 2 i times, each time decreasing y at stage i once and decreasing s at stage i + 1, 2 2 i times. At the end, s at stage i + 1 has been decremented 2 2 i × 2 2 i = 2 2 i+1 times and now our run chooses to go to outerzero2. Now, the first macro transfers the value of y into s at stage i. So, the counters at stage i in the chains s and y both have the value 2 2 i . Then the control is transferred to "Dec". Since all counters at or below stage i -1 have been initialised (they were initialised in the beginning and our calls to Dec till now left them intact by induction hypothesis) and the counter at stage i in the chain init is 1 (recall that all counters at stage i were initialised at the beginning and we have not changed init so far), we can apply the induction hypothesis. So our run now goes to "DecFinished" with s at stage i set to 0 and no other changes, and all the pointers in all the chains at stage i. At DecFinished, the control is transferred to "backtrack". Here the test (next(init) == 1) passes (since the counter at stage i + 1 in the chain init has the value 1) but the test (stack == 1) does not go through. So the control is transferred to outerexit2. Here, all the pointers are moved to stage i + 1 and the control is transferred to backtrack, exactly as stated in the lemma. Recall that we have reset the values in z and y back to 2 2 i , so we have not made any changes to any counter except decreasing the counter in the chain s at stage i + 1 by 2 2 i+1 . This proves the induction step and hence the lemma. Lemma 29. Suppose the control state is "begininit", all the pointers in all the chains are at stage 0 and all the counters at all stages have the value 0. For any i between 1 and N , there is a run ρ i ending at "initialise", such that the pointer is at stage i in all the chains and all the counters at or below stage i have been initialised.

Proof: By induction on i. For the base case i = 1, ρ 1 is the run that executes the instructions immediately after "begininit" and ends at "initialise". Now we assume the lemma is true up to i and prove it for i + 1. By induction hypothesis, there is a run ρ i ending at "initialise", with all the pointers in all the chains at stage i and all the counters at or below stage i initialised. The run ρ i+1 is obtained by appending the following sequence to ρ i . It uses the runs ρ i constructed from the previous lemma.

(outerinit; (innerinit; inc(next(y)); inc(next(z)); inc(next(s)); innertest1) 2 2 i ; innerzero1; transfer(z, s); ρ i ; DecFinished; backtrack; outertest1) 2 2 i ; outerzero1; transfer(y, s);ρ i ; DecFinished; backtrack; outerexit1; initialise Note that in the above run, we have omitted some instructions and program points but we have kept those that are the most essential for our reasoning.

The run ρ i is continued by testing if i is the last stage. If not, we go to "outerinit", decrement y, then go to "innerinit", decrement z, then increment the counters in the chains y, z and s at stage i + 1. Then our run chooses "innernonzero1", decrements and increments z and goes back to "innerinit". This inner loop is executed 2 2 i times, at the end of which the counter at stage i in the chain z has value 0, z has value 2 2 i and the counters at stage i + 1 in the chains y, z and s have been incremented 2 2 i times. Now our run chooses to go to innerzero1, where the first macro transfers the value of z into s at stage i. So, the counters at stage i in the chains s and z both have the value 2 2 i . Then inc(stack); dec(stack); sets stack to 1 at stage i and the control is transferred to "Dec". Since all the counters at or below stage i -1 have been initialised and the counter at stage i in the chain init is 1 (recall our convention that counters at stage i or below initialised implies that the counter in the chain init at stage i has the value 1), we can apply Lemma 28. So our run now goes to "DecFinished" with s at stage i set to 0 and no other changes, and all the pointers in all the chains at stage i. At DecFinished, the control is transferred to "backtrack". Here the test (next(init) == 1) does not go through and the test (stack == 1) passes, so control is transferred to "outertest1". At outertest1, our run sets stack back to 0 and chooses to go to outernonzero1. Here, y is increased, then decreased and the control is transferred back to outerloop1. Here y is decreased and the whole innerloop is again executed to increment y, z and s at stage i + 1 2 2 i times. This way, the inner loop is executed 2 2 i times, each time decreasing y at stage i once and incrementing y, z and s stage i + 1 2 2 i times. At the end, y, z and s at stage i + 1 have been incremented 2 2 i × 2 2 i = 2 2 i+1 times and now our run chooses to go to outerzero1. Now, the first macro at "outerzero1" transfers the value of y into s at stage i. So, the counters at stage i in the chains s and y both have the value 2 2 i . Then the control is transferred to "Dec". Since all counters at or below stage i -1 have been initialised (they were initialised in the beginning and our calls to Dec till now left them intact by Lemma 28) and the counter at stage i in the chain init is 1 , we can apply Lemma 28. So our run now goes to "DecFinished" with s at stage i set to 0 and no other changes, and all the pointers in all the chains at stage i. At DecFinished, the control is transferred to "backtrack". Here the test (next(init) == 1) does not go through and neither does the test (stack == 1). So the control is transferred to "outerexit1". Here, all the pointers are moved to stage i + 1, init and stack at stage i + 1 are set to 1 and the control is transferred to "initialise", exactly as in the lemma. This proves the induction step and hence the lemma.

The macros Nextstage and Prevstage move all the pointers in all the chains synchronously. Hence, in any run of the chain automaton, all the pointers are at the same stage. This condition can be temporarily violated while executing macros like inc(next(y)), but if all the pointers are at the same stage before the macro is executed, then any run that executes the macro is forced to regain the condition after the macro is executed (there is no non-deterministic choice inside the macro). Lemma 30. Suppose that in a configuration of the chain automaton, all the pointers in all the chains are at stage i, all the counters at or below stage i -1 have been initialised, the counter in the chain init at stage i has the value 1 and the control state is at "Dec". If any run starts from this configuration (say conf 1 ) and ends at a configuration conf 2 with control state at "DecFinished" and all pointers at stage i (with no other intermediate configurations satisfying these two properties), then the run decreases the counter in the chain s at stage i by 2 2 i . Proof: By induction on i. For the base case i = 1, if a run chooses the "else" branch of Dec, it gets stuck since the next instruction is to move all the pointers one stage down, which is not possible. So the run has to choose the only other option -the "if" branch, where it is forced to decrease s at stage 1 by 4 to reach "DecFinished". Now we assume the lemma is true up to i and prove it for i + 1. So suppose that in the configuration conf 1 , all the pointers are at stage i + 1, all the counters at or below stage i are initialised, the counter in the chain init at stage i + 1 is 1 and the control state is at Dec. Suppose a run starts at conf 1 and reaches conf 2 with the control state at "DecFinished" and all pointers at stage i + 1. First observe that if between conf 1 and conf 2 , the pointers are moved below stage i + 1, then the only way to get the pointers back to stage i + 1 is through the macro Nextstage at control state "outerexit2", which can only be executed if the control state was at "backtrack", which means before conf 2 , there is a configuration in which the control state is "DecFinished" and pointers are at stage i. Now let us track the instructions executed by this run. In the first transition after conf 1 , this run cannot choose the "if" branch of Dec since the test first(init)? does not go through. So the run goes to the "else" branch. It is forced to move all the pointers one stage down to i, decrement y and z at stage i, decrement s at stage i+1 and make a choice between "innernonzero2" and "innerzero2". If "innerzero2" is chosen at this stage, then in transfer(z, s), the value of s can be incremented at most once and then the control is forced to Dec. Then by induction hypothesis, no run can reach "DecFinished". So the only way to continue is to execute the innerloop2 2 2 i times, which requires decrementing s at stage i + 1 2 2 i times. At the end of this, when the control goes to Dec (after setting stack at stage i to 1), we know it has to reach "DecFinished" with pointers at stage i before reaching conf 2 . By induction hypothesis, we know that when the run first comes to "DecFinished" with pointers at stage i, it would have decreased s at stage i by 2 2 i . Now the control is forced to "backtrack", and then to "outertest2" (since init at stage i + 1 is 1 and we had set stack at stage i to 1). Here, the run is forced to set stack back to 0 and make a choice between outernonzero2 or outerzero2. As before, the run cannot continue if it chooses outerzero2 at this stage, so it is forced to choose outernonzero2. In fact, the run is forced to choose outernonzero2 2 2 i times, which forces decreasing s at stage i by 2 2 i+1 . At the end of this, the run is forced to choose outerzero2 (choosing outernonzero2 now will make the run get stuck since dec(y) no longer possible with y having the value 0), increment s at stage i 2 2 i times (to avoid getting stuck in the Dec that follows), go to Dec, then by induction hypothesis forced to go to DecFinished with s at stage i decreased by 2 2 i and all ther pointers at stage i. Now the control is forced to backtrack and then to outerexit2 (since init at stage i + 1 has the value 1 and stack at stage i has the value 0). Here, the pointers are moved one stage up to i + 1 and the control goes to DecFinished.

5) Concluding the Proof of Theorem 14: We give a reduction from the control state reachability problem for counter automata with zero tests with counters bounded by 2 2 N , where N = exp(k, n γ ) and n is the size of counter automaton. Without any loss of generality, we can assume that the initial counter values are equal zero (then these values will be updated during the initialization phase). Given such a counter automaton, we construct a chain automaton, with each chain having N counters. It will have the chains s, s, y, y, z, z, stack, stack, init and init required for zero tests as explained previously. There will be two more chains counters and counters to simulate the counters of the counter automaton. The right number of counters can be obtained by imposing that for every chain α, f (α) is set to n γ .

The initial state of the chain automaton is "begininit", the control state that launches the program for initialising the zero testing counters. The chain automaton will have all the control states of the counter automaton (in addition to others). The final state of the chain automaton is equal to the accepting state of the counter automaton. At the control state "beginsim", the chain automaton launches a program to initialise all the counters in the chain counters to 2 2 N , similar to the program for initialising the zero testing counters.

In order to initialize the first δ ≤ n counters from counters and counters that correspond to the counters of the original counter automaton, we replace the code for INC from the code for the initialization phase by the following one:

INC: inc(next(y)); inc(next(z)); inc(next(s)); next(init); if last(init)? then inc(counters); (next(counters);inc(counters)) δ-1 ; (prev(counters)) δ-1 ; prev(init); After initialization, the next control state will be the initial state of the counter automaton and the pointers of all the chains s, s, y, y, z, z, stack, stack, init will be at stage N = exp(k, n γ ). The pointers of the chains counters and counters will be at stage 0. From Lemma 29, there is a run that does all initialisations correctly and reaches the initial state of the counter automaton. From Lemma 30, any run that does not properly initialise all the counters gets stuck and hence will not reach the final state.

We denote the counters in the chains counters, counters by c 0 , c 0 , . . . , c δ-1 , c δ-1 . For every transition q, c j ← c j + 1, q of the counter automaton, the chain automaton will have the transition q, (next(counters); next(counters)) j ; inc(counters); dec(counters);

(prev(counters); prev(counters)) j , q Thus, for every incrementing transition of the counter automaton, the chain automaton can execute a corresponding incrementing transition. Conversely, for every incrementing transition executed by the chain automaton, the counter automaton can execute the corresponding incrementing transition.

For every transition q : if c j = 0 goto q 1 else c j ← c j -1 goto q 2 of the counter automaton, the chain automaton will have transitions corresponding to the following program. If the jth counter is equal to zero, then the content of the complement counter is equal to 2 2 N , which we transfer to s and then invoke Dec. We consider a slight variant of Dec so that the return address is q 1 after passing the zero-test successfully. In addition, since we need to restore the value of the complement counter, we perform a second transfer from the counter to s so that the total effect is null. q: goto nonzero or zero nonzero: (next(counters); next(counters)) j ; dec(counters); inc(counters); (prev(counters); prev(counters)) j ; goto q 2 zero: (next(counters); next(counters)) j ; transfer(counters, s); goto Dec zerorep zerorep: transfer(counters, s); goto Dec zeropass zeropass: (prev(counters); prev(counters)) j ; goto q 1 In the above, the control state Dec zerorep launches a program very similar to Dec explained previously, except that instead of backtrack, the following backtrack zerorep is called. backtrack zerorep : if (last(stack)?) then /* we are not at the end of recursion */ if (stack == 1) then goto outertest2 else goto outerexit2 else /* we are at the end of recursion */ goto zerorep fi The difference between backtrack and backtrack zerorep is that the later transfers control to zerorep after completion. The control state Dec zeropass launches a program very similar to Dec explained previously, except that instead of backtrack, backtrack zeropass is called, which transfers control to zeropass after completion. Now we explain the working of the above program in detail, starting from the state zero. If the value in the j th counter of the counter automaton is 0 when the control state is q, then the value in the counter at stage j of the chain counters in the chain automaton will have the value 2 2 N . The macro transfer(counters, s) will set the j th counter in the chain counters to 0 and set the j th counter in the chain counters to 2 2 N , while swapping the values of s and s at stage N = exp(k, n γ ). Then by Lemma 28, there is a run that swaps back the values of s and s at stage N and ends in the control state zerorep. Now the macro transfer(counters, s) will set the j th counter in the chain counters back to 2 2 N and set the j th counter in the chain counters back to 0 while swapping the values of s and s at stage N . Now the call to the decrementing algorithm at Dec zeropass swaps back the values of s and s at stage N and the control is at zeropass, with no changes in any of the counters. Hence, for any zero testing transition executed by the counter automaton, the chain automaton can execute the corresponding sequence of transitions. Conversely, by Lemma 30, for any run of the chain automaton that begins at q and ends at q 1 , the value of the j th counter in the chain counters was 2 2 N and hence the value of the j th counter in the chain counters was 0. Therefore, for any zero testing sequence of transitions executed by the chain automaton, the counter automaton can execute the corresponding zero testing transition.

We conclude that the chain automaton has a perfect run ending at its final state iff the counter automaton has an accepting run.

F. Proof of Lemma 15

Proof: Let A = Q, f, 1, Q 0 , Q F , δ be an chain system of level 1 with f : [1, n] → N, having thus n chains of counters, of respective size 2 f (1) , . . . , 2 f (n) .

The objective is to encode a word ρ ∈ δ * that represents an accepting run. For this, we use the alphabet δ of transitions, that we code using a logarithmic number of variables.

We encode a word ρ ∈ δ * that represents an accepting run. For this, we use the alphabet δ of transitions. Note that we can easily simulate the labels δ = {t 1 , . . . , t m } with the variables t 0 , . . . , t m , where a node has an encoding of the label t i iff the formula t i = t 0 ≈ t i holds true. We build a LRV formula ϕ so that there is an accepting gainy run ρ ∈ δ * of A if, and only if, there is a model σ so that σ |= ϕ and σ encodes the run ρ.

The following are standard counter-blind conditions to check. (a) Every position satisfies a for some a ∈ δ. (b) The first position satisfies (q 0 , instr, q) for some q 0 ∈ Q 0 , instr ∈ I, q ∈ Q. (c) The last position satisfies (q, instr, q ) for some q ∈ Q, instr ∈ I, q ∈ Q F . (d) There are no two consecutive positions i and i + 1 satisfying (q, u, q ) and (p, u , p ) respectively, with q = p. We use a variable x, and variables x α inc , x α dec , x α i for every chain α and i ∈ [1, f (α)]. Let us fix the bijections χ α : [0, 2 f (α) -1] → 2 [1,f (α)] for every α ∈ [1, n], that assign to each number m the set of 1-bit positions of the representation of m in base 2. We say that a position i is α-incrementing [resp. α-decrementing] if it satisfies (q, u, q ) for some q, q ∈ Q and u = inc(α) [resp. u = dec(α)].

In the context of a model σ with the properties (a)-(d), we say that a position i operates on the α-counter c, if χ α (c) = X i , where

X i = {b ∈ [1, f (α)] | σ(i)(x) = σ(i)(x α b )}. ( †)
Note that thus 0 ≤ c < 2 f (α) . For every chain α, let us consider the following properties: 'first(α)?', 'last(α)?', 'last(α)?'], we have c = 0

[resp. c = 0, c = 2 f (α) -1, c = 2 f (α) -1]. (3
) For every position i of σ operating on an α-counter c,

• if the position contains an instruction 'next(α)' [resp. 'prev(α)'], then the next position i + 1

operates on the α-counter c + 1 [resp. c -1],

• otherwise, the position i + 1 operates on the α-counter c. (4) For every α-incrementing position i of σ operating on an α-counter c there is a future α-decrementing position j > i operating on the same α-counter c, such that σ(i)(x α inc ) = σ(j)(x α dec ). Claim 31. There is a model satisfying the conditions above if, and only if, A has a gainy and accepting run.

Proof: (Only if) Suppose we have a model σ that verifies all the properties above. Since by [START_REF] Bojańczyk | Two-variable logic on data words[END_REF], all the positions have different data values for x α dec , it then follows that the position j to which property (4) makes reference is unique. Since, also by [START_REF] Bojańczyk | Two-variable logic on data words[END_REF], all the positions have different data values for x α inc , we have that the α-decrement corresponds to at most one α-increment position in condition (4). Moreover, it is an α-decrement of the same counter, that is, X i = X j (cf. ( †)). For these reasons, for every α-increment there is a future α-decrement of the same counter which corresponds in a unique way to that increment. More precisely, for every chain α, the function

γ α σ : {0 ≤ i < |σ| : i is α-incrementing} → {0 ≤ i < |σ| : i is α-decrementing} where γ α σ (i) = j iff σ(i)(x α inc ) = σ(j)(x α dec
) is well-defined and injective, and for every γ α σ (i) = j we have that j > i and X i = X j .

Consider ρ ∈ δ * as having the same length as σ and such that ρ(i) = (q, instr, q ) whenever σ, i |= (q, instr, q ) . From conditions (2) and (3), it follows that the counter c α i corresponding to position i from ρ, is equal to χ -1 (X i ). Therefore, the functions {γ α σ } α∈ [1,n] witness the fact that ρ is a gainy and accepting run of A.

(If) Let us now focus on the converse, by exhibiting a model satisfying the above properties, assuming that A has an accepting gainy run ρ ∈ δ * . We therefore have, for every α ∈ [1, n], an injective function

γ α : {i | ρ(i) is α-incrementing} → {i | ρ(i) is α-decrementing}
where for every γ(i) = j we have that j > i and c α i = c α j . We build a model σ of the same length of ρ, and we now describe its data values. Let us fix two distinct data values d, e. For any position i, we have σ(i)(l 0 ) = d; and σ(i)(l j ) = d if j ∈ λ(ρ[i]), and σ(i)(l j ) = e otherwise. In this way we make sure that the properties (a)-(d) hold.

We use distinct data values d 0 , . . . , d |σ|-1 and d 0 , . . . , d |σ|-1 (all different from d, e). We define the data values of the remaining variables for any position i:

• For every α, σ(i)(x α inc ) = d i . • For every α, -if i is α-decrementing, we define σ(i)(x α dec ) = σ(i )(x α inc ) where i = (γ α ) -1 (i); if such (γ α ) -1 (i) does not exist, then σ(i)(x α dec ) = d i ; -otherwise, if i is not α-decrementing, σ(i)(x α dec ) = d i . • σ(i)(x) = d. • For every α, σ(i)(x α l ) = σ(i)(x) = d if l ∈ χ(c α i ), otherwise σ(i)(x α l ) = e.
Observe that these last two items ensure that the properties (2) and (3) hold.

By definition, every position of σ has a different data value for x α inc . Let us show that the same holds for x α dec . Note that at any position i, x α dec has: the data value of σ(i )(x α inc ) = d i for some i < i; or the data value d i . If there were two positions i < j with σ(i)(x α dec ) = σ(j)(x α dec ) it would then be because: (i) d i = d j ; (ii) d i = d j for some i < i; (iii) d i = d j for some j < j; or (iv) d i = d j for some i < i, j < j. It is evident that none of (i), (ii), (iii) can hold since all d 0 , . . . , d |σ|-1 , d 0 , . . . , d |σ|-1 are distinct. For this reason, if (iv) holds, it means that i = j , and hence that (γ α ) -1 (i) = (γ α ) -1 (j), implying that γ α is not injective, which is a contradiction. Hence, all the positions have different data values for x α dec . Therefore, σ has the property (1). To show that σ has property (4), let i be a α-incrementing position of σ, remember that σ(i)(x α inc ) = d i . Note that position γ α (i) = j must be α-decrementing on the same counter. By definition of the value of x α dec , we have that σ(j)(x α dec ) must be equal to σ((γ α (j)) -1 )(x α inc ) = σ(i)(x α inc ) = d i . Thus, property (4) holds.

We complete the reduction by showing that all the properties expressed before can be efficiently encoded in our logic. Claim 32. Properties (a)-(d) and ( 1)-( 4) can be expressed by formulas of LRV, that can be constructed in polynomial time in the size of A.

Proof: Along the proof, we use the following formulas, for any α ∈

[1, n] and i ∈ [1, f (α)], bit α i def = x ≈ x α i .
We now show how to code each of the properties.

• Properties (a)-(d) are easy to express in LRV and present no complications.

• For expressing (1), we force x α inc and x α dec to have a different data value for every position of the model with the formula 2) is straightforward to express in LRV.

¬F x α inc ≈ ? x α inc ∧ ¬F x α dec ≈ ? x α dec . • Property (
• We express property (3) by first determining which is the bit i that must be flipped for the increment of the counter pointer of the chain α.

flip α i = ¬bit α i ∧ j>i bit α j
Then by making sure that all the bits before i are preserved.

copy α i = j<i (bit α j ⇔ X(bit α j ))
And by making every bit greater or equal to i be a zero.

zero α i = j>i X(¬bit α j )
And finally by swapping bit i.

swap α i = X bit α i
Hence, the property to check is, for every α ∈ [1, n],

(q,next(α),q )∈δ

(q, next(α), q ) ⇒ i∈[1,n] flip α i ⇒ copy α i ∧ zero α i ∧ swap α i .
The formula expressing the property for decrements of counter pointers (prev(α)) is analogous.

• Finally, we express property (4) by testing, for every α-incrementing position,

x α inc ≈ α-dec? x α dec where α-dec = (q,dec(α),q )∈δ (q, dec(α), q )

and for every

i ∈ [1, f (α)], bit α i ⇒ x α inc ≈ bit α i ? x α dec ∧ ¬bit α i ⇒ x α inc ≈ ¬bit α i ? x α dec .
If the α-increment has some data value d at variable x α inc , there must be only one future position j where x α dec carries the data value d -since every x α dec has a different value, by [START_REF] Bojańczyk | Two-variable logic on data words[END_REF]. For this reason, both positions (the α-increment and the α-decrement) operate on the same counter, and thus the formula faithfully expresses property (4).

As a corollary of Claims 31 and 32 we obtain a polynomial-time reduction from Gainy(1) into the satisfiability problem for LRV(X, F).

G. Proof of Proposition 16

Proof: (I) The developments from Section IV-A apply to the infinite case and since PLRV ω is shown decidable in [START_REF] Demri | Temporal logics of repeating values[END_REF], we get decidability of the satisfiability problem for PLRV ω . (II) First, note that LRV ω is 2EXPSPACE-hard. Indeed, there is a simple logarithmic-space reduction from the satisfiability problem for LRV into the satisfiability problem for LRV ω , which can be performed as for standard LTL. Indeed, it is sufficient to introduce two new variables x new and y new , to state that x new ≈ y new is true at a finite prefix of the model (herein x new ≈ y new plays the role of a new propositional variable) and to relativize all the temporal operators and obligations to positions on which x new ≈ y new holds true.

Concerning the complexity upper bound, from Section IV-A, we can conclude that there is a polynomial-time reduction from LRV ω to LRV ω . The satisfiability problem for LRV ω is shown decidable in [START_REF] Demri | Temporal logics of repeating values[END_REF] and we can adapt developments from Section IV-B to get also an 2EXPSPACE upper bound for LRV ω . This is the purpose of the rest of the proof.

By analyzing the constructions from [6, Section 7], one can show that φ built over the variable {x 1 , . . . , x k } is LRV ω satisfiable iff there are Z ⊆ P + ({x 1 , . . . ,

x k }), a VASS A Z φ = Q, Z, δ along with sets Q 0 , Q f ⊆ Q of initial
and final states and a Büchi automaton B Z such that: 1) A Z φ is the restriction of A φ defined in Section IV-B and q 0 , 0 * -→ q f , 0 in A Z φ for some q 0 ∈ Q 0 and q f ∈ Q f . 2) B Z accepts a non-empty language.

By similar arguments from Section IV-B, existence of a run q 0 , 0 * -→ q f , 0 can be checked in 2EXPSPACE. Observe that in the construction in [6, Section 7], counters in P + ({x 1 , . . . , x k }) \ Z are also updated in A Z φ (providing the VASS A φ ) but one can show that this is not needed because of optional decrement condition and because B Z is precisely designed to take care of the future obligations in the infinite related to the counters in P + ({x 1 , . . . , x k }) \ Z. B Z can be built in exponential time and it is of exponential size in the size of φ. Hence, non-emptiness of B Z can be checked in EXPSPACE. Finally, the number of possible Z is only at most double exponential in the size of φ, which allows to get a nondeterministic algorithm in 2EXPSPACE and provides a 2EXPSPACE upper bound by Savitch's Theorem.

H. Proof of Theorem 17

Proof: 2EXPSPACE-hardness is inherited from LRV. In order to establish the complexity upper bound, first note that LTL extended with a fixed finite set of MSO-definable temporal operators preserves the nice properties about LTL (see e.g. [START_REF] Gastin | Satisfiability and model checking for MSOdefinable temporal logics are in PSPACE[END_REF]):

• Model-checking and satisfiability problems are PSPACE-complete.

• Given a formula φ from such an extension, one can build a Büchi automaton A φ accepting exactly the models for φ and the size of A φ is in O(2 p(|φ|) ) for some polynomial p(•) (depending on the finite set of MSO-definable operators).

All the results hold because the set of MSO-definable operators is finite and fixed, otherwise the complexity for satisfiability and the size of the Büchi automata are of non-elementary magnitude in the worst case. Moreover, this holds for finite and infinite models.

In order to obtain the 2EXPSPACE, the following properties are now sufficient:

1) Following developments from Section IV-A, it is straightforward to show that there is a logarithmicspace reduction from the satisfiability problem for LRV+{⊕ 1 , . . . , ⊕ N } into the satisfiability problem for LRV + {⊕ 1 , . . . , ⊕ N }. 2) By combining [START_REF] Gastin | Satisfiability and model checking for MSOdefinable temporal logics are in PSPACE[END_REF] and [6, Theorem 4], a formula φ in LRV + {⊕ 1 , . . . , ⊕ N } is satisfiable iff q 0 , 0 * -→ q f , 0 for some q 0 ∈ Q 0 and q f ∈ Q f in some VASS A φ such that the number of states in exponential in |φ|. The relatively small size for A φ is due to the fact that A φ is built as the product of a VASS checking obligations (of exponential size in the number of variables and in the size of the local equalities) and of a finite-state automaton accepting the symbolic models of φ of exponential size thanks to [START_REF] Gastin | Satisfiability and model checking for MSOdefinable temporal logics are in PSPACE[END_REF] (see also more details in Section IV-B) . By using arguments from Section IV-B, we can then reduce existence of a run q 0 , 0 * -→ q f , 0 to an instance of the control state reachability problem in some VASS of linear size in the size of A φ , whence the 2EXPSPACE upper bound.

I. Proof of Theorem 18

Proof: Again, 2EXPSPACE-hardness is inherited from LRV. In order to get the 2EXPSPACE, we use arguments from Proposition 19. Indeed, the decidability proof from [6, Theorem 4] can be adapted to LRV + Now. The only difference is that the finite-state automaton is of double exponential size, see details below. Despite this exponential blow-up, the 2EXPSPACE upper bound can be preserved.

Let φ be a formula with k variables. There exist a VASS A dec = Q, C, δ and Q 0 , Q f ⊆ Q such that φ is satisfiable iff there are q f ∈ Q f and q 0 ∈ Q 0 such that q f , 0 * -→ q 0 , v for some counter valuation v. Note that the number of counters in A dec is bounded by 2 k , card(Q) is double exponential in |φ| and the maximal value for an update in a transition of A dec is k. Indeed, a formula from Past LTL+Now is equivalent to a Büchi automaton of double exponential size in its size [START_REF] Laroussinie | Temporal logic with forgettable past[END_REF]. Moreover, deciding whether a state in Q belongs to Q 0 [resp. Q f ] can be checked in exponential space in |φ| and δ can be decided in exponential space too. By using [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF] (see also 2 ), we can easily conclude that q f , 0 * -→ q 0 , v for some counter valuation v iff q f , 0 * -→ q 0 , v for some v such that the length of the run is bounded by p(|A dec | + max(A dec )) α(k) where p(•) is a polynomial, α is a map of double exponential growth and max(A dec ) denotes the maximal absolute value in an update (bounded by k presently). In order to take advantage of the results on VAS, we use the translation from VASS to VAS introduced in [START_REF] Hopcroft | On the reachability problem for 5dimensional vector addition systems[END_REF]: if a VASS has N 1 control states, the maximal absolute value in an update is N 2 and it has N 3 counters, then we can build a VAS (being able to preserve coverability properties) such that it has N 3 + 3 counters, the maximal absolute value in an update is max(N 2 , N 2 1 ). From A dec , we can indeed build an equivalent VAS with a number of counters bounded by 2 k + 3 and with a maximal absolute value in an an update at most double exponential in the size of |φ|. So, the length of the run is at most triple exponential in |φ|. Consequently, the satisfiability problem for LRV + Now is in 2EXPSPACE.

J. Proof of Proposition 19

Proof of Proposition 19: PSPACE-hardness is due the fact that LTL with a single propositional variable is PSPACE-hard, which can be easily simulated with the atomic formula x ≈ y. Let k ≥ 1 be some fixed value and φ ∈ LRV k . In the proof of Theorem 9, we have seen that there exist a VASS A dec = Q, C, δ and Q 0 , Q f ⊆ Q such that φ is satisfiable iff there are q f ∈ Q f and q 0 ∈ Q 0 such that q f , 0 * -→ q 0 , v for some counter valuation v. Note that the number of counters in A dec is bounded by 2 k , card(Q) is exponential in |φ| and the maximal value for an update in a transition of A dec is k. Moreover, deciding whether a state in Q belongs to Q 0 [resp. Q f ] can be checked in polynomial space in |φ| and δ can be decided in polynomial space too. By using [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF] (see also 3 ), we can easily conclude that q f , 0 * -→ q 0 , v for some counter valuation v iff q f , 0 * -→ q 0 , v for some v such that the length of the run is bounded by p(|A dec | + max(A dec )) α(k) where p(•) is a polynomial, α is a map of double exponential growth and max(A dec ) denotes the maximal absolute value in an update (bounded by k presently). Since k is fixed, the length of the run is at most exponential in |φ|. Consequently, the following polynomial-space nondeterministic algorithm allows to check whether φ is satisfiable. Guess q f ∈ Q f , q 0 ∈ Q 0 and guess on-the-fly a run of length at most p(|A dec | + max(A dec )) α(k) from q f , 0 to some q 0 , v . Note that counter valuations can be represented in polynomial space too. By Savitch's Theorem, we conclude that the satisfiability problem for LRV k is in PSPACE.

K. Proof of Lemma 20

Proof of Lemma 20: The idea of the coding is the following. Suppose we have a formula ϕ ∈ LRV using k variables x 1 , . . . , x k so that σ |= ϕ.

We will encode σ in a model σ ϕ that encodes in only one variable, say x the whole model of σ restricted to x 1 , . . . , x k . To this end, σ ϕ is divided into N segments s 1 • • • s N of equal length, where N = |σ|. A special fresh data value is used as a special constant. Suppose that d is a data value that is not in σ. Then, each segment s i has length k = 2k + 1, and is defined as the data values "d d 1 d d 2 . . . d d k d", where d j = σ(i)(x j ). Figure 7 contains an example for k = 3 and N = 3. In fact, we can force what the model has this shape with LRV 1 . Note that with this coding, we can tell that we are between two segments if there are two consecutive equal data values. In fact, we are at a position corresponding to x i (for i ∈ [1, k]) inside a segment if we are standing at the 2i-th element of of some extra variables). For such a model σ, let σ Σ (resp. σΣ) be the model obtained by restricting σ to positions labelled by Σ (resp. Σ). If u i1 • • • u im = v i1 • • • v im is a solution to pcp, the idea is to construct a LRV model whose projection to Σ ∪ Σ is u i1 v i1 • • • u im v im . To check that such a model σ actually represents a solution, we will write LRV vec (X, U) formulas to say that "for all j, if the j th position of σ Σ is labelled by a, then the j th position of σΣ is labelled by ā".

The main difficulty is to get a handle on the j th position of σ Σ . The difficulty arises since the LRV model σ is an interleaving of σ Σ and σΣ. This is handled by using two variables x and y. Positions 1 and 2 of σ Σ will have the same value of x, positions 2 and 3 will have the same value of y, positions 3 and 4 will have the same value of x and so on. Generalising, odd positions of σ Σ will have the same value of x as in the next position of σ Σ and the same value of y as in the previous position of σ Σ . Even positions of σ Σ will have the same value of x as in the previous position of σ Σ and the same value of y as in the next position of σ Σ . To easily identify odd and even positions, an additional label is introduced at each position, which can be O or E. The sequence σ Σ looks as follows.

    x Odd/Even Letter y     :     d 1 O in a 1 d 1         d 1 E a 2 d 2         d 3 O a 3 d 2         3 E a 4 d 4     • • •     d m-1 O a m-1 d m-2         d m-1 E fi a m d m     ( )
We assume that the atomic formula a (a ∈ Σ) is true at some position j of a model σ iff the position j is labelled by the letter a. We denote a∈Σ a by Σ. For a word u ∈ Σ * , we denote by φ i u the LRV formula that ensures that starting from i positions to the right of the current position, the next |u| positions are labelled by the respective letters of u (e.g., φ 3 abb def ≡ X 3 a ∧ X 4 b ∧ X 5 b). We enforce a model of the form ( ) above through the following formulas.

(1) The projection of the labeling of σ on to Σ ∪ Σ is in (u 1 v 1 + u 2 v 2 ){u i vi | i ∈ [n]} * : to facilitate writing this condition in LRV, we introduce two new variables z 1 b , z 2 b such that at any position, they have the same value only if that position is not the starting point of some pair u i v i . The same condition for σΣ, enforced with a formula similar to the one above. b)

z 1 b ≈ z 2 b ∧ i∈{1,2} (φ 0 ui ∧ φ |ui|+1 vi ∧ (X |uivi|+1 ⇒ X |uivi|+1 z 1 b ≈ z 2 b )) ∧ G   z 1 b ≈ z 2 b ∨ i∈[1,n] (φ 0 ui ∧ φ |ui|+1 vi ) ∧ (X |uivi|+1 ⇒ X |uivi|+1 z 1 b ≈ z 2 b )   (
σ Σ projected onto {O, O in , E, E fi } is in O in (EO) * E fi . O in ∧ G (O ∨ O in ) ⇒ ΣU(Σ ∧ (E ∨ E fi )) ∧ G E ⇒ ΣU(Σ ∧ O) ∧ G(E fi ⇒ ¬XFΣ) σΣ projected onto { Ō, O in , Ē, E fi } is in O in ( Ē Ō) * E fi . ΣUO in ∧ G ( Ō ∨ O in ) ⇒ ΣU( Σ ∧ ( Ē ∨ E fi )) ∧ G Ē ⇒ ΣU( Σ ∧ Ō) ∧ G(E fi ⇒ ¬X ) c)
For every position i of σ Σ labelled by O or O in , there exists a future position j > i of σ Σ labelled by E or E fi so that σ Σ (i)(x) = σ Σ (j)(x).

G ((O ∨ O in ) ⇒ x ≈ Σ ∧ (E ∨ E fi )? x)
For every position i of σΣ labelled by Ō or O in , there exists a future position j > i of σΣ labelled by Ē or E fi so that σΣ(i)(x) = σΣ(j)(x) (enforced with a formula similar to the one above). d) For every position i of σ Σ labelled by E, there exists a future position j > i of σ Σ labelled by O so that σ Σ (i)(y) = σ Σ (j)(y).

G (E ⇒ y ≈ Σ ∧ O? y)

For every position i of σΣ labelled by Ē, there exists a future position j > i of σΣ labelled by Ō so that σΣ(i)(y) = σΣ(j)(y) (enforced with a formula similar to the one above).

(3) For any position i of u i1 , the corresponding position j in v i1 • • • v im (which always happens to be in v i1 MPCP dir , since |u i1 | ≤ 2 and |v i1 | ≥ 3) should satisfy σ(i)(x) = σ(j)(x) and σ(i)(y) = σ(j)(y).

In addition, position i is labelled with a ∈ Σ iff position j is labelled with ā ∈ Σ. (5) If i and j are the last positions labeled with Σ and Σ respectively, then σ(i)(x) = σ(j)(x) and σ(i)(y) = σ(j)(y). In addition, position i is labelled with a ∈ Σ iff position j is labelled with ā ∈ Σ. Given an instance pcp of MPCP dir , the required formula φ pcp is the conjunction of all the formulas above. Lemma 35. Given an instance pcp of MPCP dir , φ pcp is satisfiable iff pcp has a solution.

Proof:

Suppose u i1 • • • u im = v i1 • • • v im is a solution of pcp.
It is routine to check that, with this solution, a model satisfying φ pcp can be built. Now suppose that φ pcp has a satisfying model σ. From condition (1), we get a sequence

u i1 v i1 • • • u im v im . It is left to prove that u i1 • • • u im = v i1 • • • v im .
Let σ Σ (resp. σΣ) be the model obtained from σ by restricting it to positions labeled with Σ (resp. Σ). Construct a directed graph whose vertices are the positions of σ Σ and there is an edge from i to j iff i < j and σ Σ (i)(x) = σ Σ (j)(x) or σ Σ (i)(y) = σ Σ (j)(y). We claim that the set of edges of this directed graph represents the successor relation induced on σ Σ by σ. To prove this claim, we first show that all positions have in degree 1 (except the first one, which has in degree 0) and that all positions have out degree 1 (except the last one, which has out degree 0). Indeed, condition (2a) ensures that for any position, both the in degree and out degree are at most 1. From conditions (2b), (2c) and (2d), each position (except the last one) has out degree at least 1. Hence, all positions except the last one have out degree exactly 1. By the definition of the set of edges, the last position has out degree 0. If more than one position has in degree 0, it will force some other position to have in degree more than 1, which is not possible. By the definition of the set of edges, the first position has in degree 0 and hence, all other positions have in degree exactly 1. To finish proving the claim (that the set of edges of our directed graph represents the successor relation induced on σ Σ by σ), we will now prove that at any position of σ Σ except the last one, the outgoing edge goes to the successor position in σ Σ . If this is not the case, let i be the last position where this condition is violated. The outgoing edge from i then goes to some position j > i + 1. Since the outgoing edges from each position between i + 1 and j -1 go to the respective successors, position j will have in degree 2, which is not possible.

Next we will prove that there cannot be two positions of σ Σ with the same value for variables x and y. Suppose there were two such positions and the first one is labeled O (the argument for E is similar). If the second position is also labeled O, then by condition (2c), there is at least one position labeled E with the same value for variable x, so there are three positions with the same value for variable x, violating condition (2a). Hence, the second position must be labelled E. Then by condition (2d), there is a position after the second position with the same value for variable y. This implies there are three positions with the same value for variable y, again violating condition (2a). Therefore, there cannot be two positions of σ Σ with the same value for variables x and y.

Finally, we prove that for every position i of σΣ, if a i is its label, then the unique position in σ Σ with the same value of x and y is position i of σ Σ and carries the label a i . For 1 ≤ i ≤ |u i1 |, this follows from condition [START_REF] Bollig | Model checking languages of data words[END_REF]. For i = |u i1 • • • u im |, this follows from condition [START_REF] David | Analyse de XML avec données non-bornées[END_REF]. The rest of the proof is by induction on i. The base case is already proved since |u i1 | ≥ 1. For the induction step, assume the result is true for all positions of σΣ up to position i. Supppose position i of σΣ is labeled by Ō (the case of Ē is symmetric). Then by induction hypothesis and (2b), position i of σ Σ is labeled by O (or O in , if i = 1). By condition (2c) and the definition of edges in the directed graph that we built, position i + 1 of σΣ (resp. σ Σ ) has same value of x as that of position i. We know from the previous paragraph that there is exactly one position of σ Σ with the same value of x and y as that of position i + 1 in σΣ. This position in σ Σ cannot be i or before due to induction hypothesis. If it is not i + 1 either, then there will be three positions of σ Σ with the same value of x, which violates condition (2a). Hence, the position of σ Σ with the same value of x and y as that of position i + 1 in σΣ is indeed i + 1 and it carries the label a i by condition (4).

As a conclusion, the satisfiability problem for LRV vec (X, U) is undecidable.

M. Implications for Logics on Data Words 1) First Order Logic: Proof of Proposition 24: Through a standard translation we can bring any formula of forward-EMSO 2 (+1, <, ∼) into a formula of the form ϕ = ∃X 1 , . . . , X n ∀x∀y χ ∧ k ∀x∃y (x ≤ y ∧ ψ k ) that preserves satisfiability, where χ and all ψ k 's are quantifier-free formulas, and there are no tests for labels. Furthermore, this is a polynomial-time translation. This translation is just the Scott normal form of EMSO 2 (+1, <, ∼) [START_REF] Bojańczyk | Two-variable logic on data words[END_REF] adapted to forward-EMSO 2 (+1, <, ∼), and can be done in the same way.

We now give an exponential-time translation tr : forward-EMSO 2 (+1, <, ∼) → LRV. For any formula ϕ of forward-EMSO 2 (+1, <, ∼), tr(ϕ) is an equivalent (in the sense of satisfiability) LRV formula, whose satisfiability can be tested in 2EXPSPACE (Corollary 10). This yields an upper bound of 3EXPSPACE for forward-EMSO 2 (+1, <, ∼).

The translation makes use of: a distinguished variable x that encodes the data values of any data word satisfying ϕ; variables x 0 , . . . , x n that are used to encode the monadic relations X 1 , . . . , X n ; and a variable x prev whose purpose will be explained later on. We give now the translation. To translate ∀x∀y χ, we first bring the formula to a form

Fig. 1 .

 1 Fig. 1. Automaton constructions from [6] (top) and from this paper (bottom).

Fig. 2 .

 2 Fig. 2.Control flow of algorithm that decrements s i 2 2 i times.

1 Fig. 3 .

 13 Fig. 3. Example of the reduction from SAT(LRV ) into SAT(LRV 1 ), for k = 3, N = 3 and d = 5.

  (a) |σ| = |σ ϕ |; (b) for every 0 ≤ i < |σ| and x ∈ vars(ϕ), σ(i)(x) = σ ϕ (i)(x); (c) there is some data value d ∈ {σ(i)(x) | x ∈ vars(ϕ), 0 ≤ i < |σ|} such that for every 0 ≤ i < |σ ϕ |, σ ϕ (i)(k) = d; (d) for every 0 ≤ i < |σ|, x ∈ vars(ϕ), and ψ ∈ sub (ϕ),

Fig. 4 .

 4 Fig. 4. Algorithm for decrementing s i 2 2 i

Fig. 5 .

 5 Fig. 5. Algorithm for initializing y i-1 , z i-1

  Dec:if first(stack)? then (dec(s))4 ; (inc(s))4 ; goto DecFinished else Prevstage outerloop2: dec(y); inc(y) /* y is the index for outer loop */ innerloop2: dec(z); inc(z) /* z is the index for inner loop */ dec(next(s)); inc(next(s)) innertest2: goto innernonzero2 or innerzero2 innernonzero2: dec(z); inc(z); goto innerloop2 /* inner loop not yet complete */ innerzero2: transfer(z, s); inc(stack); dec(stack); goto Dec /* inner loop complete. Assume control magically goes to outertest2 */ outertest2: dec(stack); inc(stack); goto outernonzero2 or outerzero2 outernonzero2: dec(y); inc(y); goto outerloop2 /* outer loop not yet complete */ outerzero2: transfer(y, s); goto Dec /* outer loop complete. Assume control magically goes to outerexit2 */ outerexit2: Nextstage; goto DecFinished fi DecFinished: goto backtrack backtrack: if (last(stack)?) then if (stack == 1) then goto outertest2 else goto outerexit2 else goto Next control state fiIn the diagram below, we explain how the "magical transfers" happen after recursive calls to "Dec".

Fig. 6 .

 6 Fig.6. Depiction of the flow of the Dec procedure. In the figure we simplify some of the instructions, for example instead of dec(s); inc(s) we just put s--, instead of dec(z); inc(z) we just put z > 0?, etc.

( 1 )

 1 Any two positions of σ have different values of x α inc [resp. of x α dec ]. (2) For every position i of σ operating on an α-counter c containing an instruction 'first(α)?' [resp.

  2) a) For every data value d, there are at most two positions i, j in σ Σ with σΣ (i)(x) = σ Σ (j)(x) = d or σ Σ (i)(y) = σ Σ (j)(y) = d. G (Σ ⇒ (¬x ≈ Σ? x) ∨ (x ≈ Σ ∧ (¬x ≈ Σ? x? x)))∧G (Σ ⇒ (¬y ≈ Σ? y) ∨ (y ≈ Σ ∧ (¬y ≈ Σ? y? y)))

a∈Σ(O( 4 )

 4 in ∧ a) ⇒ x, y ≈ O in ∧ a? x, y ∧ XΣ ⇒ a∈Σ Xa ∧ X 3 a ∧ X(x ≈ X 2 x ∧ y ≈ X 2 y) For any position i of σ with 2|u i1 | < i < |u i1 • • • u im |, if it is labeled with ā ∈ Σ, there is a future position j > i labeled with a ∈ Σ such that σ(i)(x) = σ(j)(x) and σ(i)(y) = σ(j)(y). The following formula assumes that |u i1 | ≤ 2, as it is in MPCP dir . XΣ ⇒ ΣU   X 2 G ā∈ Σ (ā ∧ ¬E fi ) ⇒ (x, y) ≈ a? (x, y)   (XΣ is true when |u i1 | = 2) ∧ X Σ ⇒ ΣU   XG ā∈ Σ (ā ∧ ¬E fi ) ⇒ (x, y) ≈ a? (x, y)   (X Σ is true when |u i1 | = 1)

  ∧ a) ⇒ x, y ≈ E fi ∧ a? x, y

  m∈M ¬∃x∃y x ≤ y ∧ χ m ∧ χ x m ∧ χ y m , ( )where every χ x m (resp. χ y m ) is a conjunction of (negations of) atoms of monadic relations on x (resp. y); and χ m = µ ∧ ν where µ ∈ {x=y, +1(x, y), ¬(+1(x, y) ∨ x=y)} and ν ∈ {x ∼ y, ¬(x ∼ y)}. Claim 36. ∀x∀y χ can be translated into an equivalent formula of the form ( ) in exponential time.Proof:As an example, if χ = ¬(x ∼ y) ∨ X(x) ∨ X(y),then the corresponding formula would be µ,χ x ,χ y (¬∃x∃y x ≤ y ∧ µ ∧ ¬X(x) ∧ χ y ) ∧ (¬∃x∃y x ≤ y ∧ µ ∧ χ x ∧ ¬X(y))

  /* z is the index for inner loop */ goto outerinit /* outer loop not yet complete */ outerzero1: transfer(y, s); goto Dec /* outer loop complete. Assume control magically goes to outerexit1 */ outerexit1: Nextstage; inc(init); inc(stack); goto initialise beginsim: start simulating the counter machine (details follow but this is standard)

	INC: inc(next(y)); inc(next(z)); inc(next(s)) innertest1: goto innernonzero1 or innerzero1 innernonzero1: dec(z); inc(z); goto innerinit /* inner loop not yet complete */ innerzero1: transfer(z, s); inc(stack); dec(stack); goto Dec /* inner loop complete. Assume control
	magically goes to outertest1 */
	outertest1: dec(stack); inc(stack); goto outernonzero1 or outerzero1
	outernonzero1: dec(y); inc(y); Dec:
	if first(init)? then
	(dec(s)) 4 ; (inc(s)) 4 ; goto DecFinished
	else
	Prevstage
	outerloop2: dec(y); inc(y) magically goes to outertest2 */
	outertest2: dec(stack); inc(stack); goto outernonzero2 or outerzero2 outernonzero2: dec(y); inc(y); goto outerloop2 /* outer loop not yet complete */ outerzero2: transfer(y, s); goto Dec /* outer loop complete. Assume control magically goes to outerexit2 */ outerexit2: Nextstage; goto DecFinished
	fi DecFinished: goto backtrack
	backtrack:
	if (next(init) == 1) then /* we are not at the end of recursion */
	if (stack == 1) then goto outertest2 else goto outerexit2
	else /* we are at the end of recursion */
	if (stack == 1) then goto outertest1 else goto outerexit1
	fi
	The control flow of the Dec procedure is presented in Figure 6.

/* y is the index for outer loop */ innerloop2: dec(z); inc(z) /* z is the index for inner loop */ dec(next(s)); inc(next(s)) innertest2: goto innernonzero2 or innerzero2 innernonzero2: dec(z); inc(z); goto innerloop2 /* inner loop not yet complete */ innerzero2: transfer(z, s); inc(stack); dec(stack); goto Dec /* inner loop complete. Assume control

Indeed, note that one can easily test whether a word is accepted by a finite automaton with the help of a monadic relation X fst that holds only at the first position. Further, the property of X fst can be expressed in forward-EMSO

[START_REF] Bojańczyk | An extension of data automata that captures XPath[END_REF] (+1, <, ∼) as (∃y . X fst (y)) ∧ (∀x∀y . x < y → ¬X fst (y)).

S. Demri, M. Jurdziński, O. Lachish, and R. Lazić. The covering and boundedness problems for branching VAS. JCSS, 79(1):23-38, 2013.

S. Demri, M. Jurdziński, O. Lachish, and R. Lazić. The covering and boundedness problems for branching VAS. JCSS, 79(1):23-38, 2013.

a segment, and we can test this with the formula

Using these formulas γ i , we can translate any test x i ≈ ? x j into a formula that 1) moves to the position 2i of the segment (the one corresponding to the x i data value), 2) tests x ≈ γ j ? x.

We can do this similarly with all formulas.

Let us now explain in more detail how to do the translation, and why it works.

Consider the following property of a given position i multiple of k of a model σ ϕ :

• for every 0 ≤ j ≤ k -1, σ ϕ (i + j)(x) = σ ϕ (i)(x) if, and only if, j is even, and

. This property can be easily expressed with a formula

Note that this formula tests that we are standing at the beginning of a segment in particular. It is now straightforward to produce a LRV 1 formula that tests

• σ ϕ , 0 |= segment-k • for every position i so that σ ϕ (i)(x) = σ ϕ (i + 1)(x), we have σ, i + 1 |= segment-k . Let us call many-segments the formula expressing such a property. Note that the property implies that σ ϕ is a succession of segments, as the one of Figure 7.

We give now the translation of a formula ϕ of LRV with k variables into a formula ϕ of LRV 1 with 1 variable.

(and similarly for ≈)

Now we have to translate x i ≈ ? x j . This would be translated in our encoding by saying that the i-th position of the current segment is equal to the j-th position of a future segment. Note that the following formula ξ i,j = X 2i-1 (x ≈ γ j ? x)

does not exactly encode this property. For example, consider that we would like to test x 2 ≈ ? x 3 at the first element of the model σ ϕ depicted in Figure 7. Although ξ holds, the property is not true, there is no future segment with the data value 1 in the position encoding x 3 . In fact, the formula ξ encodes correctly the property only when x i ≈ x j . However, this is not a problem since when x i ≈ x j the formula x i ≈ ? x j is equivalent to x j ≈ ? x j . We can then translate the formula as follows.

tr(x i ≈ ? x j ) = (tr(x i ≈ x j ) ∧ ξ j,j ) ∨ (tr(x i ≈ x j ) ∧ ξ i,j )

We then define ϕ = many-segments ∧ tr(ϕ). Claim 33. ϕ is satisfiable if, and only if, ϕ is satisfiable.

Proof: In fact, if σ |= ϕ, then by the discussion above, σ ϕ |= ϕ . If, on the other hand, σ |= ϕ for some σ , then since σ |= many-segments it has to be a succession of segments of size 2k + 1, and we can recover a model σ of size |σ |/2k + 1 where σ(i)(x j ) is the data value of the 2j-th position of the i-th segment of σ . In this model, we have that σ |= ϕ.

This coding can also be extended with past obligations in a straightforward way, tr(x i ≈ φ? -1 x j ) = (tr(x i ≈ x j ) ∧ ξ -1 j,j ) ∨ (tr(x i ≈ x j ) ∧ ξ -1 i,j ) where ξ -1 i,j = X 2i-1 (x ≈ γ j ? -1 x). Therefore, there is also a reduction from PLRV into PLRV 1 .

L. Proof of Theorem 23

Let us introduce the problem below as a variant of PCP:

This is a corollary of the undecidability proof for PCP as done in [START_REF] Hopcroft | Introduction to Automata Theory, Languages, and Computation[END_REF]. By reducing MPCP dir to satisfiability for LRV vec , we get undecidability.

Proof: In [START_REF] Hopcroft | Introduction to Automata Theory, Languages, and Computation[END_REF], the halting problem for Turing machines is first reduced to a variation of PCP called modified PCP. In modified PCP, a requirement is that the solution should begin with the pair u 1 , v 1 (this requirement can be easily eliminated by encoding it into the standard PCP, but here we find it convenient to work in the presence of a generalization of this requirement). To ensure that there is a solution of even length whenever there is a solution, we let In the encoding of the halting problem from the cited work, |u i | ≤ 3 for any i between 1 and n (this continues to hold even after we add $ to the first pair as above). A close examination of the proof in the cited work reveals that if the modified PCP instance u 1 , . . . , u n , v 1 , . . . , v n ∈ Σ * has a solution

for some k, then the j th position of u i1 • • • u im occurs in u i k for some k > k (we call this the directedness property). In short, the reason for this is that for any

Hence, for any letter in v i k+1 (which starts encoding ( + 2) th configuration), the corresponding letter cannot occur in u i1 • • • u i k +1 (unless the single string u i k+1 encodes the entire ( + 1) st configuration and starts encoding ( + 2) th configuration; this however is not possible since there are at most 3 letters in u i k+1 and encoding a configuration requires at least 4 letters). After the last configuration has been encoded, the length of u i1 • • • u i k starts catching up with the length of v i1 • • • v i k with the help of pairs (u, v) where |u| = 2 and |v| = 1. However, as long as the lengths do not catch up, the directedness property continues to hold. As soon as the lengths do catch up, it is a solution to the PCP. Only the positions of u i1 and the last position of the solution violate the directedness property.

Given an instance pcp of MPCP dir , we construct a LRV vec (X, U) formula φ pcp such that pcp has a solution iff φ pcp is satisfiable. To do so, we adapt a proof technique from [START_REF] Bojańczyk | Two-variable logic on data words[END_REF], [START_REF] Kara | Temporal logics on words with multiple data values[END_REF] but we need to provide substantial changes in order to fit our logic. Moreover, none of the results in [START_REF] Bojańczyk | Two-variable logic on data words[END_REF], [START_REF] Kara | Temporal logics on words with multiple data values[END_REF] allow to derive our main undecidability result since we use neither past-time temporal operators nor past obligations of the form x, x ≈ ϕ? -1 y, y

Let Σ = {ā | a ∈ Σ} be a disjoint copy of Σ. For convenience, we assume that each position of a LRV model is labelled by a letter from Σ ∪ Σ (these labels can be easily encoded as equivalence classes for all µ ∈ {x=y, +1(x, y), ¬(+1(x, y) ∨ x=y)}, χ x ∈ {X(x), ¬X(x)}, χ y ∈ {X(y), ¬X(y)}. We can bring the formula into this normal form in exponential time. To this end, we can first bring χ into CNF, χ = i∈I j∈Ji ν ij , where every ν ij is an atom or a negation of an atom. Then, ∀x∀y χ ≡ ∀x∀y

Note that ∃x∃y µ i,1 ∨ ∃x∃y µ i,2 is equivalent to ∃x∃y j∈Ji ¬ν ij . Hence,

is equivalent to ∀x∀y χ. Finally, every µ i,j can be easily split into a conjunction of three formulas (one of binary relations, one of unary relations on x, and one of unary relations on y), thus obtaining a formula of the form ( ). This procedure takes polynomial time once the CNF normal form is obtained, and it then takes exponential time in the worst We define tr(χ x m ) as the conjunction of all the formulas x 0 ≈ x i so that X i (x) is a conjunct of χ x m , and all the formulas ¬(x 0 ≈ x i ) so that ¬X i (x) is a conjunct of χ x m ; we do similarly for tr(χ y m ). If µ = +1(x, y) and ν = x ∼ y we translate

). We proceed similarly for µ = +1(x, y), ν = ¬(x ∼ y); and the translation is of course ⊥ (false) if µ = (x=y), ν = ¬(x∼y). The difficult cases are the remaining ones. Suppose µ = ¬(+1(x, y) ∨ x=y), ν = x∼y. In other words, x is at least two positions before y, and they have the same data value. Observe that the formula tr(χ x m ) ∧ x ≈ tr(χ y m )? x does not encode precisely this case, as it would correspond to a weaker condition x < y ∧ x ∼ y. In order to properly translate this case we make use of the variable x prev , ensuring that it always has the data value of the variable x in the previous position

We then define tr ∃y x ≤ y ∧ χ m ∧ χ x m ∧ χ y m as tr(χ x m ) ∧ x ≈ x prev ≈ tr(χ y m )? x? x prev . Note that by nesting twice the future obligation we ensure that the target position where tr(χ y m ) must hold is at a distance of at least two positions. For ν = ¬(x∼y) we produce a similar formula, replacing the innermost appearance of ≈ with ≈ in the formula above. We then define tr(∀x∀y χ) as

To translate ∀x∃y (x ≤ y ∧ ψ k ) we proceed in a similar way. As before, we bring x ≤ y ∧ ψ k into the form m∈M x ≤ y ∧ χ m ∧ χ x m ∧ χ y m , in exponential time. We then define tr(∀x∃y

Thus,

One can show that the translation tr defined above preserves satisfiability. More precisely, it can be seen that:

(1) Any data word whose data values are the x-projection from a model satisfying tr(ϕ), satisfies ϕ; and, conversely, (2) for any data word satisfying ϕ with a given assignment for X 1 , . . . , X n to the word positions, and for any model σ such that

• σ has the same length as the data word,

• for every position i, σ(i)(x) is the data value of position i from the data word, and σ(i)(x 0 ) = σ(i)(x j ) iff X j holds at position i of the data word, and • for every position i > 0, σ(i)(x prev ) = σ(i -1)(x), we have that σ |= tr(ϕ).

By Corollary 10 we can decide the satisfiability of the translation in 2EXPSPACE, and since the translation is exponential, this gives us a 3EXPSPACE upper bound for the satisfiability of forward-EMSO 2 (+1, <, ∼). Remark 37. The proof above can be also extended to work with a similar fragment of EMSO 2 (+1, . . . , +k, <, ∼), that is, EMSO 2 (+1, <, ∼) extended with all binary relations of the kind +i(x, y) for every i ≤ k, with the semantics that x is i positions after y. Hence, we also obtain the decidability of the satisfiability problem for this logic in 3EXPSPACE. We do not know if the upper bounds we give for forward-EMSO 2 (+1, <, ∼) and forward-EMSO 2 (+1, . . . , +k, <, ∼) can be improved.

Our result stating that PLRV 1 is equivalent to reachability in VASS (Corollary 22), can also be seen as a hardness result for FO 2 (<, ∼, {+k} k∈N ), that is, first-order logic with two variables on data words, extended with all binary relations +k(x, y) denoting that two elements are at distance k. It is easy to see that this logic captures PLRV 1 and hence that it is equivalent to reachability in VASS, even in the absence of an alphabet. Corollary 38. The satisfiability problem for FO 2 (<, ∼, {+k} k∈N ) is as hard as the reachability problem in VASS, even when restricted to having an alphabet Σ = ∅.

2) Temporal Logics: Consider a temporal logic with future operators F = and F = , so that F = ϕ (resp. F = ϕ) holds at some position i of the finite data word if there is some future position j > i where ϕ is true, and the data values of positions i and j are equal (resp. distinct). We also count with "next" operators X k = and X k = for any k ∈ N, where X k = ϕ (resp. X k = ϕ) holds at position i if ϕ holds at position i + k, and the data values of position i + k and i are equal (resp. distinct). Finally, the logic also features a standard until operator U, tests for the labels of positions, and it is closed under Boolean operators. We call this logic LTL(U,

There is an efficient satisfiability-preserving translation from LTL(U, F = , F = , {X k = , X k = } k∈N ) into LRV and back and hence we have the following. Proposition 39. The satisfiability problem for LTL(U,

Proof sketch: There is a straightforward polynomial-time translation into LRV that preserves satisfiability, where F = ϕ is translated as x ≈ ϕ ? x and F = ϕ is translated as x ≈ ϕ ? x; X k ϕ as X k ϕ ∧ x ≈ X k x; and any test for label a i by x 0 ≈ x i .

In fact, LTL(U, F = , F = , {X k = , X k = } k∈N ) corresponds to a fragment of the linear-time temporal logic LTL extended with one register for storing and comparing data values. We denote it by LTL ↓ 1 , and it was studied in [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. This logic contains one operator to store the current datum, one operator to test the whether the current datum is equal to the one stored. The freeze operator ↓ ϕ permits to store the current datum in the register and continue the evaluation of the formula ϕ. The operator ↑ tests whether the current data value is equal to the one stored in the register. When the temporal operators are limited to F, U and X, this logic is decidable with non-primitive-recursive complexity [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF].

Indeed LTL(U, F = , F = , {X k = , X k = } k∈N ) is the fragment where we only allow ↓ and ↑ to appear in the form of ↓ F(↑∧ϕ) and ↓ X k (↑∧ϕ) -or with ¬ ↑ instead of ↑. Markedly, this restriction allows us to jump from a non-primitive-recursive complexity of the satisfiability problem, to an elementary 2EXPSPACE complexity.