Michel Couprie

David Coeurjolly

Rita Zrour

Discrete bisector function and Euclidean skeleton in 2D and 3D

Keywords: Bisector function, skeleton, Euclidean distance transform, Voronoi diagram, digital topology

published or not. The documents may come

Discrete bisector function and Euclidean skeleton in 2D

and 3D

Introduction

The notion of skeleton, or medial axis, plays a major role in shape analysis. It has been introduced by Blum [START_REF] Blum | A transformation for extracting new descriptors of shape[END_REF] and is the subject of an abundant literature, which deals with both metrical and topological aspects, and rests on different approaches, in particular discrete geometry [START_REF] Borgefors | The Euclidean distance transform: finding the local maxima and reconstructing the shape[END_REF][START_REF] Ge | On the generation of skeletons from discrete Euclidean distance maps[END_REF][START_REF] Malandain | Euclidean Skeletons[END_REF][START_REF] Rémy | Exact Medial Axis with Euclidean Distance[END_REF], digital topology [START_REF] Davies | Thinning algorithms: a critique and a new methodology[END_REF][START_REF] Kong | Digital topology: introduction and survey[END_REF][START_REF] Lam | Thinning methodologies -a comprehensive survey[END_REF], mathematical morphology [START_REF] Talbot | Euclidean skeletons and conditional bisectors[END_REF][START_REF] Vincent | Efficient Computation of Various Types of Skeletons[END_REF], computational geometry [START_REF] Attali | Delaunay Conforming Iso-surface, Skeleton Extraction and Noise Removal[END_REF][START_REF] Attali | Modelling noise for a better simplification of skeletons[END_REF], and partial differential equations [START_REF] Siddiqi | The Hamilton-Jacobi Skeleton[END_REF]. In this paper, we focus on skeletons in the discrete grid Z 2 or Z 3 , which are centered in the shape with respect to the Euclidean distance, and which have the same topology as the original shape.

Email addresses: m.couprie@esiee.fr (Michel Couprie), david.coeurjolly@liris.cnrs.fr (David Coeurjolly), zrour@llaic3.u-clermont1.fr (Rita Zrour). Introduced by Meyer [START_REF] Meyer | Cytologie quantitative et morphologie mathématique[END_REF], and further studied by Talbot and Vincent [START_REF] Talbot | Euclidean skeletons and conditional bisectors[END_REF], the bisector function can play an important role in analyzing and filtering skeletons [START_REF] Attali | Delaunay Conforming Iso-surface, Skeleton Extraction and Noise Removal[END_REF][START_REF] Attali | Modelling noise for a better simplification of skeletons[END_REF][START_REF] Malandain | Euclidean Skeletons[END_REF]. Informally, the bisector function associates to each object point x the maximal angle formed by x (as the vertex) and the points of the background which are nearest to x (see Fig. 1). Until now, the algorithms proposed to compute the bisector function in Z 2 were based on the use of vectors produced by distance transformation algorithms (e.g., [START_REF] Danielsson | Euclidean distance mapping[END_REF]). To each object point, with such algorithms, only one vector indicates the location of a closest background point, and some other points at the same distance may be ignored.

The medial axis of an object X is composed by the centers of the balls which are included in X but which are not included in any other ball included in X. This set of points is, by nature, centered in the object with respect to the distance which is used to define the notion of ball. In discrete spaces, the medial axis has not, in general, the same topology as the original object. The use of guided and constrained discrete homotopic transformations has been proposed by several authors to obtain an homotopic skeleton which contains the medial axis (see [START_REF] Davies | Thinning algorithms: a critique and a new methodology[END_REF] which is, to our best knowledge, the first paper presenting this approach). Among them, Talbot and Vincent [START_REF] Talbot | Euclidean skeletons and conditional bisectors[END_REF] propose an algorithm for the 2D case which guarantees that the skeleton branches follow lines of steepest slope of the Euclidean distance map of the object, a property which is verified in the continuous framework. This algorithm cannot be straightforwadly extended to the 3D case. This paper contains two original contributions. First, we propose a new definition and an algorithm to compute a discrete bisector function in 2D or 3D spaces. This algorithm is based on an optimal procedure for building a complete discrete Voronoi diagram of a shape. Second, we introduce a new thinning method which produces homotopic discrete Euclidean skeletons. Unlike previously proposed approaches, this method is also valid in 3D.

Using these two original algorithms, we propose an integrated skeletonization method for objects in Z 2 and Z 3 which is based on exact discrete metrical and topological transformations, allows the filtering of the skeleton under the control of two parameters, and is computationnaly efficient.

Basic notions

In this section, we recall some basic metrical and topological notions for binary images [START_REF] Chassery | Géométrie discrète[END_REF][START_REF] Kong | Digital topology: introduction and survey[END_REF]. For the sake of simplicity, we limit this presentation to the 2D case.

We denote by Z the set of integers, by N the set of nonnegative integers, and by N * the set of strictly positive integers. We denote by E the discrete plane Z 2 . A point x in E is defined by (x 1 , x 2 ) with x i in Z. Let x, y ∈ E, we denote by d 2 (x, y) the square of the Euclidean distance between x and y, that is,

d 2 (x, y) = (x 1 -y 1 ) 2 + (x 2 -y 2 ) 2 . Let Y ⊂ E, we denote by d 2 (x, Y ) the square of the Euclidean distance between x and the set Y , that is, d 2 (x, Y ) = min{d 2 (x, y); y ∈ Y }. Let X ⊂ E (the "object"), we denote by D 2 X the map from E to N which associates, to each point x of E, the value D 2 X (x) = d 2 (x, X)
, where X denotes the complementary of X (the "background"). The map D 2 X is called the (squared Euclidean) distance map of X. Let x ∈ E, r ∈ N * , we denote by B r (x) the ball of (squared) radius r centered on x, defined by B r (x) = {y ∈ E, d 2 (x, y) < r}. Notice that, for any point x in X, the value D 2 X (x) is precisely the radius of a ball centered on x and included in X, which is not included in any other ball centered on x and included in X.

Let us recall the notion of medial axis (see also [START_REF] Rosenfeld | Digital Image processing[END_REF][START_REF] Talbot | Euclidean skeletons and conditional bisectors[END_REF]). Let X ⊆ E, x ∈ X, r ∈ N * . A ball B r (x) ⊆ X is maximal for X if it is not strictly included in any other ball included in X. The medial axis of X, denoted by MA(X), is the set of the centers of all the maximal balls for X (see Fig. 2d, see also Fig. 3). In the framework of mathematical morphology, an alternative definition of the medial axis in terms of openings has been introduced by Lantuejoul [START_REF] Soille | Morphological Image Analysis: Principles and Applications[END_REF].

Efficient algorithms have been proposed to compute exact squared Euclidean distance maps [START_REF] Saito | New algorithms for Euclidean distance transformation of an n-dimensional digitized picture with applications[END_REF][START_REF] Hirata | A unified linear-time algorithm for computing distance maps[END_REF][START_REF] Meijster | A general algorithm for computing distance transforms in linear time[END_REF], and also to extract the exact Euclidean medial axis of a shape, from an exact squared Euclidean distance map and using precomputed look-up tables [START_REF] Borgefors | The Euclidean distance transform: finding the local maxima and reconstructing the shape[END_REF][START_REF] Rémy | Exact Medial Axis with Euclidean Distance[END_REF]. An optimal, linear-time algorithm has been proposed by one of the authors to extract a subset of the medial axis which is sufficient to reconstruct the original shape [START_REF] Coeurjolly | d-Dimensional Reverse Euclidean Distance Transformation and Euclidean Medial Axis Extraction in Optimal Time[END_REF].

In discrete spaces, it is well known that the topology of the medial axis is generally not the same as the topology of the original object. In particular, if X is connected, MA(X) is generally not connected (see Fig. 2d). Let us now introduce some topological notions in Z 2 that we use in the sequel.

We consider the two adjacency relations Γ 4 and Γ 8 defined by, for each point x ∈ E:

Γ 4 (x) = {y ∈ E; |y 1 -x 1 | + |y 2 -x 2 | ≤ 1}, Γ 8 (x) = {y ∈ E; max(|y 1 -x 1 |, |y 2 -x 2 |) ≤ 1}.
In the following, we will denote by n a number such that n = 4 or n = 8. We define Γ

* n (x) = Γ n (x) \ {x}. The point y ∈ E is n-adjacent to x ∈ E if y ∈ Γ * n (x); it is n-adjacent to a subset X of E if it is n-adjacent to at least one point of X. An n-path is a sequence of points x 0 . . . x k with x i n-adjacent to x i-1 for i = 1 . . . k.
Let X be a nonempty subset of E. We say that two points x, y of X are n-connected in X if there is an n-path in X between these two points. This defines an equivalence relation. The equivalence classes for this relation are the n-connected components of X, or n-components in short. The set X is said to be n-connected if it consists of exactly one n-component. The set composed of all n-components of X which are n-adjacent to a point x is denoted by C n [x, X].

In order to have a correspondence between the topology of X and the topology of X, we have to consider two different kinds of adjacency for X and X [START_REF] Kong | Digital topology: introduction and survey[END_REF]: if we use the n-adjacency for X, we must use the n-adjacency for X, with (n, n) = [START_REF] Coeurjolly | d-Dimensional Reverse Euclidean Distance Transformation and Euclidean Medial Axis Extraction in Optimal Time[END_REF][START_REF] Bertrand | Simple points, topological numbers and geodesic neighborhoods in cubic grids[END_REF] or [START_REF] Bertrand | Simple points, topological numbers and geodesic neighborhoods in cubic grids[END_REF][START_REF] Coeurjolly | d-Dimensional Reverse Euclidean Distance Transformation and Euclidean Medial Axis Extraction in Optimal Time[END_REF]. In the sequel, we assume that the adjacency pair (n, n) = (8, 4) has been chosen and we do not write the subscripts n, n unless necessary; but the results also hold for (n, n) = (4, 8).

Informally, a simple point p of a discrete object X is a point which is "inessential" to the topology of X [START_REF] Rosenfeld | Connectivity in digital pictures[END_REF]. In other words, we can remove the point p from X without "changing the topology of X". The notion of simple point is fundamental to the definition of topology-preserving transformations in discrete spaces. We now give a definition and a local characterization of simple points in E = Z 2 . For the 3D case, see [START_REF] Bertrand | Simple points, topological numbers and geodesic neighborhoods in cubic grids[END_REF].

The point x ∈ X is simple (for X) if each n-component of X contains exactly one n-component of X \ {x} and if each n-component of X ∪ {x} contains exactly one n-component of X. Let X ⊆ E and x ∈ E, the two connectivity numbers [START_REF] Bertrand | Simple points, topological numbers and geodesic neighborhoods in cubic grids[END_REF] are defined as follows (#X stands for the cardinality of X):

T (x, X) = #C n [x, Γ * 8 (x) ∩ X]; T (x, X) = #C n [x, Γ * 8 (x) ∩ X].
The following property allows us to locally characterize simple points [START_REF] Kong | Digital topology: introduction and survey[END_REF][START_REF] Bertrand | Simple points, topological numbers and geodesic neighborhoods in cubic grids[END_REF], hence to implement efficiently topology preserving operators:

x ∈ E is simple for

X ⊆ E ⇔ T (x, X) = 1 and T (x, X) = 1.
Let X be any finite subset of E. The subset Y of E is an homotopic thinning of X if Y = X or if Y may be obtained from X by iterative deletion of simple points. We say that Y is an ultimate homotopic skeleton of X if Y is an homotopic thinning of X and if there is no simple point for Y . Let C be a subset of X. We say that Y is an ultimate homotopic skeleton of X constrained by C if C ⊆ Y , if Y is an homotopic thinning of X and if there is no simple point for Y in Y \ C (see e.g. [START_REF] Davies | Thinning algorithms: a critique and a new methodology[END_REF][START_REF] Vincent | Efficient Computation of Various Types of Skeletons[END_REF]). The set C is called the constraint set relative to this skeleton.

Complete discrete Voronoi mapping

In order to compute the bisector function, we need to know for each shape point x the set of background points which are at minimal distance from x. We propose in this section an optimal algorithm to compute these sets, based on the notion of Voronoi diagram.

Preliminaries

We first remind the definition of the Voronoi diagram in the continuous plane.

Given a set S = {s i } of points or sites in R 2 , the Voronoi diagram of S is a decomposition of the plane into a set of cells C = {c i } (one cell c i ⊂ R 2 per site s i ) such that for each point p in the (open) cell c i , we have d(p, s i ) < d(p, s j ) for any j = i. In other words, any p in c i is closer to the site s i than to any other site s j [START_REF] Preparata | Computational geometry : An Introduction[END_REF]. We also consider the closed cells defined by

c - i = {p ∈ R 2 ; d(p, s i ) ≤ d(p, s j )}.
The cell boundaries correspond to loci of points equidistant to two or more sites.

In the discrete plane, we can define a Voronoi labeling by assigning to each grid point the index of a Voronoi cell containing it. For grid points which are situated on the boundaries of the Voronoi diagram, the index of one of the neighboring cells is chosen arbitrarily. Based on this definition, algorithms can be designed to construct such a Voronoi labeling considering an errorfree Euclidean metric, see [START_REF] Coeurjolly | Algorithmique et géométrie discrète pour la caractérisation des courbes et des surfaces[END_REF][START_REF] Maurer | A Linear Time Algorithm for Computing Exact Euclidean Distance Transforms of Binary Images in Arbitrary Dimensions[END_REF][START_REF] Hesselink | Euclidean skeletons of 3D data sets in linear time by the integer medial axis transform[END_REF]. To summarize the contributions of these authors, the Voronoi labeling can be computed in linear time with respect to the number of grid points whatever the dimension of the image. However, the main drawback of these approaches lies in the arbitrary choices which are made for cell boundary points which coincide with discrete points, making the Voronoi labeling not unique.

To overcome this drawback, we propose to use the Voronoi mapping defined below (also called feature transform in [START_REF] Hesselink | Euclidean skeletons of 3D data sets in linear time by the integer medial axis transform[END_REF]) instead of the Voronoi labeling.

Let E be either R 2 or Z 2 , let S be a nonempty subset of E, and let x ∈ E. The projection of x on S, denoted by Π S (x), is the set of points y of S which are at minimal distance from x; more precisely, Π S (x) = {y ∈ S, ∀z ∈ S, d(y, x) ≤ d(z, x)}. For example in Fig. 3a, we have Π X (x) = {a, b} and Π X (y) = {c}, and in Fig. 3b, we have Π X (x) = {a} and Π X (y) = {b, c}.

We can see that a point p belongs to the closed cell c - i (using the above notations for the Voronoi diagram) if and only if the site s i belongs to the projection Π S (p). Hence, we call Voronoi mapping the map Π S which associates, to each point p of E, the set Π S (p). A subset X of the continuous plane (full ellipse, represented by its border) and its medial axis (horizontal line segment), a point x and its projection {a, b} on X, a point y and its projection {c}. Notice that y does not belong to the medial axis, since no ball centered on y and included in X is maximal for X (the ball with dashed contour contains them all). (b): A subset X of the discrete plane (represented by white dots), its complementary X (black dots) and the continuous Voronoi diagram associated to X (the gray lines represent the Voronoi boundaries). The projection of x (resp. y, z) on X is the set {a} (resp. {b, c}, {c}). See Sec. 4.1 for the use of p, q, e, and d.

A naive computation of the Voronoi mapping can be sketched as follows: first we construct the complete Euclidean Voronoi diagram using an algorithm from Computational Geometry [START_REF] Preparata | Computational geometry : An Introduction[END_REF] using points in X as sites. Then, we can digitize the Voronoi diagram to obtain the Voronoi mapping: for each point x ∈ X, we locate the closed cell c - i such that x ∈ c - i in order to define Π X (x). Although, this algorithm would not be optimal for this kind of data: if n is the number of points in X and n ′ the number of points in X, the overall computational cost would be O(n ′ log n ′ + n log n ′ ) (for the 2D case; things get worse in higher dimensions). Indeed, this algorithm does not take into account the specific regularity of the sets X and X.

In the next section, we sketch an optimal algorithm to compute the Voronoi mapping from an error-free Euclidean metric using specific features of the discrete grid.

Voronoi mapping computation

We modify the Voronoi labeling algorithm proposed in [START_REF] Hesselink | Euclidean skeletons of 3D data sets in linear time by the integer medial axis transform[END_REF] 1 . This algorithm is based on separable techniques to compute the exact squared Euclidean distance transform (SEDT) [START_REF] Saito | New algorithms for Euclidean distance transformation of an n-dimensional digitized picture with applications[END_REF][START_REF] Hirata | A unified linear-time algorithm for computing distance maps[END_REF][START_REF] Meijster | A general algorithm for computing distance transforms in linear time[END_REF], the reverse EDT or the medial axis [START_REF] Coeurjolly | d-Dimensional Reverse Euclidean Distance Transformation and Euclidean Medial Axis Extraction in Optimal Time[END_REF].

We first present here the SEDT algorithm in the 2D case: we consider a twodimensional binary image F = {f ij } in the form of a boolean array of width w and height h, and we set n = w × h. We denote by X the set {(i, j), f ij = 1} of "object" points. The output of the algorithm is a 2D image H = {h ij } storing the squared distance transform. The SEDT algorithm consists of the following steps.

(1) Build from the source image F a one-dimensional SEDT according to the first dimension (i-axis), denoted by G = {g ij }, where, for a given row j:

g ij = min (u,j)∈X {(i -u) 2 } . (1)
(2) Then, construct the image H = {h ij } with a j-axis process:

h ij = min v {g iv + (j -v) 2 , 1 ≤ v ≤ h} . (2)
To transform this SEDT algorithm in order to produce an error-free Voronoi labeling, we just have to mark one of the points in X that lead to the minimum distance [START_REF] Saito | New algorithms for Euclidean distance transformation of an n-dimensional digitized picture with applications[END_REF][START_REF] Meijster | A general algorithm for computing distance transforms in linear time[END_REF]. To maintain the complete list of projected points when #Π X (x) > 1, we propose a separable technique that constructs the error-free Voronoi mapping dimension after dimension.

First, we can easily modify the step 1 of the previous SEDT algorithm to associate to each point of x ∈ X, its projection according to the i-axis (i.e. the set of points of X on the same row as x which are at minimal distance from x). Since the step 1 of the SEDT algorithm requires O(n) computation steps, the 1D Voronoi mapping according to the i-axis can also be computed in O(n).

The second step can be viewed as a lower envelope computation of a set of parabolas in each column [START_REF] Saito | New algorithms for Euclidean distance transformation of an n-dimensional digitized picture with applications[END_REF][START_REF] Hirata | A unified linear-time algorithm for computing distance maps[END_REF][START_REF] Meijster | A general algorithm for computing distance transforms in linear time[END_REF] (see graphs on the right of Fig. 4). During this lower envelope computation, we can maintain the Voronoi mapping with the following observations related to the sweep line techniques to construct the (continuous) Voronoi diagram in computational geometry [START_REF] Berg | Computational Geometry[END_REF]. Let us consider the 1D Voronoi mapping Π computed after the step 1, and a point x ∈ X such that #Π(x) > 1 (i.e. x is on a boundary of the 1D Voronoi diagram):

(1) the Voronoi diagram boundary at x may disappear, in that case, the new projection of x may be reduced to one point ; (2) the Voronoi diagram boundary at x may be preserved, in that case the new projection of x contains the equidistant sites detected along the i-axis ; (3) new equidistant points in X can be detected when two parabolas of the lower envelope intersect in x. Hence, new points may be inserted in Π(x) (see Fig. 4).

We do not detail here the overall algorithm but the Voronoi mapping can computed in O(n ′ + m) where m = x∈X #Π X (x) and n ′ is the number of points of F which are not in X (background points). Since the size of the memory space needed to store the projection sets is in O(m), this algorithm is optimal both in space and time complexity. Furthermore, the experiments reported in Annex A show that m is usually close to the number of image object points, especially in 2D.

In three dimensions, we use the same decomposition as proposed to solve the SEDT problem: we just have to add a new lower envelope computation according to the third axis. The above observations are still valid and we also obtain an O(n ′ + m) algorithm to extract the Voronoi mapping (where n ′ and m are defined as above). The method extends to higher dimensions as well.

Bisector function

The bisector angle of a point x in X can be defined, in the continuous framework, as the maximal unsigned angle formed by x (as the vertex) and any two points in the projection of x on X [START_REF] Meyer | Cytologie quantitative et morphologie mathématique[END_REF][START_REF] Talbot | Euclidean skeletons and conditional bisectors[END_REF]. In particular, if #Π X (x) = 1, then the bisector angle of x is zero. For example in Fig. 3a, the bisector angle of x is θ, and the bisector angle of y is 0. The bisector function of X is the function which associates to each point x of X, its bisector angle in X. This very definition of the bisector function was used in [START_REF] Attali | Modelling noise for a better simplification of skeletons[END_REF] in order to provide a filtering criterion for skeletons based on Voronoi diagrams in the continuous plane. It has been also adapted to the discrete case in [START_REF] Talbot | Euclidean skeletons and conditional bisectors[END_REF][START_REF] Malandain | Euclidean Skeletons[END_REF]. The main drawback of the latter approaches is to use a non-unique Voronoi labeling in which only one site of the entire set of the equidistant sites is considered.

Extended projection

A direct extension of the above definition to the discrete case does not lead to a satisfactory notion of bisector function, in particular with respect to our goal of filtering the medial axis. Consider the set X in Fig. 3b, symbolized by the white dots. We can see that the point x of X belongs to the (discrete) medial axis of X, as defined in Sec. 2. The projection Π X (x) is {a}, thus the bisector angle of x according to the previous definition is zero. On the other hand, in the neighborhood of x there exists a (non-grid) point p on the Voronoi boundaries which has a bisector angle of π. In order to preserve this information, we would like that the value of the bisector angle associated with x be π rather than 0. Similarly, for the point y we would like to have a bisector angle greater than byc, due to the existence in the closed unit square centered on y, of a point q having a bisector angle equal to bqe. This informal discussion motivates the following definition of the extended projection and of the discrete bisector function.

Definition 1. Let X ⊂ E, and let x ∈ X. The extended projection of x on X, denoted by Π e X (x), is the union of the sets Π X (y), for all y in Γ 4 (x) such that d 2 (y, X) ≤ d 2 (x, X).

Let X ⊂ E, and let x ∈ X. The (discrete) bisector angle of x in X, denoted by θ X (x), is the maximal unsigned angle between the vectors → xy, → xz, for all y, z in Π e X (x). In particular, if #Π e X (x) = 1, then θ X (x) = 0. The (discrete) bisector function of X, denoted by θ X , is the function which associates to each point x of X, its discrete bisector angle in X.

With this definition, we can easily check that the bisector angle of the point x in Fig. 3b is equal to π; and that θ X (y) = bye, a value close to bqe.

Let us explain the role of the condition d 2 (y, X) ≤ d 2 (x, X) (1) in our definition of the extended projection. Consider the situation depicted in Fig. 5a, where a Voronoi boundary (bold line) separates the two object points x and y. A background point a (resp. b) in the projection of x (resp. y) is depicted. Observe that x is closer to X than y. Without condition (1), the extended projection of x would contain b and the extended projection of y would contain a. With condition (1), we have a ∈ Π e X (y) but b / ∈ Π e X (x). In other words, with condition (1) only y receives a high bisector angle value, while without condition (1) both x and y receive high bisector angle values. Fig. 5b and Fig. 5c show details of a bisector function computed without (1) and with (1) respectively, on the same object. For filtering purposes, Fig. 5c is clearly a better result.

Thanks to the algorithm presented in Sec. 3.2, the Voronoi mapping Π X can be computed in optimal time. For each object point x, we must then compute Π e X (x) using the adjacency relation Γ and the distance map D 2 X . The last step to obtain the bisector angle consists in the computation of the maximum unsigned angle between all the pairs of vectors { → xy, → xz} for all y, z in Π e X (x). If we denote by k the number of points in Π e X (x), the number of such pairs is quadratic with respect to k, more precisely, it is equal to k(k -1)/2. By normalizing all these vectors, we can easily see that the problem of finding a maximum angle reduces to the problem of finding a maximum diameter of a convex polygon in 2D. This last problem has been solved in 1978 by Shamos [START_REF] Shamos | Computational geometry[END_REF], who provided a simple linear-time algorithm (that is, in O(k)). In 3D, the problem is more complicated but some efficient algorithms (in O(k log k) or less) have been proposed for the maximal diameter of a set of points, see e.g. [START_REF] Malandain | Computing the diameter of a point set[END_REF]. However, in practice, the mean cardinal of the extended projections for a given shape is usually quite small. For example, it is close to 1.7 for the 2D object of Fig. 7, and close to 4.3 for the 3D object of Fig. 9. In Annex B, we show the distribution of #Π X (x) and #Π e X (x) for these objects. If we consider only the extended projection of medial axis points, the mean values are respectively of 2 and 4.5. Thus, the straightforward algorithm which considers all the pairs of points in the extended projection is the best choice in most cases. In Fig. 6, we show a set X together with its medial axis (a) and the discrete bisector function θ X (b). We illustrate the use of this function to eliminate spurious points of the medial axis: in (c), we show the points of the medial axis (in black) which have a bisector angle greater than 40 degrees. A zoomed detail of both axes is shown in (d). Notice that only the bisector angles of the medial axis points need to be computed for this application. Fig. 7 shows the bisector function of a more complex 2D shape. Let us analyse the differences between the Talbot's discrete bisector function [START_REF] Talbot | Analyse morphologique de fibres minérales d'isolation[END_REF] and ours. Let X ⊂ E, x ∈ X, and let V (x) denote a point arbitrarily chosen in Π X (x). We set B(x) = max{angle(

→ y 1 z 1 , → y 2 z 2 ), y 1 ∈ Γ 4 (x), y 2 ∈ Γ 4 (x), z 1 = V (y 1 ), z 2 = V (y 2 )} (notice that
the definition of Talbot is restricted to the points of the skeleton, and corresponds actually to B(x)/2). A first difference lies in the arbitrary choices done by the algorithm which finds a closest background point for each object point, formalized here by the notation V (x). In our case, all the points of Π X (x) are considered, thus no choice is done. Fig. 8 illustrates a second difference. Observe that depending on the contour orientation, (e.g., horizontal, vertical or diagonal) Talbot's bisector angles can be very different, even for points which are not located on the contour. On the other hand, our definition and algorithm provide a more homogeneous result, whatever the contour orientation (see also Fig. 7). This is due to the choice of considering the point x itself as the only vertex for all the angles which are considered to compute θ X (x). On the other hand, the definition of B(x) is based on angles with different vertices in Γ 4 (x).

The definition and computation of this discrete bisector function can be straightforwardly extended to Z 3 . To conclude this section, we present in Fig. 9 an illustration of the bisector function of a three-dimensional object (a vertebra).

(a 1 ) (b 1 ) (c 1 ) (a 2 ) (b 2 ) (c 2 ) (a 3 ) (b 3 ) (c 3 )

New distance-guided homotopic thinning algorithm

The skeletonization methods which are based on homotopic thinnings, in the sense of section 2, provide a formal guarantee that the skeleton and the original object have the same topology. The simplest such method consists in computing an ultimate homotopic skeleton of the object X constrained by the medial axis of X, that is, removing iteratively simple points from X which do not belong to MA(X), taking the distance map as a priority function in order to select first the points which are closest to the background. This can be done using the following procedure, with P = D X and Y = MA(X).

Procedure UltimateSkeleton (Input The drawback of this method has been well analyzed in [START_REF] Talbot | Euclidean skeletons and conditional bisectors[END_REF]. Roughly speaking the method does not guarantee that points of the homotopic skeleton outside the medial axis are "well centered" in the object; more precisely, such a point may have a null or quasi-null bisector angle.

X, P , Y , Output Z) 01. Z ← X 02. Q ← {(P (x), x); where x is any point of X \ Y } 03. While Q = ∅ Do 04. choose (p, x) in Q such that p is minimal; Q ← Q \ {(p, x)} 05. If x is simple for Z Then 06. Z ← Z \ {x} 07. Q ← Q ∪ {(P (y), y); where y ∈ Γ(x) ∩ (Z \ Y )} (a) (b) (c) (d)
Let us consider the object X in Fig. 10a, and the constraint set Y in Fig. 10c, which consists of the four corner points of the shape. The result of UltimateSkeleton(X, D X , Y ) is depicted in Fig. 10d. The isolines of the distance map D X and the bisector function of X are depicted in Fig. 10b,e respectively, for comparison.

To understand what happens, let us concentrate on a detail of the above example, depicted in Fig. 11. The numbers correspond to the distance map values. The circled point with value 1 is one of the points belonging to the constraint set Y . Suppose that all the points with a value below 8 have been processed by the homotopic thinning algorithm. At this step, the points in gray are still in X, as well as the two circled points (the point at 1 because it belongs to Y , and the one at 4 because it is not a simple point). All other points are not in X. Obviously, the point v at 8 adjacent to z at 4 will be selected before its neighbor w at 9, and since it will be a simple point at this stage, it will be deleted. Such a behaviour will be reproduced at later stages, generating a diagonal branch of the skeleton, and is in contradiction with a property of the skeleton in the continuous framework: informally, skeleton branches follow lines of steepest slope of the Euclidean distance map. Let us compute the slopes of zv and zw in our example: ( √ 8 -√ 4)/1 ≈ 0.83, and ( √ 9 -√ 4)/ √ 2 ≈ 0.71. Thus, the point v should be kept in the skeleton and the point w deleted according to this criterion.

(a) (b) (c) (d) (e) (f)
In [START_REF] Talbot | Euclidean skeletons and conditional bisectors[END_REF], Talbot and Vincent propose the following strategy to cope with this problem. During the thinning process guided by the distance map, having detected a point x which belongs to the skeleton (either a point of the constraint set or a non-simple point), the neighbor of x which corresponds to the steepest ascending slope is dynamically added to the constraint set. Although this method gives satisfactory results in 2D, it cannot be extended to the 3D case.

We propose another strategy which gives equivalent results in 2D and which also applies to the 3D case. The idea is to define a priority function which takes into account both the distance map and an auxiliary function defined in the neighborhood of each dynamically detected skeleton point. Let x be such a point, then to any neighbor y of x which is still in X and not in the constraint set Y , we associate the value p y = D X (x) + (D X (y) -D X (x))/d(x, y), with D X (x) = D 2 X (x). The new priority function, for the point y, is defined as min(p y , D X (y)). We see that (D X (y) -D X (x))/d(x, y) is the slope of xy, thus the neighbors of x will be examined in increasing order of slope, since the value p y is always less or equal to the corresponding distance value D X (y) (for all x, y in Z 2 or Z 3 with x = y, we have d(x, y) ≥ 1).

For example, in above situation, we have

D X (v) = √ 8 ≈ 2.83, D X (w) = 3, p v = √ 4 + ( √ 8 - √ 4)/1 = √ 8 and p w = √ 4 + ( √ 9 - √ 4)/ √ 2 ≈ 2
.71; thus the point w will be selected before v with this strategy. Our algorithm is given below.

Procedure EuclideanSkeleton

(Input X, D X , Y , Output Z) 01. Z ← X 02. Q ← {(D X (x), x); where x is any point of X \ Y } 03. R ← {(p x , x); where x is any point of X \ Y adjacent to Y , 04.
and where

p x = min{D X (z) + (D X (x) -D X (z))/d(x, z), z ∈ Y } } 05. While Q = ∅ Or R = ∅ Do 06. choose (p, x) in Q ∪ R such that p is minimal 07. Q ← Q \ {(p, x)}; R ← R \ {(p, x)} 08. If x ∈ Z \ Y Then 09.
If x is simple for Z Then 10.

Z ← Z \ {x} 11.

Else 12.

Y ← Y ∪ {x} 13.

R ← R ∪ {(p y , y); where y ∈ Γ(x) ∩ (Z \ Y ) 14.

and where p y = D X (x) + (D X (y) -D X (x))/d(x, y)}

In Fig. 10f, we see the result of this algorithm applied to the preceding example. Compare the shape of this skeleton with the distance map and with the bisector function of X depicted in 10b,e respectively. Note that, depending on the choice of the couple (p, x) in the case of equal priorities (line 6), different results may be obtained. The complexity of this algorithm depends on the data structure used to represent the sets Q and R. To be more precise, this data structure must allow to perform the choice in line 6 efficiently, and also the insertions in lines 12 and 13. Using for example balanced binary trees [START_REF] Cormen | Introduction to algorithms[END_REF], the overall complexity of the algorithm is in O(n log n), where n is the number of image points.

6 Filtered Euclidean skeletons in 2D and 3D

In [START_REF] Attali | Modelling noise for a better simplification of skeletons[END_REF], Attali and Montanvert show that an efficient filtering of a skeleton can be performed by removing two kinds of medial axis points: those which correspond to maximal balls of small radius, and those which have a small bisector angle (see also [START_REF] Attali | Delaunay Conforming Iso-surface, Skeleton Extraction and Noise Removal[END_REF]).

Based on the methods described in the previous sections, we propose a parametrized filtered Euclidean skeleton procedure which has the following qualities:

-flexible (it allows the removal of unwanted skeleton parts under the control of two parameters), -general (it applies to 2D and 3D objects with arbitrary topology), -based on well-defined notions (distance transform, medial axis and discrete bisector function), -topologically sound (topology preservation is guaranteed by the use of homotopic transformations), -efficient in terms of processing speed.

Procedure FilteredSkeleton

(Input X, r, α, Output Z) 01. D 2 X ← SEDT(X) 02. M ← MedialAxis(X, D 2 X ) 03. Z ← EuclideanSkeleton(X, D 2 X , M ) 04. θ X ← DiscreteBisector(X, M ) 05. Y ← {x ∈ M ; D 2 X (x) ≥ r 2 and θ X (x) ≥ α} 06. Z ← UltimateSkeleton(Z, D 2 X , Y )
The exact squared Euclidean distance transform (SEDT) may be computed in linear time, both in 2D and 3D, see [START_REF] Saito | New algorithms for Euclidean distance transformation of an n-dimensional digitized picture with applications[END_REF][START_REF] Hirata | A unified linear-time algorithm for computing distance maps[END_REF][START_REF] Meijster | A general algorithm for computing distance transforms in linear time[END_REF] and Sec. 3.2. It only has to be computed once and is used by procedures MedialAxis, EuclideanSkeleton and UltimateSkeleton. Procedure MedialAxis can be efficiently implemented in 2D and 3D thanks to the method of Coeurjolly [START_REF] Coeurjolly | d-Dimensional Reverse Euclidean Distance Transformation and Euclidean Medial Axis Extraction in Optimal Time[END_REF] or the one of Rémy and Thiel [START_REF] Rémy | Exact Medial Axis with Euclidean Distance[END_REF]. The computation of the discrete bisector function and the Euclidean skeleton are described in sections 4 and 5, respectively. The bisector function θ X need only to be computed on points of the medial axis.

Fig. 12 illustrates the FilteredSkeleton procedure in 3D. The original object (a full ellipsoid, depicted as transparent in the three views) is connected, has no cavity and no tunnel. Besides, its medial axis (a) has several small isolated components. The Euclidean skeleton has exactly the same topology as the original image, thus we can verify on b that the result is connected. A filtered skeleton is shown in c.

From any superset S of the exact medial axis of a shape X and the values D 2 X (s) for any s ∈ S, it is possible to reconstruct exactly the set X. More precisely, X is equal to the union of all the balls B Rs (s), with s ∈ S and Rs = D 2 X (s). A Linear algorithm to perform this reconstruction has been recently proposed by Coeurjolly [START_REF] Coeurjolly | d-Dimensional Reverse Euclidean Distance Transformation and Euclidean Medial Axis Extraction in Optimal Time[END_REF]. If the set S does not contain the medial axis, the reconstruction may be incomplete, that is, it may produce only a strict subset of X.

Fig. 13 illustrates the FilteredSkeleton procedure in 2D. Notice that, by construction, we have the guarantee that all the filtered skeletons are included in the non-filtered skeleton, this is indeed the reason why we use two separate homotopic thinning steps (lines 3 and 6).

The images (a', b', c', d') show the sets which have been reconstructed from the corresponding skeletons; notice that (a') is equal to the original shape. Fig. 14 illustrates the FilteredSkeleton procedure on a "real world" 3D image (the vertebra of Fig. 9) which is connected, has no cavity and has only one tunnel. Its medial axis has several small isolated components and small tunnels (see b and the upper part of d). Again, we can verify on c and the lower part of d that the small tunnels have disappeared and that the result is connected. In e, we can judge the effectiveness of the filtering on this particular object.

Conclusion

We introduced a new definition and an algorithm for the discrete bisector function, and proposed a thinning algorithm based on a new priority ordering, which produces homotopic discrete Euclidean skeletons. Both constitute significant improvements with respect to previous approaches, and apply to the 2D and 3D cases. Using these two original algorithms, together with methods for computing exact squared Euclidean distance transform and exact Euclidean medial axis, we proposed a skeletonisation method which is flexible (with two parameters for filtering), general (for 2D and 3D), exact, and ef- Annex A Let X be a set of points (i.e., a binary image) and n = #X be the number of points in X. We write m = x∈X #Π X (x). The number m corresponds to the amount of memory which is necessary to store the projections of all the points of X. In Fig. 15, we plot the value of m with respect to n, for different families of binary images.

Fig. 1 .

 1 Fig. 1. Illustration of the bisector function θ. In this example, θ(x) is the angle α, and θ(y) is the angle β.

Fig. 2 .

 2 Fig. 2. (a): a set X (in white); (b): an homotopic thinning of X; (c): ultimate homotopic skeleton of X; (d): medial axis of X, computed by the algorithm of [25]; (e): ultimate homotopic skeleton of X constrained by the medial axis of X. In (b,c,d,e) the original set X appears in gray for comparison.

Fig. 3 .

 3 Fig. 3. (a):A subset X of the continuous plane (full ellipse, represented by its border) and its medial axis (horizontal line segment), a point x and its projection {a, b} on X, a point y and its projection {c}. Notice that y does not belong to the medial axis, since no ball centered on y and included in X is maximal for X (the ball with dashed contour contains them all). (b): A subset X of the discrete plane (represented by white dots), its complementary X (black dots) and the continuous Voronoi diagram associated to X (the gray lines represent the Voronoi boundaries). The projection of x (resp. y, z) on X is the set {a} (resp. {b, c}, {c}). See Sec. 4.1 for the use of p, q, e, and d.

Fig. 4 .

 4 Fig. 4. Illustration of the dimensional decomposition of both the SEDT algorithm and the Voronoi mapping. (a): An input image (pixels of X are in gray), with the Voronoi mapping according to the i-axis (e.g., the letter a denotes a reference to point A of X, etc). (b): the SEDT of the column i = 4. (c): The set of parabola associated to this column, black dots indicate points x such as #Π(x) > 1 detected during the first (horizontal) process. (d): The final lower envelope of the set of parabolas (bold dashed line) and the final set of points x with #Π(x) > 1: the point j = 7 has disappeared (case (1)), the point j = 1 has been preserved (case (2)), and a new Voronoi diagram boundary has appeared for j = 4 (case (3)) in the Voronoi mapping.

Fig. 5 .

 5 Fig. 5. (a): illustration of the role of condition (1); (b): detail of a bisector function computed without condition (1); (c): detail of a bisector function computed with condition (1). Angle values are in degrees.

Fig. 6 .

 6 Fig. 6. (a): a set X and its medial axis [25] (in black); (b): the bisector function θ X (dark colors correspond to wide angles); (c): filtered medial axis, based on the values of θ X ; (d): detail of the non-filtered and filtered medial axis.

Fig. 7 .

 7 Fig. 7. (a): a set X (in white); (b): the bisector function of X.

Fig. 8 .

 8 Fig. 8. (a 1 , a 2 , a 3 ): a set X (in white); (b 1 , b 2 , b 3 ): Talbot's bisector function; (c 1 , c 2 , c 3 ): our bisector function.

Fig. 9 .

 9 Fig. 9. (a): a view of a subset X of Z 3 (vertebra), generated thanks to a topologically sound "Marching Cubes-like" algorithm [10]; (b,c,d): the bisector function, illustrated in an "X-ray" manner: the gray level of a point corresponds to the average of the bisector angles on a straight line parallel to one of the three axes.

Fig. 10 .

 10 Fig. 10. (a): a set X (in black); (b): isolines of the Euclidean map D X ; (c): a constraint set Y (four points located at the "corners" of the shape); (d): homotopic skeleton of X guided by D 2 X and constrained by Y ; (e): the bisector function of X; (f): the result of our algorithm EuclideanSkeleton.

Fig. 11 .

 11 Fig. 11. A detail of the preceding example.

Fig. 12 .

 12 Fig. 12. (a): a view of the medial axis M (X) of the set X (full 3D ellipsoid, shown as transparent on the three views); (b): a view of EuclideanSkeleton(X, D X , M (X)); (c): a view of FilteredSkeleton(X, 1, 1.5).

Fig. 13 .

 13 Fig. 13. (a): original shape and non-filtered skeleton; (b): filtered skeleton with parameter values r = 0, α = 2.0; (c): r = 64, α = 2.2; (d): r = 100, α = 3.14. (a',b',c',d'): the corresponding reconstructed shapes.

Fig. 14 .

 14 Fig. 14. (a): a view of the set X (vertebra, same object as in Fig. 9). (b): a view of the medial axis M (X) of the set X. (c): a view of EuclideanSkeleton(X, D X , M (X)). (d,e): details of (b) and (c), respectively. (f): a view of FilteredSkeleton(X, 15, 1.5). (g): a view of the shape reconstructed from (f).

Fig. 15 .

 15 Fig. 15. Plots of m (vertical axis) with respect to n (horizontal axis) for different 2D and 3D shapes. (a): families of 2D rectangles (r), ellipses (e) and zoomed gear images (g). (b): miscelanous 2D images (m), with rectangles (r) for comparison. (c): families of 3D boxes (b), torus (t) and zoomed vertebra images (v).

An implementation of this algorithm is available in dimension 3 at the web page: http://www.cb.uu.se/ ~tc18/code_data_set/Code/SEDTVoronoi/

Acknowledgements: the authors wish to thank Gilles Bertrand, Lilian Buzer and Laurent Najman for their insightful remarks.

Annex B

The following figures show the distribution of the size of projections and extended projections for a 2D and a 3D object.


Diego Figueira

Luc Segoufin

Future-looking Logics on Data Words and Trees

In a data word or a data tree each position carries a label from a finite alphabet and a data value from an infinite domain. Over data words we consider the logic LTL ↓ 1 (F), that extends LTL(F) with one register for storing data values for later comparisons. We show that satisfiability over data words of LTL ↓ 1 (F) is already non primitive recursive. We also show that the extension of LTL ↓ 1 (F) with either the backward modality F -1 or with one extra register is undecidable. All these lower bounds were already known for LTL ↓ 1 (X, F) and our results essentially show that the X modality was not necessary. Moreover we show that over data trees similar lower bounds hold for certain fragments of XPath.

Introduction

A data word (data tree) is a word (tree) where each position carries a label from a finite alphabet and a datum from some infinite domain. These models have been considsered in the realm of semistructured data [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF], timed automata [START_REF] Bouyer | An algebraic approach to data languages and timed languages[END_REF] and extended temporal logics [START_REF] Demri | On the freeze quantifier in constraint LTL: Decidability and complexity[END_REF][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]. In this work we consider an infinite domain with no structure where we can only test for equality or inequality between elements.

There have been various logics considered to specify properties over data words and data trees. For example from the standpoint of Temporal Logics (both on data words [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] and trees [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF]), of First Order Logics (see [START_REF] Bojańczyk | Two-variable logic on words with data[END_REF] for the data words case and [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF] for trees), or of logics based on tree patterns [START_REF] David | Complexity of data tree patterns over XML documents[END_REF][START_REF] Björklund | Optimizing conjunctive queries over trees using schema information[END_REF]. The logic LTL ↓ 1 (X, F) is the extension of LTL(X, F) with the ability to use one register for storing a data value for later comparisons. It has been studied in [START_REF] Demri | On the freeze quantifier in constraint LTL: Decidability and complexity[END_REF][START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] where satisfiability and expressivity issues have been addressed. In [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] it has been established that the satisfiability problem for LTL ↓ 1 (X, F) is decidable and non primitive recursive on data words. It is also shown in [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] that the two way extension LTL ↓ 1 (X, F, F -1 ) is undecidable over data words and, similarly, that the extension to 2 registers LTL ↓ 2 (X, F) is undecidable. Here we show that even without the X modality, all the aforementioned lower bounds remain valid: the satisfiability problem for LTL ↓ 1 (F) over data words is non primitive recursive, while for LTL ↓ 1 (F, F -1 ) and LTL ↓ 2 (F) is undecidable. Data trees can be seen as a coding of an xml document [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF][START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF]. Therefore XPath, the node selecting language of W3C [START_REF] Clark | XML path language (XPath)[END_REF], can be considered as a logic over data trees. By XPath, we refer to the 1.0 specification without all the domain specific features (arithmetic, string manipulation, etc.) As XPath is at the core of many xml standard languages (like XQuery and XSLT), deciding satisfiability of some of its fragments can be of great help during optimization stages.

A data word can be seen as a special case of an unranked ordered data tree, for instance by adding a root that is the parent of all the positions of the data word. With this consideration the fragment XPath(→, → + , =) of XPath that contains only the axis next-sibling (→) and following-sibling (→ + ) can be seen as a fragment of LTL ↓ 1 (X, F). There are nonetheless two important differences between the expressive power of XPath(→, → + , =) and LTL ↓ 1 (X, F). The first one is that the axis → + corresponds to the strict future modality in LTL, denoted F s in the sequel. Of course F can be defined using F s but the opposite is not true in the absence of X. The second difference lies in the fact that XPath can compare data values in a way strictly more limited than LTL ↓ 1 . We illustrate this with an example. At a position of a data word, LTL ↓ 1 (F) can store the current data value in the register, check for a later symbol a with a data value different from the one in the register, and then further check for a symbol b with a data value matching the one of the register. In this spirit, XPath could only compare the data values at the beginning and the end of the path and could not say anything about the data value of the intermediate a symbol. Hence XPath(→ + , =) should be seen as a fragment of LTL ↓ 1 (F s ), incomparable with LTL ↓ 1 (F) in terms of expressive power. Based on these ideas, we exhibit a syntactic fragment sLTL ↓ 1 (F s ) of LTL ↓ 1 (F s ) that limits the use of register comparisons and has the same expressive power as XPath(→ + , =) on data words. We then show that satisfiability over data words of sLTL ↓ 1 (F s ) is non primitive recursive. Similarly the same restriction on LTL ↓ 1 (F s , F s -1 ) yields a logic with the same expressive power as XPath(→ + , + ←, =), which is shown to be undecidable.

Our non primitive recursive results are proved by a reduction from the emptiness problem of faulty counter automata. These are counter automata that may have incrementing errors in their counters during the run. Non-emptiness for this class of automata was proven to be decidable and not primitive recursive [START_REF] Schnoebelen | Verifying lossy channel systems has nonprimitive recursive complexity[END_REF]. Our reduction will be centered in a strategy of using data values for codingwith some limitations-a next step move of this automaton. We show that the strict future modality together with the limited data comparison capabilities of sLTL ↓ 1 (F s ) are sufficient for our coding. With the extra power of LTL ↓ 1 (F) for comparing data values, we also show that strictness of the future modality can be avoided. Similar ideas are used for our undecidability results: The extra available expressive power is sufficient to forbid the incrementing errors and thus to code the emptiness problem of a Minsky Counter Automaton.

Related work.

There are known complexity results concerning the satisfiability problem of several data-aware fragments of XPath on data trees. When all navigational axes are present, XPath is undecidable [START_REF] Geerts | Satisfiability of XPath queries with sibling axes[END_REF]. When all vertical axes are present but in the absence of any horizontal axis, the status of the decidability of XPath(↓, ↓ + , ↑, ↑ + , =) is not yet known [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF]. In this paper we show that if decid-able, the complexity of this fragment cannot be primitive recursive, even in the absence of the axes ↓ and ↑.

In [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF] decidability over data trees of the two-variable fragment of first order logic, FO 2 (+1, ∼) is established. As a direct consequence, a fragment of XPath without any descendant/ancestor or following/previous-sibling axes in the paths of the data test expressions, is shown to be decidable. On the opposite, in the present work we focus on the satisfiability under the absence of the successor axis.

In [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] it is shown that the emptiness problem for alternating automata with one register over data trees is decidable. As a direct consequence it is shown that XPath(↓, ↓ + , →, → + , =), with some restriction on the expressions with a data value test, is decidable and non primitive recursive. As a consequence of the present work, the hardness result already holds for XPath(↓ + , →, =) and for XPath(→ + , =).

We finally remark that, nevertheless, the satisfiability of XPath(↓, ↓ + , =) is "only" ExpTime-complete [START_REF] Figueira | Satisfiability of downward XPath with data equality tests[END_REF].

Preliminaries

We fix a finite set Σ of labels and an infinite set D of data values. The models we consider are either data words or data trees. A data word σ over a finite alphabet Σ is a non-empty word of (Σ × D) * . We assume no structure on D and D will be used only to perform tests for (in)equalities. In our examples we will always use data values from N seen as a set of numbers. The data trees we will be using are unranked and ordered. The domain of an unranked ordered tree is represented by a prefix-closed set T of elements from N * such that whenever n(i + 1) ∈ T then ni ∈ T . The elements of T will be called nodes of the tree. A data tree t over Σ, D is a tree domain T together with a labeling function λ assigning an element of Σ ×D to any node of t. We use the standard terminology for trees such as descendant, ancestor, sibling, etc.

LTL with registers. The most expressive logic for data words we treat here is LTL ↓ n (F, X, F -1 , X -1 ), the Linear Temporal Logic with the freeze quantifier (↓ i ), test predicate (↑ i ) and next (X) and future (F) temporal operators together with their inverse modalities (X -1 , F -1 ). Sentences are defined:

ϕ, ψ ::= a | ↓i ϕ | ↑i | ¬ϕ | ϕ ∧ ψ | ϕ ∨ ψ | Oϕ
where a is a symbol from a finite alphabet Σ, i ∈ {1, . . . , n}, and O ranges over {F, X, F -1 , X -1 }. We also use the strict future temporal operator F s as a shortcut for XF. We will consider fragments of this logics as simple restrictions to certain temporal operators. Intuitively, in the evaluation of ↓ i ϕ, current data value is 'saved' in the register i, and any appearance of ↑ i in ϕ holds at a position iff its datum is equal to the one stored in register i.

Given a data word σ, we write σ i for the ith element (couple) of the word, and π 1 , π 2 for the projections on Σ and D. A valuation is defined as a partial map v : {1, . . . , n} → D. The satisfaction relation |= is inductively defined (we omitted X -1 and F -1 for succinctness):

σ, i |=v a iff π1(σi) = a σ, i |=v↑ k iff k ∈ dom(v) and v(k) = π2(σi) σ, i |=v↓ k ϕ iff σ, i |= v[k →π 2 (σ i )] ϕ
σ, i |=v Xϕ iff i < |σ| and σ, i + 1 |=v ϕ σ, i |=v Fϕ iff for some i ≤ j ≤ |σ| we have σ, j |=v ϕ where 1 ≤ i ≤ |σ|. We denote σ, i |= v ∅ ϕ by σ, i |= ϕ, with v ∅ the empty valuation; and we write σ |= ϕ for σ, 1 |= ϕ. Also, in the case of LTL ↓ 1 we use ↓ and ↑ instead of ↓ 1 and ↑ 1 for simplicity.

In Section 5 we will lift our results to trees and XPath. In order to do this it is convenient to introduce now a restriction of LTL ↓ 1 such that with this restriction LTL ↓ 1 corresponds to XPath. A formula of LTL ↓ 1 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 correspondence between sLTL ↓ 1 and XPath will be made explicit in Proposition 1 of Section 5.

Faulty counter systems. For proving our lower bounds we will use a reduction from faulty counter automata that we describe here. A counter automaton (CA) with zero testing is a tuple Σ, Q, q 0 , n, δ, F , where Σ is a finite alphabet, Q is a finite set of states, q 0 is the initial state, n ∈ N is the number of counters, δ ⊂ Q × Σ × L × Q is the transition relation over the instruction set L = {inc, dec, ifzero} × {1, . . . , n}, and F ⊂ Q is the set of accepting states. A counter valuation is a function v : {1, . . . , n} → N. An error-free run over w ∈ Σ * is a finite sequence q 0 , v 0 w0, 0 → q 1 , v 1 w1, 1 → • • • observing the standard interpretation of the instructions 0 , 1 , • • • ( dec, c can only be performed if c is nonzero), where v 0 , v 1 , . . . are counter valuations, v 0 assigns 0 to each counter, and w = w 0 w 1 . . . such that w i ∈ Σ ∪ {ε} for every i. A run is accepting iff it ends with an accepting state.

A Minsky CA has error-free runs. For these automata, already with only two counters, finitary emptiness is undecidable [START_REF] Minsky | Computation: finite and infinite machines[END_REF]. An Incrementing CA (from now on ICA) is defined as a Minsky CA except that its runs may contain errors that increase one or more counters non-deterministically. We write that two valuations are in the relation v ≤ v iff, for every counter c, v(c) ≤ v (c). Runs of Incrementing CA are defined by replacing the relation a,

→ by

a, , where p, u a, q, v iff there exist valuations u , v such that u ≤ u , v ≤ v and p, u a, → q, v . In [8, Theorem 2.9] it is shown that the results of [START_REF] Schnoebelen | Verifying lossy channel systems has nonprimitive recursive complexity[END_REF] and [START_REF] Ouaknine | On Metric temporal logic and faulty Turing machines[END_REF] on Channel Machines can be adapted to prove the following result.

Theorem 1. Emptiness of ICA is decidable and non primitive recursive.

3 The case of sLTL ↓ 1

In this section we show that satisfiability of sLTL ↓ 1 (F s ) is non primitive recursive over data words. We then prove that satisfiability is undecidable for

sLTL ↓ 1 (F s , F s -1
). In the next section we will show that the logic LTL ↓ 1 (F) is also non primitive recursive and that LTL ↓ 1 (F, F -1 ) is undecidable. In Section 5 we will use the results of this section for proving lower bounds for several fragments of XPath over data trees.

Lower bound for sLTL

↓ 1 (F s ).
Theorem 2. Satisfiability of sLTL ↓ 1 (F s ) on data words is non primitive recursive.

Proof. We exhibit a PTime reduction from the non-emptiness of ICA to satisfi-

ability of sLTL ↓ 1 (F s ). Let C = Σ, Q, q 0 , n, δ, F be an ICA. Let L = {(inc i ) 1≤i≤n , (dec i ) 1≤i≤n , (ifzero i ) 1≤i≤n }, and Σ = Q × (Σ ∪ {ε}) × L × Q. We construct a formula ϕ C ∈ sLTL ↓ 1 (F s )
that is satisfied by a data word iff C accepts the word. We view a run of C of the form:

q 0 , v 0 a,inci q 1 , v 1 b,decj q 2 , v 2 b,ifzeroi q 3 , v 3 • • •
as a string in Σ: q 0 , a, inc i , q 1 q 1 , b, dec j , q 2 q 2 , b, ifzero i , q 3 • • • The formula ϕ C will force that any string that satisfies it codes a run of C. In order to do this, ϕ C must ensure that:

(begin) the string starts with q 0 , (end) the string ends with a state of F , (tran) every symbol of Σ in the string corresponds to a transition of C, (chain) the last component of a symbol of Σ is equal to the first component of the next symbol, (pair) for each i, every symbol that contains inc i occurring in the string to the left of a symbol containing ifzero i , can be paired with a symbol containing dec i and occurring in between the inc i and the ifzero i .

Before continuing let us comment on the (pair) condition. If we were coding runs of a perfect Minsky CA (ie, with no incremental errors), to the left of any position containing a ifzero i , we would require a perfect matching between inc i and dec i operations in order to make sure that the value of the counter i is indeed zero at the position of the test. But as we are dealing with ICA, we only need to check that each inc i has an associated dec i to its right and before the test for zero, but we do not enforce the converse, that all dec i match an inc i . This is fortunate because this would require past navigational operators.

The first difficulty comes from the fact that (pair) is not a regular relation. The pairing will be obtained using data values. The second difficulty is to enforce (chain) without having access to the string successor relation. In order to simulate the successor relation we add extra symbols to the alphabet, with suitable associated data values.

Let Σ = Σ ∪ {N, #, @}. The coding of a run consists in a succession of blocks. Each block is a sequence of 3 or 4 symbols, "c N #" or "c @ N #", with c ∈ Σ. The data value associated to the c and # symbols of a block is the same and uniquely determines the block: no two blocks may have the same data value. The data value associated with the symbol N of a block is the data value of the next block. If a block contains a symbol c that codes a inc i operation that is later in the string followed by a ifzero i , then this block contains a symbol @ whose data value is the that of the block containing dec i that is paired with c. For instance in the example of Fig. 1 one can see four blocks b 1 , b 2 , b 3 , b 4 . Each of them starts with a symbol from Σ coding a transition of the ICA and ends with a # with the same data value marking the end of the block. Inside the block, the data value of N is the same as the data value of the next block. The data value of @ corresponds to that of a future block. In this example c 1 must correspond to a inc i while c 3 to dec i and there must be a ifzero i somewhere to the remaining part of the word (say, b 5 ). Moreover c 2 can't be a ifzero i as otherwise the data value of the symbol @ would refer to a block to the left of c 2 .

1 c0 2 N 1 # 2 c1 4 @ 3 N 2 # 3 c2 4 N 3 # 4 c3 5 N 4 # • • • b1 b2 b3 b4
Fig. 1. Coding of an ICA run.

We now show that the coding depicted above can be enforced in sLTL ↓ 1 (F s ). By π 1 , π 2 , π 3 , π 4 we denote the projection of each symbol of Σ into its corresponding component. To simplify the presentation we use the following abbreviations:

σ ≡ c∈ Σ c inc(i) ≡ c∈ Σ,π 3 (c)=inc i c inc ≡ i inc(i) dec(i) ≡ c∈ Σ,π 3 (c)=dec i c last ≡ σ ∧ ¬Fs σ iz(i) ≡ c∈ Σ,π 3 (c)=ifzero i c
The formula ϕ C that we build is the conjunction of all the folowing formulas.

Forcing the structure G(last ⇒ ¬Fs ) : The string ends with the last transition, c∈{N,@,#} G(c ⇒ ¬(↓ Fs(c ∧ ↑))) : the data value associated to each N, # and @ uniquely determines the occurrence of that symbol,

G (σ ∧ ¬last) ⇒ (↓ Fs(N ∧ Fs(#∧ ↑))) : each occurrence of Σ (except the last one)
is in a block that contains a N and then a #,

i G (inc(i) ∧ Fs(iz(i))) ⇒ ↓ Fs(@ ∧ Fs(N ∧ Fs(#∧ ↑)))
: every inc i block to the left of a ifzero i must have a @ before the N, G((σ ∧ ¬inc) ⇒ ¬ ↓ Fs(@ ∧ Fs(#∧ ↑))) : only blocks inc are allowed to have a @, s∈{N,@} G σ ⇒ ¬(↓ Fs(s ∧ Fs(s ∧ Fs(#∧ ↑)))) : there is at most one occurrence of N and @ in each block,

s∈ Σ∪{#} G(σ ⇒ ¬ ↓ Fs(s ∧ Fs(#∧ ↑))
: there is exactly one symbol # and one symbol of Σ per block, G N ⇒↓ Fs(# ∧ Fs(σ∧ ↑)) : each symbol N's datum points to a block to its right, G(N ⇒ ¬ ↓ Fs(# ∧ Fs(# ∧ Fs(σ∧ ↑)))) : in fact N has has to point be the next block.

Once the structure has the expected shape, we can enforce the run as follows. All the formulas below are based on the following trick. In a test of the form ↓ F s (N ∧ F s (#∧ ↑)) which is typically performed at a position of symbol Σ, the last symbol # must have the same data value as the initial position. Hence, because of the structure above, both must be in the same block. Thus the middle symbol N must also be inside that block. From the structure we know that the data value of this N points to the next block. Therefore by replacing the test N by one of the form N ∧ (↓ F s (↑ ∧ s)) we can transfer some finite information from the current block to the next one. This gives the desired successor relation.

Forcing a run

(begin) c∈ Σ,π 1 (c)=q 0 c (end) Fs last ∧ c∈ Σ,π 4 (c)∈F c
(tran) All elements used from Σ correspond to valid transitions. Let ΣC be that set of transitions of C,

G c∈ Σ\ ΣC ¬c (chain) For every c ∈ Σ, G c ⇒ ↓ Fs N ∧ Fs(#∧ ↑) ∧ d∈ Σ, π 4 (c)=π 1 (d) (↓ Fs(d∧ ↑))
(pair) We first make sure that the block of the @ of an inc k is matched with a block of a dec k :

k G inc(k) ⇒ ¬ ↓ Fs(@ ∧ Fs(#∧ ↑))∨ ↓ Fs @∧ ↓ Fs(dec(k)∧ ↑) ∧ Fs(#∧ ↑)
Now, every inc k block to the left of a ifzero k block: -1. The block must contain an @ element:

k G inc(k) ⇒ ↓ Fs(@ ∧ Fs(# ∧ ↑)) ∨ ¬Fs(iz(k))
-2. The data value of that @ element must point to a future block before any occurrence of ifzero k :

k G inc(k) ⇒ ¬ ↓ Fs @ ∧ ↓ Fs(iz(k) ∧ Fs ↑) ∧ Fs(# ∧ ↑)
This concludes the construction of ϕ C . The correctness proof is standard.

Undecidability of sLTL

↓ 1 (F s , F s -1 ) We now consider sLTL ↓ 1 (F s , F s -1
). The extra modality can be used to code the run of a (non faulty) Minsky CA.

Theorem 3. Satisfiability of sLTL ↓ 1 (F s , F s -1 ) is undecidable.
Proof. Consider a Minsky CA C. We revisit the proof of Theorem 2. It is easy to see that we can enforce the absence of faulty increments during the run by asking that every dec i element is referenced by some previous inc i block:

i G(dec(i) ⇒ ↓ F s -(@ ∧ ↑)).
We thus make sure that every dec is related to a corresponding inc. Hence, the coding is that of a perfect (non faulty) run. [START_REF] Bojańczyk | Two-variable logic on words with data[END_REF] The case of LTL ↓ 1

In this section we lift the lower bounds of the previous section by considering the temporal operator F instead of F s . We can only do so by removing at the same time the restriction to simple formulas. Hence the results of this section cannot be applied to XPath. Notice that LTL ↓ 1 (F) and sLTL ↓ 1 (F s ) are incomparable in terms of expressive power. Indeed, properties like ↓ F(a ∧ ↑ ∧ F(b ∧ ↑)) cannot be expressed in sLTL ↓ 1 (F s ), while LTL ↓ 1 (F) cannot express that the model has at least two elements. We do not know whether sLTL ↓ 1 (F), which is weaker than the two above mentioned logics, is already non primitive recursive. The results of this section improve the results of [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] which show that satisfiability is non primitive recursive for LTL ↓ 1 (X, F) and undecidable for LTL ↓ 1 (X, F, F -1 ).

Theorem 4. Over data words, 1. Satisfiability of LTL ↓ 1 (F) is decidable and non primitive recursive. 2. Satisfiability of LTL ↓ 1 (F, F -1 ) is undecidable.

Proof. We only prove Item 1, the proof of Item 2 being similar. Consider an ICA C and recall the coding of runs of C used in the proof of Theorem 2. In the construction of the formula ϕ C , whenever we have "s ∧ F s (s ∧ ϕ)" for some ϕ and s = s two different symbols, F s can be equivalently replaced by the F temporal operator. This is the case in all formulas except in three places: (i) The formula saying that N should point to the next block contains # ∧ F s (# ∧ ϕ). But from the structure that is enforced, this can equivalently be replaced by # ∧ F(N ∧ F(# ∧ ϕ)). (ii) To enforce that each block contains at most one occurrence of symbols in Σ ∪ {N, #, @}. (iii) To enforce that no two symbols in Σ ∪ {N, #, @} have the same data value.

In order to cope with (ii) and (iii), we use a slightly different coding for runs of C. This coding is the same as the one for the proof of Theorem 2 except that we allow succession of equal symbols, denoted as group in the sequel. Note that in a group two different occurrences of the same symbol in general may have different data values, as we can no longer enforce their distinctness. However, as we will see, we can enforce that the Σ group of elements of a block have all the same data value.

Hence a block is now either a group of c ∈ Σ followed by a group of N followed by a group of # or the same with a group of @ in between. A coding of a run is depicted in Figure 2.

This structure is enforced by modifying the formulas of the proof of Theorem 2 as follows. (i) The formulas that limit the number of occurrences of symbols in a block are replaced by formulas limiting the number of groups in a block. (ii) The formulas requiring that no two occurrences of a same symbol may have the same data values are replaced by formulas requiring that no two occurrences of a same symbol in different groups have the same data value. (iii) In all other formulas, F s is replaced by F. (iv) Finally, we ensure that although we may have repeated symbols inside a block, all symbols from Σ have the same data value.

G(σ ⇒ ¬ ↓ F((σ ∨ #) ∧ ¬ ↑ ∧F(#∧ ↑)))
Note that this implies that each N of a group must have the same data values as they all point to the next block. However there could still be @ symbols with different data values as depicted in Fig. 2.

The new sentences now imply, for instance, that:

1. Every position from a group of c ∈ Σ have the same data value which is later matched by an element of a group of #. 2. Every position from a group of N has the same data value as a position c ∈ Σ of the next block (and then, it has only one possible data value). 3. Every position from a group @ has the same data value as a position c ∈ Σ of a block to its right. Note that the data values of two @ of the same group may correspond to the data values of symbols in different blocks. This is basically the main conceptual difference with the previous proof.

The proof of correctness of the construction is left to the reader.

Note that in the previous proof we used the fact that LTL ↓ 1 (F), although it has only one register, can make (in)equality tests several times throughout a path (as used in the formula of item (iv) in the proof), something that sLTL ↓ 1 (F s ) and XPath cannot do.

Two registers. When 2 registers are available the previous result can be adapted to code a (non faulty) Minsky CA with a strategy similar to [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]Theorem 5.4].

Theorem 5. Satisfiability of LTL ↓ 2 (F) is undecidable over data words.

We now turn to data trees. An xml document can be seen as an unranked tree with attributes and data values in its nodes. While a data tree has only one data value per node, an xml document element may have several attributes each of which with an associated data value. All XPath fragments treated in this paper can force all elements of an xml document to have only one attribute. Therefore all hardness results in the present work hold also for the class of xml documents.

The logic XPath. XPath is a two-sorted language, with path expressions (α, β, . . .) and node expressions (ϕ, ψ, . . .). These are defined by mutual recursion:

α, β ::= ↓ | ↓ + | ↑ | ↑ + | → | → + | ← | + ← | ε | αβ | α ∪ β | α[ϕ] ϕ, ψ ::= σ | α | ¬ϕ | ϕ ∧ ψ | α = β | α = β (σ ∈ Σ)
A path expression essentially describes a traversal of the tree by using the axis: child (↓), descendant (↓ + ), the next-sibling (→), following-sibling (→ + ) and their inverses, with the ability to test at any stage for node conditions. Let t be a data tree with domain T and labeling function λ. The semantics of XPath is defined by induction is the usual intuitive way, we only give here some cases:

[[↓]] t = {(x, xi) | xi ∈ T } [[αβ]] t = {(x, z) | ∃y.(x, y) ∈ [[α]] t ∧ (y, z) ∈ [[β]] t } [[ α ]] t = {x ∈ T | ∃y.(x, y) ∈ [[α]] t } [[α[ϕ]]] t = {(x, y) ∈ [[α]] t | y ∈ [[ϕ]] t } [[ε]] t = {(x, x) | x ∈ T } [[α + ]] t = the transitive closure of [[α]] t [[α = β]] t = {x ∈ T | ∃y, z.(x, y) ∈ [[α]] t , (x, z) ∈ [[β]] t , π2(λ(y)) = π2(λ(z))} [[α = β]] t = {x ∈ T | ∃y, z.(x, y) ∈ [[α]] t , (x, z) ∈ [[β]] t , π2(λ(y)) = π2(λ(z))}
A key property for using results of Section 3 is that simple formulas can be translated to XPath and back. The proof of this result is straightforward by induction on the formula. Proposition 1. Over data words, sLTL ↓ 1 (F s ) and XPath(→ + , =) have the same expressive power. The same holds for sLTL ↓ 1 (F s , F s -1 ) and XPath( + ←, → + , =).

Moreover, in both cases, the transformation from sLTL ↓ 1 to XPath takes polynomial time while it takes exponential time in the other direction.

The restriction on negations in the definition of sLTL ↓ 1 corresponds to the fact that XPath path expressions are always positive: any path α is essentially a nesting of operators F with intermediate tests. We remark that there is a big difference between XPath(→ + , =) over data words and XPath(↓ + , =) over data trees. Indeed XPath(↓ + , =) is closed under bisimulation and hence it cannot assume that the tree is a vertical path. As the string structure was essential in the proof of Theorem 2, the non primitive recursiveness of XPath(→ + , =) over data words does not lift to XPath(↓ + , =) over data trees. Actually, satisfiability of XPath(↓ + , =) is ExpTime-complete [START_REF] Figueira | Satisfiability of downward XPath with data equality tests[END_REF]. However, if one considers the logic XPath(↓ + , →, =) then the axis → can be used to enforce a vertical path (¬ ↓ + [→]) and therefore it follows from Theorem 2 and Proposition 1 that: Corollary 1. Satisfiability of XPath(↓ + , →, =) on data trees is at least non primitive recursive.

Similarly, in XPath(↓ + , ↑ + , =) one can simulate a string by going down to a leaf using ↓ + and then use the path from that leaf to the root as a string using ↑ + . Corollary 2. Satisfiability of XPath(↓ + , ↑ + , =) on data trees is at least non primitive recursive.

Note that the decidability of XPath(↓ + , →, =) and of XPath(↓ + , ↑ + , =) is still an open problem.

Open problem: Is XPath(↓ + , ↑ + , =) decidable over data trees?

It would be interesting to know whether the strictness of the axis ↓ + is necessary in the above two results. This boils down to know whether sLTL ↓ 1 (F) is already not primitive recursive over data words. Note that the proof of Theorem 4 uses in an essential way the possibility to make (in)equality tests several times throughout a path. This is exactly what cannot be expressed in sLTL ↓ 1 (F).

Open problem: Is satisfiability of sLTL ↓ 1 (F) primitive recursive over data words?

We conclude with some simple consequences of Theorem 3 and Proposition 1:

Corollary 3. Satisfiability of XPath( + ←, → + , =) and of XPath(↓ + , ↑ + , →, =) over data trees is undecidable.

Corollary 4. Satisfiability of XPath(→ + , ↓, ↑, =) is undecidable.
Proof. This is similar to the proof of Theorem 3 with a slight difference. Consider that the coding of the run of the counter machine is done at the first level of the tree (i.e., at distance 1 from the root). Then, the property to ensure that every decrement has a corresponding increment is now:

i ¬ ↓ [dec(i) ∧ ¬ε =↑↓ [@]].

Discussion

By [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] it is known that satisfiability of LTL ↓ 1 (X, F) with infinite data words is undecidable. The proof of Theorem 4 can be extended to code runs of ICA over infinite data words, which is known to be undecidable, to show that this result already holds in the absence of X. Theorem 6. On infinite data words, the satisfiability problem of LTL ↓ 1 (F) is undecidable.

Summary of results

In the table below we summarize the main results and some of the consequences we have mentioned. In this table, PR stands for non primitive recursive.

A Missing proofs

A.1 Correctness of the construction of the proof of Theorem 2

Given an ICA C, the proof exhibited a formula ϕ C ∈ XPath(→ * , =) that is satisfied by a data word iff C accepts the word. We show here that the construction is correct.

From data word to an accepting ICA run Let w be a data word satisfying

ϕ C . Let B 1 B 2 • • • B m
be the decomposition of w into blocks as described above. Let c i = q i , a i , i , q i+1 be the element of B i in Σ. We show that w = a 1 a 2 • • • a m is accepted by C. We construct a run of C on w such that C is in state q i before reading letter a i of w and execute the transitions c i . By (tran) each one of these are valid transitions of the ICA, and (chain) ensures that the sequence is consistent. (begin) takes care of the initialization condition and (end) of the accepting condition. It remains to construct the valuation v 1 , . . . , v m+1 of the counter at each step such that we have q i , v i ai, i q i+1 , v i+1 as desired.

As expected v 1 is the zero valuation. We construct the rest of the valuations by induction, simulating a perfect counter machine and introducing incrementing errors in a lazy way, whenever necessary. At step i, given a transition q i , a i , i , q i+1 and the current valuation v i we set v i+1 such that q i , v i ai, i q i+1 , v i+1 .

-If i is inc k , then v i+1 := v i [k → v i (k)+1] and clearly q i , v i ai, i → q i+1 , v i+1 . -If i is dec k then: • If v i (k) > 0 then v i+1 := v i [k → v i (k) -1]. • If v i (k) = 0, then v i+1 := v i .
In both cases one can verify that q i , v i ai, i q i+1 , v i+1 , the transition being with an incrementing error of 1 in the second case.

-If i is ifzero k , we set v i+1 := v i . To ensure that q i , v i ai, i q i+1 , v i+1
we must show that necessarily v i (k) = 0. This is a consequence of condition pair. This condition enforces that each inc k must be paired with a unique dec k to its right and before the ifzero k test. Hence the lazy strategy above ensures that each increment is decremented later on and before the zero test.

From an accepting ICA run to data word Given an accepting run of the ICA q 1 , v 1 a1, 1 q 2 , v 2 a2, 2 . . . am, m q m+1 , v m+1 we construct a data word w verifying ϕ C as follows. Let c i be q i , a i , i , q i+1 . w consists of a concatenation of m blocks B 1 B 2 • • • B m each one defined:

-If i = m, B i is the word c i with data value m.

-If i < m, and i ∈ {dec k , ifzero k }, then set

B i to c i N# with respective data values i, i + 1, i. c i , i N, i + 1 #, i -If i < m and i is inc k . Consider the minimal d > i such that v d+1 (k) = v i (k)
and set B i to

• c i @ N # with respective data values i, d, i + 1, i if d exists • c i N # with respective data values i, i + 1, i if not.
This construction assigns the unique data value i to each block B i , and set the data value of each symbol N to the data value of the next block B i+1 . The constraints (begin), (end), (tran), (chain) are obviously true. It remains to verify the constraints on @: they must have a unique data value, must point to a corresponding dec instruction that occur before any corresponding zero test, and no two @ may point to the same dec instruction. Consider a position i such that i is inc k with a subsequent zero test ifzero k at position j > i.

Because the zero test is correct, the increment of counter k made at step i must be decremented at some position between i and j. Hence there is a i < d < j such that v d+1 (k) = v i (k). By construction the data value of the @ symbol of B i is the minimal such d. By minimality, c d must be a dec k instruction. Assume now that at position i < i there is also a inc k instruction. The data value of the @ symbol of B i cannot be d. Because if this would be the case then Proof (sketch). Consider a Minsky Counter Automaton C. We revisit the previous proof. We modify the coding of a run of C by also inserting a group of symbols @ in each dec block. Using F -1 , we add formulas ensuring that every block containing a dec instruction also contains a group of @ symbols such that their data values refer to previous blocks containing a matching inc instruction. We also make sure that two @ from different blocks have different data values. All this can be done by taking the F -1 counterpart of the formulas we constructed with F. We show that the new formula ϕ C is satisfied by a data word iff C accept the word. Constructing a data word that satisfies ϕ C from a word accepted by C is done as in the proof of Theorem 2.

v i (k) = v d+1 (k) = v i (k)
For the other direction one needs to show that from a word that satisfies ϕ C , the corresponding word with the obvious run and obvious valuations of the counter is accepting for C. One can verify that the new extra conditions do imply that no null counter is ever decreased and each zero test is correct, based on the fact that for every dec i there must be at least one inc i to its left, and for every inc i there must have a related dec i before any ifzero i test.

A.3 Proof of Theorem 5

First recall the statement of Theorem 5:

Theorem 5 Satisfiability of LTL ↓ 2 (F) is undecidable over data words. Proof. We adapt the proof of part 1. of Theorem 4 using ideas already present in [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF][START_REF] Lisitsa | Temporal logic with predicate lambdaabstraction[END_REF] for coding Minsky CA with only forward temporal operators. Fix a two counter machine C = Σ, Q, q 0 , 2, δ, F . The main idea is to modify the coding of Theorem 4 by adding in each block a symbol h 1 whose data value is supposed to be the one of the last inc 1 that has previously occurred, a symbol l 1 whose data value is supposed to be the one of the last inc 1 that has not been decreased yet and similarly with h 2 and l 2 for the second counter. A zero test of counter 1 can then only occur in a block where the data values of h 1 and l 1 match. The coding is depicted in Figure 3. Based on these ideas, the formula ϕ C that we construct makes sure that:

c I 0 1 h 1 l N # c I 1 2 h 1 l N #c D 2 3 h 1 l N # c I 3 3 h 2 l N # c I
(i) The structure. We enforce a structure that is a sequence of blocks of the form " q, w, l, q h 1 l 1 h 2 l 2 N#", with the possibility that there are repeated consecutive symbols. This can be done in the same way we did before.

As for the previous codings, we demand that in each block, for every element in the first group of Σ symbols there is an element in the last group of symbols # with the same data value. This is enforce with a formula of LTL ↓ 1 (F) as before. With the help of the second register we can now enforce that each group of symbols has the same data value, for all symbol s we have the formula:

G σ ⇒↓ 1 ¬F s∧ ↓ 2 F (s ∧ ¬ ↑ 2 ∧F(#∧ ↑ 1 ))
(ii) Each q, w, l, q occurring in the string is in δ. For the first one q = q 0 , and for the last one q ∈ F . For any q, w, l, q and q , w , l , q in consecutive blocks, q = q . This can be checked just as in the previous codings. (iii) In the initial block, the data values of h 1 and l 1 are the same and the data values of h 2 and l 2 are the same (we only show the formula for h 1 and l 1 ):

↓ 1 ¬F h 1 ∧ ↓ 2 F(l 1 ∧ ¬ ↑ 2 ∧F(#∧ ↑ 1 ))
(iv) In any block immediately after a ifzero instruction, the data values of h 1 ,l 1 ,h 2 ,l 2 are identical to those of the ifzero instruction. We only give the formula for ifzero 1 instruction with the h 1 symbol. ¬F iz(1)∧ ↓ 1 F h 1 ∧ ↓ 2 F(ψ ∧ F(#∧ ↑ 1 )) where ψ ≡ N∧ ↓ 1 F(h 1 ∧ ¬ ↑ 2 ∧F(#∧ ↑ 1 )) (v) In any block immediately after an inc 1 instruction, h 1 is not in the same class as any preceding h 1 (stated in the formula below) and l 1 , h 2 , l 2 are in the same class as in the previous block (this can be stated using a formula similar to the one for for item (iv)).

¬F h 1 ∧ ↓ 1 F inc(1)∧ ↓ 2 ∧F(ϕ ∧ F(#∧ ↑ 2 )) where ϕ ≡ N∧ ↓ 2 F ↑ 2 ∧F(h 1 ∧ ↑ 1 ∧F(#∧ ↑ 2 ))
We have of course corresponding formulas for blocks with inc 2 instructions. (vi) In any dec 1 block, h 1 and l 1 have different data values.

¬F dec(1)∧ ↓ 1 F h 1 ∧ ↓ 2 F(l 1 ∧ ↑ 2 ∧F(#∧ ↑ 1 ))
We have a corresponding formula for blocks with a dec 2 instruction. (vii) In any ifzero 1 block, h 1 and l 1 have the same data value. This can be expressed with a formula as above. We have a corresponding formula for ifzero 2 blocks. (viii) In any block immediately after a dec 1 block B, -h 1 is in the same class as the previous h 1 , and -l 1 is in the same class as the h 1 occurring in a block immediately after the rightmost block (occurring before B) with a h 1 that is in the same class as the l 1 of B.

-h 2 and l 2 are in the same class as their corresponding symbol of B.

The first and third conditions can be expressed using formulas similar to those above. The difficult part is to enforce the second condition. For this we introduce some macros:

InBlock i (ϕ) ≡↓ i F(ϕ ∧ F(#∧ ↑ i )) NextBlock i (ϕ) ≡↓ i F(N ∧ F(#∧ ↑ i )∧ ↓ i F(σ ∧ ϕ ∧ F(#∧ ↑ i ))) InNextBlock i (ϕ) ≡ NextBlock i (InBlock i (ϕ))
The second condition can then be stated:

¬F σ∧ ↓ 2 F h 1 ∧ ↓ 1 F N ∧ F(#∧ ↑ 2 )∧ ↓ 2 F(σ∧ ↑ 2 ∧F(h 1 ∧ ¬ ↑ 1 ∧ ↓ 2 ϕ))
where ϕ ≡ F dec(i) ∧ InBlock 2 (l 1 ∧ ↑ 1 ) ∧ InNextBlock 1 (l 1 ∧ ¬ ↑ 2 )

We have a corresponding formula for blocks following a dec 2 instruction.

A.4 Proof of Proposition 1

Proposition 1 Over data words, sLTL ↓ 1 (F s ) and XPath(→ + , =) have the same expressive power. The same hold for sLTL ↓ 1 (F s , F s -1 ) and XPath( + ←, → + , =). Moreover, in both cases, the transformation from sLTL ↓ 1 to XPath takes polynomial time while it takes exponential time in the other direction.

Proof (sketch). The translation from sLTL ↓ 1 to XPath is straightforward by induction. One then naturally obtain equality tests of the form ε = α or ε = α depending on whether the unique possible negation is present or not.

The other translation is also by induction. The non trivial part concerns the translation of node expressions of the form α = β. Over data words, one of the path expressions α or β must end first, say α. In this case the node expression can be decomposed into a disjunction of (exponentially many) expressions that first start with a path expression that merge α with the part β 1 of β that is common to with α, followed by a test of the form ε = β 2 , where β = β 1 β 2 . Tests of the form ε = β 2 are the immediate to translate into sLTL ↓ 1 .

B Complete semantics of XPath

Fig. 2 .

 2 Fig. 2. LTL ↓ 1 (F) cannot avoid having repeated consecutive symbols.

Fig. 3 .

 3 Fig. 3. Coding of a 1-counter machine run. Only data values of the h and l symbols are represented for the sake of clarity. Only one symbol per group is also represented. Elements depicted as c I i , c D i and c Z i correspond, respectively, to increment, decrement and zero testing symbols of Σ.

  and d would not be minimal for the position i . Hence (pair) is also satisfied and w |= ϕ C .

	A.2 Proof of Theorem 4.2
	Recall the statement.
	Theorem 4.2 Over data words, Satisfiability of LTL ↓ 1 (F, F -1 ) is undecidable.

The authors acknowledge the financial support of 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.

Logic

Complexity Details

XPath(↓ + , →, =) PR, decidability unknown Corollary 1

XPath(↓ + , ↑ + , =) PR, decidability unknown Corollary 2

XPath(↓ + , ↑ + , →, =) undecidable Corollary 3

XPath(→ + , ↓, ↑, =) undecidable Corollary 4