Diego Figueira

Alternating register automata on finite data words and trees *

Keywords: 1998 ACM Subject Classification: I.7.2 Document Preparation, Markup Languages, H.2.3 Database Management, Languages, H.2.3 Languages, Query Languages alternating tree register automata, XML, forward XPath, unranked ordered tree, data-tree, infinite alphabet

We study alternating register automata on data words and data trees in relation to logics. A data word (resp. data tree) is a word (resp. tree) whose every position carries a label from a finite alphabet and a data value from an infinite domain. We investigate one-way automata with alternating control over data words or trees, with one register for storing data and comparing them for equality. This is a continuation of the study started by Demri, Lazić and Jurdziński.

From the standpoint of register automata models, this work aims at two objectives: (1) simplifying the existent decidability proofs for the emptiness problem for alternating register automata; and (2) exhibiting decidable extensions for these models.

From the logical perspective, we show that (a) in the case of data words, satisfiability of LTL with one register and quantification over data values is decidable; and (b) the satisfiability problem for the so-called forward fragment of XPath on xml documents is decidable, even in the presence of DTDs and even of key constraints. The decidability is obtained through a reduction to the automata model introduced. This fragment contains the child, descendant, next-sibling and following-sibling axes, as well as data equality and inequality tests.

Introduction

In static analysis of databases as in software verification, we frequently find the need of reasoning with infinite alphabets. In program verification one may need to decide statically whether a program satisfies some given specification; and the necessity of dealing with infinite alphabets can arise from different angles. For example, in the presence of concurrency, suppose that an unbounded number of processes run, each one with its process identification, and we must deal with properties expressing the interplay between these processes. Further, procedures may have parameters and data from some infinite domain could be exchanged as arguments. On the other hand, in the databases context, static analysis on xml and its query languages recurrently needs to take into account not only the labels of the nodes, but also the actual data contained in the attributes. It is hence important to study formalisms to reason with words or trees that can carry elements from some infinite domain.

This work is about decidable alternating register automata models on data words and data trees in relation to logics manipulating data. This is a continuation of the investigation carried out by Demri, Lazić and Jurdziński [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF][START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF]. A non trivial consequence of our contribution on alternating automata is that the satisfiability problem for the forward fragment of XPath on xml documents is decidable.

We consider two kinds of data models: data words and data trees. A data word (data tree) is a finite word (unranked finite tree) whose every position carries a pair of elements: a symbol from a finite alphabet and and an element (a datum) from an infinite set (the data domain). We work on finite structures, and all the results we present are relative to finite words and trees.

Over these two models we consider two formalisms: alternating register automata on the one hand, and logics on the other. Each automata model is related to a logic, in the sense that the satisfiability of the logic can be reduced to the emptiness of the automata model. Both automata models we present (one for data words, the other for data trees) have in essence the same behavior. Let us give a more detailed description of these formalisms.

Automata. The automata model we define is based on the ARA model (for Alternating Register Automata) of [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] in the case of data words, or the ATRA model (for Alternating Tree Register Automata) of [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] in the case of data trees. ARA are one-way automata with alternating control and one register to store data values for later comparison. ATRA correspond to a natural extension of ARA over data trees. The ATRA model can move in two directions: to the leftmost child, and/or to the next sibling to the right. Both models were shown to have a decidable emptiness problem. The proofs of decidability are based on non trivial reductions to a class of decidable counter automata with faulty increments.

In the present work, decidability of these models is shown by interpreting the semantics of the automaton in the theory of well-quasi-orderings in terms of a well-structured transition system [see FS01]. The object of this alternative proof is twofold. On the one hand, we propose a direct, unified and self-contained proof of the main decidability results of [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF][START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF]. Whereas in [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF][START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] decidability results are shown by reduction to a class of faulty counter automata, here we avoid such translation, and show decidability directly interpreting the configurations of the automata in the theory of well-structured transition systems. We stress, however, that the underlying techniques used here are similar to those of [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF][START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF]. On the other hand, we further generalize these results. Our proof can be easily extended to show the decidability of the nonemptiness problem for two powerful extensions. These extensions consist in the following abilities: (a) the automaton can nondeterministically guess any data value of the domain and store it in the register; and (b) it can make a certain kind of universal quantification over the data values seen along the run of the automaton, in particular over the data values seen so far. We name these extensions guess and spread respectively. These extensions can be both added to the ARA model or to the ATRA model, since our proofs for ARA and ATRA emptiness problems share the same core. We call the class of alternating register automata with these extensions as ARA(guess, spread) in the case of data words, or ATRA(guess, spread) in the case of data trees. We demonstrate that these extensions are also decidable if the data domain is equipped with a linear order and the automata model is extended accordingly. Further, these models are powerful enough to decide a large fragment of XPath, and of a temporal logic with registers.

XPath. This work is originally motivated by the increasing importance of reasoning tasks about xml documents. An xml document can be seen as an unranked ordered tree where each node carries a label from a finite alphabet and a set of attributes, each with an associated datum from some infinite domain. A data tree is a simplification of an xml document that happens to be equivalent for the problems treated here.

XPath is arguably the most widely used xml node selecting language, part of XQuery and XSLT; it is an open standard and a W3C Recommendation [START_REF] Clark | XML path language (XPath)[END_REF]. Static analysis on xml languages is crucial for query optimization tasks, consistency checking of xml specifications, type checking transformations, or many applications on security. Among the most important problems are those of query equivalence and query containment. By answering these questions we can decide at compile time whether the query contains a contradiction, and thus whether the computation of the query on the document can be avoided, or if one query can be safely replaced by a simpler one. For logics closed under boolean combination, these problems reduce to satisfiability checking, and hence we focus on this problem. Unfortunately, the satisfiability problem for XPath with data tests is undecidable [START_REF] Geerts | Satisfiability of XPath queries with sibling axes[END_REF] even when the data domain has no structure (i.e., where the only data relation available is the test for equality or inequality). It is then natural to identify and study decidable expressive fragments.

In this work we prove that the forward fragment of XPath has a decidable satisfiability problem by a reduction to the nonemptiness problem of ATRA(guess, spread). Let us describe this logic. Core-XPath [START_REF] Gottlob | Efficient algorithms for processing XPath queries[END_REF] is the fragment of XPath that captures all the navigational behavior of XPath. It has been well studied and its satisfiability problem is known to be decidable in ExpTime in the presence of DTDs [START_REF] Marx | XPath with conditional axis relations[END_REF]. We consider an extension of this language with the possibility to make equality and inequality tests between attributes of xml elements. This logic is named Core-Data-XPath in [START_REF] Miko Laj Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF], and its satisfiability problem is undecidable [START_REF] Geerts | Satisfiability of XPath queries with sibling axes[END_REF]. Here we address a large fragment of Core-Data-XPath named 'forward XPath', that contains the 'child', 'descendant', 'self-or-descendant', 'nextsibling', 'following-sibling', and 'self-or-following-sibling' axes. For economy of space we refer to these axes as ↓, ↓ + , ↓ * , →, → + , → * respectively. Note that → + and → * are interdefinable in the presence of →, and similarly with ↓ + and ↓ * . We then refer to this fragment as XPath(↓ , ↓ * , →, → * , =), where '=' is to indicate that the logic can express equality or inequality tests between data values.

Although our automata model does not capture forward-XPath in terms of expressiveness, we show that there is a reduction to the nonemptiness problem of ATRA(guess, spread). These automata can recognize any regular language, in particular a DTD, a Relax NG document type, or the core of XML Schema (stripped of functional dependencies). Since we show that XPath(↓, ↓ * , →, → * , =) can express unary key constraints, it then follows that satisfiability of forward-XPath in the presence of DTDs and key constraints is decidable. This settles a natural question left open in [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF], where decidability for a restriction of forward-XPath was shown. The fragment treated in the cited work is restricted to data tests of the form ε = α (or ε = α ), that is, formulae that test whether there exists an element accessible via the α-relation with the same (resp. different) data value as the current node of evaluation. However, the forward fragment allows unrestricted tests α = β and makes the coding into a register automata model highly non trivial. As a consequence, we also answer positively the open question raised in [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF] on whether the downward fragment of XPath in the presence of DTDs is decidable. 1 Temporal logics. ARA(guess, spread) over data words also yield new decidability results on the satisfiability for some extensions of the temporal logic with one register denoted by LTL ↓ (U, X) in [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. This logic contains a 'freeze' operator to store the current datum and a 'test' operator to test the current datum against the stored one. Our automata model captures an extension of this logic with quantification over data values, where we can express "for all data values in the past, ϕ holds", or "there exists a data value in the future where ϕ holds". Indeed, none of these two types of properties can be expressed in the previous formalisms of [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] and [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF]. These quantifiers may be added to LTL ↓ (U, X) over data words without losing decidability. What is more, decidability is preserved if the data domain is equipped with a linear order that is accessible by the logic. Also, by a translation into ATRA(guess, spread), these operators can be added to a CTL version of this logic over data trees, or to the µ-calculus treated in [START_REF] Jurdziński | Alternation-free modal mu-calculus for data trees[END_REF] 2 . However, adding the dual of either of these operators results in an undecidable logic.

Contribution. From the standpoint of register automata models, our contributions can be summarized as follows.

• We exhibit a unified framework to show decidability for the emptiness problem for alternating register automata. This proof has the advantage of working both for data words and data trees practically unchanged. It is also a simplification of the existing decidability proofs. • We exhibit decidable extensions for these models of automata. These extensions work for automata either running over words or trees. For each of these models there are consequences on the satisfiability of some expressive logics. From the standpoint of logics, we show the following results.

• In the case of data trees, we show that the satisfiability problem for the 'forward' fragment of XPath with data test equalities and inequalities is decidable, even in the presence of DTDs (or any regular language) and unary key constraints. Decidability is shown through a reduction to the emptiness problem for ATRA(guess, spread) on data trees. • We show that the temporal logic LTL ↓ (U, X) for data words extended with some quantification over data values is decidable. This result is established thanks to a translation from formulae to alternating register automata of ARA(guess, spread).

1 The satisfiability problem on downward XPath but in the absence of DTDs is shown to be ExpTimecomplete in [START_REF] Figueira | Satisfiability of downward XPath with data equality tests[END_REF].

2 This is the conference version of [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF].

Related work.

The main results presented here first appeared in the conference paper [START_REF] Figueira | Forward-XPath and extended register automata on data-trees[END_REF]. Here we include the full proofs and the analysis for alternating register automata on data words (something that was out of the scope of [START_REF] Figueira | Forward-XPath and extended register automata on data-trees[END_REF]) as well as its relation to temporal logics. Also, we show how to proceed in the presence of a linear order, maintaining decidability. The results contained here also appear in the thesis [START_REF] Figueira | Reasoning on Words and Trees with Data[END_REF]Ch. 3 and 6].

By the lower bounds given in [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF], the complexity of the problems we treat in the work is very high: non-primitive-recursive. This lower bound is also known to hold for the logics we treat here LTL ↓ (U, X) and forward-XPath. In fact, even very simple fragments of LTL ↓ and XPath are known to have non-primitive-recursive lower bounds, including the fragment of [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] or even much simpler ones without the one-step '→' axis, as shown in [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]. This is the reason why in this work we limit ourselves to decidability / undecidability results.

The work in [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF] investigates the satisfiability problem for many XPath logics, mostly fragments without negation or without data equality tests in the absence of sibling axes. Also, in [START_REF] Figueira | Satisfiability of downward XPath with data equality tests[END_REF] there is a study of the satisfiability problem for downward XPath fragments with and without data equality tests. All these are sub-fragments of forward-XPath, and notably, none of these works considers horizontal axes to navigate between siblings. Hence, by exploiting the bisimulation invariance property enjoyed by these logics, the complexity of the satisfiability problem is kept relatively low (at most ExpTime) in the presence of data values. However, as already mentioned, when horizontal axes are present most of the problems have a non-primitive-recursive complexity. In [START_REF] Geerts | Satisfiability of XPath queries with sibling axes[END_REF], several fragments with horizontal axes are treated. The only fragment with data tests and negation studied there is incomparable with the forward fragment, and it is shown to be undecidable. In [START_REF] Figueira | Bottom-up automata on data trees and vertical XPath[END_REF] it is shown that the vertical fragment of XPath is decidable in non-primitive-recursive time. This is the fragment with both downward and upward axes, but notably no horizontal axes (in fact, adding horizontal axes to the vertical fragment results in undecidability).

The satisfiability of first-order logic with two variables and data equality tests is explored in [START_REF] Miko Laj Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF]. It is shown that FO 2 with local one-step relations to move around the data tree and a data equality test relation is decidable. [BMSS09] also shows the decidability of a fragment of XPath(↑, ↓, ←, →, =) with sibling and upward axes. However, the logic is restricted to one-step axes and to data formulae of the kind ε = α (or =), while the fragment we treat here cannot move upwards but has transitive axes and unrestricted data tests.

Preliminaries

Notation. We first fix some basic notation. Let ℘(C) denote the set of subsets of C, and ℘ <∞ (C) be the set of finite subsets of C. Let N = {1, 2, . . . } be the set of positive integers, and let [n] := {i | 1 ≤ i ≤ n} for any n ∈ N. We call N 0 = N ∪ {0}. We fix once and for all D to be any infinite domain of data values; for simplicity in our examples we will consider D = N 0 . In general we use letters A, B for finite alphabets, the letter D for an infinite alphabet and the letters E and F for any kind of alphabet. By E * we denote the set of finite sequences over E and by E ω the set of infinite sequences over E. We use '•' as the concatenation operator between sequences. We write |S| to denote the length of S (if S is a sequence), or the cardinality of S (if S is a set).

2.1. Finite words. We consider a finite word over E as a function w : [n] → E for some n ∈ N, and we define the set of words as Words(E) := {[n] → E | n ∈ N}. We write pos(w) = {1, . . . , n} to denote the set of positions (that is, the domain of w), and we define the size of w as |w| = n. Given w ∈ Words(E) and w ∈ Words(F) with pos(w) = pos(w ) = P , we write w ⊗ w ∈ Words(E × F) for the word such that pos(w ⊗ w ) = P and (w ⊗ w )(x) = (w(x), w (x)). A data word is a word of Words(A × D), where A is a finite alphabet of letters and D is an infinite domain. Note that we define data words as having at least one position. This is done for simplicity of the definition of the formalisms we work with, and the results contained here also extend to possibly-empty data words and trees. We define the word type as a function type w : pos(w) → { , ¯ } that specifies whether a position has a next element or not. That is, type w (i) = iff (i + 1) ∈ pos(w).

2.2.

Unranked ordered finite trees. We define Trees(E), the set of finite, ordered and unranked trees over an alphabet E. A position in the context of a tree is an element of N * . The root's position is the empty string and we note it ' '. The position of any other node in the tree is the concatenation of the position of its parent and the node's index in the ordered list of siblings. Along this work we use x, y, z, w, v as variables for positions, while i, j, k, l, m, n as variables for numbers. Thus, for example x•i is a position which is not the root, and that has x as parent position, and there are i -1 siblings to the left of x•i.

Formally, we define POS ⊆ ℘ <∞ (N * ) the set of sets of finite tree positions, such that:

X ∈ POS iff (a) X ⊆ N * , |X| < ∞; (b) it is prefix-closed; and (c) if n•(i + 1) ∈ X for i ∈ N, then n•i ∈ X.
A tree is a mapping from a set of positions to letters of the alphabet

Trees(E) := {t : P → E | P ∈ POS} .
Given a tree t ∈ Trees(E), pos(t) denotes the domain of t, which consists of the set of positions of the tree, and alph(t) = E denotes the alphabet of the tree. From now on, we informally write 'node' to denote a position x together with the value t(x). We define the ancestor partial order as the prefix relation x x•y for every x•y, and the strict version ≺ as the strict prefix relation x ≺ x•y for |y| > 0. Given a tree t and x ∈ pos(t), 't| x ' denotes the subtree of t at position x. That is, t| x : {y | x•y ∈ pos(t)} → alph(t) where t| x (y) = t(x•y). In the context of a tree t, a siblinghood is a maximal sequence of siblings. That is, a sequence of positions x•1, . . . , x•l ∈ pos(t) such that x•(l + 1) ∈ pos(t).

Given two trees

t 1 ∈ Trees(E), t 2 ∈ Trees(F) such that pos(t 1 ) = pos(t 2 ) = P , we define t 1 ⊗ t 2 : P → (E×F) as (t 1 ⊗ t 2 )(x) = (t 1 (x), t 2 (x)).
The set of data trees over a finite alphabet A and an infinite domain D is defined as Trees(A×D). Note that every tree t ∈ Trees(A×D) can be decomposed into two trees a ∈ Trees(A) and d ∈ Trees(D) such that t = a ⊗ d. Figure 1 shows an example of a data tree. We define the tree type as a function type t : pos(t) → { , ¯ } × { , ¯ } that specifies whether a node has children and/or siblings to the right. That is, type t (x) := (a, b) where a = iff x•1 ∈ pos(t), and where b = iff x = x •i and x •(i + 1) ∈ pos(t). The notation for the set of data values used in a data tree is

data(a ⊗ d) := {d(x) | x ∈ pos(d)} .
We abuse notation and write data(X) to refer to all the elements of D contained in X, for whatever object X may be. First-child and next-sibling coding. We will make use of the first-child and next-sibling underlying binary tree of an unranked tree t. This is the binary tree whose nodes are the same as in t, a node x is the left child of y if x is the leftmost child of y in t, and a node x is the right child of y if x is the next sibling to the right of y in t. We will sometimes refer to this tree by "the fcns coding of t". Let us define the relation between positions f cns such that x f cns y if x is the ancestor of y in the first-child and next-sibling coding of the tree, that is, if y is reachable from x by traversing the tree through the operations 'go to the leftmost child' and 'go to the next sibling to the right'.

2.3. Properties of languages. We use the standard definition of language. Given an automaton A over data words (resp. over data trees), let L(A) denote the set of data words (resp. data trees) that have an accepting run on A. We say that L(A) is the language of words (resp. trees) recognized by A. We extend this definition to a class of automata A :

L(A ) = {L(A) | A ∈ A }, obtaining a class of languages.
Equivalently, given a formula ϕ of a logic L over data words (resp. data trees) we denote by L(ϕ) the set of words (resp. trees) verified by ϕ. This is also extended to a logic

L(L ) = {L(ϕ) | ϕ ∈ L }.
We say that a class of automata (resp. a logic) A is at least as expressive as another class (resp. logic) B iff L(B) ⊆ L(A ). If additionally L(B) = L(A ) we say that A is more expressive than B.

We say that a class of automata A captures a logic L iff there exists a translation t : L → A such that for every ϕ ∈ L and model (i.e., a data tree or a data word) m, we have that m |= ϕ if and only if m ∈ L(t(ϕ)).

2.4.

Well-structured transition systems. The main argument for the decidability of the emptiness of the automata models studied here is based on the theory of well-quasiorderings. We interpret the automaton's run as a transition system with some good properties, and this allows us to obtain an effective procedure for the emptiness problem. This is known in the literature as a well-structured transition system (WSTS) [see FS01, A ČJT96]. Next, we reproduce some standard definitions and known results that we will make use of.

Definition 2.1. For a set S, we define (S, ≤) to be a well-quasi-order (wqo) iff '≤' ⊆ S×S is a relation that is reflexive, transitive and for every infinite sequence w 1 , w 2 , . . . ∈ S ω there are two indices i < j such that w i ≤ w j .

Dickson's Lemma ([Dic13]). Let ≤ k ⊆ N k 0 × N k 0 such that (x 1 , . . . , x k ) ≤ k (y 1 , . . . , y k ) iff x i ≤ y i for all i ∈ [k]. For all k ∈ N 0 , (N k 0 , ≤ k ) is a well-quasi-order.
Definition 2.2. Given a quasi-order (S, ≤) we define the embedding order as the relation

⊆ S * × S * such that x 1 • • • x n y 1 • • • y m iff there exist 1 ≤ i 1 < • • • < i n ≤ m with x j ≤ y i j for all j ∈ [n].
Higman's Lemma ( [START_REF] Higman | Ordering by divisibility in abstract algebras[END_REF]). Let (S, ≤) be a well-quasi-order. Let ⊆ S * × S * be the embedding order over (S, ≤). Then, (S * , ) is a well-quasi-order.

Corollary 2.3 (of Higman's Lemma). Let S be a finite alphabet. Let be the subword relation over S * ×S * (i.e., x y if x is the result of removing some (possibly none) positions from y). Then, (S * , ) is a well-quasi-order.

Proof. It suffices to realize that is indeed the embedding order over (S, =), which is trivially a wqo since S is finite.

Definition 2.4. Given a transition system (S, →), and T ⊆ S we define Succ(T ) := {a ∈ S | ∃ a ∈ T with a → a }, and Succ * to its reflexive-transitive closure. Given a wqo (S, ≤) and T ⊆ S, we define the upward closure of T as ↑ T := {a | ∃ a ∈ T, a ≤ a}, and the downward closure as ↓ T := {a | ∃ a ∈ T, a ≤ a }. We say that T is downward-closed (resp. upward-closed) iff ↓ T = T (resp. ↑ T = T ).

Definition 2.5. We say that a transition system (S, →) is finitely branching iff Succ({a}) is finite for all a ∈ S. If Succ({a}) is also computable for all a, we say that (S, →) is effective.

Definition 2.6 (rdc). A transition system (S, →) is reflexive downward compatible (or rdc for short) with respect to a wqo (S, ≤) iff for every a 1 , a 2 , a 1 ∈ S such that a 1 ≤ a 1 and a 1 → a 2 , there exists a 2 ∈ S such that a 2 ≤ a 2 and either a 1 → a 2 or a 1 = a 2 .

Our forthcoming decidability results on alternating register automata of Sections 3.2 and 5.1 will be shown as a consequence of the following propositions.

Proposition 2.7 ([FS01, Proposition 5.4]). If (S, ≤) is a wqo and (S, →) a transition system such that (1) it is rdc, (2) it is effective, and (3) ≤ is decidable; then for any finite T ⊆ S it is possible to compute a finite set U ⊆ S such that ↑ U = ↑ Succ * (T ).

Lemma 2.8. Given (S, ≤, →) as in Proposition 2.7, a recursive downward-closed set V ⊆ S, and a finite set T ⊆ S. The problem of whether there exists a ∈ T and b ∈ V such that a → * b is decidable.

Proof. Applying Proposition 2.7, let U ⊆ S finite, with ↑ U = ↑ Succ * (T ). Since T is finite and V is recursive, we can test for every element of b ∈ U if b ∈ V . On the one hand, if there is one such b, then by definition b ∈ ↑ Succ * (T ), or in other words a → * a ≤ b for some a ∈ T , a ∈ Succ * (a). But since V is downward-closed, a ∈ V and hence the property is true. On the other hand, if there is no such b in U , it means that there is no such b in ↑ U either, as V is downward-closed. This means that there is no such b in Succ * (T ) and hence that the property is false. Definition 2.9 (≤ ℘ ). Given an ordering (S, ≤), we define the majoring ordering over ≤ as (℘ <∞ (S), ≤ ℘ ), where S ≤ ℘ S iff there exists an injective function f : S → S so that for every a ∈ S, a ≤ f (a).

Proposition 2.10. If (S, ≤) is a wqo, then the majoring order over (S, ≤) is a wqo.

Proof. The fact that this order is reflexive and transitive is immediate from the fact that ≤ is a quasi-order. The fact of being a well -quasi-order is a simple consequence of Higman's Lemma. Each finite set {a 1 , . . . , a n } can be seen as a sequence of elements a 1 , . . . , a n , in any order. In this context, the embedding order is stricter than the majoring order. In other words, if a 1 , . . . , a n a 1 , . . . , a m , then {a 1 , . . . , a n } ≤ ℘ {a 1 , . . . , a m }. By Higman's Lemma the embedding order over (S, ≤) is a wqo, implying that the majoring order is as well.

The following technical Proposition will become useful in Section 5.1 for transferring the decidability results obtained for class of automata ARA(guess, spread) on data words to the class ATRA(guess, spread) on data trees.

Proposition 2.11. Let ≤, → 1 1 , → 2 1 , → 3 1 ⊆ S ×S, let P ⊆ S be downward-and upward-closed set with respect to ≤, let ≤ ℘ , → 2 ⊆ ℘ <∞ (S) × ℘ <∞ (S) where ≤ ℘ is the majoring order over (S, ≤) so that S → 2 S iff either

• S = {a} ∪ Ŝ, S = {b 1 , b 2 } ∪ Ŝ, a ∈ P, and a → i 1 b i for all i ∈ {1, 2}, or • S = {a} ∪ Ŝ, S = {b} ∪ Ŝ, a ∈ P, and a → i 1 b for some i ∈ {1, 2}, or • S = {a} ∪ Ŝ, S = {b} ∪ Ŝ, and a → 3 1 b. Suppose that (S, ≤) is a wqo which is rdc with respect to → i 1 , for every i ∈ {1, 2, 3}. Then, (℘ <∞ (S), ≤ ℘ ) is a wqo which is rdc with respect to → 2 .

Proof. The fact that (℘ <∞ (S), ≤ ℘ ) is a wqo is given by Proposition 2.10. The rdc property with respect to → 2 is simple. Suppose that a ∈ P and

S ≤ ℘ {a} ∪ S → 2 {b 1 , b 2 } ∪ S
with a → i 1 b i for all i ∈ {1, 2}. Let f be the witnessing function for S ≤ ℘ S. If f -1 (a) does not exist, then S ≤ ℘ S, and the relation is reflexive compatible since this means that S ≤ ℘ {b 1 , b 2 } ∪ S. Otherwise, let a = f -1 (a) and note that S \ {a } ≤ ℘ S. Since a ∈ P and P is downward-closed, then a ∈ P. Further, since a ≤ a → i 1 b i we obtain, by rdc of

→ i 1 , that either • a ≤ b 1 or a ≤ b 2 , in which case S ≤ ℘ {b 1 , b 2 } ∪ S, or • there are b 1 , b 2 so that a → i 1 b i and b i ≤ b i for all i ∈ {1, 2}, in which case S → 2 S \ {a } ∪ {b 1 , b 2 } ≤ ℘ {b 1 , b 2 } ∪ S.
The second possiblity-where a ∈ P and we have S ≤ ℘ {a} ∪ S → 2 {b} ∪ S-is analogous, this time using the fact that P is upward-closed. The third possibility is also easy.

Part 1. Data words

In this first part, we start our study on data words. In Section 3 we introduce our automata model ARA(guess, spread), and we show that the emptiness problem for these automata is decidable. This extends the results of [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. To prove decidability, we adopt a different approach than the one of [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] that enables us to show the decidability of some extensions, and to simplify the decidability proofs of Part 2, which can be seen as a corollary of this proof. In Section 4 we introduce a temporal logic with registers and quantification over data values. This logic is shown to have a decidable satisfiability problem by a reduction to the emptiness problem of ARA(guess, spread) automata.

ARA model

An Alternating Register Automaton (ARA) consists in a one-way automaton on data words with alternation and one register to store and test data. In [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] it was shown that the emptiness problem is decidable and non-primitive-recursive. Here, we consider an extension of ARA with two operators: spread and guess. We call this model ARA(spread, guess). Definition 3.1. An alternating register automaton of ARA(spread, guess) is a tuple A = A, Q, q I , δ such that

• A is a finite alphabet;

• Q is a finite set of states;

• q I ∈ Q is the initial state; and • δ : Q → Φ is the transition function, where Φ is defined by the grammar

a | ā | ? | store(q) | eq | eq | q ∧ q | q ∨ q | q | guess(q) | spread(q, q ) where a ∈ A, q, q ∈ Q, ∈ { , ¯ }.
This formalism without the guess and spread transitions is equivalent to the automata model of [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] on finite data words, where is to move to the next position to the right on the data word, store(q) stores the current datum in the register and eq (resp. eq) tests that the current node's value is (resp. is not) equal to the stored. We call a state q ∈ Q moving if δ(q) = q for some q ∈ Q.

As this automaton is one-way, we define its semantics as a set of 'threads' for each node that progress synchronously. That is, all threads at a node move one step forward simultaneously and then perform some non-moving transitions independently. This is done for the sake of simplicity of the formalism, which simplifies both the presentation and the decidability proof.

Next we define a configuration and then we give a notion of a run over a data word w. A configuration is a tuple i, α, γ, ∆ that describes the partial state of the execution at position i. The number i ∈ pos(w) is the position in the data word w, γ = w(i) ∈ A × D is the current position's letter and datum, and α = type w (i) is the word type of the position i. Finally, ∆ ∈ ℘ <∞ (Q × D) is a finite set of active threads, each thread (q, d) consisting in a state q and the value d stored in the register. We will always note the set of threads of a configuration with the symbol ∆, and we write ∆

(d) = {q ∈ Q | (q, d) ∈ ∆} for d ∈ D, ∆(q) = {d ∈ D | (q, d) ∈ ∆} for q ∈ Q.
By C ara we denote the set of all configurations. Given a set of threads ∆ we write data(∆) := {d | (q, d) ∈ ∆}, and data( i, α, (a, d), ∆ ) := {d} ∪ data(∆). We say that a configuration is moving if for every (q, d) ∈ ∆, q is moving.

To define a run we first introduce three transition relations over node configurations: the non-moving relation → ε and the moving relation → . We start with → ε . If the transition corresponding to a thread is a store(q), the automaton sets the register with current data value and continues the execution of the thread with state q; if it is eq, the thread accepts (and in this case disappears from the configuration) if the current datum is equal to that of the register, otherwise the computation for that thread cannot continue. The reader can check that the rest of the cases defined in Figure 2 follow the intuition of an alternating automaton.

The cases that follow correspond to our extensions to the model of [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. The guess instruction extends the model with the ability of storing any datum from the domain D.

ρ → ε i, α, (a, d), {(q j , d )} ∪ ∆ if δ(q) = q 1 ∨ q 2 , j ∈ {1, 2} (3.1) ρ → ε i, α, (a, d), {(q 1 , d ), (q 2 , d )} ∪ ∆ if δ(q) = q 1 ∧ q 2 (3.2) ρ → ε i, α, (a, d), {(q , d)} ∪ ∆ if δ(q) = store(q ) (3.3) ρ → ε i, α, (a, d), ∆ if δ(q) = eq and d = d (3.4) ρ → ε i, α, (a, d), ∆ if δ(q) = eq and d = d (3.5) ρ → ε i, α, (a, d), ∆ if δ(q) = α? (3.6) ρ → ε i, α, (a, d), ∆ if δ(q) = b and b = a (3.7) ρ → ε i, α, (a, d), ∆ if δ(q) = b and b = a (3.8) Figure 2: Definition of the transition relation → ε ⊆ C ara × C ara , given a configuration ρ = i, α, (a, d), {(q, d )} ∪ ∆ .
Whenever δ(q) = guess(q ) is executed, a data value (nondeterministically chosen) is saved in the register.

ρ → ε i, α, (a, d), {(q , e)} ∪ ∆ if δ(q) = guess(q ), e ∈ D (3.9)
Note that the store instruction may be simulated with the guess, eq and ∧ instructions, while guess cannot be expressed by the ARA model. The 'spread' instruction is an unconventional operator in the sense that it depends on the data of all threads in the current configuration with a certain state. Whenever δ(q) = spread(q 2 , q 1 ) is executed, a new thread with state q 1 and datum d is created for each thread q 2 , d present in the configuration. With this operator we can code a universal quantification over all the data values that appeared so far (i.e., that appeared in smaller positions). We demand that this transition may only be applied if all other possible → ε kind of transitions were already executed. In other words, only spread transitions or moving transitions are present in the configuration.

ρ → ε i, α, (a, d), { q 1 , d | q 2 , d ∈ ∆} ∪ ∆ (3.10)
iff δ(q) = spread(q 2 , q 1 ) and for all q, d ∈ ∆ either δ(q) is a spread or a moving instruction. We also use a weaker one-argument version of spread.

ρ → ε i, α, (a, d), { q 1 , d | ∃q 2 . q 2 , d ∈ ∆} ∪ ∆ (3.11)
iff δ(q) = spread(q 1 ) and for all q, d ∈ ∆ either δ(q) is a spread or a moving instruction. Notice that the one-argument version of spread can be simulated with the two-argument version, and hence we do not include it in the definition of the automaton. Also, note that we enforce the spread operation to be executed once all other non-moving transitions have been applied, in order to take into account all the data values that may have been introduced in these transitions, as a result of guess operations. This behavior simplifies the reduction from the satisfiability of forward-XPath we will show later. This reduction will only need to use the weak one-argument version of spread.

The → transition advances all threads of the node simultaneously, and is defined, for any type α ∈ { , ¯ } and symbol and with data value

γ ∈ A × D, i, , γ, ∆ → i + 1, α , γ , ∆ (3.12) iff (i) for all (q, d) ∈ ∆, δ(q) is moving; and (ii) ∆ = { q , d | (q, d) ∈ ∆, δ(q) = q }.
Finally, we define the transition between configurations as := → ∪ → ε .

A run over a data word w = a ⊗ d is a nonempty sequence C 1 1) } (i.e., the thread consisting in the initial state with the first datum), such that for every j ∈ [n] with C j = i, α, γ, ∆ : (1) i ∈ pos(w);

• • • C n with C 1 = 1, α 0 , γ 0 , ∆ 0 and ∆ 0 = { q I , d(
(2) γ = w(i); and (3) α = type w (i). We say that the run is accepting iff C n = i, α, γ, ∅ contains an empty set of threads. If for an automaton A we have that L(A) = ∅ we say that A is nonempty.

Properties. We show the following two statements

• L(ARA(guess, spread)) is not closed under complementation,

• the ARA(guess, spread) class is more expressive than ARA. In fact in the proof below we show the first one, that implies the second one, given the fact that the ARA model is closed under complementation. Proposition 3.2 (Expressive power).

(a) the ARA(guess) class is more expressive than ARA;

(b) the ARA(spread) class is more expressive than ARA.

Proof. Let w = a ⊗ d be a data word. To prove (a), consider the property "There exists a datum d and a position i with d(i) = d, a(i) = a, and there is no position j ≤ i with d(j) = d, a(j) = b.". This property can be easily expressed by ARA(guess). It suffices to guess the data value d and checks that we can reach an element (a, d), and that for every previous element (b, d ) we have that d = d . We argue that this property cannot be expressed by the ARA model. Suppose ad absurdum that it is expressible. This means that its negation would also be expressible by ARA (since they are closed under complementation). The negation of this property states "For every data value d, if there is an element (a, d) in the word, then there is a previous element (b, d)."

With this kind of property one can code an accepting run of a Minsky machine, whose emptiness problem is undecidable. This would prove that ARA(guess) have an undecidable emptiness problem, which is in contradiction with the decidability proof that we will give in Section 3.2. Let us see how the reduction works.

The emptiness problem for Minsky machine is known to be undecidable even with an alphabet consisting of one symbol, so we disregard the letters read by the automaton in the following description. Consider then a 2-counter alphabet-blind Minsky machine whose instructions are of the form (q, , q ) with ∈ {inc, dec, ifzero} × {1, 2} being the operation over the counters, and q, q states from the automaton's set of states Q. A run on this automaton is a sequence of applications of transition rules, for example (q 1 , inc 1 , q 2 ) (q 2 , inc 2 , q 3 ) (q 3 , inc 1 , q 2 ) (q 2 , dec 1 , q 1 ) (q 1 , dec 1 , q 2 ) (q 2 , ifzero 1 , q 3 ) This run has an associated data word over the alphabet

Q × {inc, dec, ifzero} × {1, 2} × Q, a b a a a a ≠ Figure 3: A property not expressible in ARA.
where the corresponding data value of each instruction is used to match increments with decrements, for example,

(q 1 , inc 1 , q 2 ) (q 2 , inc 2 , q 3 ) (q 3 , inc 1 , q 2 ) (q 2 , dec 1 , q 1 ) (q 1 , dec 1 , q 2 ) (q 2 , ifzero 1 , q 3 ). 1 2 3 2 1 4
Using the ARA model we can make sure that (i) all increments have different data values and all decrements have different data values; and (ii) for every ( , inc i , ) element with data value d that occurs to the left of a ( , ifzero i , ), there must be a ( , dec i , ) element with data value d that occurs in between. [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] shows how to express these properties using ARA. However, properties (i) and (ii) are not enough to make sure that every prefix of the run ending in a ifzero i instruction must have as many increments as decrements of counter i. Indeed, there could be more decrements than increments -but not the opposite, thanks to (ii).

The missing condition to verify that the run is correct is: (iii) for every decrement there exists a previous increment with the same data value. In fact, we can see that property (P1) can express condition (iii): we only need to change a by a decrement transition in the coding, and b by an increment transition of the same counter. But then, assuming that property (P1) can be expressed by ARA(guess), the emptiness problem for ARA(guess) is undecidable. This is absurd, as the emptiness problem is decidable, as we will show later on in Theorem 3.5.

Using a similar reasoning as before, we show (b): the ARA(spread) class is more expressive than ARA. Consider the property: "There exists a position i labeled b such that d(i) = d(j) for all j < i with a(j) = a." as depicted in Figure 3. Let us see how this can be coded into ARA(spread). Assuming q 0 is the initial state, the transitions should reflect that every datum with label a seen along the run is saved with a state q a , and that this state is in charge of propagating this datum. Then, we guess a position labeled with b and check that all these stored values under q a are different from the current one. For succinctness we write the transitions as positive boolean combinations of the basic operations.

δ(q 0 ) = (b ∧ spread(q a , q 1 )) ∨ (ā ∨ store(q a )) ∧ q 0 , δ(q 1 ) = eq, δ(q a ) = ( ¯ ? ∨ q a ).
This property cannot be expressed by the ARA model. Were it expressible, then its negation "for every element b there exists a previous one labeled a with the same data value" (P2)

would also be. Just as before we can use property (P2) to express condition (iii), and force that for every decrement in a coding of a Minsky machine there exists a corresponding previous increment. This leads to a contradiction by proving that the emptiness problem for ARA(spread) is undecidable.

Corollary 3.3. ARA(guess), ARA(spread) and ARA(guess, spread) are not closed under complementation.

Proof. If they were closed under complementation, then we could express some of the properties described in the proof of Proposition 3.2, resulting in an undecidable model, which is in contradiction with Theorem 3.5.

We then have the following properties of the automata model.

Proposition 3.4 (Boolean operations). The class L(ARA(spread, guess)) has the following properties:

(i) it is closed under union, (ii) it is closed under intersection, (iii) it is not closed under complementation.

Proof sketch. Items (i) and (ii) are straightforward if we notice that the first argument of spread ensures that this transition is always relative to the states of one of the automata being under intersection or union. Item (iii) follows from Corollary 3.3.

Emptiness problem.

This section is dedicated to show the following theorem.

Theorem 3.5. The emptiness problem for ARA(guess, spread) is decidable.

As already mentioned, decidability for ARA was proved in [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. Here we propose an alternative approach that simplifies the proof of decidability of the two extensions spread and guess.

The proof goes as follows. We will define a wqo over C ara and show that (C ara , ) is rdc with respect to (Lemma 3.10). Note that strictly speaking is an infinite-branching transition system as → may take any value from the infinite set D, and → ε can also guess any value. However, it can trivially be restricted to an effective finitely branching one. Then, by Lemma 2.8, (C ara , ) has a computable upward-closed reachability set, and this implies that the emptiness problem of ARA(guess, spread) is decidable.

Since our model of automata only cares about equality or inequality of data values, it is convenient to work modulo renaming of data values. Definition 3.6 (∼). We say that two configurations ρ, ρ ∈ C ara are equivalent (notation Notice that by the definition above we are 'abstracting away' the information concerning the position i. We finally define to be modulo ∼. Definition 3.8 ( ). We define ρ ρ iff there is ρ ∼ ρ with ρ ρ .

ρ ∼ ρ ) if there is a bijection f : data(ρ) → data(ρ ) such that f (ρ) = ρ ,
The following lemma follows from the definitions. Lemma 3.9. (C ara , ) is a well-quasi-order.

Proof. The fact that is a quasi-order (i.e., reflexive and transitive) is immediate from its definition. To show that it is a well -quasi-order, suppose we have an infinite sequence of configurations ρ 1 ρ 2 ρ 3 • • • . It is easy to see that it contains an infinite subsequence τ 1 τ 2 τ 3 • • • such that all its elements are of the form i, α 0 , (a 0 , d), ∆ with

• α 0 and a 0 fixed, and • ∆(d) = C 0 fixed, This is because we can see each of these elements as a finite coloring, and apply the pigeonhole principle on the infinite set {ρ i } i .

Consider then the function g ∆ : ℘(Q) → N 0 , such that g ∆ (S) = |{d | S = ∆(d)}| (we can think of g ∆ as a tuple of (N 0 ) ℘(Q) ). Assume the relation † defined as ∆ † ∆ iff g ∆ (S) ≤ g ∆ (S) for all S. By Dickson's Lemma † is a wqo, and then there are two

τ i = i , α 0 , (a 0 , d i ), ∆ i , τ j = j , α 0 , (a 0 , d j ), ∆ j , i < j such that ∆ i † ∆ j . For each S ⊆ Q, there exists an injective mapping f S : {d | ∆ i (d) = S} → {d | ∆ j (d) = S} such that f C 0 (d i ) = d j ,
as the latter set is bigger than the former by † . We define the injection f : data(τ i ) → data(τ j ) as the (disjoint) union of all f S 's. The union is disjoint since for every data value d and set of threads ∆, there is a unique set S such that

d ∈ {d | S = ∆(d )}. We then have that τ i ∼ f (τ i ) τ j . Hence, τ i τ j .
The core of this proof is centered in the following lemma.

Lemma 3.10. (C ara , → ε ) and (C ara , → ) (and therefore (C ara , )) are rdc with respect to (C ara , ).

Proof. We shall show that for all ρ, τ, ρ ∈ C ara such that ρ τ and ρ ρ, there is τ such that τ τ and either ρ τ or τ = ρ . Since by definition of we work modulo ∼, we can further assume that ρ ρ without any loss of generality. The proof is a simple case analysis of the definitions for . All cases are treated alike, here we present the most representative. Suppose first that ρ → ε τ , then one of the definition conditions of → ε must apply.

If Eq. (3.4) of the definition of → ε (Fig. 2) applies, let

ρ = i, α, (a, d), {(q, d)} ∪ ∆ → ε τ = i, α, (a, d), ∆ with δ(q) = eq. Let ρ = i , α, (a, d), ∆ ρ. If (q, d) ∈ ∆ , we can then apply the same → ε -transition obtaining ρ ρ → ε τ τ .
If there is no such (q, d), we can safely take ρ = τ and check that τ τ . If Eq. (3.3) applies, let

ρ = i, α, (a, d), {(q, d )} ∪ ∆ → ε τ = i, α, (a, d), {(q , d)} ∪ ∆
with ρ → ε τ and δ(q) = store(q ). Again let ρ ρ containing (q, d ) ∈ ∆ . In this case we can apply the same → ε -transition arriving to τ where τ τ . Otherwise, if (q, d ) ∈ ∆ , we take ρ = τ and then τ τ . If a guess is performed (Eq. (3.9)), let

ρ = i, α, (a, d), {(q, d )} ∪ ∆ → ε τ = i, α, (a, d), {(q , e)} ∪ ∆ with δ(q) = guess(q ). Let ρ = i , α, (a, d), ∆
ρ. Suppose there is (q, d ) ∈ ∆ , then we then take a guess transition from ρ obtaining some τ by guessing e and hence τ τ . Otherwise, if (q, d ) ∈ ∆ , we take τ = ρ and check that τ τ .

Finally, if a spread is performed (Eq. (3.10)), let

ρ = i, α, γ, {(q, d )} ∪ ∆ → ε τ = i, α, γ, {(q 1 , d) | (q 2 , d) ∈ ∆} ∪ ∆
with δ(q) = spread(q 2 , q 1 ). Let ρ = i , α, γ, ∆ ρ and suppose there is (q, d ) ∈ ∆ (otherwise τ = ρ works). We then take a spread instruction ρ → ε τ and see that τ τ , because any (q 1 , e) in τ generated by the spread must come from (q 2 , e) of ρ , and hence there is some (q 2 , e) in ρ; now by the spread applied on ρ, (q 1 , d ) is in τ .

The remaining cases of → ε are only easier.

Finally, there can be a 'moving' application of . Suppose that we have

ρ = i, , (a, d), ∆ → τ = i + 1, α 1 , (a 1 , d 1 ), ∆ 1 . Let ρ = i , , (a, d), ∆ ρ.
If ρ is such that ρ τ , the relation is trivially compatible. Otherwise, we shall prove that there is τ such that ρ τ and τ τ . Condition i of → (i.e., that all states are moving) holds for ρ , because all the states present in ρ are also in ρ (by definition of ) where the condition must hold. Then, we can apply the → transition to ρ and obtain τ of the form i + 1, α 1 , (a 1 , d 1 ), ∆ 1 . Notice that we are taking α 1 , a 1 and d 1 exactly as in τ , and that ∆ 1 is completely determined by the → transition from ∆ . We only need to check that τ τ . Take any (q, d ) ∈ ∆ 1 . There must be some (q , d ) ∈ ∆ with δ(q ) = q. Since ∆ ⊆ ∆, we also have (q, d) ∈ ∆ 1 . Hence, ∆ 1 ⊆ ∆ 1 and then τ τ .

We just showed that (C ara , ) is rdc with respect to (C ara , ). The only missing ingredient to have decidability is the following, which is trivial.

Lemma 3.11. The set of accepting configurations of C ara is downward closed with respect to .

We write C ara /∼ to the set of configurations modulo ∼, by keeping one representative for every equivalence class. Note that the transition system (C ara /∼, ) is effective. This is just a consequence of the fact that the -image of any configuration has only a finite number of configurations modulo ∼, and representatives for every class are computable. Hence, we have that (C ara /∼, , ) verify conditions (1) and (2) from Proposition 2.7. Finally, condition (3) holds since (C ara , ) is computable. We can then apply Lemma 2.8, obtaining that for a given A ∈ ARA(guess, spread), testing wether there exists a final configuration τ and an element ρ in

{ 1, α, (a, d 0 ), {(q I , d 0 )} | α ∈ { , ¯ }, a ∈ A} -for any fixed d 0 -such that ρ ∼ ρ
* τ (for some ρ ) is decidable. Thus, we can decide the emptiness problem and Theorem 3.5 follows.

3.3. Ordered data. We show here that the previous decidability result holds even if we add order to the data domain. Let (D, <) be a linear order, like for example the reals or the natural numbers with the standard ordering. Let us replace the instructions eq and eq with δ(q) := . . .

| test(>) | test(<) | test(=) | test( =)
and let us call this model of automata ARA(guess, spread, <). The semantics is as expected. test(<) verifies that the data value of the current position is less than the data value in the register, test(>) that is greater, and test(=) (resp. test( =)) that both are (resp. are not) equal. We modify accordingly → ε , for ρ = i, α, (a, d), {(q, d )} ∪ ∆ .

ρ → ε i, α, (a, d), ∆ if δ(q) = test(<) and d < d (3.13) ρ → ε i, α, (a, d), ∆ if δ(q) = test(>) and d > d (3.14) ρ → ε i, α, (a, d), ∆ if δ(q) = test(=) and d = d (3.15) ρ → ε i, α, (a, d), ∆ if δ(q) = test( =) and d = d (3.16)
All the remaining definitions are preserved. We can show that the emptiness problem for this extended model of automata is still decidable.

Theorem 3.12. The emptiness problem for ARA(guess, spread, <) is decidable.

As in the proof in the previous Section 3.2, we show that there is a wqo < < ⊆ C ara ×C ara that is rdc with respect to , such that the set of final states is < <-downward closed. However, we need to be more careful when showing that we can always work modulo an equivalence relation. Definition 3.13. A function f : D → D is an order-preserving bijection on D ⊆ D iff it is injective, and furthermore for every {d,

d } ⊆ D, if d < d then f (d) < f (d ).
The following Lemma is straightforward from the definition just seen. Definition 3.15 (∼ ord ). Let ρ, ρ be two configurations. We define ρ ∼ ord ρ iff f (ρ) = ρ for some order-preserving bijection f on data(ρ).

Remark 3.16. If ρ ρ then there exists d ∈ D such that { d} ∪ data(ρ) = { d} ∪ data(ρ ). This is a simple consequence of the definition of .

Let us define a version of that works modulo ∼ ord , and let us call it ord .

Definition 3.17. Let ρ 1 , ρ 2 be two configurations. We define ρ 1 ord ρ 2 iff ρ 1 ρ 2 for some ρ 1 ∼ ord ρ 1 and ρ 2 ∼ ord ρ 2 .

In the previous section, when we had that ∼ was simply a bijection and we could not test any linear order <, it was clear that we could work modulo ∼. However, here we are working modulo a more complex relation ∼ ord . In the next lemma we show that working with or working with ord is equivalent.

Lemma 3.18. If ρ 1 ord • • • ord ρ n , then there exist ρ 1 , . . . , ρ n so that ρ 1 • • • ρ n , with ρ i ∼ ord ρ i for every i. Proof. The case n = 1 is trivial. Otherwise, if n > 1, we have ρ 1 ord • • • ord ρ n-1 ord ρ n .
Then, by inductive hypothesis, we obtain ρ 1

• • • ρ n-1 and ρ n-1 ρ n with ρ i ∼ ord ρ i for every i ∈ {1, . . . , n -1}, and ρ j ∼ ord ρ j for every j ∈ {n -1, n}. Let g be the witnessing bijection such that g(ρ n-1 ) = ρ n-1 , and let us assume that { d} ∪ data(ρ n-1 ) = { d} ∪ data(ρ n ) by Remark 3.16.

Let f be an order-preserving bijection on i≤n-1 data(ρ i ) as in Lemma 3.14. We can then pick a data value d such that

• for every d > d with d ∈ data(ρ n-1 ), f (g(d)) > d, and

• for every d < d with d ∈ data(ρ n-1 ), f (g(d)) < d. Let h := (g • f )[ d → d]. We then have • h(ρ n-1 ) h(ρ n ), • f (ρ 1 ) • • • f (ρ n-1 ), • f (ρ n-1 ) = h(ρ n-1 ).
In other words, f (ρ 1 )

• • • f (ρ n-1 ) h(ρ n ), with h(ρ n ) ∼ ord ρ n and f (ρ i ) ∼ ord ρ i for every i ≤ n -1.
Now that we proved that we can work modulo ∼ ord , we show that we can decide if we can reach an accepting configuration by means of ord , by introducing some suitable ordering < < and showing the following lemmas.

Lemma 3.19. (C ara , < <) is a well-quasi-order. Lemma 3.20. (C ara , < <) is rdc with respect to ord .

Lemma 3.21. The set of accepting configurations of C ara is downward closed with respect to < <.

We next define the order < < and show that the aforementioned lemmas are valid. In the same spirit as before, < < is defined as modulo ∼ ord . Definition 3.22 (< <). ρ 1 < < ρ 2 iff ρ 1 ρ 2 for some ρ 1 ∼ ord ρ 1 and ρ 2 ∼ ord ρ 2 .

To prove Lemma 3.19, given a configuration ρ = i 0 , α, (a, d), ∆ , with data(ρ

) = {d 1 < • • • < d n } we define abs(d j ) = ∆(d j ) ∪ { | d j = d} ⊆ Q ∪ { } abs(ρ) = abs(d 1 ), . . . , abs(d n ) ∈ (℘(Q ∪ { })) *
where ∈ Q is to denote that the data value is the one of the current configuration.

Proof of Lemma 3.19. This is a consequence of Higman's Lemma stated as in Corollary 2.3. As stated above, we can see each configuration ρ = (i, α, (a, d), ∆) as a word over (℘(Q ∪ { })) * . As shown in Lemma 3.9 if there is an infinite sequence, there is an infinite subsequence ρ 1 , ρ 2 , . . . , with the same type α and letter a. Then for the infinite sequence abs(ρ 1 ), abs(ρ 2 ), . . . , Corollary 2.3 tells us that there are i < j such that abs(ρ i ) is a substring of abs(ρ j ). This implies that they are in the < < relation.

Proof of Lemma 3.20. Note that although < < is a more restricted wqo, for all the nonmoving cases in which the register is not modified (that is, all except guess, spread, and store), the → ε transition continues to be rdc. This is because for any τ < < ρ → ρ , ρ = i, α, γ, ∆ and ρ = i , α , γ , ∆ are similar in the following sense. Firstly data(ρ) = data(ρ ), and moreover the only difference between ρ and ρ is that ∆ is the result of removing some thread (q, d) from ∆ and inserting another one (q , d) with the same data value d. This kind of operation is compatible, since τ can perform the same operation τ → ε τ on the data value d , supposing that d is the preimage of d given by the < < ordering. In this case, τ < < ρ . Otherwise, if there is no preimage of d, then τ < < ρ . The compatibility of spread is shown equivalently.

Regarding the store instruction, we see that the operation consists in removing some (q, d) from ∆ and inserting some (q , d 0 ) with d 0 the datum of the current configuration. This is downwards compatible since τ can perform the same operation on the configuration's data value, which is necessarily the preimage of d 0 .

For the remaining two cases (guess and ) we rely on the premise that we work modulo ∼ ord . The idea is that we can always assume that we have enough data values to choose from in between the existing ones. That is, for every pair of data values d < d in a configuration, there is always one in between. We can always assume this since otherwise we can apply a bijection as the one described by Lemma 3.14 to obtain this property. Thus, at each point where we need to guess a data value (as a consequence of a guess(q) or a q instruction) we will have no problem in performing a symmetric action, preserving the embedding relation.

More concretely, suppose the execution of a transition δ(q) = guess(q ) on a thread (q, d j ) of configuration ρ with data(ρ

) = {d 1 < • • • < d n } guesses a data value d with d i < d < d i+1 .
Then, for any configuration τ < < ρ with data(τ ) = {e 1 < • • • < e m } and the property just described, there must be an order-preserving injection f : data(τ ) → data(ρ) with f (τ ) ρ. If τ contains a thread (q, e j ) with f (e j ) = d j the operation is simulated by guessing a data value e such that e > e for all e such that f (e ) ≤ d i and e < e k for all e k such that f (e k ) > d i . Such data value e exists as explained before. The rdc compatibility of a δ(q) = q instruction is shown in an analogous fashion.

Proof of Lemma 3.21. Given that < < is a subset of , and that by Lemma 3.11 the set of accepting configurations is -downward closed, it follows that this set is also < <-downward closed.

Finally, we should note that (C ara /∼ ord , ord ) is also finitely branching and effective. As in the proof of Section 3.2, by Lemmas 3.19, 3.20 and 3.21 we have that all the conditions of Proposition 2.7 are met and by Lemma 2.8 we conclude that the emptiness problem for ARA(guess, spread, <) is decidable.

Remark 3.23. Notice that this proof works independently of the particular ordering of (D, <). It could be dense or discrete, contain accumulation points, be open or closed, etc. In some sense, this automata model is blind to these kind of properties. If there is an accepting run on (D, <) then there is an accepting run on (D, < ) for any linear order < .

Open question 3.24. It is perhaps possible that these results can be extended to prove decidability when (D, <) is a tree-like partial order, this time making use of Kruskal's tree theorem [START_REF] Kruskal | Well-quasi-ordering, the tree theorem, and Vazsonyi's conjecture[END_REF] instead of Higman's Lemma. We leave this issue as an open question.

Remark 3.25 (constants). One can also extend this model with a finite number of constants {c 1 , . . . , c n } ⊆ D. In this case, we extend the transitions with the possibility of testing that the data value stored in the register is (or is not) equal to c i , for every i. In the proof, it suffices to modify ∼ ord to take into account every constant c i . In this case we define that ρ ∼ ord τ iff f (ρ) = ρ for some order-preserving bijection f on data(ρ) ∪ {c 1 , . . . , c n } such that f (c i ) = c i for every i. In this case Lemma 3.14 does not hold anymore, as there could be finitely many elements in between two constants. This is however an easily surmountable obstacle, by adapting Lemma 3.14 to work separately on the n + 1 intervals defined by c 1 , . . . , c n . Suppose c 1 < • • • < c n . Without any loss of generality we can assume that between c i and c i+1 there are infinitely many data values, or none (we can always add some constants to ensure this). Then, for every infinite interval [c i , c i+1 ], we will have a lemma like Lemma 3.14 that we can apply separately.

3.4. Timed automata. Our investigation on register automata also yields new results on the class of timed automata. An alternating 1-clock timed automaton is an automaton that runs over timed words. A timed word is a finite sequence of events. Each event carries a symbol from a finite alphabet and a timestamp indicating the quantity of time elapsed from the first event of the word. A timed word can hence be seen as a data word over the rational numbers, whose data values are strictly increasing. The automaton has alternating control and contains one clock to measure the lapse of time between two events (that is, the difference between the data of two positions of the data word). It can reset the clock, or test whether the clock contains a number equal, less or greater than a constant, from some finite set of constants. For more details on this automaton we refer the reader to [START_REF] Alur | A theory of timed automata[END_REF].

Register automata over ordered domains have a strong connection with timed automata. The work in [START_REF] Figueira | Relating timed and register automata[END_REF] shows that the problems of nonemptiness, language inclusion, language equivalence and universality are equivalent-modulo an ExpTime reduction-for timed automata and register automata over a linear order. That is, any of these problems for register automata can be reduced to the same problem on timed automata, preserving the number of registers equal to the number of clocks, and the mode of computation (nondeterministic, alternating). And in turn, any of these problems for timed automata can also be reduced to a similar problem on register automata over a linear order. We argue that this is also true when the automata are equipped with guess and spread.

Consider an extension of 1-clock alternating timed automata, with spread and guess, where

• the operator spread(q, q ) works in the same way as for register automata, duplicating all threads with state q as threads with state q , and • the guess(q) operator resets the clock to any value, non deterministically chosen, and continues the execution with state q. The coding technique of [START_REF] Figueira | Relating timed and register automata[END_REF] can be adapted to deal with the guessing of a clock (the spread operator being trivially compatible), and one can show the following statement.

Remark 3.26. The emptiness problem for alternating 1-clock timed automata extended with guess and spread reduces to the emptiness problem for the class ARA(guess, spread, <).

Hence, by Remark 3.26 cum Theorem 3.12 we obtain the following.

Remark 3.27. The emptiness problem for alternating 1-clock timed automata extended with guess and spread is decidable.

3.5.

A note on complexity. Although the ARA(guess, spread) and ARA(guess, spread, <) classes have both non-primitive-recursive complexity, we must remark that the decision procedure for the latter has much higher complexity. While the former can be roughly bounded by the Ackermann function applied to the number of states, the complexity of the decision procedure we give for ARA(guess, spread, <) majorizes every multiply-recursive function (in particular, Ackermann's). In some sense this is a consequence of relying on Higman's Lemma instead of Dickson's Lemma for the termination arguments of our algorithm.

More precisely, it can be seen that the emptiness problem for ARA(guess, spread, <) sits in the class F ω ω in the Fast Growing Hierarchy [LW70]-an extension of the Grzegorczyk Hierarchy for non-primitive-recursive functions-by a reduction to the emptiness problem for timed one clock automata (see §3.4), which are known to be in this class. 3 However, the emptiness problem for ARA(guess, spread) belongs to F ω in the hierarchy. The lower bound follows by a reduction from Incrementing Counter Automata [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF], which are hard for F ω [START_REF] Schnoebelen | Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets[END_REF][START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's lemma[END_REF]. The upper bound is a consequence of using a saturation algorithm with a wqo that is the component-wise order of the coordinates of a vector of natural numbers in a controlled way. The proof that it belongs to F ω goes similarly as for Incrementing Counter Automata [see FFSS11, §7.2]. We do not know whether the emptiness problem for ARA(guess, spread, <) is also in F ω .

LTL with registers

The logic LTL ↓ (U, X) is a logic for data words that corresponds to the extension of the Linear-time Temporal Logic LTL(U, X) on data words, with the ability to use one register for storing a data value for later comparisons, studied in [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF][START_REF] Demri | On the freeze quantifier in constraint LTL: Decidability and complexity[END_REF]. It contains the next (X) and until (U) temporal operators to navigate the data word, and two extra operators. 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.

As it was shown in [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF], if we allow more than one register to store data values, satisfiability of LTL ↓ (U, X) becomes undecidable. We will then focus on the language that uses only one register. We study an extension of this language with a restricted form of quantification over data values. We will actually add two sorts of quantification. On the one hand, the operators ∀ ↓ ≤ and ∃ ↓ ≤ quantify universally or existentially over all the data values occurring before the current point of evaluation. Similarly, ∀ ↓ ≥ and ∃ ↓ ≥ quantify over the future elements on the data word. For our convenience and without any loss of generality, we will work in Negation Normal Form (nnf), and we use Ū to denote the dual operator of U, and similarly for X. Sentences of

LTL ↓ nnf (U, Ū, X, X, O), where O ⊆ {∀ ↓ ≤ , ∃ ↓ ≤ , ∀ ↓ ≥ , ∃ ↓ ≥ } are defined as follows, ϕ ::= a | ¬a | ↑ | ¬ ↑ | ↓ ϕ | Xϕ | Xϕ | U(ϕ, ϕ) | Ū(ϕ, ϕ) | op ϕ | ϕ ∧ ϕ | ϕ ∨ ϕ
where a is a symbol from a finite alphabet A, and op ∈ O. For economy of space we write LTL ↓ nnf (F, O) to denote this logic. In this notation, F is to mark that we have all the forward modalities: U, Ū, X, X. Notice that the future modality can be defined Fϕ := U(ϕ, ) and its dual Gϕ as the nnf of ¬F¬ϕ.

Figure 4 shows the definition of the satisfaction relation |=. For example, in this logic we can express properties like "for every a element there is a future b element with the same data value" as G(¬a ∨ ↓ (F(b ∧ ↑))). We say that ϕ satisfies w = a ⊗ d, written w |= ϕ, if w, 1 |= d(1) ϕ.

4.1. Satisfiability problem. This section is dedicated to the satisfiability problem for LTL ↓ nnf (F, ∀ ↓ ≤ , ∃ ↓ ≥ ). But first let us show that ∃ ↓ ≤ and ∀ ↓ ≥ result in an undecidable logic.

Theorem 4.1. Let ∃ ↓ < be the operator ∃ ↓ ≤ restricted only to the data values occurring strictly before the current point of evaluation. Then, on finite data words:

3 The emptiness problem for timed one clock automata can be at the same time reduced to that of Lossy Channel Machines [START_REF] Parosh | Decidability and complexity results for timed automata via channel machines[END_REF], which are known to be 'complete' for this class, i.e., in Fωω \F<ωω

[see CS08]. (w, i) |= d a iff a(i) = a (w, i) |= d ↑ iff d = d(i) (w, i) |= d ↓ ϕ iff (w, i) |= d(i) ϕ (w, i) |= d U(ϕ, ψ) iff for some i ≤ j ∈ pos(w) and for all i ≤ k < j we have (w, j) |= d ϕ and (w, k) |= d ψ (w, i) |= d Xϕ iff i + 1 ∈ pos(w) and (w, i + 1) |= d ϕ (w, i) |= d ∃ ↓ ≥ ϕ iff there exists i ≤ j ∈ pos(w) such that (w, i) |= d(j) ϕ (w, i) |= d ∀ ↓ ≤ ϕ iff for all 1 ≤ j ≤ i we have (w, i) |= d(j) ϕ Figure 4: Semantics of LTL ↓ (U, Ū, X, X, ∃ ↓ ≥ , ∀ ↓ ≤ )
for a data word w = a ⊗ d and i ∈ pos(w).

(1) satisfiability of

LTL ↓ nnf (F, G, ∃ ↓ < ) is undecidable; and (2) satisfiability of LTL ↓ nnf (F, G, ∀ ↓ ≥ ) is undecidable. Proof.
We prove (1) and (2) by reduction of the halting problem for Minsky machines. We show that these logics can code an accepting run of a 2-counter Minsky machine as in Proposition 3.2. Indeed, we show that the same kind of properties are expressible in this logic. To prove this, we build upon some previous results [START_REF] Figueira | Future-looking logics on data words and trees[END_REF] showing that LTL ↓ nnf (F, G) can code conditions (i) and (ii) of the proof of Proposition 3.2. Here we show that both LTL ↓ nnf (F, G, ∃ ↓ < ) and LTL ↓ nnf (F, G, ∀ ↓ ≥ ) can express condition (iii), ensuring that for every decrement (dec i ) there is a previous increment (inc i ) with the same data value. Let us see how to code this.

(1) The LTL ↓ nnf (F, G, ∃ ↓ < ) formula G(dec i → ∃ ↓ < ↑) states that the data value of every decrement must not be new, and in the context of this coding this means that it must have been introduced by an increment instruction.

(2

) The LTL ↓ nnf (F, G, ∀ ↓ ≥ ) formula ∀ ↓ ≥ (F(dec i ∧ ↑) → F(inc i ∧ ↑
)) evaluated at the first element of the data word expresses that for every data value: if there is a decrement with value d, then there is an increment with value d. It is then easy to ensure that they appear in the correct order (first the increment, then the decrement). The addition of any of these conditions to the coding of [START_REF] Figueira | Future-looking logics on data words and trees[END_REF] results in a coding of an n-counter Minsky machine, whose emptiness problem is undecidable.

Corollary 4.2. The satisfiability problem for both LTL ↓ nnf (F, ∃ ↓ ≤ ) and LTL ↓ nnf (F, ∀ ↓ ≥ ) are undecidable.

Proof. The property of item (1) in the proof of Theorem 4.1 can be equally coded in

LTL ↓ nnf (F, ∃ ↓ ≤ ) as G(X(dec i ) → ∃ ↓ ≤ (X ↑)).
The undecidability of LTL ↓ nnf (F, ∀ ↓ ≥ ) follows directly from Theorem 4.1, item (2).

We now turn to our decidability result. We show that LTL ↓ nnf (F, ∀ ↓ ≤ , ∃ ↓ ≥ ) has a decidable satisfiability problem by a translation to ARA(guess, spread).

The translation to code LTL ↓ nnf (F, ∀ ↓ ≤ , ∃ ↓ ≥ ) into ARA(guess, spread) is standard, and follows same lines as [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] 4 (which at the same time follows the translation from LTL ↓ (U, X) to alternating finite automata). We then obtain the following result.

Proposition 4.3. ARA(guess, spread) captures LTL ↓ nnf (F, ∃ ↓ ≥ , ∀ ↓ ≤ ). From Proposition 4.3 and Theorem 3.5 it will follow the main result, stated next.

Theorem 4.4. The satisfiability problem for LTL ↓ nnf (F, ∃ ↓ ≥ , ∀ ↓ ≤ ) is decidable. We now show how to make the translation to ARA(guess, spread) in order to obtain our decidability result.

Proof of Proposition

4.3. Let η ∈ LTL ↓ nnf (F, ∀ ↓ ≤ , ∃ ↓ ≥ ). We show that for every formula η ∈ LTL ↓ nnf (F, ∀ ↓ ≤ , ∃ ↓ ≥ )
there exists a computable ARA(spread, guess) A η such that for every data word w, w satisfies η iff A η accepts w. In the construction of A ϕ , we first make sure to maintain all the data values seen so far as threads of the configuration. We can do this by having 4 special states q 0 , q 1 , q 2 , q save in A η , defining q 0 as the initial state, and δ as follows.

δ(q 0 ) = q η ∧ q 1 δ(q 1 ) = store(q 2 ) δ(q 2 ) = ( ¯ ? ∨ q 1 ) ∧ q save δ(q save ) = ¯ ? ∨ q save Now we can assume that at any point of the run, we maintain the data values of all the previous elements of the data word as threads (q save , d). Note that these threads are maintained until the last element of the data word, at which point the test ¯ ? is satisfied and they are accepted. Now we show how to define A η . We proceed by induction on |η|. If η = a or ¬a, we simply define the set of states as Q = {q 0 , q 1 , q 2 , q save , q η } and δ(q η ) = a or δ(q η ) = ā (δ(q 0 ), δ(q 1 ), δ(q 2 ) and δ(q save ) are defined as above). If η = ↓ψ (or η = ↑, η = ¬↑) we define it as follows. We add one new state q η to the set of states of A ψ , we extend the definition of δ with δ(q η ) = store(q ψ ) (or δ(q η ) = eq(q ψ ), δ(q η ) = eq(q ψ )), and we redefine δ(q 1 ) with δ(q 1 ) = store(q 2 ) ∧ q η . If η = Fψ, η = Gψ, or η = U(ψ, ψ ), it is easy to define δ(q η ) from the definition of A ψ and A ψ , perhaps adding some new states. On the other hand, if ϕ = ψ ∧ ψ or ϕ = ψ ∨ ψ , it is also straightforward as it corresponds to the alternation and nondeterminism of the automaton.

Suppose now that η = ∀ ↓ ≤ ψ. We define A η as A ψ with the extra state q η and we define δ(q η ) = spread(q save , q ψ ) ∧ ↓q ψ . This ensures that at the moment of execution of this instruction, all the previous data values in the data word will be taken into account, including the current one.

(w, i)

|= d ↑ > iff d > d(i) (w, i) |= d ↑ < iff d < d(i)
Figure 5: Semantics for the operators ↑ > , ↑ < for a data word w = a ⊗ d and i ∈ pos(w).

Finally, if η = ∃ ↓ ≥ ψ, we build A η from A ψ in the same fashion as before, adding new states q η , q η , q η , defining δ(q η ) = guess(q η ), δ(q η ) = q ψ ∧ q η , δ(q η ) = eq ∨ q η . Note that q η checks that the guessed data value appears somewhere in a future position of the word.

Moreover, we argue that these extensions add expressive power.

Proposition 4.5. On finite data words:

(i) The logic LTL ↓ nnf (F, ∀ ↓ ≤ ) is more expressive than LTL ↓ nnf (F); (ii) The logic LTL ↓ nnf (F, ∃ ↓ ≥ ) is more expressive than LTL ↓ nnf (F).
Proof. This is a consequence of LTL ↓ nnf (F) being closed under negation and Theorem 4.1. Ad absurdum, if one of these logics were as expressive as LTL ↓ nnf (F), then it would be closed under negation, and then we could express conditions (1) or (2) of the proof of Theorem 4.1 and hence obtain that LTL ↓ nnf (F) is undecidable. But this leads to a contradiction since by Theorem 4.4 LTL ↓ nnf (F) is Remark 4.6. The translation of Proposition 4.3 is far from using all the expressive power of spread. In fact, we can consider a binary operator ∀ ↓ ≤ (ϕ, ψ) defined w, i |= d ∀ ↓ ≤ (ϕ, ψ) iff for all j ≤ i such that w, j |= d(j) ψ, we have w, i |= d(j) ϕ. with ψ ∈ LTL ↓ nnf (F). This operator can be coded into ARA(guess, spread), using the same technique as in Proposition 4.3. The only difference is that instead of 'saving' every data value in q save , we use several states q save(ψ) . Intuitively, only the data values that verify the test ↓ ψ are stored in q save(ψ) . Then, a formula ∀ ↓ ≤ (ϕ, ψ) is translated as spread(q save(ψ) , q ϕ ).

4.2. Ordered data. If we consider a linear order over D as done in Section 3.3, we can consider

LTL ↓ nnf (F, ∃ ↓ ≥ , ∀ ↓ ≤ ) with richer tests ϕ ::= ↑ > | ↑ < | . . .
that access to the linear order and compare the data values for =, <, >. The semantics are extended accordingly, as in Figure 5. Let us call this logic ord -LTL ↓ nnf (F, ∃ ↓ ≥ , ∀ ↓ ≤ ). The translation from ord -LTL ↓ nnf (F, ∃ ↓ ≥ , ∀ ↓ ≤ ) to ARA(guess, spread, <) as defined in Section 3.3 is straightforward. Thus we obtain the following result.

Proposition 4.7. The satisfiability problem for ord -LTL ↓ nnf (F, ∃ ↓ ≥ , ∀ ↓ ≤ ) is decidable.

Part 2. Data trees

The second part of this work deals with logics and automata for data trees. In Section 5, we extend the model ARA(guess, spread) to the new model ATRA(guess, spread) that runs over data trees (instead of data words). The decidability of the emptiness follows easily from the decidability result shown for ARA(guess, spread). As in the case of data trees, this model allows to show the decidability of a logic.

In Section 6 we introduce 'forward XPath', a logic for xml documents. The satisfiability problem for this logic will follow by a reduction to the emptiness problem of ATRA(guess, spread). This reduction is not as easy as that of the first part, since XPath is closed under negation and our automata model is not closed under complementation. Indeed, ATRA(guess, spread) and forward XPath have incomparable expressive power.

ATRA model

Herein, we introduce the class of Alternating Tree Register Automata by slightly adapting the definition for alternating (word) register automata. This model is essentially the same automaton presented in Part 1, that works on a (unranked, ordered) data tree instead of a data word. The only difference is that instead of having one instruction that means 'move to the next position', we have two instructions and meaning 'move to the next sibling to the right' and 'move to the leftmost child'. This class of automata is known as ATRA(guess, spread). This model of computation will enable us to show decidability of a large fragment of XPath.

An Alternating Tree Register Automaton (ATRA) consists in a top-down tree walking automaton with alternating control and one register to store and test data. [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] shows that its emptiness problem is decidable and non-primitive-recursive. Here, as in the Part 1, we consider an extension with the operators spread and guess. We call this model ATRA(spread, guess). Definition 5.1. An alternating tree register automaton of ATRA(spread, guess) is a tuple A = A, Q, q I , δ such that A is a finite alphabet; Q is a finite set of states; q I ∈ Q is the initial state; and δ : Q → Φ is the transition function, where Φ is defined by the grammar

a | ā | ? | store(q) | eq | eq | q ∧ q | q ∨ q | q | q | guess(q) | spread(q, q ) where a ∈ A, q, q ∈ Q, ∈ { , ¯ , , ¯ }.
We only focus on the differences with respect to the ARA class.

and are to move to the leftmost child or to the next sibling to the right of the current position, and as before ' ?' tests the current type of the position of the tree. For example, using ¯ ? we test that we are in a leaf node, and by ? that the node has a sibling to its right. store(q), eq and eq work in the same way as in the ARA model. We say that a state q ∈ Q is moving if δ(q) = q or δ(q) = q for some q ∈ Q.

We define two sorts of configurations: node configurations and tree configurations. In this context a node configuration is a tuple x, α, γ, ∆ that describes the partial state of the execution at a position x of the tree. x ∈ pos(t) is the current position in the tree t, γ = t(x) ∈ A × D is the current node's symbol and datum, and α = type t (x) is the tree type of x. As before, ∆ ∈ ℘ <∞ (Q × D) is a finite collection of execution threads. N atra is the set of all node configurations. A tree configuration is just a finite set of node configurations, like { , α, γ, ∆ , 1211, α , γ , ∆ , . . . }. We call T atra = ℘ <∞ (N atra ) the set of all tree configurations.

We define the non-moving relation → ε over node configurations just as in page 10. As a difference with the ARA mode, we have two types of moving relations. The first-child relation → , to move to the leftmost child, and the next-sibling relation → to move to the next sibling to the right.

The → and → are defined, for any

α 1 ∈ { , ¯ , , ¯ }, γ, γ 1 ∈ A × D, h ∈ { , ¯ }, v ∈ { , ¯ }, as follows x, ( , h), γ, ∆ → x•1, α 1 , γ 1 , ∆ , (5.1) x•i, (v, ), γ, ∆ → x•(i + 1), α 1 , γ 1 , ∆ (5.2)
iff (i) the configuration is 'moving' (i.e., all the threads (q, d) contained in ∆ are of the form δ(q) = q or δ(q) = q ); and (ii

) for ∈ { , }, ∆ = {(q , d) | (q, d) ∈ ∆, δ(q) = q }. Let → := → ε ∪ → ∪ → ⊆ N atra × N atra .
Note that through → we obtain a run over a branch of the tree (if we think about the underlying binary tree according to the first-child and next-sibling relations). In order to maintain all information about the run over all branches we need to lift this relation to tree configurations. We define the transition between tree configurations that we write . This corresponds to applying a 'non-moving' → ε to a node configuration, or to apply a 'moving' → , → , or both to a node configuration according to its type. That is, we define S 1 S 2 iff one of the following conditions holds:

(1)

S 1 = {ρ} ∪ S , S 2 = {τ } ∪ S , ρ → ε τ ; (2) S 1 = {ρ} ∪ S , S 2 = {τ } ∪ S , ρ = x, ( , ¯ ), γ, ∆ , ρ → τ ; (3) S 1 = {ρ} ∪ S , S 2 = {τ } ∪ S , ρ = x, ( ¯ , ), γ, ∆ , ρ → τ ; (4) S 1 = {ρ} ∪ S , S 2 = {τ 1 , τ 2 } ∪ S , ρ = x, ( , ), γ, ∆ , ρ → τ 1 , ρ → τ 2 .
A run over a data tree t = a ⊗ d is a nonempty sequence S 1

• • •

S n with S 1 = { , α 0 , γ 0 , ∆ 0 } and ∆ 0 = {(q I , d( ))} (i.e., the thread consisting in the initial state with the root's datum), such that for every i ∈ [n] and x, α, γ, ∆ ∈ S i : (1) x ∈ pos(t); (2) γ = t(x); and (3) α = type t (x). As before, we say that the run is accepting if

S n ⊆ { x, α, γ, ∅ | x, α, γ, ∅ ∈ N atra }.
Note that the transition relation that defines the run replaces a node configuration in a given position by one or two node configurations in children positions of the fcns coding. Therefor the following holds.

Remark 5.2. Every run is such that any of its tree configurations never contains two node configurations in a descendant/ancestor relation of the fcns coding.

The ATRA model is closed under all boolean operations [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF]. However, the extensions introduced guess and spread, while adding expressive power, are not closed under complementation as a trade-off for decidability. It is not surprising that the same properties as for the case of data words apply here.

Proposition 5.3. ATRA(spread, guess) models have the following properties:

(i) they are closed under union, (ii) they are closed under intersection, (iii) they are not closed under complementation.

Example 5.4. We show an example of the expressiveness that guess adds to ATRA. Although as a corollary of Proposition 3.2 we have that the ATRA(guess, spread) class is more expressive than ATRA, we give an example that inherently uses the tree structure of the model. We force the node at position 2 and the node at position 1•1 of a data tree to have the same data value without any further data constraints. Note that this datum does not necessarily have to appear at some common ancestor of these nodes. Consider the ATRA(guess) defined over A = {a} with δ(q 0 ) = guess(q 1 ), δ(q 1 ) = q 2 , δ(q 2 ) = q 3 ∧ q 4 , δ(q 3 ) = q 5 , δ(q 4 ) = q 5 , δ(q 5 ) = eq.

a, 1 a, 1 a, 2 a, 2 a, 1 a, 1 a, 3 a, 2
For the data trees of Figure 6, any ATRA either accepts both, or rejects both. This is because when a thread is at position 1, and performs a moving operation splitting into two threads, one at position 1•1, the other at position 2, none of these configurations contain the data value 2. Otherwise, the automaton should have read the data value 2, which is not the case. But then, we see that the continuation of the run from the node configuration at position 2 and at position 1 are isomorphic independently of which data values we choose (either the data 2 and 3, or the data 2 and 2). Hence, both trees are accepted or rejected. However, the ATRA(guess) we just built distinguishes them, as it can introduce the data value 2 in the configuration, without the need of reading it from the tree. Equivalently, the property of "there are two leaves with the same data values" is expressible in ARA(guess) and not in ARA.

Emptiness problem.

We show that the emptiness problem for this model is decidable, reusing the results of Part 1. We remind the reader that the decidability of the emptiness of ATRA was proved in [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF]. Here we extend the approach used for ARA and show the decidability of the two extensions spread and guess.

Theorem 5.5. The emptiness problem of ATRA(guess, spread) is decidable.

Proof. The proof goes as follows. We will reuse the wqo used in Section 3.2, which here is defined over the node configurations. The only difference being that to use over N atra we work with tree types instead of word types. Since → and → are analogous, by the same proof as in Lemma 3.10 we obtain the following.

Lemma 5.6. (N atra , → ), (N atra , → ), (N atra , → ε ), (and therefore (N atra , →)) are rdc with respect to (N atra , ).

We now lift this result to tree configurations. We instantiate Proposition 2.11 by taking • S as N atra , ≤ as , and ≤ ℘ as the majoring order over (N atra , ),

• → 1 1 as → , → 2 1 as → , → 3 1 as → ε , • P ⊆ N atra as the set of all configurations ρ so that ρ = x, ( , ), γ, ∆ (it is immediate to se that it is downward-and upward-closed with respect to ), • → 2 to be , as it verifies the hypotheses demanded in the Lemma.

We thus obtain the following.

Lemma 5.7. (T atra , ) is rdc with respect to (T atra , ≤ ℘ ).

Hence, condition (1) of Proposition 2.7 is met. Let us write ≡ for the equivalence relation over T atra such that S ≡ S iff S ≤ ℘ S and S ≤ ℘ S. Similarly as for Part 1, we have that (T atra /≡, ) is finitely branching and effective. That is, the -image of any configuration has only a finite number of configurations up to isomorphism of the data values contained (remember that only equality between data values matters), and representatives for every class are computable. Hence, we have that (T atra /≡, , ≤ ℘ ) verifies condition (2) of Proposition 2.7. Finally, condition (3) holds as (T atra /≡, ≤ ℘ ) is a wqo (by Proposition 2.10) that is a computable relation. We conclude the proof by the following obvious statement.

Lemma 5.8. The set of accepting tree configurations is downwards closed with respect to ≤ ℘ .

Hence, by Lemma 2.8, we conclude as before that the emptiness problem for the class ATRA(guess, spread) is decidable.

Forward-XPath

We consider a navigational fragment of XPath 1.0 with data equality and inequality. In particular this logic is here defined over data trees. However, an xml document may typically have not one data value per node, but a set of attributes, each carrying a data value. This is not a problem since every attribute of an xml element can be encoded as a child node in a data tree labeled by the attribute's name (cf. Section 6.3). Thus, all the decidability results hold also for XPath with attributes over xml documents.

Let us define a simplified syntax for this logic. XPath is a two-sorted language, with path expressions (α, β, . . . ) and node expressions (ϕ, ψ, . . . ). We write XPath(O, =) to denote the data-aware fragment with the set of axes O ⊆ {↓, ↓ * , →, → * , ←, * ←, ↑, ↑ * }. It is defined by mutual recursion as follows,

α, β ::= o | [ϕ] | αβ | α ∪ β o ∈ O ∪ {ε} ϕ, ψ ::= a | ¬ϕ | ϕ ∨ ψ | ϕ ∧ ψ | α | α = β | α = β a ∈ A
where A is a finite alphabet. A formula of XPath(O, =) is either a node expression or a path expression. We define the 'forward' set of axes as F := {↓, ↓ * , →, → * }, and consequently the fragment 'forward-XPath' as XPath(F, =). We also refer by XPath ε (F, =) to the fragment considered in [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] where data tests are of the restricted form ε = α or ε = α . 5

There have been efforts to extend XPath to have the full expressivity of MSO, e.g. by adding a least fix-point operator (cf. [tC06, Sect. 4.2]), but these logics generally lack clarity and simplicity. However, a form of recursion can be added by means of the Kleene star, which allows us to take the transitive closure of any path expression. Although in general this is not enough to already have MSO [START_REF] Balder Ten | XPath, transitive closure logic, and nested tree walking automata[END_REF], it does give an intuitive language 5 [JL11] refers to XPath ε (F, =) as 'forward XPath'. Here, 'forward XPath' is the unrestricted fragment XPath(F, =), as we believe is more appropriate. with a counting ability. By regXPath(O, =) we refer to the enriched language where path expressions are extended by allowing the Kleene star on any path expression.

α, β ::= o | [ϕ] | αβ | α ∪ β | α * o ∈ O ∪ {ε}
Let t be a data tree. The semantics of XPath is defined as the set of elements (in the case of node expressions) or pairs of elements (in the case of path expressions) selected by the expression. The data aware expressions are the cases α = β and α = β . The formal definition of its semantics is in Figure 7. We write t |= ϕ to denote [[ϕ]] t = ∅, and in this case we say that t satisfies ϕ.

Example 6.1. In the model of Figure 1

on page 7, [[ ↓ * [b ∧ ↓ [b] =↓ [b] ] ]] t = { , 1, 1•2}.
We define sub(ϕ) to denote the set of all substrings of ϕ which are formulae, psub(ϕ) := {α | α ∈ sub(ϕ), α is a path expression}, and nsub(ϕ) := {ψ | ψ ∈ sub(ϕ), ψ is a node expression}.

6.1. Key constraints. It is worth noting that XPath(F, =) -contrary to XPath ε (F, =)can express unary key constraints. That is, whether for some symbol a, all the a-elements in the tree have different data values. Lemma 6.2. For every a ∈ A let key(a) be the property over a data tree t = a ⊗ d: "For every two different positions x, x ∈ pos(t) of the tree, if a(x) = a(x ) = a, then d(x) = d(x )." Then, key(a) is expressible in XPath(F, =) for any a.

Proof. It is easy to see that the negation of this property can be tested by first guessing the closest common ancestor of two different a-elements with equal datum in the underlying first-child next-sibling binary tree. At this node, we verify the presence of two a-nodes with equal datum, one accessible with a "↓ * " relation and the other with a compound "→ + ↓ * " relation (hence the nodes are different). The expressibility of the property then follows from the logic being closed under negation. The reader can check that the following formula expresses the property

key(a) ≡ ¬ ↓ * [ ε[a] =↓ + [a] ∨ ↓ * [a] =→ + ↓ * [a] ]
where '↓ + ' = '↓↓ * ' and '→ + ' = '→→ * '.

Note that while ATRA cannot express, for instance, that there are two different nodes with the same data value, ATRA(guess) can express it. However, on the other hand, ATRA(guess, spread) cannot express the negation of the property. Lemma 6.3. The class ATRA(guess, spread) cannot express the property "all the data values of the data tree are different".

Proof. Ad absurdum, suppose that there exists an automaton A expressing the property, and let Q be its set of states. Notice that for any accepting run of minimal length there are no more that f (|Q|, n) consecutive -transitions (i.e., transitions that are fired by an underlying → transition on node configurations), for some fixed function f , where n is the number of moving transitions from the initial configuration. This is because of the rdc property of (T atra , ) with respect to (T atra , ≤ ℘ ) (Lemma 5.7) and the fact that preserves current position's letter and datum. Using this, one can see that, if there is an accepting run S 1

• • • S N on a data tree t containing non-moving

S i • • • S i+k so that S i ≤ ℘ S i+k , then there are S i+k+1 ≤ ℘ S i+k+1 , . . . , S N ≤ ℘ S N so that S 1 • • • S i S i+k+1
• • • S N is an accepting run on t. Since ≤ ℘ is a wqo this must always happen for a sufficiently large k, computable from A and i.

Consider a data tree t with

pos(t) = { } ∪ {1, 2, 3, . . . , N } ∪ {11, 111, . . . , 111 • • • 1 N times } for N = f (|Q|, 0) + f (|Q|, 1) + 4
That is, the root of the tree has N children, and the first child has a long branch with N nodes. All positions of t have different data values, and they all carry the same label, say a.

Consider a minimal accepting run of A on t, S 1

• • •

S n . Let S i be the first tree configuration containing a node configuration with position 2. That is, the first configuration after the second moving transition. Since there are at most f (|Q|, 0) + f (|Q|, 1) non-moving transitions before S i in the run, we have that i ≤ f (|Q|, 0) + f (|Q|, 1) + 2. In particular, this means that S i cannot contain more than f (|Q|, 0) + f (|Q|, 1) + 2 different data values.

Therefore, there is a position x with 2 ≤ x ≤ N and a position y with y 1 such that neither d(x) or d(y) are in data(S i ). (Remember that by definition of t, d(x) = d(y).) This is because there are N -1 = f (|Q|, 0) + f (|Q|, 1) + 3 different possible data values of x and for y.

Consider t as the result of replacing d(x) by d(y) in t. Clearly, t does not have the property "all the data values of the data tree are different". Now, consider the run obtained as the result of replacing d(x) by d(y) in S 1 , . . . , S n . Note that this is still a run, and it is still accepting. Therefore A accepts t and thus A does not express the property. 6.2. Satisfiability problem. This section is mainly dedicated to the decidability of the satisfiability problem for XPath(F, =), known as 'forward-XPath'. This is proved by a reduction to the emptiness problem of the automata model ATRA(guess, spread) introduced in Section 5. [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] shows that ATRA captures the fragment XPath ε (F, =). It is immediate to see that ATRA can also easily capture the Kleene star operator on any path formula, obtaining decidability of regXPath ε (F, =). However, these decidability results cannot be further generalized to the full unrestricted forward fragment XPath(F, =) as ATRA is not powerful enough to capture the full expressivity of the logic. Indeed, while XPath(F, =) can a, 0 b, 0 c, 0 <a> <b @att1="4" @att2="6"> <c @att1="2"/> </b> </a> express that all the data values of the leaves are different, ATRA(guess, spread) cannot (Lemma 6.3). Although ATRA(guess, spread) cannot capture XPath(F, =), in the sequel we show that there exists a reduction from the satisfiability of regXPath(F, =) to the emptiness of ATRA(guess, spread), and hence that the former problem is decidable. This result settles an open question regarding the decidability of the satisfiability problem for the forward-XPath fragment XPath(F, =). The main results that will be shown in Section 6.4 are the following.

Theorem 6.4. Satisfiability of regXPath(F, =) in the presence of DTDs (or any regular language) and unary key constraints is decidable, non-primitive-recursive.

And hence the next corollary follows from the logic being closed under boolean operations.

Corollary 6.5. The query containment and the query equivalence problems are decidable for XPath(F, =). Moreover, these decidability results hold for regXPath(F, =) and even for two extensions:

• a navigational extension with upward axes (in Section 6.5), and • a generalization of the data tests that can be performed (in Section 6.6).

6.3. Data trees and XML documents. Although our main motivation for working with trees is related to static analysis of logics for xml documents, we work with data trees, being a simpler formalism to work with, from where results can be transferred to the class of xml documents. We discuss briefly how all the results we give on XPath over data trees, also hold for the class of xml documents. While a data tree has one data value for each node, an xml document may have several attributes at a node, each with a data value. However, every attribute of an xml element can be encoded as a child node in a data tree labeled by the attribute's name, as in Figure 8. This coding can be enforced by the formalisms we present below, and we can thus transfer all the decidability results to the class of xml documents. In fact, it suffices to demand that all the attribute symbols can only occur at the leaves of the data tree and to interpret attribute expressions like '@attrib1 ' of XPath formulae as child path expressions '↓ [attrib1 ]'. 6.4. Decidability of forward XPath. This section is devoted to the proof of the following statement. Proposition 6.6. For every η ∈ regXPath(F, =) there is a computable ATRA(guess, spread) automaton A such that A is nonempty iff η is satisfiable.

x•i
Figure 9: The disjoint values property states that for every position x•i, the intersection of the grey zones is present in the last configuration for x•i appearing in the run.

Markedly, the ATRA(guess, spread) class does not capture regXPath(F, =). However, given a formula η, it is possible to construct an automaton that tests a property that guarantees the existence of a data tree verifying η.

Disjoint values property. To show the above proposition, we need to work with runs with the disjoint values property as stated next. Definition 6.7. A run S 1 • • • S n on a data tree t has the disjoint values property if for every x•i ∈ pos(t) and ρ a moving node configuration of the run with position x•i, then

data(t| x•i ) ∩ x•j∈pos(t) j>i data(t| x•j ) ⊆ data(ρ) .
Figure 9 illustrates this property.

The proof of Proposition 6.6 can be sketched as follows:

(1) We show that for every nonempty automaton A ∈ ATRA(guess, spread) there is an accepting run on a data tree with the disjoint values property. (2) We give an effective translation from an arbitrary forward XPath formula η to an ATRA(guess, spread) automaton A such that

• any tree accepted by a run of the automaton A with the disjoint values property verifies the XPath formula η, and

• any tree verified by the formula η is accepted by a run of the automaton A

with the disjoint values property. We start by proving the disjoint values property normal form. Proposition 6.8. For any nonempty automaton A ∈ ATRA(guess, spread) there exists an accepting run over some data tree with the disjoint values property.

Proof. Given any accepting run S 1

• • •

S n on a data tree t = a ⊗ d, we show how to modify the run and the tree in order to satisfy the disjoint values property. We only need to replace some of the data values, so that the resulting tree and accepting run will be essentially the same.

The idea is as follows. For a given position x•k of the tree, we consider the moving node configuration of the run at position x•k, and we replace all the data values from t| x•k by fresh ones except for those present in the node configuration, obtaining a new data tree t . We also make the same replacement of data values for all node configurations in the run of nodes below x•k. Thus, we end up with a modified data tree t and accepting run that satisfy the disjoint values property at x•k. That is, such that

data(t | x•k ) ∩ x•j∈pos(t) j>k data(t | x•j ) ⊆ data(ρ x•k )
where ρ x•k is the moving node configuration at position x•k of the run. If we repeat this procedure for all nodes of the tree, we obtain a run and tree with the disjoint values property.

Next, we formalize this transformation.

Take any x•k ∈ pos(t), and let ρ x•k ∈ S i for some i be such that ρ x•k is a moving node configuration with position x•k. Consider any injective function

f : data(t| x•k ) \ data(ρ x•k ) → D \ data(t)
and let f :

data(t| x•k ) → D be such that f (d) = d if d ∈ data(ρ x•k ), or f (d) = f (d) otherwise.
Note that f is injective. Let us consider then S 1 , . . . , S n where S j consists in replacing every node configuration ρ ∈ S j with h(ρ), where6

h(ρ) = f (ρ) if ρ has a position y x•k ρ otherwise.
Take t to be the data tree that results from the replacement in t of every data value of a position y x•k by f (d(y)).

Claim 1.

data(t | x•k ) ∩ x•j∈pos(t) j>k data(t | x•j ) ⊆ data(ρ x•k ) .
Proof. The only difference between t and t is in the data values below x•k. Any node y of t which is below x•k contains a data value f (d(y)) such that

• f (d(y)) is in data(ρ x•k ), or • f (d(y))
is not in data(t), and therefore it is not in x•j∈pos(t) j>k data(t | x•j ).

Claim 2. S 1 • • • S n is an accepting run of A over t .

Proof. Take any leaf y which is rightmost (i.e., with no siblings to its right) and consider the sequence of node configurations ρ 1 ∈ S 1 , . . . , ρ n ∈ S n that are ancestors of y in the first-child next-sibling underlying tree structure. There is exactly one configuration in each S i due to Remark 5.2. This is the 'sub-run' that leads to y: for every ρ i , ρ i+1 either ρ i = ρ i+1 or ρ i → ρ i+1 . Let ρ j = h(ρ j ) for all j ∈ [n].

• If y x•k, take to be the last index such that ρ = ρ x•k (there must be one).

Note that ρ j = f (ρ j ) for every < j ≤ n. The sequence ρ +1 ∈ S +1 , . . . , ρ n ∈ S n is isomorphic, modulo renaming of data values, to ρ +1 , . . . , ρ n since f is injective.

We then have that ρ 1 , . . . , ρ , . . . ρ n is a correct run on node configurations, since ρ 1 , . . . , ρ is equal to ρ 1 , . . . , ρ (it is not modified by h), -ρ +1 , . . . , ρ n is isomorphic to ρ +1 , . . . , ρ n (we apply an injection f to every data value), and the pair (ρ , ρ +1 ) is isomorphic to (ρ , ρ +1 ), as

* ρ = f (ρ x•k ) = ρ x•k = ρ , * ρ +1 = f (ρ +1
) is isomorphic to ρ +1 , and * data(ρ ) ∩ data(ρ +1 ) = data(ρ ) ∩ data(ρ +1 ) since f is the identity on data(ρ ), and does not send any data value from D \ data(ρ ) to data(ρ ).

• If y x•k, then nothing was modified:

ρ 1 = ρ 1 ∈ S 1 , . . . , ρ n = ρ n ∈ S n .
In any case, we have that ρ 1 , . . . , ρ n is a correct run on node configurations. This means that the modified data values are innocuous for the run. As the structure of the run is not changed, this implies that S 1 • • • S n is an accepting run (that verifies the disjoint values property for x•k by the previous Claim).

If we perform the same procedure for every position of the tree, we end up with an accepting run and tree with the disjoint values property.

We define a translation from regXPath(F, =) formulae to ATRA(guess, spread). Let η be a regXPath(F, =) formula and let A be the corresponding ATRA(guess, spread) automaton defined by the translation. We show that (i) if a data tree t is accepted by A by a run verifying the disjoint values property, then t |= η, and in turn (ii) if t |= η, then t is accepted by A. Thus, by the disjoint values normal form (Proposition 6.8) we obtain our main result of Proposition 6.6, which by decidability of ATRA(guess, spread) (Theorem 5.5) implies that the satisfiability problem for regXPath(F, =) is decidable.

Normal form. For succinctness and simplicity of the translation, we assume that η is in a normal form such that the ↓-axis is interpreted as the leftmost child. To obtain this normal form, it suffices to replace every appearance of '↓' by '↓→ * '. Also, we assume that every data test subformula of the form α = β or α = β is such that α = ε, α =↓ γ, or α =→ γ for some γ, and idem for β. This will simplify the translation and the proofs for correctness. It is easy to see that every expression α = β can be effectively transformed into a disjunction of formulae of the aforementioned form.

The translation. Let η be a regXPath(F, =) node expression of the above form in negation normal form (nnf for short). Let t be a data tree and let z 0 f cns z n be two positions of t at distance n ∈ N 0 such that, if z 0 = z n ,

z 0 ≺ f cns z 1 ≺ f cns • • • ≺ f cns z n-1 ≺ f cns z n
for some z 1 , . . . , z n-1 , we define str(z 0 , z n ) ∈ A * η to be the string a 1 S 1 • • • a n-1 S n-1 where a i is either → or ↓ depending on the relation between z i-1 and z i , and

S i = {ψ ∈ nsub(η) | z i ∈ [[ψ]] t }.
If n = 0, then str(z 0 , z 0 ) = . Note that str(z 0 , z n ) does not take into account z 0 , since we are working under the normal form where no path subformulae makes tests on the node where they start. For every path expression α ∈ psub(η), consider a deterministic complete finite automaton H α over the alphabet A η = 2 nsub(η) ∪ {↓, →} which corresponds to that regular expression, in the sense that the following claim holds. Claim 3. For every α ∈ psub(η), and x f cns y, we have that H α accepts str(x, y) if, and

only if, (x, y) ∈ [[α]] t . nnf(ϕ ∧ ψ) := nnf(ϕ) ∧ nnf(ψ) nnf(ϕ ∨ ψ) := nnf(ϕ) ∨ nnf(ψ) nnf(¬(ϕ ∧ ψ)) := nnf(¬ϕ) ∨ nnf(¬ψ) nnf(¬(ϕ ∨ ψ)) := nnf(¬ϕ) ∧ nnf(¬ψ) nnf(α β) := nnf(α) nnf(β) nnf([ϕ]) := [nnf(ϕ)] nnf(α * ) := (nnf(α)) * nnf(o) := o o ∈ F nnf( α β ) := nnf(α) nnf(β) nnf(¬ α β ) := ¬ nnf(α) nnf(β) nnf(a) := a nnf(¬a) := ¬a nnf(¬¬ϕ) := nnf(ϕ) nnf( α ) := nnf(α)
Table 1: Definition of the Negation Normal Form for XPath.

We assume the following names of its components: H α = A η , δ α , Q α , 0, F α , where Q α ⊆ N 0 is the finite set of states and 0 ∈ Q α is the initial state. We assume that Q α is partitioned into moving and testing states, such that in every accepting run the states of the run alternate between moving and testing states, starting in the moving state 0.

We next show how to translate η into an ATRA(guess, spread) automaton A. For the sake of readability we define the transitions as positive boolean combinations of ∨ and ∧ over the set of basic tests and states. Any of these -take for instance δ(q) = (store(q 1 ) ∧ q 2 ) ∨ (q 3 ∧ ā)-can be rewritten into an equivalent ATRA with at most one boolean connector per transition (as in Definition 5.1) in polynomial time. The most important cases are those relative to the following data tests:

(1)

α = β (2) α = β (3) ¬ α = β (4) ¬ α = β
We define the ATRA(guess, spread) automaton

A := A, Q, (|η| ), δ with
Q := {(|ϕ| ), (|α| ) i , (|α| ) test,i , (|α| ) F , (|α, β| ) i,j , (|α, β| ) test,i,j | ϕ ∈ nsub ¬ (η), α, β ∈ psub ¬ (η), ∈ {=, =, ¬=, ¬ =}, i ∈ Q α , j ∈ Q β }
where op ¬ is the smallest superset of op closed under negation under nnf, i.e., if ϕ ∈ op ¬ (η) then nnf(¬ϕ) ∈ op ¬ (η) (where nnf is defined as shown in Table 1). The idea is that a state (|ϕ| ) verifies the formula ϕ. A state (|α| ) = i (resp. (|α| ) = i ) verifies that there is a forward path in the tree ending at a node with the same (resp. different) data value as the one in the register, such that there exists a partial run of H α over such path that starts in a moving state i and ends in a final state. Similarly, a state (|α| ) = test,i or (|α| ) = test,i verifies the same when i is a testing state. A state (|α, β| ) = i,j (resp. (|α, β| ) = i,j ) verifies that there are two paths ending in two nodes with the same (resp. one equal, the other different) data value as that of the register; such that one path has a partial accepting run of H α starting in a moving state i, and the other has a partial accepting run of H β starting in a moving state j. A state like (|α| ) = F is simply to mark that the run of H α on a path has ended, and the only remaining task is to test for equality of the data value with respect to the register. Finally, a state (|α| ) ¬= Here, (|α| ) F holds at the endpoint of a path matching α.

δ((|α|

) i ) := (|α| ) test,δα(↓,i) ∨ (|α| ) test,δα(→,i) ∨ i∈Fα (|α| ) F δ((|α| ) test,i ) := S⊆nsub(α) (|α| ) δα(S,i) ∧ ϕ∈S (|ϕ| )
Next, we focus only on the data-aware test formulae, since the tests α and ¬ α are interpreted as the equivalent formulae α = α and ¬ α = α respectively. Using the guess operator, we can easily define the cases corresponding to the data test cases (1) and (2) as follows.

δ((|α = β| )) := guess((|α, β| ) = ) δ((|α, β| ) = ) := (|α| ) = 0 ∧ (|β| ) = 0 δ((|α| ) = F ) := eq δ((|α = β| )) := guess((|α, β| ) = ) δ((|α, β| ) = ) := (|α| ) = 0 ∧ (|β| ) = 0 δ((|α| ) = F ) :=
) := (|¬ α | ) ∨ (|¬ β | ) ∨ guess((|α, β| ) ¬ = ) δ((|α, β| ) ¬ = ) := (|α| ) ¬ = 0 ∧ (|β| ) ¬ = 0 δ((|α| ) ¬ = F ) := eq δ((|α| ) ¬= F ) := eq δ((|α| ) ¬ i ) := ( ¯ ? ∨ (|α| ) ¬ test,δα(↓,i) ) ∧ ( ¯ ? ∨ (|α| ) ¬ test,δα(→,i) ) ∧ final
where φ stands for nnf(¬ϕ) and final =

(|α| ) ¬ F if i ∈ F α , true otherwise. δ((|α| ) ¬ test,i ) := S⊆nsub(α) (|α| ) ¬ δα(S,i) ∧ ϕ∈S (|ϕ| )
The difficult part is the translation of the data test case (3). The main reason for this difficulty is the fact that ATRA(guess, spread) automata do not have the expressivity to make these kinds of tests. An expression ¬ α = β forces the set of data values reachable by an α-path and the set of those reachable by a β-path to be disjoint. We show that nonetheless the automaton can test for a condition that is equivalent to ¬ α = β if we assume that the run and tree have the disjoint values property. Example 6.9. As an example, suppose that η = ¬ ↓α = →β is to be checked for satisfiability. One obvious answer would be to test separately α and β. If both tests succeed, one can then build a model satisfying η out of the two witnessing trees by making sure they have disjoint sets of values. Otherwise, η is clearly unsatisfiable. Suppose now that we have η = ϕ ∧ ¬ ↓α = →β , where ϕ is any formula with no data tests of type (3). One could build the automaton for ϕ and then ask for "spread( (|↓α| ) ¬= 0 ∨ (|→β| ) ¬= 0 )" in the automaton. This corresponds to the property "for every data value d taken into account by the automaton (as a result of the translation of ϕ), either all elements reachable by α do not have datum d, or all elements reachable by β do not have datum d". If ϕ contains a α = β formula, this translates to a guessing of a witnessing data value d. Then, the use of spread takes care of this particular data value, and indeed of all other data values that were guessed to satisfy similar demands. In other words, it is not because of d that ¬ ↓α = →β will be falsified. But then, the disjoint values property ensures that no pair of nodes accessible by α and β share the same datum. This is the main idea we encode next.

) ¬= i,j ) := spread (|α| ) ¬= i ∨ (|β| ) ¬= j ∧ ( ¯ ? ∨ (|α, β| ) ¬= test,δα(↓,i),δ β (↓,j) ) ∧ ( ¯ ? ∨ (|α, β| ) ¬= test,δα(→,i),δ β (→,j) ) ∧ final α ∧ final β where final α = store((|β| ) ¬= j ) if i ∈ F α , true otherwise,
and final β = store((|α|

) ¬= i ) if j ∈ F β , true otherwise. δ((|α, β| ) ¬= test,i,j ) := S⊆nsub(α) (|α, β| ) ¬= δα(S,i),δ β (S,j) ∧ ϕ∈S (|ϕ| )
The first line of δ((|α, β| ) ¬= i,j ) corresponds to the tests (1) and (2) above, and the third line corresponds to the cases where x f cns y and y f cns x.

Next we show the correctness of this translation. We say that A has an accepting run from a thread (q, d) on t| x if there is a sequence of tree configurations S 1 • • • S n such that S 1 is at position x and contains (q, d), and S n is accepting. We say that there is a dvp-run if S 1 We suppose that η is in nnf. We proceed by induction on the lexicographic order of (f (x), |ϕ|), where f (x) is the length of a maximal path from x to a leaf in the fcns coding (roughly, the height of t| x ). The base cases when ϕ = a or ϕ = ¬a are easy. Suppose then that the proposition is true for all position y f cns x, and for all ψ ∈ sub(η), |ψ| < |ϕ| at position x. The cases ϕ = ϕ 1 ∧ ϕ 2 or ϕ = ϕ 1 ∨ ϕ 2 are straightforward from the inductive hypothesis. The following claim also follows from the inductive hypothesis. Proof. By induction, suppose that Claim 4 holds for all α, x , y such that (f (x ), |α|) < lex (f (x), |ϕ|). As a consequence of the inductive hypothesis on ( †), for all positions z with x ≺ f cns z f cns y, and for every subformula If ϕ = ¬ α = β , then t| x is such that for every pair of paths ending in some positions y, y , if the paths satisfy α and β respectively, then d(y) = d(y ). Since δ(¬ α = β ) = (|α, β| ) ¬= , we show that there is an accepting run from ((|α, β| ) ¬= , d), for any d ∈ D. Using the inductive hypothesis on all the nodes below x (as we did in Claim 4), note that every time that the automaton has an accepting dvp-run from ((|ψ| ), d) at x for some d ∈ D, then x ∈ [[ψ]] t . By definition of the transition relation on (|α, β| ) ¬= , this means that a sufficient condition for the automaton to have an accepting dvp-run from ((|α, β| ) ¬= , d) is: for every node z f cns x, if the states of H α , H β are respectively i, j after reading str(x, z), then there is an accepting dvp-run from (spread (|α| ) ¬= i ∨ (|β| ) ¬= j , d) on t| z . To simplify the argument, we can assume that the configuration contains all the data values of the tree and therefore that opspread takes into account all possible data values (this is not a necessary condition, but certainly a sufficient one to have an accepting dvp-run). Also using the inductive hypothesis, there is an accepting dvp-run from ((|α| ) ¬= i , d ) on t| z if for every node z f cns z such that H α takes the state i to a final state after reading str(z, z ), we have d(z ) = d . Therefore, there is an accepting dvp-run from spread (|α| ) ¬= i ∨(|β| ) ¬= j if for every data value d and nodes y, y that complete the paths, it cannot be that d = d(y) = d(y ). This is true, since t| x |= ¬ α = β . On the other hand, note that by the same reason, for every node z such that (z, z ) ∈ Let z be the closest common ancestor of y, z in the fcns coding. Since there is an accepting dvp-run from (|α, β| ) ¬= , there must be some states i , j assumed by H α and H β after reading str(x, z ), such that the following holds. Lemma 6.10 together with Proposition 6.8 concludes the proof of Proposition 6.6. We then have that Theorem 6.4 holds.

ψ ∈ nsub(η), if z ∈ [[ψ]]
Proof of Theorem 6.4. By Proposition 6.6, satisfiability of regXPath(F, =) is reducible to the nonemptiness problem for ATRA(guess, spread). On the other hand, we remark that ATRA(guess, spread) automata can encode any regular tree language -in particular a DTD, the core of XML Schema, or Relax NG-and are closed under intersection by Proposition 5.3. Also, the logic can express any unary key constraint as stated in Lemma 6.2. Hence, by Theorem 5.5 the decidability follows.

Extensions

We consider some operators that can be added to regXPath(F, =) preserving the decidability of the satisfiability problem. For each of these operators, we will see that they can be coded as a ATRA(guess, spread) automaton, following the same lines of the translation in Section 6.4. 6.5. Allowing upward axes. Here we explore one possible decidable extension to the logic regXPath(F, =), whose decidability can be reduced to that of ATRA(guess, spread). In this extension we can make use of upward (↑) and leftward (←) axes to navigate the tree in a restricted way. We can test, for example, that all the ancestors of a given node labeled with a have the same data value as all the descendants labeled with b, with the formula ¬ ↑ * We must note that regXPath B (F, =) contains regXPath(F, B), that is, the full data-unaware fragment of XPath. We also remark that it is not closed under negation. Indeed, we cannot express the negation of "there exists an a such that all its ancestors labeled b have different data value" which is expressed by ↓ * We argue that satisfiability for this extension can be decided in the same way as for regXPath(F, =). It is straightforward to see that positive appearances can easily be translated with the help of the guess operator. On the other hand, for negative appearances, like ¬{ {α 1 s 1 , . . . , α n s n } }, we proceed in the same way as we did for regXPath(F, =). The only difference being that in this case the automaton will simulate the simultaneous evaluation of the n expressions and calculate all possible configurations of the closest common ancestors of the endpoints, performing a spread at each of these intermediate points.

Remark 6.12. Satisfiability of regXPath + (F, =) under key constraints and DTDs is decidable.

Concluding remarks

We presented a simplified framework to work with one-way alternating register automata on data words and trees, enabling the possibility to easily show decidability of new operators by proving that they preserve the downward compatibility of a well-structured transition system. It would be interesting to hence investigate more decidable extensions, to study the expressiveness limits of decidable logics and automata for data trees.

Also, this work argues in favor of exploring computational models that although they might be not closed under all boolean operations, can serve to show decidability of logics closed under negation -such as forward-XPath-or expressive natural extensions of existing logics -such as LTL ↓ nnf (F, ∃ ↓ ≥ , ∀ ↓ ≤ ). We finally mention that even though XPath(↓, ↓ * , →, → * , =) (i.e., forward-XPath) has a non-primitive-recursive complexity, the results of [START_REF] Figueira | A decidable two-way logic on data words[END_REF] suggest that it seems plausible that XPath(↓, ↓ * , → * , =) or even XPath(↓, ↓ * , → * , * ←, =) are decidable in elementary time [see Fig11, Conjecture 1].

Figure 1 :

 1 Figure 1: A data tree.

  where f (ρ) stands for the replacement of every data value d by f (d) in ρ. Definition 3.7 ( ). We first define the relation (C ara , ) such that i, α, γ, ∆ i , α , γ , ∆ iff α = α , γ = γ , and ∆ ⊆ ∆ .

  Lemma 3.14. Let D ⊆ D, |D| < ∞. There exists an order-preserving bijection f on D such that • for every {d, d } ⊆ D such that d < d there exists d such that f (d) < d < f (d ), • for every d ∈ D there exists d such that f (d) < d, and there exists d such that d < f (d).

Figure 6 :

 6 Figure 6: Two indistinguishable data trees for ATRA.

Figure 7 :

 7 Figure 7: Semantics of regXPath(F, =) for a data tree t = a ⊗ d.

Figure 8 :

 8 Figure 8: From XML documents to data-trees.

0

  (resp. (|α| ) ¬ = 0 ) verifies that every node reachable by α has different (resp. equal) data than the register, and similar for the other universal states of the form(| • • • | ) ¬••• ••• . Wefirst take care of the boolean connectors and the simplest tests. δ((|a| )) := a δ((|ϕ ∨ ψ| )) := (|ϕ| ) ∨ (|ψ| ) δ((|¬a| )) := ā δ((|ϕ ∧ ψ| )) := (|ϕ| ) ∧ (|ψ| ) First, we define the transitions associated to each H α , for i ∈ Q α , C ⊆ Q α , ∈ {=, =}.

  We define δ((|¬ α = β | )) := (|α, β| ) ¬= 0,0 . Given ¬ α = β , the automaton systematically looks for the closest common ancestor of every pair (x, y) of nodes accessible by α and β respectively, and tests, for every data value d present in the node configuration, that either (1) all data values accessible by the remaining path of α are different from d, or (2) all data values accessible by the remaining path of β are different from d. δ((|α, β|

Claim 4 .

 4 For any path subformula α of psub(η), and y f cns x , (a) if (x, y) ∈ [[α]] t then there is an accepting dvp-run from ((|α| ) = 0 , d(y)) on t| x , (b) if there is an accepting dvp-run from ((|α| ) = 0 , d) on t| x , then (x, y) ∈ [[α]] t for some y such that d(y) = d, (c) if (x, y) ∈ [[α]] t , there is an accepting dvp-run from ((|α| ) = 0 , d) with d = d(y) on t| x , (d) if there is an accepting dvp-run from ((|α| ) = 0 , d) on t| x , then (x, y) ∈ [[α]] t for some y with d = d(y).

  t then there is an accepting dvp-run of A from ((|ψ| ), d) on t| z for any d ∈ D.(a) Suppose first that (x, y) ∈ [[α]] t . Therefore, H α accepts str(x, y) by Claim 3. Further, suppose that S ∈ A η is the (2i)-th element of str(x, y), and that z is the position of the i-th element in the path between x and y of the fcns coding. For any ψ ∈ S we have that z ∈ [[ψ]] t , and applying the inductive hypothesis on ( †) we have that there is an accepting dvp-run from ((|ψ| ), d) on t| z . Hence, by definition of the transition of (|α| ) = 0 , we have that there is an accepting dvp-run from ((|α| ) = 0 , d ) on t| x if we take d = d(y). (b) For any z with x ≺ f cns z f cns y, if there is an accepting dvp-run from ((|ψ| ), d) on t| z , by inductive hypothesis on ( ‡), we have that z ∈ [[ψ]] t . Therefore, if there is an accepting dvp-run from ((|α| ) = , d) on t| x , by the definition of the transition relation there must be some y f cns x such that str(x, y) is accepted by H α and further d(y) = d. Hence, (x, y) ∈ [[α]] t .An identical reasoning applies to show (c) and (d).(⇒) Suppose that t| x |= ϕ. We focus on the data test cases.If ϕ = α = β , then δ((|ϕ| )) = guess((|α, β| ) = ). Since δ((|α, β| ) = ) = (|α| ) = 0 ∧ (|β| ) = 0 ,we then have that for any data value d, there is an accepting run from ((|ϕ| ), d) on t| x if there exists a data value d ∈ D such that ((|α| ) = 0 , d ) and ((|β| ) = 0 , d ) have accepting dvp-runs. Since t| x |= α = β , there must be two positions y and y below x such that d(y) = d(y ) where (x, y) ∈ [[α]] t and (x, y ) ∈ [[β]] t . By Claim 4.a there are accepting dvp-runs from ((|α| ) = 0 , d ) and ((|β| ) = 0 , d ) on t| x . These two dvp-runs can be simply combined to build an accepting dvp-run from ((|ϕ| ), d). The case ϕ = α = β is similar, using Claims 4.a and 4.c.

  [[β]] t , there are accepting dvp-runs for ((|α| ) ¬= i , d(z )) and for (store((|α| ) ¬= i ), d ) from z (and respectively swapping α and β). Thus, by combining all the accepting dvp-runs from (spread (|α| ) ¬= i ∨ (|β| ) ¬= j , d) for every such z, we obtain an accepting dvp-run from ((|ϕ| ), d) on t| x .Finally, ifϕ = ¬ α = β , then δ((|ϕ| )) = (|¬ α | ) ∨ (|¬ β | ) ∨ guess((|α, β| ) ¬ = ). Since x ∈ [[ϕ]] t ,we have that either (i), (ii), or (iii) (on page 36) holds for t| x . The first two conditions correspond to the properties for which ¬ α and ¬ β are satisfied, which are equivalent to ¬ α = α and ¬ β = β . By the case already shown, this means that (|¬ α = α | ) or (|¬ β = β | ) have accepting dvp-runs on t| x respectively. Since the definition of (|¬ α = α | ) and (|¬ α | ) (idem with β) are treated identically by the automaton, ((|ϕ| ), d) has an accepting dvp-run on t| x . We now show that the third condition corresponds to having an accepting dvp-run from (guess((|α, β| ) ¬ = ), d) on t| x for any data value d. By definition of δ, there is an accepting dvprun if there is a data value d such that there are accepting dvp-runs from ((|α| ) ¬ = 0 , d ) and ((|β| ) ¬ = 0 , d ). By applying the inductive hypothesis on all positions below x and subformulas of nsub(η), we have the following, for D α x = {d(y) | (x, y) ∈ [[α]] t }, D β x = {d(y) | (x, y) ∈ [[β]] t }. Claim 5. For any e ∈ D α x , there is an accepting dvp-run from ((|α| ) ¬= , e) on t| x . If D α x = {e}, there is an accepting dvp-run from ((|α| ) ¬ = , e) on t| x . Idem for β and D β x . Note that since t| x |= ¬ α = β , condition (i) corresponds to D α x = ∅, condition (ii) to D β x = ∅, and condition (iii) to D α x = D β x = {e}. Therefore, if condition (iii) holds, there are accepting dvp-runs from ((|α| ) ¬ = , e) and ((|β| ) ¬ = , e), and hence also from (guess((|α, β| ) ¬ = ), d) for any d, by guessing the data value e. Thus, there is an accepting dvp-run from ((|ϕ| ), d) if conditions (i), (ii) or (iii) hold. Therefore, there is an accepting dvp-run from ((|ϕ| ), d) on t| x . (⇐) Consider an accepting dvp-run S 1 • • • S n from ((|ϕ| ), d) on t| x . We show that t| x |= ϕ. If ϕ = α = β , by definition of δ the automaton guesses a data value d and creates a thread ((|α, β| ) = , d), which means that there is an accepting dvp-run from ((|α, β| ) = , d). Then, there are accepting dvp-runs from ((|α| ) = , d) and ((|β| ) = , d). By Claim 4.a, there must be two nodes y, z such that (x, y) ∈ [[α]] and (x, z) ∈ [[β]] with d = d(z) = d(y). Hence, t| x |= ϕ. The case ϕ = α = β is treated in a similar way. If ϕ = ¬ α = β , suppose ad absurdum that there is a data value d and two positions y, z such that (x, y) ∈ [[α]] t and (x, z) ∈ [[β]] t , and d(y) = d(z) = d.

Claim 6 .

 6 There is a moving configuration S r containing (|α, β| ) ¬= i ,j with position z such that• if z = y, then ((|α|) ¬= i , d(y)) is in some S s , s > r, with position z , • if z = z, then ((|β| ) ¬= j , d(z)) is in some S s , s > r, with position z , • for every data value d of S r , ((|α| ) ¬= , d) i or ((|β| ) ¬= , d) j are in some S s , s > r, with position z .Hence, by Claim 6 there must be a configuration S r with position z , where z is the common ancestor of y and z in the fcns coding, such that for all data values d of S r it is not true that d(x) = d(y) = d . But by the fact that this is a dvp-run, this means that there cannot be any data value d such that d(y) = d(z) = d . In particular, d, and thus we have a contradiction. Then, t| x |= ϕ. The cases of y f cns z or z f cns y are only easier. Finally, if ϕ = ¬ α = β , then A must have an accepting dvp-run on t| x from ((|¬ α | ), d), ((|¬ β | ), d), or ((|α, β| ) ¬ = 0,0 , d) for some d ∈ D. In the first two cases this means that [[ α ]] t|x = ∅ or [[ β ]] t|x = ∅ (by reduction to the case ¬ α = α already treated) and hence that t |= ϕ. In the latter case, by definition of δ, all positions y whose paths from x satisfy α or β are such that d(y) = d. This implies that t |= α = β , and hence t |= ϕ.

  [a] = ↓ * [b] , but we cannot test its negation. Let regXPath B (F, =) be the fragment of regXPath(F ∪ B, =) where B := {↑, ↑ * , ←, * ←} defined by the grammar ϕ, ψ ::= ¬a | a | ϕ ∧ ψ | ϕ ∨ ψ | α f | α b | α f β f | ¬ α f β f | ¬ α b = β f | ¬ α b = β f with ∈ {=, =}, a ∈ A, and α f , β f ::= [ϕ] | α f β f | α f ∪ β f | o α f | (α f ) * o ∈ {↓, →, ε}, α b , β b ::= [ϕ] | α b β b | α b ∪ β b | o α b | (α b ) * o ∈ {↑, ←, ε}.

  [a ∧ ¬ ↑ * [b] = ε ].As shown in Proposition 3.2, if the negation of this property were expressible, then its satisfiability would be undecidable. It is not hard to see that we can decide the satisfiability problem for this fragment.Consider the data test expressions of the types¬ α b = β f and ¬ α b = β fwhere β f ∈ regXPath(F, =) and α b ∈ regXPath(B). We can decide the satisfaction of these kinds of expressions by means of spread( , ), using carefully its first parameter to select the desired threads from which to collect the data values we are interested in. Intuitively, along the dvp-run we throw threads that save the current data value and try out all possible ways to verify α r b ∈ regXPath(F, =), where ( ) r stands for the reverse of the regular expression. Let the automaton arrive with a thread ((|α b | ), d) whenever α r b is verified. This signals that there is a backwards path from the current node in the relation α b that arrives at a node with data value d. Hence, at any given position, the instruction spread((|α b | ), (|α f | ) ¬ ) translates correctly the expression ¬ α b β f . Furthermore, α b need not be necessarily in regXPath(B), as its intermediate node tests can be formulae from regXPath(F, =). We then obtain the following result. Remark 6.11. Satisfiability for regXPath B (F, =) under key constraints and DTDs is decidable. 6.6. Allowing stronger data tests. Consider the property "there are three descendant nodes labeled a, b and c with the same data value". That is, there exists some data value d such that there are three nodes accessible by ↓ * [a], ↓ * [b] and ↓ * [c] respectively, all carrying the datum d. Let us denote the fact that they have the same or different datum by introducing the symbols '∼' and ' ∼', and appending it at the end of the path. Then in this case we write that the elements must satisfy ↓ * [a]∼, ↓ * [b]∼, and ↓ * [c]∼. We then introduce the node expression { {α 1 s 1 , . . . , α n s n } } where α i is a path expression and s i ∈ {∼, ∼} for all i ∈ [1..n]. Semantically, it is a node expression that denotes all the tree positions x from which we can access n positions x 1 , . . . , x n such that there exists d ∈ D where for all i ∈ [n] the following holds: (x, x i ) ∈ [[α i ]]; if s i = ∼ then d(x i ) = d; and if s i = ∼ then d(x i ) = d. Note that now we can express α = β as { {α∼, β∼} } and α = β as { {α∼, β ∼} }. Let us call regXPath + (F, =) to regXPath(F, =) extended with the construction just explained. This is a more expressive formalism since the first mentioned property -or, to give another example, { {↓ * [a]∼, ↓ * [b]∼, ↓ * [a] ∼, ↓ * [b] ∼} }is not expressible in regXPath(F, =).

  eq The test case (4) involves also an existential quantification over data values. In fact,

¬ α = β means that either (i) there are no nodes reachable by α, (ii) there are no nodes reachable by β, or (iii) there exists a data value d such that both (a) all elements reachable by α have datum d, and (b) all elements reachable by β have datum d. δ((|¬α = β| )

  |= η then A accepts t with a dvp-run, and (⇐) if A accepts t with a dvp-run, then t |= η.

	• • •	S n has the disjoint values property.
	Lemma 6.10. For any data tree t,
	(⇒) if t

Proof. Let t = a⊗d. We show that for every subformula ϕ ∈ sub(η) and position x ∈ pos(t), if t| x |= ϕ then A has an accepting dvp-run from ((|ϕ| ), d) on t| x for any d ∈ D. ( †) And conversely, if A has an accepting dvp-run from ((|ϕ| ), d) on t| x for some d ∈ D, then t| x |= ϕ. ( ‡)

Note that this logic already contains LTL ↓ (U, X).

By f (ρ) we denote the replacement of every data value d by f (d) in ρ.

Acknowledgements

I am very grateful to Alexander Kartzow, Claudia Carapelle and the reading group of Universität Leipzig for pointing out errors, and suggesting solutions.

Work supported by the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under the FET-Open grant agreement FOX, number FP7-ICT-233599.