Diego Figueira

A decidable two-way logic on data words

We study the satisfiability problem for a logic on data words. A data word is a finite word where every position carries a label from a finite alphabet and a data value from an infinite domain. The logic we consider is two-way, contains "future" and "past" modalities, where these are considered as reflexive and transitive relations, and data equality and inequality tests. This logic corresponds to the fragment of XPath with the 'following-sibling-or-self' and 'preceding-sibling-or-self' axes over a data word. We show that this problem is decidable, EXPSPACE-complete. This is surprising considering that with the strict navigation relations (non-reflexive) the satisfiability problem is undecidable. To show this we first reduce the problem to a derivation problem for an infinite transition system, and then we show how to abstract this problem into a reachability problem of a finite transition system.

I. INTRODUCTION

We work on data words. A data word is a finite string where each position carries a label from a finite alphabet and a data value from some infinite domain. This kind of structure has been considered in the realm of semistructured data, timed automata, program verification, and generally in systems manipulating data values. Finding automata and logics with decidable satisfiability problems over data words is an important quest when studying systems manipulating data values.

Suppose that a data word models a database of 'actions' that were performed throughout the time, where the linear structure of the data word corresponds to the flow of time. Over these structures one may want to model the behavior of a system, and may want to check that the specified behavior is satisfiable. In other words, that it does not contain any contradiction. The satisfiability problem is crucial to solve this and other static analysis problems.

In this paper we consider a formalism to express properties of data words, where the data values can only be tested for equality or inequality. Logics or automata that can test equality of data values and that can express meaningful properties are important to find, although they become very easily undecidable.

We investigate a natural two-way logic on data words and show that it has a decidable EXPSPACE satisfiability problem. We call this logic Two-way Path Logic (or PathLogic for short). PathLogic can be seen as an extended temporal logic [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] or as a fragment of XPath [START_REF] Clark | XML path language (XPath)[END_REF] on data words. It has future and past modalities to navigate the word and data equality test expressions. For example, it can test the following property of a node: "there is a node x to the left and two nodes y < z to the right with labels a, b, and c respectively, such that x and z have the same data value". This property is very easily expressed in PathLogic with the formula ← -

[a] = ---→ [b]•[c] . ( )
Although we can test the relative appearances of labels, the left and right relations are interpreted as transitive-reflexive relations. Thus, ← -

[a] = ---→ [b]•[b] is equivalent to ← - [a] = - → [b]
. Our main result is the following.

Main Theorem. The satisfiability problem for PathLogic is EXPSPACE-complete.

This logic has links with other logics. As mentioned before, PathLogic is inspired in the logic for XML documents XPath with data equality tests and the reflexive-transitive axes 'following-sibling-or-self' and 'preceding-sibling-or-self' 1 We note this axes → * and * ← respectively for economy of space and XPath(→ * , * ←, =) to the logic. PathLogic is in fact expressive-equivalent (through an EXPTIME translation) to XPath(→ * , * ←, =) interpreted over data words. Indeed, PathLogic is a simplification of the syntax of XPath( * ←, → * , =) that preserves only the essential. This has also the advantage of simplifying the decidability proofs. In terms of XPath our result is translated as follows.

Theorem 1. The satisfiability problem for XPath( * ←, → * , =) is in 2EXPSPACE.

This may be surprising given the known results in this area. In fact, [FS09] shows that XPath(→ + , =) is decidable with non-primitive recursive complexity. This is the fragment that contains the non-reflexive 'following-sibling' axis. Even more, XPath( + ←, → + , =) or even XPath( * ←, → + , =) are undecidable. Simply reducing the navigation by having reflexivetransitive relations instead of only transitive, we change from an undecidable problem to an elementarily decidable one. Thus, the → * and * ← axes behave surprisingly much better. This result opens some promising conjectures on the decidability of several fragments of XPath on XML documents.

Decidable two-way logics on data words are scarce. Very often two-way logics on data words have an undecidable satisfiability problem. One such prominent example is the case of LTL ↓ 1 (F, F -1 ), a temporal logic with with future and past modalities and one register to store and compare data values. Wether we interpret the F and F -1 modalities as either reflexive or strict, its satisfiability problem remains undecidable. Further, if only one of these modalities is allowed, it becomes decidable, but with non-primitive recursive complexity [FS09]. PathLogic can be seen as a fragment of LTL ↓ 1 (F, F -1 ) (this is the fragment identified in [FS09] as "simple-LTL ↓ 1 (F, F -1 )").

Related work

This paper addresses a topic related to the work of [FS09], about the complexity and decidability of logics for data words and trees with transitive relations. [FS09] showed lower bounds for several fragments of LTL ↓ 1 and XPath with transitive relations for navigation. In particular, it was shown that all fragments of XPath with data equality tests containing transitive and non-reflexive axes → + , + ← or ↑ + have a satisfiability problem of non-primitive recursive complexity.

To obtain such results it was necessary to study the behavior of XPath on non-branching structures, i.e., on data words. The present paper also centers on data words, showing a positive result with the spirit of obtaining in the future positive results for fragments of XPath over XML documents. Bojańczyk et al. [BMS + 06] study the satisfiability problem for first order logics with two variables on data words. In particular they study the fragment FO 2 (<, ∼). This is firstorder logic restricted to two variables, a binary relation < which corresponds to the order in the word, and a binary relation ∼ to test for data equality or inequality of nodes. They show that the satisfiability problem is decidable, NEXPTIMEcomplete. In fact, they show that the decidability is also preserved if we allow any predicate '+k', relating any two nodes at distance k in the data word. 2 This logic is in some sense two-way, since it can navigate both in the future and past directions. Since it also includes equality and inequality of nodes, the transitive < relation and the reflexive-transitive relation ≤ are one definable in terms of the other. Although close, FO 2 (<, ∼) is incomparable with PathLogic in terms of expressive power. This decidability result was extended to FO 2 (<, ), where x y tests that x carries a data value smaller or equal to that of y. The satisfiability of this logic is EXPSPACE [START_REF] Schwentick | Two-variable logic with two order relations[END_REF].

Demri and Lazić [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] study the logic LTL ↓ 1 , which is a two-way temporal logics on data words. It is based on the linear temporal logic LTL with special constructs to store and test for equality of data values. This logic with Future, Next and Until modalities is shown to be decidable [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF], but any fragment with Future and Past modalities becomes undecidable [FS09]. Nevertheless, [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] identifies a decidable fragment that is equivalent to FO 2 (<, ∼, +1, . . . , +k), and hence decidable. [KSZ10] also investigates a decidable two-way fragment but this time over multi-attributes data words, were every position carries a set of data values. These logics are intimately related with FO 2 and they are hence also incomparable to PathLogic in expressive power.

Organization: In Section II we introduce our logic PathLogic and we briefly comment on the relation with XPath, LTL ↓ 1 , and FO 2 . Sections III, IV and V are dedicated to prove our main result, that the satisfiability problem of PathLogic 2 For this logic no primitive-recursive upper bound is known. is in EXPSPACE. In Section VI we discuss about the lower bound. Section VII contains some corollaries of our result in terms of XPath fragments. Finally, in Section VIII we propose some conjectures and future lines of work. Due to space limitations some proofs are in the Appendix.

II. A TWO-WAY LOGIC

Notation: We consider a finite word over E as a function w : [n] → E for some n > 0, where [n] = {1, . . . , n}. We define the set of words as Words(E)

:= {[n] → E | n > 0}.
We write pos(w) = {1, . . . , n} to denote the set of positions (that is, the domain of w). 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 w = a⊗d ∈ Words(A × D), where A is a finite alphabet of letters and D is an infinite domain. We use A for a finite alphabet, D as an infinite domain, and we refer to its elements with the letters a, b, c ∈ A and d, e ∈ D. We use w, a and d for words of Words(A×D), Words(A) and Words(D) respectively. We use the loosely term node to denote the pair of label and data value of a position. We write ℘(S) and ℘ <∞ (S) to denote the powerset and finite powerset of a set S respectively.

We work with a logic with a simple syntax and same expressive power as XPath( * ←, → * , =). We call this logic PathLogic. This is an equivalent formalism which is more convenient to work with for the proofs presented here.

PathLogic is a two-sorted formulas with path expressions (that we note α, β) and node expressions (ϕ, ψ). A path expression is a succession of node expressions, noted α

= [ψ 1 ]• • • • •[ψ n ]
and we say that a position i of the data word reaches another position j through -→ α if there are witness

positions i ≤ i 1 ≤ • • • ≤ i n = j
where ϕ k holds true at position i k , for every k. On the other hand, a node expression is a boolean combination of tests for labels or formulas ←α = -→ β that demand the existence of one position to the left and one to the right reachable by ←α and -→ β respectively, that carry the same data value. Analogously, ←α = -→ β expresses the same property except that the positions must carry different data values. Expressions are formally defined as follows.

ϕ ::= ← - α = - → β | ← - α = - → β | a | ¬ϕ | ϕ ∨ ϕ α, β ::= ε | [ϕ]•α
And semantics are defined according to the intuition we just gave. See Figure 1 for a more precise definition.

In this context, we define w, i |= ϕ iff i ∈ [[ϕ]] w , and w |= ϕ iff w, 1 |= ϕ. We also define the test -→ α , which checks if there is a node reachable by α, as -→ α = -→ α , and likewise for ←α . The satisfiability problem is the problem of, given ϕ ∈ PathLogic, whether there is a data word w such that w |= ϕ. Our main result is that this problem is decidable.

Comparison with other logics a) XPath:

PathLogic corresponds precisely to XPath( * ←, → * , =) in terms of expressiveness. The only difference is that the syntax is simplified. While XPath( * ←, → * , =) may change of direction inside a path expression, PathLogic cannot. But in fact this does not change the expressive power: we can always factorize path expressions with mixed axes into formulas whose path expressions use only one axis. Thus, there is an EXPTIME translation from XPath( * ←, → * , =) into PathLogic.

[[a]] w def = {i ∈ pos(w) | a(i) = a} [[ϕ ∨ ψ]] w def = [[ϕ]] ∪ [[ψ]] [[¬ϕ]] w def = pos(w) \ [[ϕ]] [[ ← - α = -→ β ]] w def = {i ∈ pos(w) | ∃j, k ∈ pos(w), (i, j) ∈ [[α]] w ← , (i, k) ∈ [[β]] w → , d(j) = d(k)} [[ ← - α = -→ β ]] w def = {i ∈ pos(w) | ∃j, k ∈ pos(w), (i, j) ∈ [[α]] w ← , (i, k) ∈ [[β]] w → , d(j) = d(k)} [[ε]] w → def = [[ε]] w ← = {(i, i) | i ∈ pos(w)} [[[ϕ]•α]] w → def = {(i, j) ∈ (pos(w)) 2 | ∃k ≥ i s.t. k ∈ [[ϕ]] w , (k, j) ∈ [[α]] w → } [[[ϕ]•α]] w ← def = {(i, j) ∈ (pos(w)) 2 | ∃k ≤ i s.t. k ∈ [[ϕ]] w , (k, j) ∈ [[α]] w ← }
b) LTL ↓ 1 : PathLogic also corresponds to the fragment of simple-LTL ↓ 1 as defined in [FS09], denoted by sLTL ↓ 1 (F, F -1 ). 3 Here, the F and F -1 are interpreted as reflexive-transitive relations. A formula of LTL ↓ 1 in negated normal form is said to be simple if (i) there is at most one occurrence of ↑ within the scope of each occurrence of ↓ and, (ii) there is no negation between an occurrence of ↑ and its matching ↓, except maybe immediately before ↑. We denote by sLTL ↓ 1 the fragment of LTL ↓ 1 containing only simple formulas. The logic sLTL ↓ 1 (F, F -1 ) is equivalent to XPath( * ←, → * , =) (and hence also to PathLogic) in terms of expressive power. As shown in [FS09], there is a PTIME translation in both senses. c) FO 2 : As already mentioned, FO 2 (<, ∼) is incomparable with PathLogic. Indeed, FO 2 (<, ∼) can express that the word contains at least two nodes, while we cannot express this property using only reflexive-transitive modalities. In turn, PathLogic can easily express a property like "all nodes labeled a verify the property ( )" (as discussed in the Introduction), that is unlikely to be expressible in FO 2 (<, ∼). We argue that over a fixed alphabet, PathLogic captures FO 2 (<, ∼) in terms of expressive power over the class of duplicate-free data words, defined as those words that do not contain two successive identical nodes (i.e., that do not contain (a, d)(a, d) as a substring for any a and d).

Lemma 1. Given a fixed alphabet, PathLogic is more expressive than FO 2 (<, ∼) on duplicate-free data words.

III. THE SATISFIABILITY PROBLEM

We solve the satisfiability problem through a series of two reductions. First, we reduce the problem into a derivation problem for an infinite transition system . And second, we abstract this transition system, reducing this problem into a similar problem for a finite transition system K . In truth, K is not a finite transition system, but we will see that it can be easily restricted to a finite one.

Organization: In this section we present the general outline of the decidability proof, and we show our first reduction to a derivation problem for . Section IV contains the most difficult result, which is the reduction to the derivation problem for K . Finally, in Section V we solve the derivation problem for K with an EXPSPACE procedure.

A. Outline of the proof

We first reduce the problem of testing whether some formula ϕ is satisfiable into a derivation problem for an infinite state transition system that depends on ϕ. This problem consists in testing whether there exists a finite sequence µ 1

• • • µ n such that µ 1 and µ n satisfy certain local properties. The domain of this transition system is the set of mosaics: abstractions of a position of a data word, containing all the data values that can be found to the right and to the left, and further with which path expressions of the logic they can be reached. The transition system corresponds to the property of when two of these mosaics can be matched: that is, that could abstract two positions that are one next to another. We show that from a derivation µ 1

• • • µ n with some good properties, one can build a data word of length n that satisfies the input formula ϕ. In turn, if there is no such derivation, ϕ is unsatisfiable. To obtain this reduction, we work with formulas of PathLogic in a certain normal form. This normal form enables to have a simple definition of the transition specially convenient for our proofs. Next, in Section IV, we solve the derivation problem for by a reduction to a similar derivation problem for another transition system K . This transition system is parametrized by a set K of data values. The definition of K introduces an important concept of rigid data values, which are data values that play a determined function in a sequence µ 1 • • • µ n . We denote by K such data values of important interest. Based on this concept we define a quasi-order ≤ K over the set of mosaics, which is monotone with respect to . This monotonicity serves to finally show the reduction from derivation problem for to the derivation problem for K . The derivation problem for K may seem in appearance more difficult than for , since we are dealing now with a family of transition systems K , one for every K. Nevertheless, in Section V we show that the parameter K is harmless and we can bound and fix a value for it. Also, we will see that we only need to work with the minimal classes of equivalences of ≤ K which are also finite and bounded. These observations give us indeed a finite transition system. Hence, we can use a standard reachability algorithm that solves the derivation problem for K and hence the satisfiability problem for PathLogic.

Organization of this section:

We give a more detailed informal description of the normal form for PathLogic and the transition system , together with some fundamental definitions and notation that we use throughout. We then state the target problem for the reduction.

B. A normal form

We will assume a certain normal form of the formula ϕ to test for satisfiability. This will simplify the necessary machinery to solve our problem. This normal form consists simply of having formulas without nesting of data tests. That is, we avoid treating formulas like

← ---------- [ ← - [a] = - → [b] ] = ---→ [c]•[d] .
Let us call BC(labels) to all the formulas which are a boolean combination of tests for labels of A. If a formula is such that all its path expressions α contain only tests for labels (i.e., α ∈ (BC(labels)) * abusing notation) we call it a non-recursive formula.

In the normal form we suppose that ϕ = ϕ 1 ∧ ϕ 2 where ϕ 1 is a non-recursive formula and ϕ 2 is a conjunction of tests of the form "every node with label a satisfies ψ" for some non-recursive formula ψ. Formally, ϕ 2 contains a conjunction of tests of the form

¬ -----→ [a ∧ ¬ψ]
for a ∈ A a label and ψ a non-recursive formula. Then, we obtain the following.

Lemma 2 (normal form

). There is a polynomial-time translation that for every formula ψ ∈ PathLogic returns a formula ϕ in normal form such that ψ is satisfiable iff ϕ is satisfiable.

Proof: Given a formula ϕ we define the alphabet of the formula in normal form as the set of all subformulas of ϕ plus some extra element ⊥. We denote these letters by a ψ , for ψ a subformula of ϕ. Given a formula η let us call tr(η) to the same formula where every instance of a path expression

[ψ 1 ]• • • • •[ψ n ] (which does not appear nested inside another path expression) is replaced by [a ψ1 ]• • • • •[a ψn ].
To build the normal form, we define on the one hand ϕ 1 = tr(ϕ). On the other hand, we build ϕ 2 as a conjunction of formulas

¬ ---------→ [a ψ ∧ ¬tr(ψ)]
for all subformulas ψ of ϕ. It follows that this translation is polynomial since the set of subformulas of ϕ is polynomial.

We fix once and for all A as the finite alphabet and D as the infinite domain we are going to work with. Given ϕ = ϕ 1 ∧ϕ 2 in normal form, we call Ω ϕ to all non-recursive subformulas of ϕ, and γ ϕ :

A → Ω ϕ to the function such that γ ϕ (a) = ψ iff ϕ 2 contains ¬ [a ∧ ¬ψ] . Finally, we define Ω p ϕ = {α ∈ Ω ϕ |
α is a path expression different from ε}. We exclude ε from Ω p ϕ simply because we are interested in those path expressions that are 'moving', unlike ε.

C. The transition system

Given a formula ϕ in normal form, we show an abstraction of the important information that we need to keep track of in a model that satisfies ϕ. Each piece of information is called a mosaic. A mosaic maintains all necessary facts about some position i of a data word w such that w |= ϕ, namely

• the letter and datum of the current position,

• the data values that are to be found to the right of i, and with which paths of Ω p ϕ are reachable, • and likewise for the data values to the left. We say that a mosaic is the ϕ-abstraction of a position i of a data word w if it contains all the aforementioned details of the position. A mosaic that abstracts a position i of w contains enough information to test whether ψ is satisfied at position i (i.e., w, i |= ψ) for any subformula ψ of ϕ. In order to be a valid mosaic, the mosaic must also comply with γ ϕ (a) where a ∈ A is the label of the mosaic.

Given two mosaics µ 1 , µ 2 , we can check if they match, that one can be next to the other, that there are no incompatibilities. For example, suppose that µ 1 is the ϕ-abstraction of a position i. If µ 1 asserts that there is a data value d different from the current one that can be reached with [a] navigating to the right, then the mosaic that abstracts i + 1 must also contain the information that d can be reached with [a]. Otherwise these two mosaics would not match. We will write for this matching relation, and we call a sequence to any sequence

µ 1 • • • µ n . (In general, we call a → sequence to µ 1 → • • • → µ n for any transition →.)
Indeed, the ϕ-abstraction of the positions of a data word w and formula ϕ such that w |= ϕ verify that they are a sequence. Moreover, the leftmost mosaic must not contain information of data values to the left simply because there are no more elements to the left. For the same reasons, the rightmost mosaic must not contain information on the data values to the right. We call such mosaics left-complete and right-complete respectively. A sequence is complete if the leftmost element is left-complete and the rightmost element is right-complete. We show that from any complete sequence for ϕ whose first element verifies ϕ, we can build a data word satisfying ϕ. And in turn, the sequence of ϕ-abstractions of a word that satisfies ϕ is indeed a complete sequence for ϕ. Now the satisfiability problem reduces to the problem of testing if there is a complete sequence whose first element satisfies ϕ. We call this the derivation problem.

Definitions: Let us now turn to the basic definitions. An important object we will work with is that of a profile. A profile of a data value d is a subset of Ω p ϕ describing all the possible ways to reach d in a data word w from a position i ∈ pos(w) by going in one direction (either to the right or to the left). We use π, ρ ⊆ Ω p ϕ as names for profiles.

We define some useful operations on profiles. There is a constant profile σ a for every a ∈ A, which consists in all the path expressions that can be satisfied locally at a certain node, assuming that the node's label is a. (Note that σ a is a constant whereas π, ρ are names.)

σ a def = {α ∈ Ω p ϕ | α = [ψ 1 ]• • • • •[ψ n ], ∀i : a |= ψ i } a ∈ A
where a |= ψ i means that ψ i is verified by the label aremember that ψ i ∈ BC(labels). Also, given a profile π and a label a ∈ A, we write aπ for the concatenation of the profiles of σ a and π.

aπ def = π ∪ {α•β ∈ Ω ϕ | α ∈ σ a , β ∈ π}
Finally, we write π + a for the union of the profiles π and σ a .

π + a def = π ∪ σ a
Remark 1. These are idempotent and commutative operations:

a(aπ) = aπ; (π + a) + a = π + a; a(π + a) = aπ + a. Definition 1 (mosaic). A mosaic over ϕ is a tuple µ = (a, d, ← χ , → χ ) where a ∈ A, d ∈ D, and ← χ , → χ ∈ ℘ <∞ (D × Ω p ϕ ).
The idea is that ← χ is contains the profiles of the data values that can be found to the left and → χ of those to the right.

We use letters µ, ν for mosaics and we fix the nomenclature We call µ(e) the profile of e in µ. Note that we call a profile either to a subset of Ω p ϕ or to a pair of subsets of Ω p ϕ . The intended meaning will be clear from the context.

µ i = (a i , d i , ← χ i , → χ i ) for every i. We adopt the following notation for χ ∈ { ← χ , → χ }, α ∈ Ω p ϕ ,
Given a formula ϕ = ϕ 1 ∧ ϕ 2 in normal form, a data word w and a position i, we say that a mosaic µ over ϕ is the ϕ-abstraction of (w, i) if it is defined in the expected way by taking into account the data values of w and the path expressions

Ω p ϕ . That is, if w = a⊗d and µ = (a, d, ← χ , → χ ) we define (a, d) = w(i), → χ = {(e, [ψ 1 ]• • • • •[ψ n ]) ∈ D × Ω p ϕ | there are i ≤ j 1 ≤ • • • ≤ j n ≤ |w| where a(j k ) |= ψ k for all k and d(j n ) = e}. Likewise for ← χ i .
For every atomic expression α = β , α = β or a from Ω ϕ one can decide if the formula holds at position i of w simply by inspecting the ϕ-abstraction of (w, i). Hence, one can define a satisfaction relation , where the following holds.

Lemma 3. For every formula ϕ in normal form and subformula ψ ∈ Ω ϕ and for every data word w and position i, w, i |= ϕ iff µ ψ, where µ is the ϕ-abstraction of (w, i).

Not all mosaics are consistent with the ϕ-abstraction. For example, a mosaic over ϕ with a label a ∈ Ω ϕ such that → χ ([a]) = ∅ cannot be the ϕ-abstraction of any (w, i): Finally, M(ϕ) is the set of all valid mosaics over ϕ. Henceforth we say mosaic to denote a valid mosaic unless otherwise stated. Observe that the ϕ-abstraction of a data word w and position i results always in a valid mosaic.

→ χ ([a]) must contain the mosaic's datum. Definition 2 (validity). A mosaic (a, d, ← χ , → χ ) is valid if it satisfies the following restrictions for all χ ∈ { ← χ , → χ } 1. for every d ∈ D, χ(d ) is suffix closed: if α•β ∈ χ(d ) then β ∈ χ(d ),
Lemma 4. The ϕ-abstraction of (w, i) is a valid mosaic of M(ϕ), assuming w |= ϕ and i ∈ pos(w).

The importance of the normal form presented before is that it allows us to work separately on each data value. The left profile of a data value at position i + 1 depends solely on the profile of the data value at position i, and the labels of these positions. In fact, all the interaction between the profiles of different data values is encapsulated in the restrictions imposed by the function γ ϕ . This is due to the fact that all path expressions contained in Ω p ϕ depend solely on the label of the mosaic. We can hence define a relation that tests whether it is possible that two profiles of a data value can abstract two consecutive positions.

We define the relations

m(a, 1, π 1 , b, j, π 2 ) def ⇔ π 1 = aπ 2 + a (1) → m(a, 0, π 1 , b, j, π 2 ) def ⇔ π 1 = aπ 2 (2) ← m(a, i, ρ 1 , b, j, ρ 2 ) def ⇔ → m(b, j, ρ 2 , a, i, ρ 1 ) (3) We define m(a, i, (ρ 1 , π 1 ), b, j, (ρ 2 , π 2 )) iff → m(a, i, π 1 , b, j, π 2 ) and ← m(a, i, ρ 1 , b, j, ρ 2 ).
We use the expression d ? =d to denote 1 if d = d or 0 otherwise. Now we can define the transition system : Definition 3 ( ). We say that µ 1 and µ 2 match, and we write it

µ 1 µ 2 , iff for all d ∈ D m(a 1 , d 1 ? =d, µ 1 (d), a 2 , d 2 ? =d, µ 2 (d)) .
We define the necessary properties that the abstractions of the borders (i.e., of the first and last elements) should admit.

← -- dem(µ) def = {(e, ρ) ∈ ← χ | (e = d ∧ ρ = ∅) ∨ (e = d ∧ ρ = σ a )} --→ dem(µ) def = {(e, π) ∈ → χ | (e = d ∧ π = ∅) ∨ (e = d ∧ π = σ a )}
We say that a mosaic is left-complete (resp. right-complete) if it does not have left-demands (resp. right-demands).

Definition 5. A sequence is a sequence of mosaics µ 1 , . . . , µ n such that µ i µ i+1 for all i < n. We say that the sequence is complete if

← -- dem(µ 1 ) = --→ dem(µ n ) = ∅.
We state the derivation problem for a transition system →.

The derivation problem for → INPUT: A formula ϕ = ϕ 1 ∧ ϕ 2 in normal form. OUTPUT: Is there a complete → sequence over M(ϕ)

whose leftmost mosaic µ verifies µ ϕ 1 ?

D. From the satisfiability problem to the derivation problem

We can reduce the satisfiability problem for ϕ into a the derivation problem for over M(ϕ).

Proposition 1. A PathLogic formula ϕ = ϕ 1 ∧ ϕ 2 in normal form is satisfiable iff the derivation problem for with input ϕ has a positive answer.

IV. THE DERIVATION PROBLEM FOR

In this section we show how to solve the derivation problem for . The general idea is that we introduce a quasi-order ≤ K on the set of mosaics, parametrized by a set of data values K. The parameter of this relation relies on the concept of rigid values, which are data values with a specific role in an sequence. We show that ≤ K is (upward) monotone with respect to . This monotonicity allows us to define a transition relation K that has en equivalent derivation problem. We postpone the solving of the derivation problem for K to Section V.

We fix once and for all a formula ϕ of PathLogic in normal form, and M(ϕ) as the domain of the transition relation .

A. Rigid and flexible data values

Not all data values are the same in a data word satisfying a formula, different data values have different roles. We introduce here two categories of data values: rigid and flexible. Rigid data values are important for the satisfaction of the formula and special care is needed to treat these, whereas flexible values are not crucial, and they can be sometimes removed from the word. Let us give some more precise intuition. We use the logic PathLogic to make this intuition clear, but we will then state the definitions in terms of our transition system.

Given a data word w such that w |= ϕ, suppose there is a data value d such that if d can be accessed through a path α from some position i, then d is the only value that can be accessed through α at position i. When there is such a d we call it a rigid value for i, since the logic can identify it and pinpoint it from the rest of the data values. If d is rigid for at least one position of w we say that d is rigid for w. All the remaining data values (which are the flexible values) of w play the role of assuring that "there are at least two data values reachable through α from position i" for some α and i. As such, its importance is only relative. For example, if w is a data word satisfying ϕ and containing d as a flexible value, then consider w the result of replacing, for some fresh data value d , every appearance of (a, d) in w by (a, d) (a, d ). w will continue to satisfy ϕ. But this is not necessarily true if d is a rigid value. The same notions hold for our sequences. We say that a mosaic µ is K-compliant for K ⊆ D if all its rigid values are inside K.

Definition 6 (K-compliant). Given a finite set K ⊆ D we say that a mosaic µ = (a, d,

← χ , → χ ) is K-compliant iff for all α ∈ Ω p ϕ and χ ∈ { → χ , ← χ } χ(α) = {d } implies d ∈ K .
This notion of K-compliance will be central for our second reduction to the more abstract transition system. Observe that for every sequence there is a trivial K such that all its mosaics are K-compliant: the set of all data values of the data word. Later on, we will see that we can effectively bound K as a function of ϕ. This bound is independent of the length of the sequence. Based on this idea of rigid values, we define a relation ≤ K specially suited for mosaics that are K-compliant. In this definition, if two mosaics are in the relation, then all the profiles from K must remain untouched. For any other flexible value we are only interested in having at least as many data values with a certain profile in the bigger profile. We also preserve the existence or non-existence of a flexible data value with a given profile.

Definition 7 (≤ K ). µ 1 ≤ K µ 2 iff: 1. they have the same label 2. ∀d ∈ K, µ 1 (d) = µ 2 (d), 3. µ 1 (d 1 ) = µ 2 (d 2 ) for d i the data value of µ i , 4. ∀(ρ, π) ∈ ℘(Ω p ϕ ) × ℘(Ω p ϕ ), |µ -1 1 (ρ, π) \ K| ≤ 1 |µ -1 2 (ρ, π) \ K| where n ≤ 1 m iff 0 = n = m or 1 ≤ n ≤ m. Lemma 5. Given µ 1 ≤ K µ 2 we have 1. if both mosaics are valid, then µ 1 is left-complete iff µ 2 is left-complete, and likewise for right-complete, 2. if µ 1 is K-compliant, then µ 2 is K-compliant, 3. if µ 1 is valid, then µ 2 is valid, 4. if both are K-compliant, for all ψ ∈ Ω ϕ , µ 1 ψ iff µ 2 ψ.

B. A more abstract transition system

We define a transition system K over the set of Kcompliant mosaics, which is also parametrized by K. We then reduce the derivation problem for to the derivation problem for K .

Definition 8 ( K ). µ 1 K µ 2 iff µ 1 and µ 2 are K-compliant and µ 1 ≤ K µ 1 µ 2 ≥ K µ 2 for some mosaics µ 1 , µ 2 . ∀ ∃ µ 3 µ 1 µ 2 µ 4 • • • ≤ K ≤ K
Fig. 2. The forward monotonicity Lemma.

Note that K is a looser relation than . This will enable us to easily bound the domain. But we leave this issue to the next Section V. Our present goal is to show that there is indeed a reduction.

Proposition 2. There exists a K-compliant complete K sequence over M(ϕ) whose first element µ 1 verifies µ 1 ϕ 1 iff there exists a K-compliant complete sequence over M(ϕ) whose first element µ 1 verifies µ 1 ϕ 1 .

To prove the above proposition, first we need to show a monotonicity property of the transition system . The next Lemma asserts that is upward compatible with respect to ≤ K , as in Figure 2. This is a crucial technical Lemma of our proof.

Lemma 6 (forward monotonicity). For every K-compliant

mosaics µ 3 ≥ K µ 1 µ 2 there is a K-compliant mosaic µ 4 such that µ 3 + µ 4 ≥ K µ 2 .
Since all our definitions are symmetrical, by the proof of Lemma 7 we will also obtain a similar result for backward monotonicity.

Lemma 7 (backward monotonicity). For every K-compliant mosaics µ 1 µ 2 ≤ K µ 4 there is a K-compliant mosaic µ 3 such that µ 1 ≤ K µ 3 + µ 4 .

Before going into the details of the proof, we state some simple facts.

Lemma 8 (about m). For any two valid mosaics µ 1 , µ 2 ∈ M(ϕ) and d ∈ D, suppose that a 1 = a 2 = a for some a ∈ A.

Let (ρ 1 , π 1 ) = µ 1 (d), (ρ 2 , π 2 ) = µ 2 (d), i = (d ? =d 1 ), j = (d ? =d 2 ). Then → m(a, i, π 1 , a, j, π 2 ) holds iff either i = 1, j = 0 and π 1 = π 2 + a, (4)
i = 0, j = 0 and π 1 = π 2 , (5) i = 1, j = 1 and π 1 = π 2 , or (6)
i = 0, j = 1 and π 1 = π 2 . ( 7
)
Analogously, ← m(a, i, π 1 , a, j, π 2 ) holds iff either i = 1, j = 0 and ρ 1 = ρ 2 , (8) i = 0, j = 0 and ρ 1 = ρ 2 , (9) i = 1, j = 1 and ρ 1 = ρ 2 , or (10) i = 0, j = 1 and ρ 2 = ρ 1 + a.

(11)

Proof of Lemma 7 (monotonicity):

Let µ i = (a i , d i , ← χ i , → χ i ) for all i ∈ {1, 2, 3, 4}.
In this context we will call flexible value to a value d ∈ D \ K and a rigid one to a value d ∈ K. Notice that a 1 = a 3 by definition of µ 1 ≤ K µ 3 . By µ 1 µ 2 we can assume µ 1 (d 1 ) = (ρ 1 , a 1 π 1 + a 1 ) and µ 2 (d 1 ) = (a 2 ρ 1 , π 1 ) for some ρ 1 of the form ρ 1 = a 1 ρ + a 1 . Similarly, we assume µ 2 (d 2 ) = (a 2 ρ 2 + a 2 , π 2 ) and µ 1 (d 2 ) = (ρ 2 , a 1 π 2 ) for some π 2 of the form π 2 = a 2 π + a 2 . Hence, if d 1 = d 2 we have that ρ 2 = ρ 1 and π 2 = π 1 . We divide this proof into two parts. The first one groups all the easy cases, where the simulation can be done in one step: µ 3 µ 4 . For the second part, we will need to use more than one step to arrive to such µ 4 mosaic.

Easy situation. The easy situation is when all data values in µ 3 can be 'simulated' by the behavior of data values of µ 1 . We say that a flexible data value d of µ 3 can simulate another flexible data value d of µ 1 if they have the same same profile and one is equal to d 3 iff the other one is equal to d 1 . If this holds, d can have the same profile as d by making a one-step transition, reading the same letter as µ 2 . If all flexible data values of µ 3 simulate some data value of µ 1 and in turn every flexible data value from µ 1 is simulated by at least one data value from µ 3 , we can arrive to a mosaic µ 4 ≥ K µ 2 ; but there is one caveat. There cannot be more than one data value that is chosen to simulate d 2 , since only one of them can become the data value of µ 4 . In this case the simulation would fail. But if there were another flexible data value d with the same profile as d 2 in µ 1 , then we can choose only one data value to simulate d 2 , and all the rest to simulate d . We call this last restriction the condition B. By definition of ≤ K it is a fact that for every data value d such that µ 3

(d) = µ 3 (d 3 ) (= µ 1 (d 1 ))
there is at least one data value in µ 1 that can simulate. Then, in order to assure that every data value of µ 3 can be simulated, it suffices to check that either d 1 is rigid (and hence also d 3 ), or if d 1 is flexible, that there are at least another flexible data value with the same profile as d 1 . We call this the condition A. If this would not hold, there could happen that there is only d 1 with the profile µ 1 (d 1 ) in µ 1 , and that there is a flexible data value d = d 3 with µ 3 (d) = µ 1 (d 1 ). This data value d cannot simulate any value, and the simulation would then fail.

We formalize the properties we have discussed. If A and B hold, by definition of ≤ K then there exists a surjective function ξ : D → D such that for every d ∈ D,

1. d = d 3 iff ξ(d) = d 1 , 2. |ξ -1 (d 2 )| = 1. 3. µ 3 (d) = µ 1 (ξ(d)) 4. if d ∈ K then ξ(d) = d,
In other words, ξ behaves as the identity on K, sends data values from µ 3 to data values with the same profile in µ 1 , and sends only one data value to d 1 (namely d 3 ) and to d 2 . We call ξ a simulating function between µ 3 and µ 1 . If ξ is defined only for subsets D 1 , D 2 ⊆ D, we call ξ : D 1 → D 2 a partial simulating function on D 1 , D 2 between µ 3 and µ 1 , and in this case conditions 1 and 2 are replaced by

1 . if d 3 ∈ D 1 , d = d 3 iff ξ(d) = d 1 , 2 . if d 2 ∈ D 2 , |ξ -1 (d 2 )| = 1. We build µ 4 = (a 4 , d 4 , ← χ , → χ ) where a 4 = a 2 , {d 4 } = ξ -1 (d 2 ) and we define µ 4 (d) = µ 2 (ξ(d)) for all d ∈ D. It is straightforward to check that for every d ∈ D m(a 1 , d ? =d 3 , µ 3 (d), a 2 , d ? =d 4 , µ 4 (d)) iff m(a 1 , ξ(d) ? =d 1 , µ 1 (ξ(d)), a 2 , ξ(d) ? =d 2 , µ 2 (ξ(d))) .
Complex situation 1. We suppose first that the condition A just seen does not hold, but that condition B holds. In other words, d 1 is the only flexible value with profile µ 1 (d 1 ) in µ 1 . In particular, d 1 = d 2 . Otherwise we would have a contradiction, since A and B would express the same property, and we assume that one holds but the other does not.

Note that in this case we cannot define a function ξ just as before, because there may be a flexible data value d = d 3 with µ 3 (d) = µ 1 (d 1 ). (If there is no such data value, we proceed just as in the easy case.) We basically do not know what to do with this data value d, since it cannot simulate any other data value from µ 1 . Let P be the set of these problematic data values,

P = {d ∈ D \ K | d = d 3 , µ 3 (d) = µ 1 (d 1 )} If P = {e 1 , .
. . , e n }, we will create n intermediary mosaics µ 1 , . . . , µ n with

µ 3 µ 1 • • • µ n µ 4 ≥ K µ 2
where µ i has the same letter a 1 as µ 3 and e i as data value. Further, all data values except {d 3 , e 1 , . . . , e n } will preserve the same profile they have in µ 3 all along µ 1 , . . . , µ n . This is just a consequence of (5). Each mosaic µ i is defined as follows • a 1 is the label, and e i is the data value,

• d 3 , e 1 , . . . , e i-1 have profile (ρ 1 , a 1 π 1 ),

• e i , . . . , e n have profile (ρ 1 , a 1 π 1 + a 1 ), and • any other data value d ∈ {d 3 , e 1 , . . . , e n } has profile µ 3 (d). These are indeed legal mosaics.

Claim 1. For all i ∈ [n], µ i is valid and K-compliant. Claim 2. µ 3 µ 1 , and for all i ∈ [n -1], µ i µ i+1 .
Proof: To simplify notation, let us define µ 0 = µ 3 and e 0 = d 3 . Take an arbitrary data value d ∈ {e 0 , e 1 , . . . , e n } and take any pair of mosaics µ i , µ i+1 with 0 ≤ i < n. Then we have that: d is not the data value of µ i nor µ i+1 ; and µ i and µ i+1 carry the same letter a 1 . We can thus apply conditions (5) and (9) and obtain that µ i (d) = µ i+1 (d) verifies m. If d ∈ {e 0 , . . . , e i-1 , e i+2 , . . . , e n }, the same applies, since d is not the data value of µ i nor µ i+1 , and then µ i (d) = µ i+1 (d) verifies m. If d = e i+1 we have that µ i (e i+1 ) = µ i+1 (e i+1 ) = (ρ 1 , a 1 π 1 + a 1 ). a 1 π 1 + a 1 verifies → m by condition (7), and ρ 1 verifies ← m by condition (11), since ρ 1 = a 1 ρ + a 1 and then ρ 1 + a 1 = ρ 1 by idempotence of +a 1 . Finally, if d = e i we have that µ i (d) = (ρ 1 , a 1 π 1 + a 1 ) and µ i+1 (d) = (ρ 1 , a 1 π 1 ). The fact that ρ 1 is preserved is verified by ← m by condition (8). And on the other hand, by (4) a 1 π 1 + a 1 and a 1 π 1 verify → m.

Let D 1 = D\{d 3 , e 1 , . . . , e n }, D 2 = D\{d 1 } and ξ : D 1 → D 2 be a partial simulating function on D 1 , D 2 between µ 3 and µ 1 . It must exist since condition B holds.

Claim 3. There exists a partial simulating function ξ : D 1 → D 2 between µ 3 and µ 1 .

We then define µ 4 as µ 4 = (a 4 , d 4 , First, take any e ∈ {d 3 , e 1 , . . . , e n-1 }. We have that µ n (e) = (ρ 1 , a 1 π 1 ) and µ 4 (e) = (a 2 ρ 1 , π 1 ). It is immediate that → m(a 1 , 0, a 1 π 1 , a 2 , 0, π 1 ) and ← m(a 1 , 0, ρ 1 , a 2 , 0, a 2 ρ 1 ) and hence that e behaves correctly. Now take e n , where we have µ n (e n ) = (ρ 1 , a 1 π 1 + a 1 ) and µ 4 (e n ) = (a 2 ρ 1 , π 1 ). We simply need then to verify → m(a 1 , 1, a 1 π 1 + a 1 , a 2 , 0, π 1 ) and ← m(a 1 , 1, ρ 1 , a 2 , 0, a 2 ρ 1 ), which are clearly true.

← χ 4 , → χ 4 ) with a 4 = a 2 , {d 4 } = ξ -1 (d 2 ), µ 4 (d) = (a 2 ρ 1 , π 1 ) for all d ∈ {d 3 ,

Claim 5. µ 4 ≥ K µ 2

There are two other complex situations: when neither conditions A nor B hold, and when condition A holds but B does not. These conditions are treated in an analogous way. Indeed, if condition A holds but B does not, we use a symmetrical strategy, creating intermediate mosaics but this time with the same label as µ 2 . If neither of the conditions hold, we combine both approaches. The details are in the Appendix.

We can now show that the reduction from the derivation problem for to the derivation problem for K is sound and complete by the following two lemmas.

VI. LOWER BOUND

There is also a lower bound of EXPSPACE for the satisfiability problem of PathLogic. This bound also translates into a EXPSPACE-hardness for XPath( * ←, → * , =) since there is a PTIME translation from PathLogic to XPath( * ←, → * , =), as shown in the next Section. This can be shown by coding a solution for an instance of the 2 n corridor tiling problem. The coding, although it is not quite straightforward, utilizes several coding techniques developed in [FS09]. In particular, the coding of [FS09] was introduced to show non-primitive recursiveness of the logic XPath(→ + , =), whereas here we work with a logic which is expressive-equivalent to XPath(→ * , =). Although the precise coding of [FS09] fails for XPath(→ * , =), we reuse the same kind of techniques. The main idea is in the Appendix.

Since the coding for this problem need only to use expressions in one direction, we also obtain the EXPSPACE-hardness for XPath(→ * , =).

VII. COROLLARIES ON XPATH AND XML DOCUMENTS

Let us call plain-XPath( * ←, → * , =) to the fragment of XPath such that that • all path expressions do not mix * ← and → * , i.e., each path expressions uses only * ← or only → * , and • all test node expressions α = β and α = β are such that α uses only * ← and β only → * . It is immediate that this basically corresponds to PathLogic.

Lemma 15. There are PTIME translations such that for every node expression of plain-XPath( * ←, → * , =) (resp. of PathLogic) return an equivalent node expression PathLogic (resp. plain-XPath( * ←, → * , =)).

Corollary 2. The satisfiability problem for plain-XPath( * ←, → * , =) on data words is EXPSPACE-complete.

In fact, plain-XPath( * ←, → * , =) (and hence PathLogic) is expressive-equivalent to XPath( * ←, → * , =) through an EXP-TIME translation.

Lemma 16. There exists a computable EXPTIME translation that for every node expression ϕ of XPath( * ←, → * , =) returns an equivalent node expression ψ of plain-XPath( * ←, → * , =).

VIII. DISCUSSION

We believe that the proof we give here allows to extend existing decidability results of XPath fragments on XML with navigation through reflexive-transitive axes. However, obtaining such results is non-trivial, since one has to combine the techniques of such results with the ones contained in our main proof. We propose that the following are candidates of (nontrivial) corollaries of the work contained in this paper and known results on XPath.

Conjecture 1. Satisfiability of XPath(↓, ↓ * , * ←, → * , =) on XML documents is decidable, with elementary complexity.

This would be an extension of the result of [START_REF] Figueira | Satisfiability of downward XPath with data equality tests[END_REF] stating that XPath(↓, ↓ * , =) is EXPTIME-complete, and in contrast to the fact that XPath(↓, ↓ * , * ←, → + , =) is undecidable and XPath(↓, ↓ * , → + , =) has non-primitive recursive complexity [FS09]. In fact, we believe that this can be pushed to show the following.

Conjecture 2. Satisfiability of XPath(↓, ↓ * , ↑ * , * ←, → * , =) on XML documents is decidable, with elementary complexity. Furthermore, it is plausible that the following fragment of XPath is decidable.

Conjecture 3. Satisfiability of XPath(↓, ↓ * , ↑, ↑ * , * ←, → * , =) on XML documents is decidable.
This would be an extension of a recent result stating that XPath(↓, ↓ * , ↑, ↑ * , =) is decidable [START_REF] Figueira | Bottom-up automata on data trees and vertical XPath[END_REF]. However, even XPath(↓,

↓ * , ↑, ↑ * , → + , =) or XPath(↓, ↓ * , ↑, ↑ * , →, =) are undecidable [FS09].

Future work

We conclude by mentioning some open questions. 1. Decidability of XPath fragments. Is any of the aforementioned conjectures true? 2. Infinite words. Is PathLogic decidable on infinite data words? Observe that PathLogic does not enjoy the finite model property. 3. Linear order. As a possible extension, one may add comparisons between data values with respect to a linear order.

over M(ϕ) such that µ 1 ϕ 1 . We build a data word w of length n such that µ i is the ϕ-abstraction of (w, i). The data word is defined as w(i) = (a i , d i ) where (a i , d i ) is the label and data value of µ i . We claim that for every i, µ i is the ϕ-abstraction of (w, i). In the following proof we only work with the → χ part of the mosaics. The proof for ← χ will follow by symmetry.

(sound) If from a position i we can access a data value d by going to the right with a path expression α ∈ Ω p ϕ , we want to show that (d, α) ∈ → χ . We proceed by combined induction on the size of α and the index ni. The base cases for i = n are immediate since everything is satisfied locally. If α = [ψ] and d i = d, then the data value can be accessed locally. By item 2 of validity of µ i , π i = a i π i + a i , where

π i = → χ i (d) α.
Since α ∈ σ ai then α ∈ π i . If on the other hand d i = d, this means that there is a future position j > i with data value d j = d such that a j |= ψ. This means that d can be accessed through α from position i + 1. We then apply the inductive hypothesis and we obtain that

(d, α) ∈ → χ i+1 . By Eq. (2) of → m, π i = a i π i+1 where π i+1 = → χ i+1 (d). Since α ∈ π i+1 , then α ∈ π i .
This concludes the base case. For the inductive case, suppose α = [ψ]•α . Suppose first that a i |= ψ. Observe that if we can access d through α we can also access d through α . By inductive hypothesis we have that α ∈ → χ i (d). By item 3 of validity of µ i we have that

→ χ i (d) = a i π for some π. since [ψ] ∈ σ ai , then [ψ]•α ∈ → χ i (d). Suppose now that a i |= ψ.
This means that d can be accessed actually from position i + 1 through α. We then apply the inductive hypothesis and obtain that α ∈ → χ i+1 (d). By Eq. (1) or (2) (depending on whether d = d i or not) we obtain in both cases that α must also be in (2) of → m, π i = a i π i+1 . Since α has only one element, by definition of a i π i+1 , α ∈ π 2 . We can then apply the inductive hypothesis and obtain that d can be accessed through α from position (w, i + 1), which implies that it can also be accessed from position (w, i).

Finally, if d i = d but a |= ψ then µ i is not right-complete and there must be a mosaic µ i+1 where

→ m(a i , 1, π i , a i+1 , d i+1 ? =d, π i+1 )
where

π i = → χ i (d) α and π i+1 = → χ i+1 (d). By Eq. (1) of → m, π i = a i π i+1 + a i .
Since a i |= ψ we must have that α ∈ π i+1 . Again, we apply the inductive hypothesis and obtain that d can be accessed through α from position (w, i + 1), which implies that it can also be accessed from position (w, i). This concludes the base case. For the inductive case, suppose

α = [ψ]•α . If a i |= ψ then by condition 1 of a valid mosaic, since α ∈ → χ i (d) then α ∈ → χ i (d).
By applying inductive hypothesis we obtain that d can be reached from position i through α and since a i |= ψ it can also be reached through [ψ]•α . If on the other hand a i |= ψ, then by equations (1) or (2) (depending on whether d i = d or not) we obtain that π i = a i π i+1 or π i = a i π i+1 + a i . In any case, since ψ ∈ a i , we obtain that α ∈ π i+1 and we apply the inductive hypothesis just as in the base case.

(only if) This direction is easier. Given a data words we have to show that the ϕ-abstraction of each position results in a complete sequence whose first element verifies ϕ 1 . Given a data word w = a⊗d such that w |= ϕ we can build a sequence µ 1 , . . . , µ |w| over M(ϕ) that is complete, such that µ 1 ϕ. We define µ i = (a i , d i , ← χ i , → χ i ) as the ϕabstraction of (w, i).

Let us first show that µ 1 , . . . , µ |w| are valid mosaics of M(ϕ). It is easy to see that the path expressions of

→ χ (d) are suffix closed since if i ∈ [[α•β]] w → then i ∈ [[β]] w → .
Hence, item 1 holds. Items 2 and 3 are also very easy to verify. Finally, we need to show that all mosaics with a letter a verify γ ϕ (a). But this must be true by the formula ϕ 2 holding at the leftmost element. We then have that item 4 of the validity conditions is also met.

Secondly, we show that µ 1 , . . . , µ |w| is a sequence. Let us analyze a pair of arbitrary positions i, i+1 and a data value

d ∈ D. Let us show that → m(a i , d i ? =d, → χ i (d), a i+1 , d i+1 ? =d, → χ i+1 (d))
holds true. Take an arbitrary path expression α

= [ψ 1 ]• • • • •[ψ n ] ∈ Ω p ϕ . If (d, α) ∈ → χ i+1
then there are n ordered positions greater or equal to i + 1 satisfying respectively ψ 1 , . . . , ψ n by definition of ϕ-abstraction. Then in particular they are greater or equal to i, and hence (d, α) ∈

→ χ i . Thus, → χ i+1 (d) ⊆ → χ i (d).
On the other hand, suppose there is a prefix of α, say

[ψ 1 ]• • • • •[ψ k ], such that a i |= ψ j for all j ∈ [1..k], and that (d, [ψ k+1 ]• • • • •[ψ n ]) ∈ → χ i+1 (d).
Then, there are witness positions for ψ k+1 , . . . , ψ n which are greater or equal to i + 1. Also, there is a witness for ψ 1 , . . . , ψ k at position i. Then, d can be accessed through α from position i, and then α ∈ ) is completely analogous. We conclude that the sequence µ 1 , . . . , µ |w| is a sequence over M(ϕ). Now, we show that it is complete. By way of contradiction, suppose that µ 1 is not left-complete. Let (d, π) ∈ ← -dem(µ 1 ). Then:

• If d = d 1 and π = σ a , this means that there is α ∈ Ω p ϕ such that (d, α) ∈ ← χ (µ 1
) and a |= ψ where [ψ] is a particle of α. By construction of µ 1 and the fact that (d, α) ∈ ← χ (µ 1 ), this means that there is a position to the left of the first position that can reach the data value d through α. But since a |= ψ this position must be strictly to the left. This is a contradiction, since there are no positions to the left of the first one.

• Otherwise, d = d 1 and (d, α) ∈ ← χ (µ 1 ). Again, we conclude that there must be a position strictly to the left of the first one, which is a contradiction. Then, we have that necessarily µ 1 is left-complete. Proceeding in a similar way, w prove that µ |w| is right-complete.

Finally, we show that µ 1 ϕ 1 . But this is immediate by Lemma 3 from the fact that w, 1 |= µ 1 .

APPENDIX TO SECTION IV

Proof of Lemma 5: We show, one by one, all conditions of the Lemma.

Condition 1: If µ 1 is not right-complete, then either:

• There is a path expression α ∈ σ a1 and a data value e = d 1 such that (e, α) ∈ → χ 1 . Then for the profile (ρ, π) = µ 1 (e) there must be at least one data value e such that µ 2 (e ) = (ρ, π). Hence, µ 2 is not right-complete either.

• There is a path expression α ∈ σ a1 such that

(d 1 , α) ∈ → χ 1 . Since µ 1 (d 1 ) = µ 2 (d 2 ), then (d 2 , α) ∈ → χ 2 and µ 2 is not right-complete.
• There is a path expression α ∈ σ a1 such that (d 1 , α) ∈ → χ 1 . But in this case µ 1 is not valid, since d 1 must contain at least all the path expressions from σ a1 .

The back condition is identical, and the condition for leftcomplete is completely symmetrical.

Condition 2: Suppose that µ 2 is not K-compliant. Then suppose without any loss of generality that there is α ∈ Ω p ϕ such that → χ 2 (α) = {e} for e ∈ K. Let µ 2 (e) = (ρ, π), and hence µ

-1 2 (ρ, π) = {e}. By µ 1 ≤ K µ 2 , |µ -1 1 (ρ, π) \ K| ≤ 1 |µ -1
2 (ρ, π) \ K|, and by definition of ≤ 1 we have that |µ -1 2 (ρ, π) \ K| = 1. Then there is also a data value e such that → χ 1 (α) = {e }. Hence, µ 1 is not K-compliant.

Condition 4: Suppose that µ 1 ψ. Let ψ = ←α = -→ β for some path expressions α, β. Suppose first that either α is equal to ε. Then the test amounts to having

(d 1 , β) ∈ → χ 1 . Since µ 1 (d 1 ) = µ 2 (d 2 ) we have that (d 2 , β) ∈ → χ 2
and hence that µ 2 ψ. If none of α, β are ε then there must be a data value e ∈ D such that (e, α) ∈ ← χ 1 and (e, β) ∈ → χ 1 ). Consider the profile of this data value (ρ, π) = µ 1 (e). By µ 1 ≤ K µ 2 there must be a data value e such that µ 2 (e ) = (ρ, π). Then,

µ 2 ← - α = - → β . If ψ = ← - α = - → β we proceed in a similar way. If ψ = ¬ ← - α = - → β this means that µ 1 (α) ∩ µ 1 (β) = ∅. By way of contradiction, suppose that µ 2 (α) ∩ µ 2 (β) e. Let (ρ, π) = µ 2 (e).
Then we have that by µ 1 ≤ K µ 2 there must be a data value e such that µ 1 (e) = (ρ, π). Hence µ

1 (α) ∩ µ 1 (β) e which is a contradiction. Finally, if ψ = ¬ ← - α = - → β , then either • ← χ 1 (α) = ∅, • → χ 1 (β) = ∅, or • ← χ 1 (α) = → χ 1 (β) = {e} for some e ∈ D.
We can see that in each of this cases a similar property holds for µ 2 . In particular for the last one, this condition necessarily means that e ∈ K since µ 1 is K-compliant. Let (ρ, π) = µ 1 (e). Then we have that |µ -1 1 (ρ, π) \ K| = 0 and hence |µ -1 2 (ρ, π)\K| = 0. This, added to the fact that µ 2 (e) = (ρ, π)

yields that ← χ 2 (α) = → χ 2 (β) = {e}.
Condition 3: This condition is immediate from Condition 4 and the fact that there is a data value e with µ 1 (e) = (ρ, π) iff there is a data value e with µ 2 (e ) = (ρ, π).

Proof of Lemma 8: We only prove conditions (4), (5), (6) and (7), since the second set of conditions is completely symmetrical.

If i = 1, j = 0, then d = d 1 , d = d 2 . By (1) π 1 = aπ 2 + a. On the other hand, since a 2 = a, by condition 3 of validity applied to µ 2 , π 2 = aπ 2 for some π 2 . By idempotence we have that aπ 2 = π 2 and hence that π 1 = aπ 2 + a = π 2 + a.

If i = 0, j = 0 by (2) π 1 = aπ 2 and aπ 2 = π 2 by the same reason as before.

If i = 1, j = 1, by (1) we have that π 1 = aπ 2 + a and π 2 = aπ 2 + a by condition 2 of validity of µ 2 , since d = d 2 . Again by idempotence we obtain π 1 = aπ 2 + a = π 2 . andH(f (i, j), f (i + 1, j)), V (f (i, j), f (i, j + 1)) for all possible i, j. In this case we say that the problem has a solution. This problem is known to be complete for EXPSPACE [START_REF] Chlebus | Domino-tiling games[END_REF]. We will see f as a matrix of 2 n columns and k rows, whose indices grow to the left and to the top, like in Figure 4.

n × k → T such that f (1, 1) = T 0 , f (2 n , k) = T s ,
Groups: Since PathLogic cannot avoid having repeated consecutive nodes with the same symbol, in this coding we will always have to work with groups of nodes with the same symbol. Unfortunately this makes the coding somewhat more cumbersome. For the purpose of this poof, we consider a data values as elements of (A × D) * , as opposed to the functional definition given in Section II. (Of course, both definitions are equivalent.) This will simplify the description of the structure in our coding.

Let us fix an instance of the 2 n corridor tiling problem. We will code a solution like the one in Figure 4 in a data word by coding each of the position of the matrix, starting with the first row from left to right, then with the second row, etc.

The particular strategy to link consecutive columns and rows follows a similar coding idea as the one developed in [FS09]. Let A = {b 1 , . . . , b n , N → , N ↑ , #, @, beg, end, T 1 , . . . , T s } .

We will use data values as pointers to future elements, in the sense that "a node (a, d) points to another node (b, e)" if (b, e) appears to the right of (a, d) and d = e. The coding of a run consists in a succession of blocks. Each block corresponds to a position of the solution matrix. We first describe the general structure of the block in terms of the labels it must contain, and then we describe more precise properties that this structure must verify.

The shape of each block is of the form where w ∈ (A × D) * , and such that for every d i there exists e j with d i = e j . Further, every data value of w is not equal to any d i nor e j . Also, w is of the form T ile N um N ext → N ext ↑ such that

• T ile ∈ (T × D) + is a group of nodes with the same symbol T i , for some i ≤ s (the data values will play no role here). It is easy to see that there exists a model with these properties iff the 2 n corridor tiling problem instance has a solution.

It is possible to code these conditions using similar techniques as in [FS09]. The cited work uses a different logic that is expressive equivalent XPath(→ + , =) to code a much harder (non-primitive recursive) problem which involves properties that we cannot express with PathLogic. However, in order to code these properties we do not need the strict transitive relation → + , we can use → * . Remark 3. The above coding of EXPSPACE-hardness uses only formulas that move in one direction.

APPENDIX TO SECTION VII XPath( * ←, → * , =) and plain-XPath( * ←, → * , =) are expressive-equivalent. There is a translation that transforms each node expression of XPath( * ←, → * , =) in an exponential disjunction of node expressions of plain-XPath( * ←, → * , =).

Proof idea of Lemma 16: We can factorize any atomic node expression like α = β or α = β uses path expressions with two directions into a disjunction of expressions, such that each one of these is in plain-XPath( * ←, → * , =). We proceed by induction on the nesting depth of the subformula, defined as the maximum number of nested path expressions it contains. The base case is immediate. Take an expression α = β where N α and N β are the sets of node expressions [ψ] that use respectively α and β, where each of these is a formula of plain-XPath( * ←, → * , =) by inductive hypothesis. The translation consists in checking from all the possible linearizations of N α ∪ N β ∪ {curr} those that are consistent with α, β. Here, curr represents the current point of evaluation. For example, the linearization

[ψ 1 ][ψ 3 ]curr[η][ψ 2 ] is consistent with α = * ←[ψ 1 ]→ * [ψ 2 ] * ←[ψ 3 ], β = → * [η]. However, [ψ 1 ][ψ 2 ][ψ 3 ]curr[η]
is not. For each consistent linearization the translation produces one disjunct α = β with the aforementioned properties. For our example of linearization it would produce

[ψ 1 ] * ←[ψ 3 ] * ← = → * [η]→ * [ψ 2 ] .
The procedure for formulas α = β is similar. This translation is exponential.

Fig. 1 .

 1 Fig. 1. Syntax and semantics of PathLogic for a data word w = a⊗d.

=

  and e ∈ D. χ(e) def = {α ∈ Ω p ϕ | (e, α) ∈ χ} µ(e) {e ∈ D | (e, α) ∈ χ}

χ

  (d) = aπ + a and ← χ (d) = aρ + a for some π, ρ ⊆ Ω p ϕ , 3. for every d ∈ D, χ(d ) = aπ for some π ⊆ Ω p ϕ , and 4. µ γ ϕ (a).

m

  that evidence this dependency of profiles that we discussed for a given data value d. Intuitively, the first three components of the relation specify the situation for d on the left position: the label of the node, whether d is equal (1) or not (0) to the current data value, and its profile ( → χ (d) or ← χ (d) respectively for → m, ← m). The other three components contain a similar description for the same data value on the right position. The idea is that → m and ← m hold if it is possible to have this situation in a data word.

→

Definition 4 .

 4 We define the left and right demands of a mosaic µ = (a, d, ← χ , → χ ). A left-(resp. right-) demand consists of the data values that necessarily have to be found to the left (resp. to the right).

  (A) If d 1 is a flexible value, then there are other flexible values with the same profile. That is, there exists d = d 1 with µ 1 (d ) = µ 1 (d 1 ). (B) The same applies to d 2 : if it is a flexible value then there exists another flexible value d = d 2 with µ 1 (d ) = µ 1 (d 2 ).

Proposition 4 .

 4 The satisfiability problem for PathLogic is EXPSPACE-hard.

→

  χ i (d). (complete) Suppose that (d, α) ∈ → χ i , we want to show that from position i we can access d by going to the right with a path expression α. We proceed first by induction on the length of α and then by induction on the index ni. Suppose first that α = [ψ]. If a i |= ψ and d i = d, then α is satisfied locally and we are done. If d i = d then µ i is not right-complete, this means that there is a mosaic µ i+1 where → m(a i , 0, π i , a i+1 , d i+1 ? =d, π i+1 ) where π i = → χ i (d) α and π i+1 = → χ i+1 (d). By Eq.

→

  χ i (d) by definition of ϕ-abstraction. We just showed that a i → χ i+1 (d) ⊆ → χ i (d), that will be useful next. We separate the two different cases from the definition of → m: either d i = d or d i = d. Suppose first d i = d. Any path α ∈ → χ i (d) has a (possibly empty) prefix which is satisfied at position i by letter a i , and a suffix that is satisfied at positions bigger or equal to i + 1. But this suffix cannot be empty, since this would mean that d i = d. Then, we have that → χ i (d) ⊆ a i → χ i+1 (d) and we conclude that a i → χ i+1 (d) = → χ i (d). On the other hand, if d i = d, we can show that in this case a i → χ i+1 +a i = → χ i proceeding in a similar way. We showed that → m(a i , d i ? =d, → χ i , a i+1 , d i+1 ? =d, → χ i+1 ) holds. The proof for ← m(a i , d i ? =d, ← χ i , a i+1 , d i+1 ? =d, ← χ i+1

Fig. 4 .

 4 Fig. 4. 2 n corridor tiling. Each depicted box contains a tile from T . Each number inside a box is the index of the position. APPENDIX TO SECTION VI Proof of Proposition 4: We show this by coding an instance of the 2 n corridor tiling problem. An instance of this problem consists in a size of the corridor n (encoded in unary), a set of tiles T = {T 1 , . . . , T s }, a special final tile T s , an initial tile T 1 , and the horizontal and vertical tiling relations H, V ⊆ T × T . The problem consists in answering whether there is k ∈ N and a function f : 2n × k → T such that f (1, 1) = T 0 , f (2 n , k) = T s , and H(f (i, j), f (i + 1, j)), V (f (i, j), f (i, j + 1)) for all possible i, j. In this case we say that the problem has a solution. This problem is known to be complete for EXPSPACE[START_REF] Chlebus | Domino-tiling games[END_REF]. We will see f as a matrix of 2 n columns and k rows, whose indices grow to the left and to the top, like in Figure4.Groups: Since PathLogic cannot avoid having repeated consecutive nodes with the same symbol, in this coding we will always have to work with groups of nodes with the same symbol. Unfortunately this makes the coding somewhat more cumbersome. For the purpose of this poof, we consider a data values as elements of (A × D) * , as opposed to the functional definition given in Section II. (Of course, both definitions are equivalent.) This will simplify the description of the structure in our coding.Let us fix an instance of the 2 n corridor tiling problem. We will code a solution like the one in Figure4in a data word by coding each of the position of the matrix, starting with the first row from left to right, then with the second row, etc.The particular strategy to link consecutive columns and rows follows a similar coding idea as the one developed in [FS09]. Let

(

  beg, d 1 ) • • • (beg, d n ) w (end, e 1 ) • • • (end, e m )

  • N ext → ∈ ({N → } × D) * , such that each element (N → , d) points to an element (beg, d) of a future block. (The idea will be that every one of these nodes point to the next block of the same row and next column.)• N ext ↑ ∈ ({N ↑ } × D) * , such that each element (N → , d)points to an element (beg, d) of a future block. (The idea is that these nodes point to the block of the same column and next row.)• N um ∈ ({b 1 , . . . , b n } × D) * is the coding of a binarynumber of n bits (the data values play no role here). We interpret that the i-th bit is 1 iff b i is in N um. From now on we call the index of the block, to the number coded in N um. Figure4shows the indices for each position of the matrix. Now we constrain this general structure to ensure that it encodes a valid solution of the problem. In the sequel we say that a block B points to a block B through some symbol S iff B contains an element (S, d) and B contains an element (beg, d ) such that d = d .• The first block has the tile T 1 .• The last block has the tile T s .• If the N ext → part of a block B is the empty string, then B is the last block. • The first block of the data word has index 0.• For every pair of blocks B, B such that B points to B through N → then the index n of B and n of B are such that n = n + 1 (mod 2 n ) -B is the next immediate block of B the tile t i of B and t j of B are in H-relation.• If B points to B through N ↑ thenthe index of B equals to the index of B there is exactly one block B of index 0 between B and B . the tile t i of B and t j of B are in V -relation.

  e 1 , . . . , e n } and µ 4 (d) = µ 2 (ξ(d)) for all other d ∈ D. It then follows that µ n µ 4 and that µ 4 ≥ K µ 2 .Proof: For every data value d that is simulated by ξ we have that m(a 1 , d Hence, since ξ does all the work for us for all data values except {d 3 , e 1 , . . . , e n }, we concentrate on these values.

	Claim 4. µ n	µ 4

? =e n , µ n (d), a 2 , d ? =d 4 , µ 4 (d)).

Strictly speaking these axes do not exist in XPath[START_REF] Clark | XML path language (XPath)[END_REF], they must be interpreted as the reflexive version of the 'following-sibling' and 'precedingsibling' axes respectively.

This fragment has no connection with the simple fragment of LTL ↓ 1 defined in[START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF].

Lemma 9 (complete). For every K-compliant complete sequence µ 1

• • • µ n over M(ϕ) there exists a Kcompliant complete sequence µ 1 K • • • K µ n over M(ϕ).

Proof: Trivial, since over K-compliant mosaics is a particular case of K by reflexivity of ≤ K .

Lemma 10 (sound). For every K-compliant sequence µ 1 K • • • K µ n over M(ϕ) there exists a K-compliant sequence µ 1

• • • µ m over M(ϕ) with µ 1 ≤ K µ 1 and µ n ≤ K µ m .

Proof: We proceed by induction on n. The base case is immediate. For the inductive step, suppose we have a sequence µ 1 K • • • K µ n K µ n+1 . By inductive hypothesis we obtain ν 1

• • • ν m with ν 1 ≥ K µ 1 and ν m ≥ K µ n , as ind. hyp.

backward monotonicity forward monotonicity claim definition shown in Figure 3. Since µ n K µ n+1 , then

for some µ n and µ n+1 by definition of K . Let µ † be such that µ † ≥ K ν m and µ † ≥ K µ n . It always exists such µ † .

Claim 6. For any three mosaics µ 1 , µ 2 , µ 3 with µ 1 ≥ K µ 3 and µ 2 ≥ K µ 3 , there exists a mosaic ν such that µ 1 ≤ K ν and µ 2 ≤ K ν.

By applying the monotonicity lemma we obtain on the one hand a sequence

where ν † l = µ † and ν 1 ≤ K ν † 1 , and by the backwards monotonicity lemma that

where µ † 1 = µ † and µ † k ≥ K µ n+1 . This is depicted in Figure 3. Further, these sequences are K-compliant. Then,

is the the desired sequence. By Lemmas 9 and 10 the Proposition 2 follows. The completeness and the fact that the first mosaic verifies ϕ 1 follow from Lemma 5.

V. THE DERIVATION PROBLEM FOR K

In this Section we solve the derivation problem for K . Since the transition system K is parametrized by K, in fact the derivation problem for K is in fact: "is there a finite set K ⊆ D such that the derivation problem for K over M(ϕ) has a positive solution?".

Note that we are dealing with many sources of infinity here: the choice of K, the domain of the transition system (i.e., the set of all mosaics), and the definition of K , which involves making a potentially infinite number of tests. Nevertheless, they can all be tamed. This is the objective of this section.

We now show that the object that we are dealing with can be effectively bounded, to end up with finite objects that can be treated by an algorithm.

A. A bound on the rigid values

We will show that for every complete sequence over M(ϕ) there are only linearly bounded many rigid values. This Lemma will allow us to bound the number of minimal ≤ K classes of equivalence.

Lemma 11. For every complete sequence µ 1

Corollary 1. If there is a finite set K ⊆ D such that the derivation problem for K has a solution, then the derivation problem for K has also a solution, where K is any fixed subset of D of 2 • |ϕ| elements.

Thus, henceforth we assume without any loss of generality that K is any fixed subset of D of 2 • |Ω p ϕ | elements.

B. A bound on the domain

Let us write MIN M(ϕ) for the set of mosaics of M(ϕ) that are minimal with respect to ≤ K . This set contains only one element (arbitrarily chosen) for every minimal class of equivalence of ≤ K .

Remark 2. Notice that if µ 1 K µ 2 then µ 1 K µ 2 for any µ 1 ≤ K µ 1 and µ 2 ≤ K µ 2 . Hence, we can restrict the domain of K to MIN M(ϕ) . That is, to mosaics that are minimal with respect to ≤ K .

Lemma 12. The number of elements of MIN M(ϕ) is double exponential in |ϕ|.

From the previous statements we obtain the following.

C. A bound on the relation

The lemmas above show that we have that the problem now reduces to find a complete small K sequence for a small K. In fact, we can test the relation K between any two elements in polynomial space.

We define the space of a mosaic µ that we denote it by |µ| as the space needed to write the multiset of all non-empty profiles of the mosaic. It is not hard to see that K can be in fact checked in polynomial space. Lemma 14. Given two K-compliant mosaics µ 1 , µ 2 , we can test µ 1 K µ 2 in space polynomial in |µ 1 | and |µ 2 |.

D. The algorithm

With all these ingredients we can now build the algorithm.

Finally, if i = 0, j = 1, by (2) we have that π 1 = aπ 2 and by condition by condition 2 of validity of µ 2 we have π 2 = aπ 2 + a. By idempotence, π 1 = aπ 2 + a = π 2 .

Proof of Claim 1: The only thing that changes between µ i-1 and µ i (or between µ 3 and µ 1 ) is that e i-1 is perhaps no longer reachable by some α ∈ σ a1 . There is however always at least one data value (namely e i ) that can reach α. In fact there are always two data values that can reach α except, perhaps, in µ n , where e n may be the only (flexible) data value that can reach α.

So the only possibility to falsify the validity property 4 of a mosaic is that γ ϕ (a 1 ) demands that there exists at least two data values reachable by α, and that this is not true in µ n . Suppose ad absurdum that α is accessible by only one data value in µ n . First, note that α is accessible by at least two data values in µ 1 , namely d 1 and d for some d = d 1 . If only d 1 could access α, then d 1 would be a rigid value, contradicting our assumption.

If µ 1 (d ) = (ρ 1 , a 1 π 1 + a 1 ) then d must be rigid (because d 1 is the only flexible value with that profile), and µ n (d ) = (ρ 1 , a 1 π 1 + a 1 ) and in this case there are two data values (e n and d ) that can access α.

If µ 1 (d ) = (ρ 1 , a 1 π 1 +a 1 ) then there is a data value d such that µ 3 (d ) = µ 1 (d ) by definition of µ 1 ≤ K µ 3 where, of course, d ∈ {d 3 , e 1 , . . . , e n }. Since µ n and µ 3 coincide in the profiles of all data values except perhaps in {d 3 , e 1 , . . . , e n } we obtain that µ n (d ) = µ 3 (d ) = µ 1 (d ). Hence, there are two data values (namely e n and d ) that can access α at µ n .

The properties 1, 2, and 3 of validity are immediate to check. Finally, we prove by a similar argument that all µ i are K-compliant. Suppose ad absurdum that there is α ∈ Ω p ϕ accessible only by one value that is flexible in µ i . Then it must be a data value from {e 1 , . . . , e n } since the other values do not change of profile with respect to µ 3 , which is K-compliant. Further, it must be at µ n since otherwise α can be accessed both by e n-1 and e n . As we already showed, if α is accessible by only one data value in µ n then it is also accessible by only one data value in µ 1 and it is then rigid, by K-compliance of µ 1 , which is in contradiction with our hypothesis.

Proof of Claim 3:

be a flexible data value from D 1 with µ 3 (d) = (ρ, π) (there must exist by ≤ K ). We define ξ(d) = d 2 , and for every other d ∈ D 1 \ {d} with the same profile we define ξ(d ) = d for some d ∈ D 2 (where there exists at least one element), again making sure that ξ is surjective onto D 2 . We can see that ξ satisfies conditions 3, 4, and 2 . (condition 1 . is trivially satisfied).

Proof of Claim 5: Note that condition 1 of ≤ K is immediate by definition of µ 4 . We now check condition 2. Let d ∈ K. Then we have that µ

To check condition 4, first consider the profile (a 2 ρ 1 , π 1 ). µ -1 2 (a 2 ρ 1 , π 1 ) contains d 1 , perhaps some rigid data values, and perhaps some flexible data values d (with µ 1 (d) = µ 1 (d 1 ), since condition A does not hold). We know that µ -1 4 (a 2 ρ 1 , π 1 ) contains d 3 , e 1 , . . . , e n . So both sets contain at least one element. We show that for every data value in

By ξ, we have that for every data value

, and that condition 4 holds. We thus have that µ 4 ≥ K µ 2 .

Continuation of the Proof of Lemma 7 (monotonicity):

Complex situation 2. Now, suppose that neither condition A nor B hold. Then we can generate µ 1 , . . . , µ n just as before, but now our problem is that from µ n we cannot generate µ 4 as before since condition B fails. Let us call

These are the data values that can only be simulated by d 2 (otherwise B would hold). Notice that d 2 is necessarily flexible by the negation of condition B, and that R is non-empty by µ 1 ≤ K µ 3 . We will also be using the data values P and mosaic µ i 's as defined for the first complex situation. Observe that if d 1 = d 2 , then {d 3 } ∪ P = R, and otherwise ({d

The strategy we will take is similar as the previous one, we will create intermediary mosaics µ 1 , . . . , µ m , but this time with a 2 as letter, to obtain

Each of the data values e i of R will change its profile first from (ρ 2 , a 1 π 2 ) = µ n (e i ) to (a 2 ρ 2 , π 2 ) = µ 1 (e i ), and then to

The only exception is the case of e 1 , that will only change once its profile, directly to (a 2 ρ 2 + a 2 , π 2 ) in µ 1 . Consider a simulating function ξ : D 1 → D 2 with D 1 = D\{d 3 , e 1 , . . . , e n , e 1 , . . . , e m }, D 2 = D\{d 1 , d 2 } between µ 3 and µ 1 . It is easy to verify that it must exist.

Claim 7. There exists a partial simulating function ξ : D 1 → D 2 between µ 3 and µ 1 .

ξ is also a partial simulating function between µ n and µ 1 because it only simulates data values whose profiles were not changed with respect to µ 3 . We build µ 1 , . . . , µ m where each µ i

• has letter a 2 and data value e i • e 1 , . . . , e i have profile (a 2 ρ 2 + a 2 , π 2 ) • e i+1 , . . . , e m have profile (a 2 ρ 2 , π 2 ) • all data value from ({d 3 } ∪ P ) \ R (if any) have profile (a 2 ρ 1 , π 1 ), • any other data value d ∈ D 1 has profile µ 2 (ξ(d)). Finally, the role of µ 4 is played by µ m . As before, we must verify that everything closes.

To check condition 4, first we proceed as in the proof of Claim 5 to show that |µ -1

Indeed, for d 2 we have d 4 and for any other data value d ∈ µ -1 4 (a 2 ρ 2 + a 2 , π 2 ) we can take any data value from ξ -1(d), which has the same profile. Moreover,

Observe that all data values from D \ D 1 have one of the two µ 4 -profiles we have just treated. Then, for any other mosaic (ρ, π) we know that all its data values are simulated by data values of µ 2 , and we can then easily prove that

Then we conclude that condition 4 of µ 2 ≤ K µ 4 holds.

Claim 9. µ n µ 1 .

Proof: For simplicity of notation let us call e 0 = d 3 . Suppose first that d 2 = d 1 , and hence that ({e 0 } ∪ P ) ∩ R = ∅, as already pointed out. Take any e i . If i = n, then µ n (e i ) = (ρ 1 , a 1 π 1 ) and µ 1 (e i ) = (a 2 ρ 1 , π 1 ), which verifies m(a 1 , 0, (ρ 1 , a 1 π 1 ), a 2 , 0, (a 2 ρ 1 , π 1 )).

The pathological case is when d 2 = d 1 . As we already remarked, in this situation we have {e 0 } ∪ P = R. Also, we have ρ 2 = ρ 1 and π 2 = π 1 . Then take any data value e i = e j . If i = n and j = 1, µ n (e i ) = (ρ 1 , a 1 π 1 ) and µ 1 (e i ) = µ 1 (e j ) = (a 2 ρ 2 , π 2 ) = (a 2 ρ 1 , π 1 ); it is immediate to verify that m(a 1 , 0, (ρ 1 , a 1 π 1 ), a 2 , 0, (a 2 ρ 1 , π 1 )) holds true. If i = n and j = 1, µ n (e i ) = (ρ 1 , a 1 π 1 + a 1 ) and µ 1 (e i ) = (a 2 ρ 1 , π 1 ), and hence m(a 1 , 1, (ρ 1 , a 1 π 1 + a 1 ), a 2 , 0, (a 2 ρ 1 , π 1 )). If i = n and j = 1, µ n (e i ) = (ρ 1 , a 1 π 1 ), µ 1 (e i ) = (a 2 ρ 2 +a 2 , π 2 ) = (a 2 ρ 1 +a 2 , π 1 ), which verifies m(a 1 , 0, (ρ 1 , a 1 π 1 ), a 2 , 1, (a 2 ρ 1 + a 2 , π 1 )). Finally, if i = n and j = 1, µ n (e i ) = (ρ 1 , a 1 π 1 + a 1 ), µ 1 (e i ) = (a 2 ρ 1 + a 2 , π 1 ) which trivially verifies m(a 1 , 1, (ρ 1 , a 1 π 1 + a 1 ), a 2 , 1, (a 2 ρ 1 + a 2 , π 1 )). Claim 10. For every i ∈ [m -1], µ i µ i+1 .

Proof: Since µ i and µ i+1 have the same letter, it is immediate that the preservation of the profile for every data value other then those of R is compatible with the definition of m. In other words, that m(a 2 , 0, µ i (d), a 2 , 0, µ i+1 (d)) for every d ∈ R, since µ i (d) = µ i+1 (d). For e i+1 we have to verify m(a 2 , 0, (a 2 ρ 2 , π 2 ), a 2 , 1, (a 2 ρ 2 + a 2 , π 2 )) which is true by ( 7) and (11). For e i we verify m(a 2 , 1, (a 2 ρ 2 + a 2 , π 2 ), a 2 , 0, (a 2 ρ 2 + a 2 , π 2 )). Notice that in this case, (4) is verified since π 2 of the form π 2 = a 2 π + a 2 , and then we have that π 2 + a 2 = π 2 by idempotence of +a 2 and (8) is trivially verified. Finally, for e j with j < i or j > i + 1, we can apply (5) and (9) since they preserve the profile. Claim 11. For all i ∈ [n], µ i is valid and K-compliant.

Proof: This proof is completely equivalent and symmetrical to the proof of Claim 1. There, it was showed that µ 1 , . . . , µ n are valid and K-compliant from the fact that µ 3 is valid and K-compliant. The same argument works to show that µ m-1 , . . . , µ 1 are valid and K-compliant from the fact that µ m is valid and K-compliant. Observe that µ m is valid an K-compliant by Lemma 5 since µ m ≥ K µ 2 .

Complex situation 3. Finally, if condition A hold true, it is the same procedure as before with P = ∅.

Proof of Claim 6: By definition of ≤ K we have that µ 1 and µ 2 verify the properties 1, 2 and 3 of ≤ K , but not necessarily 4. However, we still conserve the following property. For every profile (ρ, π),

because this property must coincide with the mosaic µ 3 verifying |µ -1 3 (ρ, π) \ K| = 0. This is a consequence of the property 4 of µ 3 ≤ K µ 1 and µ 3 ≤ K µ 2 .

We define ν = (a, d,

, where a and d are the label and data value of µ 1 (the label is also equal to that of µ 2 ). Consider the mosaic µ 2 which is the result of renaming some data values of µ 2 in such a way that it has the same data value d as µ 1 , and the only data values shared between µ 2 and µ 1 are a subset of K ∪ {d}. We then define

Observe that this definition preserves all the profiles of the rigid values and of the data value d. Further, for every profile (ρ, π) both the flexible data values of µ -1 1 (ρ, π) and of (µ 2 ) -1 (ρ, π) are subsets of those of ν -1 (ρ, π). This, combined with the property (12) ensures that the condition 4 of the definition of of ≤ K holds both for µ 1 and µ 2 , and we hence have ν ≥ K µ 1 , ν ≥ K µ 2 . Since µ 2 and µ 2 are equal modulo renaming of data values from D \ K, by definition of ≤ K we obtain ν ≥ K µ 2 , and we conclude the proof. APPENDIX TO SECTION V Proof of Lemma 12: Notice that, by definition of ≤ K , we need count the following We then obtain that there are not more than

In fact, |A| can be considered to be polynomial in |ϕ|, since otherwise we can replace all letters not appearing in ϕ by a single one '⊥'. Hence the number of minimal elements of M(ϕ) with respect to ≤ K is double exponential in |ϕ|.

Proof of Lemma 13: Let μi be a mosaic such that μi ≤ K µ i and μi ∈ MIN M(ϕ) for all 1 ≤ i ≤ n (it always exist). Then we have that

Further, the sequence is complete, because ≤ K preserves the left/right completeness of a mosaic by Lemma 5. If there are two indices i < j such that μi = μj , then we can remove all the mosaics between them obtaining still a complete K sequence with the aforementioned properties. We can repeat this procedure until we obtain a K sequence where all the elements are different. Hence, the sequence is bounded by |MIN M(ϕ) |.

A. Proof of Lemma 14

To prove Lemma 14, we first need to be able to compute K . The following lemma shows how to compute such relation.

Proof of Lemma 17: (if) Suppose we have two mosaics µ 1 and µ 2 that verify the conditions imposed by the Lemma through a witnessing bijection f :

where µ -1 1 (ρ 1 , π 1 ) contains at least one flexible data value e by condition 2b. We then define µ

where µ -1 2 (ρ 2 , π 2 ) contains at least one flexible data value e by condition 2c. We then define µ

µ 2 . Note that by Lemma 5 we will obtain that µ 1 and µ 2 are also valid and K-compliant.

µ 1 ≥ K µ 1 . The conditions 1, 2 of ≤ K are easily verified by construction of µ 1 . Condition 3 also holds since because d 1 = d 1 and because µ 1 (d 1 ) = ∅ it is defined by conditions (iii) or (iv) in which µ 1 (d 1 ) = µ 1 (d 1 ). To check that condition 4 is verified, take any profile (ρ, π). First note that

Further, if µ -1 1 (ρ, π) has no flexible values, this means that condition 2b of the Lemma is never true for the profile (ρ, π). Note that the only possible step in the construction where µ 1 is defined to be something else than the same profile as in µ 1 is in step ii, but this step is never reached with the profile (ρ, π) since it needs 2b to hold true. Then, we have 14) Hence, by ( 13) and ( 14), condition 4 of ≤ K is met and we have µ 1 ≥ K µ 1 .

µ 2 ≥ K µ 2 . The conditions 1, 2 of ≤ K are easily verified by construction of µ 2 . If d 2 ∈ K, condition 3 is also easily verified. If d 2 ∈ K, we have by construction that d 2 = f -1 (d 2 ). We need to show that µ 2 (d 2 ) = µ 2 (f -1 (d 2 )). For f -1 (d 2 ) condition (i) cannot be true, since it cannot be true that µ 2 (f (f -1 (d 2 ))) = µ 2 (d 2 ) = (∅, ∅) by definition of mosaic. Condition (iii) cannot either be true for the same reason. Then, µ 2 (f -1 (d 2 )) has to be built according to condition (ii) or (iv), which define

Then, condition 3 of µ 2 ≥ K µ 2 holds. To check that condition 4 is verified, take any profile (ρ, π). First note that

Further, if µ -1 2 (ρ, π) has no flexible values, this means that condition 2c of the Lemma is never true for the profile (ρ, π). As before the only possible step in the construction where µ 2 (d) is defined to be something different to µ 2 ( f (d)) is in step (iii), but this step is never reached with the profile (ρ, π) since it needs 2c to hold true. Then, we have

we proceed in a similar way. By step (iv) of the construction we have that µ (only if) If we have two mosaics µ 1 K µ 2 then there must exist µ 1 ≤ K µ 1 µ 2 ≥ K µ 2 . By µ 1 ≤ K µ 1 there is a bijection of data values f 1 : D \ K → D \ K that sends each data value of µ 1 with non-empty profile to a data value in µ 2 with the same profile. Similarly we have a bijection f 2 that relates the data values between µ 2 and µ 2 . We can then define f = f 1 • f -1 2 and it is easy to check that it verifies all the conditions defined in the Lemma.

Proof of Lemma 14: By Lemma 17, we only need to test the conditions specified there. We disregard the space needed to encode the data values, because we can always abstract them away in classes of equivalence. The algorithm simply needs to first guess a bijection f only restricted to the data values of µ 1 and µ 2 that have non-empty profiles. That is, we are only interested in pairs of data values (d, d ) such that µ 1 (d) = ∅ or µ 2 (f (d)) = ∅. Then, this bijection f needs only polynomial space. Then, we verify the conditions for each data value in the bijection, each condition taking polynomial space to test.

Proof of Lemma 11: Consider any complete sequence µ 1

• • • µ n over M(ϕ). Consider also a pair of functions f l , f r : D → ℘(Ω p ϕ ) that assign to each data value a set of path expressions such that the following holds for every d ∈ D

We claim that for every two data values d = d , f l (d) ∩ f l (d ) = ∅, and f r (d) ∩ f r (d ) = ∅. By way of contradiction, suppose that α ∈ f l (d)∩f l (d ), and assume that the witnessing positions for this membership are i and i . Suppose that i ≤ i without any loss of generality. This means that from position i we can access the data value d by going to the left through a path expression α. Since we can reach it from i we can also reach it from i , since i ≤ i . Then we can reach both d and d form i , which is in contradiction with i being the witnessing position for α ∈ f l (d ).

Then, there are not more than |Ω p ϕ | data values d such that f l (d) = ∅, and likewise for f r . We can build K by collecting these data values, and we will have that |K| ≤ 2 • |Ω p ϕ |.

Proof of Proposition 3: For simplicity we build a NEXPSPACE algorithm. Since NEXPSPACE = EXPSPACE (Savitch's Theorem) this proves the proposition. The algorithm tries to build progressively a complete sequence µ 1 K • • • K µ m such that µ i ∈ MIN M(ϕ) for every i and µ 1 ϕ 1 . It answers 'yes' iff there is such a sequence. By Lemma 13 we know that if there is some complete K sequence then there is one over minimal elements of size bounded by |MIN M(ϕ) |. The algorithm will count the length of the sequence it is building. Once the counter reaches |MIN M(ϕ) | it fails, answering that there is no complete sequence.

The algorithms maintains two variables:

• one counter c to count from 1 up to |MIN M(ϕ) |, and

• the last mosaic it has treated µ. Both variables require exponential space by Lemma 12. In the first step it initializes the counter c = 1, and the variable µ with a mosaic from MIN M(ϕ) that it guesses. Next, it checks that it is left-complete and that verifies ϕ 1 (otherwise it answers 'no'). Then it enters in a loop. At each step it checks if µ is complete to the right. If it is right-complete, it answers 'yes'. Otherwise it performs the following actions.

• If c < |MIN M(ϕ) | it increments c by one, otherwise it answers 'no'. • It guesses a mosaic µ ∈ MIN M(ϕ) ,

• It checks that µ K µ using exponential space by Lemma 14. If it does not hold it answers'no'.

• Finally, it overwrites µ with µ . If there is a complete sequence as the one described in Lemma 13, it will first guess µ 1 , then µ 2 up to µ m and it will answer 'yes'. If there is no complete sequence, it will answer 'no' because for every possible guessed sequence µ 1 • • • µ m either

• µ 1 is not left-complete, or

• µ 1 ϕ 1 , or • µ m is not right-complete • there is some µ i and µ i+1 that are not in the K relation, or

In each one of these cases the algorithm answers 'no'.