Nicole Bidoit
email: bidoit@lri.fr

Sandra De Amo

Luc Segoufin
email: luc.segoufin@inria.fr

Order independent temporal properties

Keywords: database, expressiveness, query languages, temporal logic

The paper investigates temporal properties that are invariant with respect to the temporal ordering and that are expressible by temporal query languages either explicit like FO(≤) or implicit like TL. In the case of an explicit time representation, these "order invariant" temporal properties are simply those expressible in the language FO(=). In the case of an implicit time representation, we introduce a new language, TL(E i ) that captures exactly these properties. The expressive power of the language TL(E i ) is characterized via a game à la Ehrenfeucht-Fraïssé.

This provides another proof, using a more classical technique, that the implicit temporal language TL is strictly less expressive than the explicit temporal language FO(≤). This alternative proof is interesting by itself and opens new perspectives in the investigation of results of the same kind for more expressive implicit temporal languages than TL.

Introduction

It is well-known that the choice between an implicit and explicit representation of time in a temporal data model does not affect the meaning of the information stored in a temporal database [START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps to Query Temporal Databases[END_REF][START_REF] Bidoit | Implicit temporal query languages : towards completeness[END_REF][START_REF] Niwinski | First Order Queries over Temporal Databases Inexpressible in Temporal Logic[END_REF]. However, one cannot state the same about temporal query languages. Following an implicit time representation approach, a temporal database is defined as a finite sequence of instances which can be interpreted as the evolution of the database states during its lifetime; on the other hand, following an explicit time representation approach, tuples in a relation are timestamped and time can represent, for instance, the valid date associated to the information in the real world (valid time) or the date this information has been entered into the database (transaction time). We notice that in both approaches, the underlying temporal structure is linear. Although non linear time (branching time) is potentially applicable to database problems like version management or workflows, we concentrate on temporal domains that are linearly ordered sets.

In the context of an implicit time representation, the linear temporal logic TL, with connectives Until Since Next Previous, and its extensions are the basic formalisms underlying query languages specification [START_REF] Chomicki | Temporal Query Languages: a survey, Temporal Logic, First Int. conf[END_REF][START_REF] Emerson | Temporal and Modal Logic[END_REF]. When time is explicitly represented, queries are specified using the standard relational query languages [START_REF] Abiteboul | Foundations of Databases[END_REF] with built-in linear order on the timestamps. One of these languages, the relational calculus with timestamps (i.e., the first-order theory of linear order), denoted by FO(≤), provides a natural formalism to specify queries in the explicit perspective.

The comparison between the two approaches was done in [START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps in Temporal Query Languages[END_REF][START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps to Query Temporal Databases[END_REF][START_REF] Sturm | First-order expressivity for S5-models: modals vs. twosorted languages[END_REF][START_REF] Hodkinson | Decidable fragments of first-order temporal logics[END_REF] where many fragments (restriction on the quantifier prefix as in [START_REF] Sturm | First-order expressivity for S5-models: modals vs. twosorted languages[END_REF]) and extensions (more temporal connectives as in [START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps to Query Temporal Databases[END_REF][START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps in Temporal Query Languages[END_REF]) of the logics presented above are studied and compared. Their motivations ranged from obtaining decidability for satisfiability ( [START_REF] Sturm | First-order expressivity for S5-models: modals vs. twosorted languages[END_REF]) or separating query language in term of expressiveness ([2, 1]).

In this paper we focus on TL and FO(≤). In particular the work of [START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps in Temporal Query Languages[END_REF][START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps to Query Temporal Databases[END_REF] has shed new light on their relative expressiveness as temporal query languages: surprisingly, TL is strictly less expressive than FO(≤), in particular TL is unable to express the existence of two identical states in the temporal database, while this property is easily expressible in FO(≤). These results are of major interest and stand in contrast with the propositional case. In [START_REF] Gabbay | On the Temporal Basis of Fairness[END_REF][START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF], the notion of a complete temporal language is introduced via equivalence with FO(≤) and the authors show that propositional TL is complete.

The fact that TL is strictly less expressive than FO(≤) has clearly stimulated subsequent research work in proposing implicit and explicit query languages more expressible than TL. For instance, [START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps in Temporal Query Languages[END_REF][START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps to Query Temporal Databases[END_REF] propose a hierarchy of implicit and explicit temporal languages which, it is worth to remark, are either strictly less expressive or strictly more expressive than FO(≤). [START_REF] Bidoit | Implicit temporal query languages : towards completeness[END_REF] has introduced another hierarchy of implicit temporal languages, with the purpose of proving the following open problem: Is there a complete implicit temporal query language ? Investigations aiming at solving this problem are motivated, as pointed out in [START_REF] Chomicki | Temporal Logic in Information Systems, Logics for Databases and Information Systems[END_REF], by the simplicity and computational advantages of temporal logic which make it especially attractive as a query language for temporal databases. Indeed, because the references to time are hidden, queries are formulated in an abstract, representation-independent way. Furthermore, temporal logic and the first-order theory of linear order have very different complexity properties : for instance, the satisfiability problem for propositional TL (given a propositional formula p is there a model for p ?) is PSPACE-complete ( [START_REF] Sistla | The complexity of proposicional linear temporal logic[END_REF]) whereas the same problem for first-order theory is non elementary ( [START_REF] Meyer | Weak monadic second order theory of successor is not elementary recursive[END_REF]).

It is important at this point, to make some brief comments about the technique employed in [START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps in Temporal Query Languages[END_REF][START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps to Query Temporal Databases[END_REF] in order to prove that TL is strictly less expressive than FO(≤). This technique is based on communication protocols [START_REF] Kushilevitz | Communication Complexity[END_REF]. Intuitively, a communication protocol involves two partners exchanging information in order to prove or discover something. Each partner is in possession of some amount of information and is able to execute calculations. By exchanging messages, the two partners can inform each other of partial results of these calculations. Their messages take the form of finite relations. The calculations carried out by one partner can only involve the information he/she owned at the beginning of the communication process or the one he/she obtained from messages exchanged with his/her partner. Thus, the execution of a protocol is essentially characterized by a series of messages exchanged between the two partners. A protocol may be designed to test some property over the initial dataset. The number of messages exchanged during the protocol execution measures, in some extent, the communication complexity of the property. The proof we are interested in can be outlined as follows: [START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps in Temporal Query Languages[END_REF] it can be shown that all properties expressible in TL have a constant communication complexity (does not depend on the size of the dataset); (2) the property consisting in verifying the existence of two distinct states in a temporal database has a non-constant communication complexity (roughly speaking, in order to be verified, this property requires a number of messages which depends on the number of states in the temporal instance). So, TL cannot express this property which, on the other hand, can be easily formulated in FO(≤).

In this paper, we propose a different proof of this same result, but using a more classical technique based on games à la Ehrenfeucht-Fraïssé. Nevertheless, the proof we present does not follow the direct proof schema used to show, for instance, that graph connectivity is not a first order property: (1) characterize elementary equivalence restricted to formulas of quantifier depth r by a game with r moves ; (2) find a connected graph and a non-connected one and a winning strategy over these two structures, implying that they cannot be distinguished by first order formulas. Concerning the language TL, developing a similar proof schema is not an easy task due to the fact that the time order structure is linear and discrete. We notice, for instance, that in [START_REF] Niwinski | First Order Queries over Temporal Databases Inexpressible in Temporal Logic[END_REF], a technique of games à la Ehrenfeucht-Fraïssé is successfully used mainly because the time order considered is dense.

Our proof that TL is strictly less expressive than FO(≤) can be outlined as follows. First, we notice that the witness property used in [START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps in Temporal Query Languages[END_REF][START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps to Query Temporal Databases[END_REF][START_REF] Niwinski | First Order Queries over Temporal Databases Inexpressible in Temporal Logic[END_REF], "are there two identical states in the database?", which we call twin henceforth, is order independent, in the sense that its verification on a temporal database does not depend on the particular ordering of its states. As a matter of fact, the communication protocol technique described above takes advantage of this aspect of the twin property, since the temporal database is viewed by the two partners as a set of instances rather than a sequence of instances. We denote by FO(=) the fragment of FO(≤) which includes neither the order predicate ≤ nor temporal constants. Next, we introduce an implicit temporal query language, denoted by TL(E i ) and its explicit counterpart in FO(=), denoted by FO tl (=), and show that they correspond exactly to the order independent properties expressible in TL. The proof of this result is quite complex and requires a strong notion of order independence involving finite and infinite instances, since a well-known counterexample given by Y. Gurevich (see exercise 17.27 in [START_REF] Abiteboul | Foundations of Databases[END_REF]) guarantees the existence of an order independent (with respect to finite instances) property expressible in TL which is not expressible in FO(=) (therefore, not expressible in TL(E i )). After establishing these syntactic (implicit and explicit) characterizations of the order independent properties expressible in TL, we show, via a game à la Ehrenfeucht-Fraïssé for TL(E i ), that this restricted temporal language is unable to express the twin property. We conclude that twin is not expressible in TL since it is order independent.

The most important contribution of this paper consists in (1) the syntactic characterization of the order independent properties expressible in TL via the restricted temporal language TL(E i ), which by itself sheds new light on the expressiveness of implicit temporal query languages and (2) the alternative proof schema it provides, allowing the use of a more classical tool to show a known result on relative expressiveness of temporal query languages.

Paper Organization: In section 2, we briefly recall the definitions of the query languages TL and FO(≤) and present some well-known results which give the necessary background for understanding the problem we propose. Section 3 introduces the implicit temporal language TL(E i ) and its explicit counterpart FO tl (=), and show that TL(E i ) and FO tl (=) correspond exactly to the order independent properties expressible in TL. Section 4 develops a game à la Ehrenfeucht-Fraïssé in order to show that twin is not expressible in TL(E i ). Finally, we conclude the paper by discussing the perspectives of using this technique to solve some similar inexpressiveness problems.

Preliminaries

In the following, we consider a (static) database schema R and a unique domain Dom. The timestamp of R, denoted R ts is obtained from R by adding a new attribute T to each relation of R. This temporal attribute ranges over the temporal domain which is usually N + in this paper.

An implicit temporal (finite) instance I over R, is a (finite) sequence (I 1 ,I 2 ,. . .,I n ) of (finite) instances over R which domain is a (finite) subset of Dom.

I 1 is called the initial state of I, I n its final state, and for each i, I i is called the state of I at instant i.

An explicit temporal instance is a finite instance over R ts where, for each tuple, the temporal attribute ranges over N + while the remaining attributes range over Dom.

To each implicit temporal instance I corresponds an explicit temporal instance I ts and vice versa. Figure 2 shows the two alternative approaches for time representation.

The query language TL. The linear temporal logic TL [START_REF] Emerson | Temporal and Modal Logic[END_REF] is a well-known formalism for specifying queries in an implicit time approach. The syntax of TL over a

I 1 I 2 I 3 R A a b c R A b d R A a c d
The implicit temporal instance I.

R ts A T a 1 b 1 c 1 b 2 d 2 a 3 c 3 d 3
The explicit tempral instance I ts database schema R is obtained using the formation rules for standard first order logic over R together with the additional formation rule:

• if ϕ 1 et ϕ 2 are formulas then ϕ 1 Until ϕ 2 , ϕ 1 Since ϕ 2 , Next ϕ 1 and
Previous ϕ 1 are formulas.

Given a temporal instance I = (I 1 ,. . .,I n ) over R, and a TL formula ϕ over R, the active domain of I, denoted by Adom(I), is the set of elements of Dom appearing in I i (R), for some R ∈ R and some i ∈ {1, . . . , n}. As for the relational calculus, different kinds of problems ("unsafe queries") may arise if the conventional definitions from linear temporal logic are adapted directly to the current context (see [START_REF] Abiteboul | Foundations of Databases[END_REF] for a discussion). We opt here for restricting variables to range over the active domain of the input temporal database.

In the following, we briefly recall the (active domain) semantics of a TL formula ϕ over an implicit temporal instance I. Definition 2.1 (Semantics of TL) The truth of ϕ over I at instant i ∈ {1, . . . , n}, given the valuation ν of the free variables of ϕ ranging over Adom(I), denoted [I,i,ν] |= tl ϕ, is defined as follows:

[I, i, ν] |= tl R(x 1 , . . . , x k ) if (ν(x 1 ), ν(x 2 ), . . . , ν(x k )) ∈ I i (R).
If ϕ is a boolean combination of formulas or a quantification (∃, ∀) of a formula then the definition is as usual.

[I,i,ν] |= tl ϕ 1 Until ϕ 2 iff there exists j > i such that [I,j,ν] |= tl ϕ 2 and for each

k such that i ≤ k < j, [I,k,ν] |= tl ϕ 1 .
[I,i,ν] |= tl ϕ 1 Since ϕ 2 iff there exists j < i such that [I,j,ν] |= tl ϕ 2 and for each

k such that j < k ≤ i, [I,k,ν] |= tl ϕ 1 . [I,i,ν] |= tl Next ϕ 1 iff i < n and [I,i + 1,ν] |= tl ϕ 1 . [I,i,ν] |= tl Previous ϕ 1 iff i > 1 and [I,i -1,ν] |= tl ϕ 1 .
It is sometimes convenient to use the following derived temporal modalities: F ϕ 1 ≡ true Until ϕ 1 ("sometimes in the future ϕ 1 "), G ϕ 1 ≡ ¬ F ¬ϕ 1 ("always in the future ϕ 1 ") P ϕ 1 ≡ true Since ϕ 1 ("sometimes in the past ϕ 1 "), H ϕ 1 ≡ ¬ P ¬ϕ 1 ("always in the past ϕ 1 "), Historically TL has been used as an implicit temporal query language by evaluating its formulas at the initial time. We will use this notion together with a more general one where the instant of evaluation is not specified and thus can be used as a parameter for the output. Recall that, in the following definition, x denotes a sequence of variables and the valuations ν always ranges over the active domain of the temporal instance. The query language FO(≤). A natural query language over timestamp temporal databases is obtained by considering the first order logic over R ts with two kinds of variables: temporal variables (denoted by t, u, v, s) and data variables (denoted by x, y, z, w). The language signature contains also the binary predicate ≤ which is defined only for temporal variables and which is interpreted by a linear order over the temporal active domain included in N + .

In order to make a fair comparison with TL (respectively TL * ) we will consider queries whose answers contain only data values and no free temporal variables (resp. one temporal variable). The corresponding language is denoted by FO(≤) (respectively FO * (≤)). Definition 2.4 (Query in FO(≤)) A query in FO(≤) over R is an expression of the form {( x) | φ( x)}, where φ( x) is a formula of FO(≤) over R ts where the free variables x are data variables. The answer of Q evaluated on a timestamp temporal instance I ts is defined as for relational calculus, where valuations of variables range over the active domain of I ts . Definition 2.5 (Extended query in FO * (≤)) A query in FO * (≤) over R is an expression of the form {( x, t) | φ( x, t)}, where φ( x, t) is a formula of FO * (≤) over R ts where the free variables x are data variables. The answer of Q evaluated on a timestamp temporal instance I st is defined as for relational calculus, where valuations of variables range over the active domain of I st .

In the following, FO(=) and FO * (=) denote the restriction of the previous query languages where the predicate ≤ and the temporal constants are not allowed. Thus, the only possible atomic formulas involving temporal variables are those of the form t = s, where both t, s are temporal variables.

Example 2.6 Let R and I be the database schema and temporal instance of figure 1.

The TL query {(x) | R(x) ∧ F R(x)} evaluated on I returns {a, b, c}. The TL * query {(x, t) | R(x) ∧ F R(x)} evaluated on I returns {(a, 1
), (b, 1), (c, 1), (d, 2)}. These queries can be equivalently expressed in FO(≤) and FO * (≤) by the expressions {(x) | ∃t(first(t)∧R ts (x, t)∧∃s(t < s∧R ts (x, s)))} and {(x, t) | R ts (x, t)∧∃s(t < s∧R ts (x, s))} respectively. The formulas t < s and t > s are abbreviations for t ≤ s ∧ t = s and s ≤ t ∧ s = t respectively and the formula first(t) is an abbreviation for ¬∃u(u < t). Definition 2.7 (Global and Initial Equivalence) Two formulas are said to be globally equivalent if the corresponding extended queries are equivalent. They are initially equivalent if the corresponding queries are equivalent.

Known results concerning TL and FO(≤).

In [START_REF] Gabbay | On the Temporal Basis of Fairness[END_REF] and in [START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF] it is shown that, in the propositional case, TL and FO(≤) are globally equivalent, which means that the query languages TL * and FO * (≤) have the same expressive power. This implies initial equivalence between TL * and FO * (≤), which simply means that the query languages TL and FO(≤) have the same expressive power.

However, [START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps in Temporal Query Languages[END_REF][START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps to Query Temporal Databases[END_REF] have proved that in the first order case, the equivalence between TL and FO(≤) does not hold, and so, these query languages have different expressive power.

Theorem 2.8 [1, 2] TL FO(≤)

The property separating TL from FO(≤), which we call twin, checks if the input temporal instance contains two identical states. This property can be expressed in FO(≤) by ∃i∃j(i = j ∧ ∀x[S st (x, i) ↔ S st (x, j)]) and its satisfiability does not depend on the ordering of the states I 1 , I 2 , . . . , I n in I. The technique employed in [START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps in Temporal Query Languages[END_REF][START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps to Query Temporal Databases[END_REF] in order to prove that twin is not expressible in TL is based on communication protocols [START_REF] Kushilevitz | Communication Complexity[END_REF]. In section 4, we will prove the same result using a more classical technique based on Ehrenfeucht-Fraïssé's games. In order to do so, we will first give a syntactic characterization of the order independent properties expressible in TL. This is the main issue of the next section.

3 The temporal query language TL(E i )

In this section we introduce a very simple implicit temporal language which deals with an (implicit) temporal instance I as a set of states rather than a sequence of states. In other words, this language completely ignores the ordering of the states in a temporal instance.

The main result of this section (Theorem 3.15) guarantees that this language, denoted by TL(E i ), expresses exactly the properties of TL which are order independent. It contains an enumerable set of operators E i (i ≥ 1). Intuitively, a formula E i ϕ expresses that there exists i distinct states satisfying ϕ.

Definition 3.1 [Syntax]

We define the language TL * (E i ) by adding the following extra rule to the usual formation rules of first order logic:

• If ϕ is a formula then E i ϕ is a formula for any i ∈ N.

The formulas of TL(E i ) are the formulas of the form E i ϕ where ϕ is in TL * (E i ).

[Semantics] Given a temporal instance I=(I 1 ,. . ., I n ), an instant j and a valuation ν of the variables ,

• [I,j,ν] |= tl E i ϕ if and only if there exists i distinct instants j 1 , . . . , j i , such that [I,j k ,ν] |= tl ϕ for each k ∈ {1, . . . , i}.

The notions of a TL(E i ) query, TL * (E i ) query and their answers are defined as for TL and TL * queries (definition 2.2 and 2.3).

For instance, the query E 2 ∃xR(x) evaluated on a temporal instance I, expresses the existence of two states in I with non-empty set R.

We will need later on the following definitions:

Definition 3.2
The quantifier temporal rank of a formula ϕ of TL * (E i ), denoted by qtr(ϕ), is defined as

: (i) qtr(ϕ) = 0 if ϕ is atomic; (ii) qtr(ϕ 1 ∧ ϕ 2 ) = max{ qtr(ϕ 1 ), qtr(ϕ 2 ) }; (iii) qtr(¬ϕ) = qtr(ϕ); (iv) qtr(∃xϕ) = qtr(ϕ)+1; (v) qtr(E i ϕ 1 ) = qtr(ϕ 1 ) + 1.
The width of a TL * (E i ) formula, denoted by wth(ϕ), is defined in the same way except for (v) wth(E i ϕ 1 )= max{i, wth(ϕ 1 )}.

For instance, consider the formula ϕ = ∃xE 2 (∀yE 3 (R(x, y))). In this case, we have: qtr(ϕ) = 4 and wth(ϕ) = 3.

The following proposition is an immediate consequence of definition 3.1: Proposition 3.3 Let ϕ be a formula of TL(E i ). Let I = (I 1 , I 2 , . . . , I n ) be a temporal instance, i ∈ {1, . . . , n} and ν a valuation of variables. Then:

[I, i, ν] |= tl ϕ ⇐⇒ ∀k, 1 ≤ k ≤ n, [I, k, ν] |= tl ϕ
The following proposition establishes, as expected, that the language TL(E i ) is a sublanguage of both TL and FO(=).

Proposition 3.4 TL * (E i ) ⊆ TL * ∩ FO * (=), i.e., for each formula ϕ ∈ TL * (E i ) there exists a formula ϕ tl ∈ TL * (respectively a formula ϕ f o ∈ FO * (=)) such that ϕ is equivalent to ϕ tl (respectively to ϕ f o ).
Proof : The proof of the inclusion TL * (E i ) ⊆ FO * (=) does not present any difficulty and relies on the natural translation of TL * (E i ) formulas into FO * (=). Next, we prove that TL * (E i ) ⊆ TL * . This is achieved by induction on the structure of TL * (E i ) formulas. For the initial step and the induction steps refering to boolean combinations and quantification of TL * (E i ) formulas, the proof is straightforward. Let ϕ = E i ψ, where ψ is a TL * (E i ) formula. Without loss of generality, we consider the case where i = 2, the other cases can be treated in a similar way. By the induction hypothesis, ψ is equivalent to a TL * formula ψ tl . It is easy to check that ϕ is equivalent to the following TL * formula: (ψ tl ∧F ψ tl )∨(ψ tl ∧P ψ tl )∨(F (ψ tl ∧F ψ tl ))∨(F ψ tl ∧P ψ tl )∨(P (ψ tl ∧P ψ tl )).

Next, we will characterize the fragment of FO * (≤) and FO * (=) which are equivalent to TL * and TL * (E i ) respectively. In order to do this, let us consider the language FO * tl (≤) that is the set of FO * (≤) formulas such that each of their subformulas in the scope of a data quantifier has at most one free temporal variable. For instance, the formula ∃i∃j(i = j ∧ ∀x[S st (x, i) ↔ S st (x, j)]) does not belong to FO * tl (≤), because its subformula [S st (x, i) ↔ S st (x, j)] lies in the scope of the data quantifier ∀x and has two free temporal variables i and j. In the same way, we can define the language FO * tl (=) as a sublanguage of FO * (=).

The following theorem gives the desired syntactic characterization of the fragments of FO * (≤) and FO * (=) equivalent to the implicit temporal languages TL * and TL * (E i ) respectively. Note that part (1) of the following theorem was independently obtained in [START_REF] Hodkinson | Decidable fragments of first-order temporal logics[END_REF] and was used in order to show decidability of the satisfiability problem for the monadic fragment of TL. The proof of Theorem 3.5 will make use of two intermediate results. The first one has been shown in [START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF][START_REF] Gabbay | On the Temporal Basis of Fairness[END_REF] and establishes that the propositional fragment of TL * is equivalent to FO * (≤) (without data variables). The second one (lemma 3.6) establishes a similar equivalence between the propositional fragment of TL * (E i ) and FO * (=).

Lemma 3.6 Propositional TL * (E i ) is equivalent to FO * (=).
Proof : (⊆) follows from Proposition 3.4. We thus concentrate on the proof of (⊇). Let p 1 , . . . , p k be the propositions in the signature of TL * (E i ). Because we don't have access to the order here, a temporal instance can be viewed as a set of states, instead of a sequence of states as in the general setting. For each state I, its type is the tuple (u 1 , . . . , u k ), where u i is the truth value of proposition p i at state I, for i ∈ {1, . . . , k}. Let Θ be the set of all possible types, thus the cardinality of Θ is 2 k . Because each state is fully characterized by its type, a temporal instance I (with no order) is thus characterized by a function α I from Θ to N which associates to each type τ the number of states of type τ in I. For each type τ , it is naturally associated a propositional formula φ τ : for instance, if τ = (1, 0, 0, 1) then

φ τ = p 1 ∧ ¬p 2 ∧ ¬p 3 ∧ p 4 .
So, if τ is the type of a state I then φ τ is true at a state J if and only if J = I. Now let ϕ ∈ FO * (=). Assume without loss of generality that ϕ never quantifies twice over the same variable name. Let r be the number of variables occurring in ϕ. From classical finite model theory we know that first order formulas with only r variables can only count up to r without the presence of an order [START_REF] Ebbinghaus | Finite Model Theory[END_REF]. Let A r be the finite set of pairs (I, i) where I = (I 1 , ..., I n ) is a temporal instance such that a given type τ never occurs more than r times (∀τ ∈ Θ α I (τ ) ≤ r) and i ∈ {1, . . . , n}. For each pair (I, i) of A r , let ψ I,i be the formula of TL * (E i ):

τ i ∧ τ ∈Θ E α I (τ ) φ τ , where τ i is the type of state I i . Let A 1 r (respectively A 2 r
) be the subset of A r of pairs (I, i) such that ϕ is true (resp. false) on I at instant i. Consider the following formula ψ of TL * (E i ):

(I,i)∈A 1 r ψ I,i ∧ (I,i)∈A 2 r ¬ψ I,i
It is easy to verify that ψ and ϕ agree on all pairs (I, i) in A r . We have already seen that ϕ can count the multiplicity of an occurrence of a type only up to r. It is easy to verify that this is also the case for each ψ I,i constructed above and therefore for ψ. We will show that ϕ and ψ agree on all pairs (I,i) (and not only on those in A r ). Indeed, if I = (I 1 , . . . , I n ) is a temporal instance, consider I r = (J 1 , . . . , J m ) the temporal instance which contains exactly the same types as in I with the same multiplicity if this one is less than r and r otherwise (α Ir (τ ) = min{r, α I (τ )}). For instance, if I = (I, J, J) and r = 1 then I 1 = (I, J). Let i ∈ {1, . . . , n}. Then, there exists j ∈ {1, . . . , m} such that (a) [I, i] |= tl ψ if and only if [I r , j] |= tl ψ and (b) [I, i] |= ϕ if and only if [I r , j] |= ϕ1 (we take j such that J j = I i ). Because (I r , j) ∈ A r , ψ and ϕ have the same truth value on (I r , j). Thus they have the same truth value on (I, i). This proves the Lemma.

Remark 3.7 Note that the proof of the Lemma 3.6 shows that the formula of FO * (=) with r variables are equivalent to a formula of TL * (E i ) of quantifier temporal rank 1 and width r. This fact will be needed later on.

Proof of Theorem 3.5: The inclusion of TL * into FO * tl (≤) is easily proved by considering the natural translation of a TL * formula into a FO * (≤) formula. The same argument can be used to show that TL * (E i ) is included in FO * tl (=). Let us prove the inclusion FO * tl (=) ⊆ TL * (E i ). This proof is by induction on the quantifier-data depth of a formula f (t, x) in FO * tl (=) which is defined as follows: (i) qdd(f ) = 0 if f is atomic; (ii) qdd(f ∧ g) = max{qdd(f ),qdd(g)}; (iii) qdd(¬f ) = qdd(f ); (iv) qdd(∃tf ) = qdd(f ) if t is a temporal variable; (v) qdd(∃xf ) = 1 + qdd(f ) if x is a data variable. Initial step: Let qdd(f ) = 0 (f does not contain any data quantifier). We apply the following transformations on f : atomic formulas of the form R(s, z) are replaced by unary predicates R z (s) and atomic formulas of the form (y 1 = y 2 ) or (y = a) are replaced by unary predicates EQ y 1 =y 2 (t) and EQ y 1 =a (t) respectively. Remind that t is the only free variable of f and that the interpretations of the equality predicate involving data variables or constants and the interpretation of constants are time-invariant (in the database context). After this transformation, we obtain a formula ϕ(t) of FO * (=). By Lemma 3.6, there exists a propositional TL * (E i ) formula θ which is equivalent to ϕ(t). Now, the "propositions" R z , EQ y 1 =y 2 and EQ y 1 =a in θ are replaced by the corresponding atomic formula R( z), (y 1 = y 2 ) and (y 1 = a). In this way, we obtain a formula θ f in in TL * (E i ) which is equivalent to f .

∧ ∃y ∨ ∀w R(s, x, w) P (s, x, y) ∀z T (t, x, z) Q(s, x) ∃s R 1 x (s) R 2 x (t) Qx(s) ∧ Figure 2: Transformation of the FO * tl (=) formula f (t, x) into the FO * (=) formula ϕ(t)
Induction step: Suppose the inclusion holds for formulas with quantifier-data depth

≤ n and let f (t, x) = Q 1 y 1 . . . Q m y m g(t, x) ∈ FO * tl (=) with qdd(f ) = n + 1
, where m ≥ 0, t is a temporal variable, x are the free data variables of f , Q i are quantifiers (∃ or ∀) and y 1 . . . y m are data variables included in x. Case 1: m = 0 -Let us consider the data-quantified subformulas of f , which are formulas of the form ∃xh(s, x, y), where s is a temporal variable, x is a data variable and y is a set of data variables. We say that a data-quantified subformula h 1 is maximal if it is not a subformula of another data-quantified subformula h 2 with h 1 = h 2 . For each maximal data-quantified subformula ∃xh(s, x, y) of f we associate a new relational symbol R, with arity equal to the number of variables in y. We replace the maximal data-quantified subformulas ∃xh(s, x, y) of f by the corresponding atomic formulas R(s, y). The maximal data-quantified subformulas of f with no free temporal variable are replaced in the same way, by an atomic formula R(t, y). So, after this transformation we obtain a FO * tl (=) formula f ′ with qdd(f ′ ) = 0. In this case, we have already shown that there exists a TL * (E i ) formula θ f ′ which is equivalent to f ′ . Figure 2 illustrates the idea: the FO * tl (=) formula f (t, x) = ∃s(∃y(∀wR(s, w, z) ∨ S(s, x, y))

∧ ∀zT (t, x, z) ∧ Q(s, x)) transforms into a FO * (=) formula ϕ(t) = ∃s(R 1 x (s) ∧ R 2 x (t) ∧ Q x (s)), which is equivalent to a propositional TL * (E i ) formula.
Let us consider each maximal data-quantified subformula ∃xh(s, x, y) of f . It is clear that qdd(h(s, x, y)) = n. Applying the induction hypothesis on h(s, x, y), we obtain an equivalent TL * (E i ) formula θ h (x, y). So, ∃xh(s, x, y) is equivalent to the TL * (E i )formula ∃xθ h (x, y). Now, we replace the "propositions" R y in θ f ′ (which "encapsulates" the maximal data-quantified subformulas) by the equivalent TL * (E i ) formulas. In this way, we obtain a formula θ f in TL * (E i ) which is equivalent to f . Case 2: m > 0 -From Case 1, we know that there exists θ g ∈ TL * (E i ) which is equivalent to g. Then Qy 1 . . . Qy m θ g is equivalent to f . The proof of the other inclusion FO * tl (≤) ⊆ TL * is obtained in the same way, using the Lemma 3.6 instead of Kamp's Theorem.

Remark 3.8 The proof of Theorem 3.5 showed the importance of blocks of temporal variables in the translation, a block being defined as a set of temporal variables quantified between two data quantifications. Remark 3.7 and the same induction as in the proof of Theorem 3.5 shows that a formula of FO * tl (=) is translated into a formula of TL * (E i ) whose width corresponds to the maximal size of blocks in the formula and whose quantifier temporal rank is counted in the standard way but adding one for each block instead of the full size of the block. Corollary 3.9 The explicit query languages FO tl (≤) and FO tl (=) are (initially) equivalent to the implicit query languages TL and TL(E i ) respectively.

Proof : The equivalence between FO tl (≤) and TL follows immediately from Theorem 3.5 (a) and the inclusion TL(E i ) ⊆ FO tl (=) relies on the natural translation of TL(E i ) formulas into FO tl (=). Conversely, let f be a FO tl (=) query. We define the maximal temporal quantified subformulas of f in a similar way as we have defined the maximal data quantified subformulas in the proof of Theorem 3.5. From Theorem 3.5(b), each such formula ∃tg(t, x) is globally equivalent to E 1 ϕ, where ϕ is a TL * (E i ) formula. Then, it is clear that f is globally equivalent to a formula ψ in the closure of TL(E i ) with respect to the boolean combinations and quantification. Notice that ψ is not necessarily in TL(E i ). By applying Proposition 3.3 to the formula ψ, we conclude that f is initially equivalent to the TL(E i ) formula E 1 ψ. Corollary 3.9 provides a syntactic characterization of the queries in FO(≤) and FO(=) which are equivalent to queries in TL and TL(E i ) respectively. We are going to use this syntactic characterization in order to prove the main result of this section, Theorem 3.15, establishing that TL(E i ) corresponds exactly to the order independent properties expressible in TL.

We start by a semantic characterization of the properties expressible in TL which are order independent. Intuitively this means that the property is not affected by a reordering of the states of a temporal instance. We do not take the standard definition of order independence which consists of being unaffected by a reordering over a finite temporal instance. Instead we consider a stronger variant which requires the property to be also unaffected by a reordering over infinite instances. The reason for this is detailed below. Definition 3.10 A property P is said to be order independent if, for any temporal instance (finite or infinite) I = (I i ) i∈V and for any bijection s of V , we have: I satisfies P iff I s satisfies P, where I s = (I s(i) ) i∈V .

An important condition for being order independent is that it should be the case for both finite and infinite instances. Infinite means here that the temporal instance may contain infinitely many states, each of them being possibly over an infinite active domain. With the weaker notion of order independence which only considers finite instances, Theorem 3.15 stating that the order independent properties expressible in TL are exactly the ones expressible in TL(E i ) doesn't hold as we now show.

Gurevich gave an example of a query which is generic, expressible in FO(≤), but not in FO(=) (see exercise 17.27 in [START_REF] Abiteboul | Foundations of Databases[END_REF]). In this context, the genericity of a query corresponds to invariance up to isomorphisms over finite databases but it can easily be modified in order to give an order independent TL query as follows:

Example 3.11 Consider (finite) implicit temporal instances over the database schema containing only one unary relation S. Recall that each such an instance is a finite sequence I = (I i ) i∈V of finite states. For each non-empty subset W of states, an element x W of the active domain of S is called a witness for W if ∀i ∈ V x W ∈ I i (S) iff I i ∈ W . Consider the temporal instance depicted in Figure 3. It has a witness for each subset of {I 1 , I 2 , I 3 }. Indeed a is a witness for {I 1 } because it is in S only in the first state, c is a witness of {I 3 }, f is a witness for {I 1 , I 3 }, and so on. Consider the TL(E i ) query q 1 which says that for each non-empty subset W of V there exists a witness x W . The query q 1 can be expressed in TL(E i ) by establishing that: (1) all singletons W have a witness and (2) the set of (finite) sets of states having a witness is closed under finite union. This is done as follows.

1. ¬E 1 (∀x[E 2 (S(x)) ∨ ¬S(x)])

∀x ∀y ∃z ¬E 1 (¬(S(z) ↔ (S(x) ∨ S(y)))

For example it is easy to verify that the instance depicted in Figure 3 verifies q 1 . Consider now the query q of TL which selects the implicit temporal instances satisfying q 1 and having an even number of states. This can be done by adding to q 1 the query q 2 which checks for the existence of a witness for the subset containing exactly one state out of two in the order given by the sequence (i.e. the subset {I 1 , I 3 , . . . , ...}). The query q 2 can be expressed in TL by:

∃x[S(x) ∧ Next(¬S(x)) ∧ G(S(x) ↔ Next(¬S(x)))]
It can be verified that the instance of Figure 3 does not satisfy q 2 . For instance, f cannot be a valuation for x: it is clear that I 1 |= S(f ), I 2 |= ¬S(f ) and I 3 |= S(f ). But, because S(f ) ↔ Next(¬S(f )) has to be verified at I 3 then I 3 must verify Next(¬S(f )). However, this is not the case, since there is no state I i with i > 3.

Notice first that the query q = q 1 ∧ q 2 is order independent (in the weak sense). Indeed q 1 insure that there is a witness for each subset which is a finite union of singleton. For finite instances it thus insure the existence of a witness for any subset. This first characteristic is trivially order independent. Therefore, if a temporal instance has an even number of states, no matter how we reorder them, there will always be a witness for the subset containing all the states of even position.

Because q checks for a parity condition, a standard Ehrenfeucht-Fraïssé's games argument shows that q cannot be expressed in FO(=) and therefore in TL(E i ).

Notice now that q is not order independent in the strong sense. Indeed q 1 only guarantees the existence of a witness for each finite subset. If the temporal instance is infinite it does not imply the existence of a witness for any subset. To see that q is indeed not order independent in the strong sense consider the following example.

Let (V i ) i∈N + be an enumeration of the finite subsets of N + such that V 1 corresponds to the emptyset. Let W be the subset of all odd numbers.

Consider the following infinite temporal instance I = (I i ) i∈N + over the domain (x i,j ) i∈N + ,j∈{0,1} , such that I k |= S(x i,0 ) iff k ∈ V i and I k |= S(x i,1 ) iff k ∈ V i or k is odd. Intuitively I is constructed in such a way that x i,0 is a witness for the finite set V i and x i,1 a witness for the set W ∪ V i .

Notice first that I satisfies q 2 because x 1,1 is a possible valuation for x in q 2 . By construction I contains a witness for exactly each subset U which is either finite or the union of W with a finite set. Thus I satisfy q 1 and therefore q.

Consider now the infinite temporal instance J = (I 1 , I 3 , I 2 , I 4 , I 5 , I 7 , I 6 , I 8 . . .). It can be checked that J does not satisfy q 2 and therefore q. Thus q is not order independent in the strong sense.

If the notion of genericity is extended in order to indicate invariance up to isomorphisms over any (finite or infinite) databases, it is folklore knowledge (as a consequence of Craig Interpolation Theorem, [START_REF] Chang | Model Theory[END_REF]) that FO(≤) and FO(=) express exactly the same extended generic queries.

As we will use exactly the same ideas we recall here how the above result can be proved.

Theorem 3.12 [Folklore] Let P be an extended generic query expressible in FO(≤). Then P is expressible in FO(=).

Proof: The proof is by contradiction. Assume that there is a query f expressible in FO(≤) which is extended generic and not expressible in FO(=). Let lin(R) be a FO(R) formula expressing the fact that R is a binary predicate corresponding to a linear order. Let f 1 (R) the following FO(R) formula lin(R) ∧ f (R) and let f 2 (S) be the following FO(S) formula: lin(S) → f (S), where f (R) is the formula obtained from f after replacing in it all occurrences of the symbol ≤ by R. Because f is extended generic, we have for any (finite or infinite) instance:

I |= ∃R f 1 (R) → ∀S f 2 (S).
We now need the following Lemma which is an equivalent rephrasing of Craig Interpolation Theorem [START_REF] Chang | Model Theory[END_REF]. We have seen above that f 1 and f 2 satisfy the premises of Lemma 3.13 and thus there exists h in FO(=) such that for all temporal instances (finite or infinite) I we have: (i) I |= ∃R f 1 (R) → h and (ii) I |= h → ∀S f 2 (S). We now prove that f (≤) and h actually define the same property. Indeed, let I be any instance and assume that I satisfies f (≤), then I satisfies ∃R f 1 (R) (the order ≤ of I being a valid assignment for R). From (i) we conclude that I satisfies h. Assume now that I satisfies h, from (ii) we conclude that I satisfies ∀S f 2 (S) and, in particular, f 2 (≤) is true in I and therefore I satisfies f (≤).

This prove the theorem.

We are looking for a variant of Theorem 3.12 for order independent queries, TL and TL(E i ). Recall from Corollary 3.9 that TL is equivalent to FO (≤) and that TL(E i ) is equivalent to FO tl (=). Moreover the linearity of a relation R can also be expressed in FO tl (=) thus the proof of Theorem 3.12 can be readily applied to show that the order independent queries of FO tl (≤) are expressible in FO tl (=) as long as a Craig Interpolation Theorem (Lemma 3.13) holds for FO tl . This Craig Interpolation Theorem could be prove using an adaptation of the standard case to our special setting. But it turns out that this result also falls into a more general picture. Indeed [START_REF] Barwise | Interpolation, Preservation, and Pebble games[END_REF] showed that, in general, Craig interpolation holds for a logic L as long as there exists a precise characterization of the logic using Ehrenfeucht-Fraïssé games such that winning strategies can be expressed in the logic. We will prove such a characterization in Theorem 4.5 of Section 4. From Theorem 4.5 and [START_REF] Barwise | Interpolation, Preservation, and Pebble games[END_REF] we thus have:

Lemma 3.14 Let f ∈ FO tl (R) and g ∈ FO tl (S) be such that ∃R f (R) |= ∀S g(S).
Then there exists h ∈ FO tl (=) such that:

∃R f (R) |= h and h |= ∀S g(S).
Lemma 3.14 and Corollary 3.9 immediately yield: Theorem 3.15 Let P be an order independent property expressible in TL. Then P is expressible in TL(E i ).

Corollary 3.16 TL(E i ) ≡ TL ∩ FO(=).

Proof: The inclusion from left to right follows immediately from Proposition 3.4. For the converse inclusion: Let f be a property expressible in TL and in FO(=). Because f is expressible in FO(=), f is order independent. As f is also expressible in TL, Theorem 3.15 applies and we can conclude that f is expressible in TL(E i ).

TL(E i ) Expressiveness

This section is devoted to investigating the expressive power of the query language TL(E i ). We will establish that this language is unable to express all order independent properties. Because of Theorem 3.15 stating that order independent properties in TL are in TL(E i ), it will moreover provide a new proof that TL is strictly less expressive than FO(≤).

The main result of this section states that:

Theorem 4.1 TL(E i ) FO(=) and more precisely, the query twin cannot be expressed in TL(E i ).

As a matter of fact, we will prove that the query twin cannot be expressed in TL * (E i ). Recall that the formulas in TL * (E i ) are build using the first order rules plus the E i modalities without restriction concerning the encapsulation under E i modalities that holds for the language TL(E i ). In order to prove this result, we develop a technique à la Ehrenfeucht-Fraïssé based on two-player games. Ehrenfeucht-Fraïssé's games [START_REF] Ebbinghaus | Finite Model Theory[END_REF] offer an elegant alternative semantics for first order logic and provide a methodology for proving that a property is not definable in classical first order logic.

Next, we proceed in a very classical manner to the presentation of two-player games for our temporal language TL * (E i ). We then show that these games characterize TL * (E i ) definable properties: two temporal instances can be distinguished by a TL * (E i ) property if and only if these two instances can be distinguished by our games. Our games, called T-games, are in fact very similar to Ehrenfeucht-Fraïssé's games. We just need to modify and add rules in order to take into account the modalities E i of the temporal language TL * (E i ).

From now on, we use the following objects:

• I = (I 1 , . . ., I n ) and J = (J 1 , . . ., J m ) are two temporal instances over the same vocabulary (same schema), whose domains are respectively dom I and dom J .

• a = (a 1 , . . . , a s ), respectively b = (b 1 , . . . , b s ) are two vectors of s elements of dom I , respectively dom J .

• x = (x 1 , . . . , x s ) is a vector of s variables.

• int I , respectively int J are the sets of indices {1, . . . , n}, respectively {1, . . . , m}.

• i 0 and j 0 are indices in int I , respectively int J .

A T-game is played by two-players. One of the player is called the spoiler and the other one is named the duplicator. They play with two kinds of pebbles: a bunch (sufficiently many) of pairs (p 1 , q 1 ), . . . , (p k , q k ) of data pebbles and one pair (t I , t J ) of temporal pebbles. One move of the game consists of either a data move (d-move) or a temporal move (t-move).

Data move:

The spoiler chooses a pair of data pebbles (p i , q i ) and either places the pebble p i on an element of dom I or places the pebble q i on an element of dom J . Then, in the first case, the duplicator ought to answer (in J ) by placing the pebble q i on an element of dom J and alternatively in the second case by placing the pebble p i on an element of dom I . Thus at the end of the d-move the pair of data pebbles (p i , q i ) is instantiated with a pair (a, b) of dom I ×dom J . Note that d-moves of T-games are exactly the moves described in Ehrenfeucht-Fraïssé's games for classical first order logic.

Temporal move of width w: This move is decomposed in two steps. (Step 1)

The spoiler chooses to play in I (respectively in J ). He picks a sequence (i 1 , . . . , i w ) of w distinct integers in int I (respectively in int J ). The duplicator is then obliged to play in the opposite instance and picks a sequence (j 1 , . . . , j w ) of w distinct integers in int J (respectively in int I ). Note here that none of the sequences are required to be ordered. (Step 2) Finally, the spoiler makes the choice of a pair (i k , j k ) of integers which becomes the instantiation of the temporal pebbles (t I , t J ). Note that, sometimes it may be impossible to play a t-move of width w. This may happen when the length of one of the instances I or J is less than w. Such a situation is refered to as an uncompleted t-move.

In general, for a T-game, some data pebbles (of course pairs of pebbles) could be placed before any round is started. It is also assumed that each round of a T-game always starts with an instantiation (i 0 ,j 0 ) of the temporal pebbles. T G r (I, i 0 , a, J , j 0 , b) denotes a T-game played with r + s pairs of data pebbles, in r moves and such that the temporal pebbles are initialized by (i 0 ,j 0 ), and for i = 1..s, the data pebbles pairs (p i , q i ) are initialized by (a i , b i ).

Let us now explain how a round of such a T-game is played by the spoiler and the duplicator. A round is a sequence of at most r moves, each move is either a d-move or a t-move as described above and the sequence satisfies the following restrictions:

• Restriction on d-moves: If a move is the d th d-move of the round then it instantiates the (s + d) th data pairs of pebbles. Note that the spoiler is forced to choose a new pair of data pebbles at each d-move. Because one has reserved sufficiently many pairs (r + s) of data pebbles, a round may be composed of dmoves only. But in general, it can happen that at the end of a round some pairs of data pebbles have not been used.

• Winning completed moves: After a move is completed, assume that the instantiation of (t I , t J ) is (i, j) and that (a 1 , b 1 ), . . . , (a s+d , b s+d ) are all the instantiations of the played data pebbles (meaning that d d-moves have been played already). Let us denote α the mapping defined over {a l | l = 1 . . . (s + d)} by α(a l ) = b l . The duplicator wins the current move if the mapping α is a partial isomorphism of the states I i and J j .

• Uncompleted t-moves: An uncompleted t-move is a winning move for the spoiler and thus a loosing move for the duplicator.

• Next move: If the duplicator wins the move then the round can continue if the number of moves already played is strictly less than r.

The duplicator wins a round of the T-game T G r (I, i 0 , a, J , j 0 , b) if the round terminates after r moves and the last move is a winning move for the duplicator. It should be clear that the only case where a round of a T-game ends before r moves have been played is when the duplicator looses a move.

The duplicator has a winning strategy for the game T G r (I, i 0 , a, J , j 0 , b) if he/she is able to win all possible rounds. A winning strategy for the duplicator is denoted by (I, i 0 , a) ∼ r (J , j 0 , b). It is quite easy to show from the definition of the T-games that the relation ∼ r is an equivalence relation. Intuitively, the equivalence (I, i 0 , a) ∼ r (J , j 0 , b) indicates that the temporal instances I and J cannot be distinguished by looking at several instants and focussing only on restricted sets of constants, the observation starting at the instant i 0 with the elements a for the temporal instance I and at the instant j 0 with the elements b for the temporal instance J .

In the following, we may need to restrict the width of the temporal moves of a T-game to be bounded. We write (I, i 0 , a) ∼ w r (J , j 0 , b) to denote that the duplicator has a winning strategy for the game T G w r (I, i 0 , a, J , j 0 , b) whose t-moves have a width less or equal to w.

Example 4.2 Let us consider2 the binary relational schema R and the two states I and J depicted as graphs in figure 4. If we consider the temporal instances I = (I) and J = (J), it is quite trivial to see that the duplicator has a winning startegy for the T-Game T G 2 (I, 1, , J , 1, ) which is played in two moves, all data pebbles being off the board before each round. However, the duplicator has no winning strategy for the T-game T G 3 (I, 1, , J , 1, ) with three moves. Indeed, let us consider the round starting by the two d-moves (1,1), [START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps to Query Temporal Databases[END_REF][START_REF] Abiteboul | Temporal Connectives Versus Explicit Timestamps to Query Temporal Databases[END_REF]. Then assume that the spoiler places the data pebble p 3 over 3 in I. The duplicator is unable to answer appropriately because (1,2), (2,3) and (3,1) are "edges" in I but there is no a ∈ dom J such that (1,2), (2,a) and (a, 1) are in J . Let us now consider the temporal instances I = (I,I,J,I) and J = (I,J,I,J). It is not difficult to check that the duplicator has a winning strategy for the T-game T G 3 (I, 1, , J , 1, ) because even in a situation where for instance the initial move is a t-move of width 4 and where the duplicator is forced by the spoiler to put a state I in correspondence with a state J, by the first part of the example, we can infer that the duplicator has a winning strategy for the following 2 moves. Let us detail the first t-move: the spoiler starts by picking the 4 instants (1, 2, 3, 4) in I; the duplicator answers by the 4 instants (1, 3, 2, 4); finally the spoiler chooses to instantiate the time pebbles with the pair [START_REF] Barwise | Interpolation, Preservation, and Pebble games[END_REF][START_REF] Barwise | Interpolation, Preservation, and Pebble games[END_REF]. If the two following moves are d-moves, the duplicator has a winning strategy. Of course, he/she has a wining strategy for the two following moves.

However, considering the T-game T G 4 (I, 1, , J , 1, ) with 4 moves, leads to a winning strategy but this time for the spoiler. Indeed, the duplicator maintains a winning strategy for the T-game T G 2 4 (I, , 1, J , 1, ) that is, when restricting the width of tmoves to be 1 or 2. But as soon as t-moves of width 3 are allowed, during an initial t-move, the spoiler is able to force the duplicator to put a state I in correspondence with a state J and then, by the first part of the example, we know that the duplicator has no winning strategy for the 3 moves that remain to be played if these moves are d-moves.

We now turn to the fundamental relationship between our T-games and the temporal language TL * (E i ). As a matter of fact, we establish that the equivalence relation ∼ w r characterizes the elementary equivalence ≡ w r of instances with respect to the language TL * (E i ).

Definition 4.3 The temporal instances I and J are w r -equivalent with respect to a, b and with respect to the instants i 0 , j 0 , and we write (I, i 0 , a) ≡ w r (J , j 0 , b) iff for all formula ϕ in TL * (E i ) such that qtr(ϕ) ≤ r and wth(ϕ) ≤ w, we have:

[I, i 0 , ν a ] |= tl ϕ iff [J , j 0 , ν b ] |= tl ϕ
where the valuations ν a and ν b are defined by ν a (x l ) = a l , respectively ν b (x l ) = b l .

The relationship between the duplicator having a winning strategy for a T-game T G w r played over two temporal instances I and J and the equivalence of these two temporal instances with respect to TL * (E i ) formulas having a quantifier temporal rank bounded by r and a width bounded by w will be formally established by Theorem 4.5. The purpose of the following example is to illustrate this relationship.

Example 4.4 For instance, as we have seen in the second part of example 4.2, (I, 1, ) ∼ 3 4 (J , 1, ). Indeed, the spoiler's winning strategy summarized in this example can be viewed as playing the following formula F:

E 3 (∃x 1 ∃x 2 ∃x 3 (R(x 1 , x 2 ) ∧ R(x 2 , x 3 ) ∧ R(x 3 , x 1 )))
Note that the quantifier temporal rank of this sentence is 4 and its width is 3. Note of course that (I, 1, ) ≡ 3 4 (J , 1, ), because [I, 1] |= tl F and [J , 1] |= tl F.

In order to establish the relationship between equivalence of temporal structures and winning strategies for certain T-games, we need an intermediate technical tool which is a slight variant of the Hintikka formulas [START_REF] Ebbinghaus | Finite Model Theory[END_REF]. The T-Hintikka formulas Φ a,i 0 ρ,w [I]( x, t), associated with the temporal instance I and the vector a at time points i 0 with free variables x, t, are intended to capture all FO * tl (=) formulas which are satisfied by I at i 0 given the valuation ν a of the free variables x. These formulas are inductively defined as follows:

• Φ a,i 0 0,w [I]( x, t) is the conjunction of all atomic formulas φ( x, t) such that [I, i 0 , ν a ] |= φ( x, t).

• for ρ ≥ 1:

Φ a,i 0 ρ,w [I]( x, t) = Φ a,i 0 ρ-1,w [I]( x, t) a∈dom I ∃x s+1 Φ aa,i 0 ρ-1,w [I]( xx s+1 , t)
strategy for the T-game TG w r (J , i 0 , a, J , j 0 , b), he/she has a winning strategy for the T-game TG w r-1 (I, i f , a, J , j f , b). More precisely, this entails (by induction hypothesis) that we have both (I, i f , ν a ) ∼ w r-1 (J , j f , ν b ) and (I, i f , a) ≡ w r-1 (J , j f , b). This is a contradiction with the fact that [I, i f , ν a ] |= tl ψ and [J , j f , ν b ] |= tl ψ.

The previous theorem is quite powerful because, as in the framework of classical first order logic, it provides a methodology for determining what cannot be said in the temporal language TL * (E i ). Basically, in order to show that a property P cannot be expressed by a formula in TL * (E i ), it is sufficient to show, for each w and for each r, that there exists two temporal instances I w r and J w r such that, on the one hand I w r satisfies the property P and J w r does not, and on the other hand I w r and J w r cannot be distinguished by a T-game TG w r (i.e. I w r ∼ w r J w r ). This methodology is developed for establishing the following: Lemma 4.6 The twin property is not TL * (E i ) definable, and thus it is not TL(E i ) definable.

Proof: Let us fix both w and r for the rest of the presentation of this proof. The temporal instances that are constructed now are closely related to the ones used by Toman and Niwinski in [START_REF] Niwinski | First Order Queries over Temporal Databases Inexpressible in Temporal Logic[END_REF]. In the sequel, we consider a set S = {1, . . . , 2k + 1}, for k sufficiently big, together with the following pairs of temporal instances I and J (for the sake of readability, we do not insert the indices w and r but the reader should keep in mind that these indices are parameters for building our temporal instances):

• I is an enumeration of the (k+1)-subsets3 of S with exactly two occurrences of each subset. Note that, by definition of I, we have that [I, t] |= tl twin, for any t.

• J is an enumeration of the k-subsets and (k+1)-subsets of S, this time with exactly one occurrence of each subset. Note that, by construction, we have that [J , t] |= tl twin, for any t.

For instance, if k = 1, S = {1, 2, 3}, a possible temporal instance I is {1, 2}, {1, 3}, {2, 3}, {1, 2}, {1, 3}, {2, 3} and a possible temporal instance J is {1}, {2}, {3}, {1, 2}, {1, 3}, {2, 3}. Although it not very important for the remaining, the reader may notice that the temporal instances I and J have the same number of states because of 2k + 1

k = 2k + 1 k + 1
. We are now going to show that these two temporal instances cannot be distinguished by the T-game TG w r . For the time being, we only assume that k is big enough. The exact condition on k will be given later.

In order to show that (I, i 0 , ) ∼ w r (J , j 0 , ) that is, in order to exhibit a winning strategy for the duplicator playing the T-game TG w r (I, i 0 , , J , j 0 , ), we assume that g moves of a round have been successfully played by the duplicator. Consider that d moves among these g moves are d-moves and thus d pairs of data pebbles are instantiated with the pairs of elements (a 1 , b 1 ), . . ., (a d , b d ) on the one hand and the temporal pair of pebbles is instantiated with (i, j). Let us examine the two possible cases for the next (g+1) th move.

[case 1]: The spoiler chooses to play a d-move in I (the dual move in J would be treated in a similar way). Consider that the spoiler places the pebble p d+1 on the element a d+1 of S. Then the duplicator is going to answer with an element b d+1 that he/she will carefully choose such that a d+1 ∈ I i iff b d+1 ∈ J j . Because of the cardinality of S, he/she is always able to make to such a choice.

[case 1]: The spoiler chooses to play a t-move in I and starts by providing v distinct instants i 1 , . . . , i v with v ≤ w. The duplicator is then going to answer as follows. First, he/she considers the set of states of I corresponding to the choice of the spoiler. Let us assume that this set is E={I i 1 , . . ., I iv }. Next, he/she builds the equivalence classes of E induced by the equivalence relation ∂ defined by I t ∂ I t ′ iff I t ∩ {a 1 , . . . , a d }=I t ′ ∩ {a 1 , . . . , a d }. Intuitively, I t and I t ′ are in the same equivalence class if they share the same "played" elements in I. The reader can notice here that the maximal number of equivalent states (or the maximal cardinality of an equivalence class) is less or equal to v and thus to w. Let us denote E 1 , . . . , E z the partition of E induced by ∂. Each class E ℓ is characterized by the set I t ∩ {a 1 , . . . , a d } where I t ∈ E ℓ and that set is enumerated as a h 1 . . . a h ℓ . The cardinality of E ℓ is denoted c ℓ (notice that, c ℓ ≤ w). Then, for a class E ℓ , the duplicator is going to select c ℓ states K in J such that K ∩ {b 1 , . . . , b d } = {b h 1 , . . . , b h ℓ }. This choice entails that each of the c ℓ states K is partially isomorphic to any of the instance in the equivalence class E ℓ . This choice can always be done as soon as the cardinality of the set S on which is based the construction of I and J is big enough. The cardinality 2k+1 of S is determined to satisfy the following: the number of subsets of S including u fixed elements and excluding pu other fixed elements is greater or equal to w + 1 for p = 1 • • • r and u = 1 • • • p. This is insured as soon as k satisfies 2k + 1 -r kr ≥ w + 1. Of course, because of the construction of the duplicator's answer, the second step of the t-move leads to a winning move for the duplicator. Proof: Indeed, if we assume that the property twin can be expressed in TL then Theorem 3.15 entails that twin can be expressed in TL(E i ), since it is order independent. This is a contradiction with the fact that twin cannot be defined in TL * (E i ).

Conclusion

The alternative proof schema provided for showing that TL is strictly less expressive than FO(<) via the syntactic characterization of the order independent properties expressible in TL, seems to open a new direction for similar results concerning other temporal languages as a matter of fact temporal languages that are more expressive than TL. For instance, in [START_REF] Bidoit | Implicit temporal query languages : towards completeness[END_REF], the implicit query language RNTL has been introduced and proved to be more expressive than TL. This language is obtained from TL by adding two new temporal modalities ℵ et ℜ. The operator ℵ, which has been independently introduced in [START_REF] Laroussinie | A hierarchy of temporal logics with past[END_REF], restricts the scope of the usual TL past operators Since and Prev. Usually, the evaluation of the past operators in a TL formula ϕ is made by considering the initial instant 1 as the (unique) origin of time. However, when evaluating a RNTL formula of the form ℵ(ϕ) at an instant t, a new origin of time is created: the instant t of evaluation becomes the starting point with respect to which the past operators of ϕ will be evaluated. The time interval going from 1 to t is temporally "forgotten". The operator ℜ plays a dual role by restoring the time fragments which have been "forgotten" when evaluating subformulas containing ℵ. We will not present here the temporal language RNTL in detail, but only remind some important results concerning its expressive power [START_REF] Bidoit | Implicit temporal query languages : towards completeness[END_REF].

First, RNTL is able to express the twin property. By the way, this property can be expressed in NTL, a sublanguage of RNTL, obtained by adding only the operator ℵ to TL. In fact, the NTL formula expressing twin is the following: F ℵF (∀x(S(x) ↔ P (First ∧ S(x))))

where First is the formula ¬Prev true.

Despite being conjectured in [START_REF] Bidoit | Implicit temporal query languages : towards completeness[END_REF], the equivalence between RNTL and FO(≤) remains an open problem. We think that, using a proof schema similar to the one proposed in the present paper, it is possible to show that RNTL is strictly less expressive than FO(≤). The property which seems to be the candidate to separate these two languages is gen-twin, stating that "each state has a twin". This property can easily be expressed in FO(≤) by the formula ∀i∃j(i = j ∧ ∀x[S st (x, i) ↔ S st (x, j)]). In order to prove that this property cannot be expressed in RNTL, we would have to introduce a counterpart of the language TL(E i ) with respect to RNTL, that is, a language L which expresses exactly the order independent properties of RNTL. And then, we would have to develop a technique based on Ehrenfeucht-Fraïssé's games, in order to show that the order independent property gen-twin is not expressible in the language L.

Figure 1 :

 1 Figure 1: Implicit and explicit time representations

Definition 2 . 2 (

 22 Query in TL) A query Q in TL over a database schema R is specified by an expression of the form {( x) | ϕ( x)} where ϕ( x) is a formula of TL over R with free variables x. The answer of Q over a temporal instance I is the relationQ(I)={ν( x) | [I,1,ν] |= tl ϕ( x), ν a valuation of x ranging over Adom(I)}. Definition 2.3 (Extended query in TL * ) A query Q in TL * over a database schema R is specified by an expression of the form {( x, t) | ϕ( x)} where ϕ( x) is a formula of TL over R with free variables x. The answer of Q over a temporal instance I is the relation Q(I)={(ν( x), i) | [I,i,ν] |= tl ϕ( x), ν a valuation of x ranging over Adom(I)}.

Theorem 3. 5 ( 1 )

 51 TL * and FO * tl (≤) are equivalent. (2) TL * (E i ) and FO * tl (=) are equivalent.

3 Figure 3 :

 33 Figure 3: An instance satisfying q 1 but not q 2

Lemma 3 . 13 [

 313 Craig Interpolation Theorem] Let f ∈ FO(R) and g ∈ FO(S) be such that ∃R f (R) |= ∀S g(S). Then there exists h ∈ FO(=) such that: ∃R f (R) |= h and h |= ∀S g(S).

Figure 4 :

 4 Figure 4: Two states for our running example

Corollary 4 . 7

 47 The twin property cannot be expressed in TL.

In order to obtain (b), it is important to recall that formulas in FO * (=) have no constant symbols. Indeed, if ϕ is the formula (t = 3 ∧ p(t)) and I = (I, I, I) and p is true at state I then [I, 3] |= ϕ but [I, i] |= ϕ, for i = 3. So, if r < 3, there is no i ∈ {1,

2} such that [I, 3] |= ϕ if and only if [I r , i] |= ϕ.

This example is adapted from[START_REF] Immerman | Descriptive Complexity[END_REF].

a i-subset is a subset of cardinality i

The author was supported by an individual research grant from CNPq (Brazil) and in part by the program Capes-Cofecub 301/00-1

where:

a,i j ρ-1,w [I]( x, t j ), and

.n]".

It is rather immediate to show that the T-Hintikka formulas Φ a,i 0 ρ,w

), for all i. Finally note that by Theorem 3.5 and remark 3.8 the formula Φ a,i 0 ρ,w [I]( x, t) is equivalent to a TL * (E i ) formula whose quantifier temporal rank is less or equal to ρ, and whose width is less or equal to w. Therefore, in the following, we will use Φ a,i 0 ρ,w indistinctly to denote a formula of FO * tl (=) or TL * (E i ).

Finally, we have all necessary ingredients to state the following important result:

The following statements are equivalent:

Proof of theorem 4.5:

We are going to prove successively that [2. ⇒ 3. ], [3. ⇒ 1. ], and [1.

, as a TL * (E i ) formula, has the desired temporal quantifier rank and width. [3. ⇒ 1.] We proceed by induction on the number µ of moves.

It is then obvious that the duplicator has a winning strategy for the 0-move game TG w 0 (I, i 0 , a, J , j 0 , b) because our assumption entails that the states I i 0 and I j 0 are equivalent for first order formulas without quantifiers.

Induction

Step: Suppose that [3. ⇒ 1.] has been proved for µ < r and assume that

Let us consider the T-game TG w r (I, i 0 , a, J , j 0 , b). Two cases arise:

20

[case 1] The first move is a t-move. Assume that the spoiler plays in I and picks the sequence of distinct instants (i 1 ,. . .,i v ) where v ≤ w. Because of the assumption [#], we have that [J , j 0 , ν b ] |= tl Ψ a r,w [I]( x). Thus, by definition, there exists a sequence of distinct instants (j 1 ,. . .,j v ) such that ∀ℓ ∈ {j 1 , . . . , j v }, [J , j ℓ , ν b ] |= tl Φ a,i ℓ ρ-1,w [I]( x). Thus the duplicator's answer to the spoiler is {j 1 , . . . , j v }. Assume that during the second phase of the t-move, the spoiler makes the choice to put the temporal pebbles t I and t J over the instants i ℓ and j ℓ . This t-move is a winning move for the duplicator because, by construction of the duplicator's answer, we have that [J , j ℓ , ν b ] |= tl Φ a,i ℓ r-1,w [I]( x). At this point, the induction hypothesis tells us that the duplicator has a winning strategy for the T-game TG w r-1 (I, i ℓ , a, J , j ℓ , b) and allows us to conclude that the duplicator has a winning strategy for the T-game TG w r (I, i 0 , a, J , j 0 , b). Assume now that the spoiler plays in the temporal instance J and picks the sequence of distinct instants (j 1 ,. . .,j v ) where v ≤ w. Because of the assumption [#], we have that [J , j 0 , ν b ] |= tl Ψ ′ a r,w [I]( x). Thus, by definition, one of the disjuncts must be true and this gives a sequence of distinct instants (i

and we conclude as above that this is indeed a winning strategy.

[case 2] Suppose now that the first move is a d-move. Assume that the spoiler plays over I and places the pebble p s+1 over a. Let us consider the T-Hintikka formula Φ aa,i 0 r-1,w [I]( xx s+1 ) associated with I. By definition of Φ a,i 0 r,w [I]( x) and by our assumption

). This allows the duplicator to choose a constant b such that [J , ν bb , j 0 ] |= tl Φ aa,i 0 r-1,w [I]( xx s+1 ). and to win the move. At this point, the induction hypothesis tells us that the duplicator has a winning strategy for the T-game TG w r-1 (I, i 0 , aa, J , j 0 , bb) and thus he/she has a winning strategy for the T-game TG w r (I, i 0 , a, J , j 0 , b). Assume now that the spoiler plays over J and places the pebble q s+1 over b. Because of the assumption [#], we have that [J , j 0 , ν b ] |= tl ∀x s+1 a∈dom I Φ aa,i 0 ρ-1,w [I]( xx s+1 ) and thus there exists an element a such that [J , j 0 , ν bb ] |= tl Φ aa,i 0 ρ-1,w [I]( xx s+1 ). Let this element a be the duplicator's answer to win the move. At this point, the induction hypothesis leads to conclude that the duplicator has a winning strategy for the T-game TG w r (I, i 0 , a, J , j 0 , b).

[1. ⇒ 2.] We obviously proceed by induction on the number ρ of moves. Initial step: Immediate. Induction step: We now assume that [1. ⇒ 2.] has been proved for ρ < r and suppose that (I, i 0 , a) ∼ w r (J , j 0 , b). In order to prove that (I, i 0 , a) ≡ w r (J , j 0 , b), we proceed by contradiction and assume that there exists a formula Ψ with qtr(Ψ)=r such that [I, i 0 , ν a ] |= tl Ψ and [J , j 0 , ν b ] |= tl Ψ. First assume that Ψ is ∃x s+1 ψ with qtr(ψ)=r -1. This case is rather simple and treated as in the proof for the classical first order logic. Now assume that Ψ is E v ψ. The spoiler is starting a t-move by selecting a sequence of v distinct indices (i 1 , . . . , i v ) of I such that [I, i ℓ , ν a ] |= tl ψ for ℓ = 1..v. Of course, the duplicator prepares an answer (j 1 , . . . , j v ) of v distincts indices of J and because [J , j 0 , ν b ] |= tl Ψ the spoiler is able to complete the move by a choice of (i f , j f ) such that [I, i f , ν a ] |= tl ψ and [J , j f , ν b ] |= tl ψ. However because the duplicator has a winning