Aiming at ontology-based data access to temporal data, we investigate the problems of determining the data complexity of answering an ontology-mediated query (OMQ) given in linear temporal logic LTL and deciding whether it is rewritable to an FO(<)-formula, possibly with extra built-in predicates. Using known facts about the complexity of regular languages, we show that OMQ answering in AC0 coincides with FO(<; N)-rewritiability, which admits unary predicates x 0 (mod n), and that deciding FO(<)- and FO(<; N)-rewritiability of LTL OMQs is ExpSpace-complete. We further observe that answering any OMQ is either in ACC0, in which case it is FO(<; MOD)-rewritable, or NC1complete, and prove that distinguishing between these two cases can be done in ExpSpace. Finally, we identify fragments of LTL for which some of these decision problems become PSpace-, 2p- and coNP-complete.
Classical ontology-based data access (OBDA) [
Here we take rst steps towards extending the non-uniform analysis to OBDA
over temporal data (see [
(1) (2) (3)
A = fMalfunction(2); Malfunction(5); Malfunction(6); Fixed(6); Malfunction(7)g using LTL-formulas such as { = Malfunction ^
Fi Fixed ^
: Fj InOperation ; _ 1 i 5
_ 1 j 5 which can be understood as a Boolean query asking whether there was a malfunction that was xed in 5m but within the next 5m the equipment went out of operation again. The certain answer to the OMQ (O; {) over A is yes.
Our aim in this paper is to understand the complexity of deciding whether
a given LTL OMQ is rewritable to an FO(<)-formula with the order relation <
over timestamps and possibly other built-in predicates. As shown in [
Using the connection with regular languages and the seminal results of [
FO(<)
FO(<; N) in ACC0 / NC1-comp.
FO(<; MOD)/FO(RPR)
LTL OMQs LTLhoPrn OMAQs LTLkrom OMPEQs lin. LTLhorn OMAQs
P LTLkrom OMAQs LTLcore OMPEQs
ExpSpace [Th.1,5,6] ExpSpace [Th.4,5,6] ExpSpace [Th.4] PSpace [Th. 7] coNP [Th. 8] 2p [Th. 9]
PSpace [Th. 7]
all in AC0 [
PSpace [Th. 7] { {
In our setting, the alphabet of linear temporal logic LTL comprises a set of atomic concepts Ai, i < !. Basic temporal concepts, C, are de ned by the grammar C ::=
Ai j 2F C j 2P C j
F C j
P C with the operators 2F /2P (always in the future/past) and F / P (at the next/ previous moment). A temporal ontology, O, is a nite set of axioms of the form C1 ^ ^ Ck !
Ck+1 _
_ Ck+m;
(4)
where k; m 0, the Ci are basic temporal concepts, the empty ^ is >, and the
empty _ is ?. Following the DL-Lite convention [
An ABox is a nite set A of atoms Ai(`), for ` 2 Z, together with a nite interval tem(A) = [min A; max A] of integers such that min A < max A and whenever Ai(`) 2 A then min A ` max A. Without loss of generality, we always assume that min A = 0. The interval tem(A) is called the active domain of A. If tem(A) is not speci ed explicitly, it is assumed to be [0; m], where m is the maximal timestamp in A. By a signature, , we mean any nite set of atomic concepts. An ABox A is said to be a -ABox if Ai(`) 2 A implies Ai 2 .
We query ABoxes by means of temporal concepts, {, which are LTL-formulas built from the atoms Ai, Booleans ^, _, :, temporal operators F , 2F , 3F (eventually), U (until), and their past-time counterparts P , 2P , 3P (some time in the past) and S (since). If { does not contain :, 2F , 2P , U and S, we call it a positive existential temporal concept.
A (temporal) interpretation is a structure I = (Z; A0I ; A1I ; : : : ) with AiI Z,
for every i < !. The extension {I of a temporal concept { in I is de ned
inductively as usual in LTL under the `strict semantics' [
n 2 Z j k 2 {I ; for all k > n ; n 2 Z j there is k > n with k 2 {I ; ({1 U {2)I =
n 2 Z j there is k > n with k 2 {2I and m 2 {1I for n < m < k ; and symmetrically for the past operators. An axiom (4) is true in I if we have C1I \ \ CkI CkI+1 [ [ CkI+m. An interpretation I is a model of O if all axioms of O are true in I; it is a model of A if Ai(`) 2 A implies ` 2 AI . i
An LTLco ontology-mediated query (OMQ) is a pair of the form q = (O; {), where O is an LTLco ontology and { a temporal concept. If { is a positive existential temporal concept, we call q a positive existential OMQ (OMPEQ), and if { is an atomic concept, we call q atomic (OMAQ). The set of atomic concepts occurring in an OMQ q is denoted by sig(q). We can treat q as a Boolean OMQ, which returns yes/no as an answer, or as a speci c OMQ, which returns timestamps from the ABox in question assigned to the free variable, say x, in the standard FO-translation of {. In the latter case, we write q(x) = (O; {(x)).
More precisely, a certain answer to a Boolean OMQ q = (O; {) over an ABox A is yes if, for every model I of O and A, there is k 2 Z such that k 2 {I , in which case we write (O; A) j= 9x{(x). If (O; A) 6j= 9x{(x), the certain answer to q over A is no. We write (O; A) j= {(k), for k 2 Z, if k 2 {I in all models I of O and A. A certain answer to a speci c OMQ q(x) = (O; {(x)) over A is any k 2 tem(A) with (O; A) j= {(k). By the evaluation (or answering ) problems for q and q(x) we understand the decision problems `(O; A) j=? 9x{(x)' and `(O; A) j=? {(k)' with input A and, resp., A and k 2 tem(A). We say that q or q(x) is in a complexity class C if the corresponding evaluation problem is in C. Example 2. (i) Let q1 = (O1; C ^ D) with O1 = f3P A ! B; 2F B ! Cg. The certain answer to q1 over A1 = fD(0); B(1); A(1)g is yes, but over A2 = fD(0); A(1)g it is no. The only answer to q1(x) = O1; (C ^ D)(x) over A1 is 0. (ii) Let O2 = f P A ! B; P B ! A; A ^ B ! ? g. The answer to q2 = (O2; C) over A1 = fA(0)g is no, but over A2 = fA(0); A(1)g it is yes. There are no answers to q2(x) = (O1; C(x)) over A1, while over A2 there are two of them: 0 and 1. (iii) Let O3 = f P Bk ^ A0 ! Bk; P B1 k ^ A1 ! Bk j k = 0; 1g. For any word e = e1 : : : en 2 f0; 1gn, let Ae = fB0(0)g [ fAei (i) j 0 < i ng [ fE(n)g. The answer to q3 = (O3; B0 ^ E) over Ae is yes i the number of 1s in e is even. (iv) Let O4 = fA ! F Bg and q4 = (O4; B). Then, the answer to q4 over A = fA(0)g is yes; however, there are no certain answers to q4(x) = (O4; B(x)) over A. (v) Let O5 = fA ! B _ F Bg. The certain answer to q5 = (O5; B) over A = fA(0); C(1)g is yes; however, there are no certain answers to q5(x) over A. Remark 1. Let O be as in Example 1 and let O0 be the result of replacing (1) in O by Malfunction ^ 2F X ! ? and > ! X _ Fixed, for a fresh concept name X. Then the OMQ q = (O; {) in Example 1 is `equivalent' to q0 = (O0; {) in the sense that q and q0 have the same certain answers over any sig(q)-ABox A.
Let L be a class of FO-formulas that can be interpreted over nite linear orders. A Boolean OMQ q is L-rewritable over -ABoxes if there is an L-sentence Q such that, for any -ABox A, the certain answer to q over A is yes i SA j= Q. Here, SA is a structure with domain tem(A) ordered by <, in which SA j= Ai(`) i Ai(`) 2 A. A speci c OMQ q(x) is L-rewritable over -ABoxes if there is an L-formula Q(x) with one free variable x such that, for any -ABox A, k is a certain answer to q over A i SA j= Q(k). The sentence Q and the formula Q(x) are called L-rewritings of the Boolean and speci c OMQ q, respectively.
We require four languages L for rewriting LTL OMQs:
FO(<) (monadic) rst-order formulas with the built-in predicate < for order;
FO(<; N) FO(<)-formulas with predicates x
0 (mod N ), for any N > 1;
FO(<; MOD) FO(<)-formulas with quanti ers 9N , for N > 1, de ned by taking
dSiAvisj=ibl9eNbxy N(x()xi t0he(mcoarddNina)lcitaynoofbtvhieousselty fbne 2detenme(dAa)sj9SNAy(jy=< (xn)))g; is
FO(RPR) FO(<) with relational primitive recursion [
Example 3. (i) An FO(<)-rewriting of q01(x) is
'1(x) = D(x) ^ [C(x) _ 9y(A(y) ^ 8z ((x < z
y) ! B(z)))];
9x'1(x) is an FO(<)-rewriting of q1. (ii) An FO(<; N)-rewriting of q2(x) is
'2(x) = C(x) _ 9x; y [(A(x) ^ A(y) ^ odd(x; y)) _ (B(x) ^ B(y) ^ odd(x; y)) _
(A(x) ^ B(y) ^ :odd(x; y))];
where odd(x; y) = x 0 (mod 2) $ y 6 0 (mod 2) implies that the distance
between x and y is odd, and an FO(<; N)-rewriting of q2 is 9x'2(x). (iii) The
OMQ q3 is not rewritable to an FO-formula with any numeric predicates as
PARITY is not in AC0 [
A uniform classi cation of speci c LTL OMQs by their rewritability type has
been obtained in [
For any q and sig(q), we regard the set = 2 as an alphabet. A -ABox A can be given as a -word wA = a0 : : : an with ai = fA j A(i) 2 Ag. Conversely, any -word w = a0 : : : an can be understood as an ABox Aw with tem(Aw) = [0; n] and A(i) 2 Aw i A 2 ai. The language L (q) of the Boolean OMQ q is the set of -words wA such that the certain answer to q over A is yes. For a speci c q(x), we take = [ 0 , for a disjoint copy 0 of , and represent a pair (A; i) with a -ABox A and i 2 tem(A) as a word wA;i = a0 : : : a0i : : : an, where aj = fA j A(j) 2 Ag 2 for j 6= i, and a0i = fA j A(i) 2 Ag 2 0 . The language L (q(x)) is the set of -words wA;i such that i is a certain answer to q(x) over A.
Proposition 1. Let L be one of the classes of FO-formulas introduced above. (i) A Boolean OMQ q = (O; {) is L-rewritable over -ABoxes i L (q) is Lde nable. (ii) A speci c OMQ q(x) = (O; {(x)) is L-rewritable over -ABoxes i L (q(x)) is L-de nable. Both L (q) and L (q(x)) are regular for any . Proof. We only show that L (q) is regular. Let subq be the set of temporal concepts in q and their negations. A type is any maximal subset of subq that is consistent with O. The set of all types is denoted by T . We de ne an NFA A over whose language is n L (q). The states in A comprise the set Q:{ = f 2 T j :{ 2 g. The transition relation !a, for a 2 , is de ned by setting 1 !a 2 if the following conditions hold (assuming that the temporal operators are expressed via U and S): a 2, C1 U C2 2 1 i C2 2 2 or C1 U C2 2 2 and C1 2 2, and symmetrically for S. The set of initial states comprises 2 Q:{ with [ f2P :{g is consistent with O; the set of accepting states comprises those 2 Q:{ for which [ f2F :{g is consistent with O. It is readily seen that, for every a 2 we have a 2 L(A) i (O; Aa) 6j= 9x{(x). The number of states in A does not exceed O(2jqj). Since LTL-satis ability is in PSpace, the NFA A can be constructed in exponential time in jqj.
The following table summarises known results connecting de nability of
regular languages L with properties of their syntactic monoids M (L) and syntactic
morphisms L (see Section 3 and [
Since deciding FO(<)-de nability of regular languages given by NFAs is
PSpacecomplete [
The exact complexity of deciding FO(<; N)-de nability and NC1-hardness
of regular languages seems to be open (their decidability was shown in [
A monoid M = (B; ; e) has an associative binary operation and an identity e with a e = e a = a, for all a 2 B. We shorten a b to ab. Given a DFA A = (Q; ; ; q0; F ) and w 2 , de ne a map fwA : Q ! Q by setting fwA(q) = q0 i q !w q0. The transition monoid of A takes the form M = (ffwA j w 2 g; ; f"A), where " is the empty word and fwAfvA = fwAv, for any fwA, fvA. The syntactic monoid M (L) of a regular language L is isomorphic to the transition monoid of a minimal DFA accepting L [23, Chaprter V.1]. A monoid is aperiodic if it does not contain non-trivial groups (with the monoid operation). Let A be a minimal automaton of L and B the domain of M (L). The map L : ! B de ned by L(w) = fwA is called a syntactic morphism of L. Given a set W , we set L(W ) = f L(w) j w 2 W g. The syntactic morphism L is quasi-aperiodic if, for any t > 0, the set L( t) does not contain non-trivial groups. Theorem 2. Deciding FO(<; N)-de nability of L(A), A an NFA, is in PSpace. Proof. First, we show the theorem for a minimal DFA A, then extend it to an arbitrary DFA and, nally, to an NFA. Let A = (Q; ; ; q0; F ) be minimal. We use the following criterion: L(A) is not FO(<; N)-de nable i there are w and n 2 N such that fwA 6= fwA2 , fwA = fwAn , and fwA = fvA, fwA2 = fuA, for some u and v with jvj = juj. Indeed, let L = L(A). ()) In this case, L is quasi-aperiodic, and so there is t such that L( t) contains a non-trivial group G. Let e be the identity element of G and let a 6= e, a 2 G. We have ajGj = e, ajGj+1 = ae = a and, since a; e 2 L( t), there are w; u 2 t such that a = fwA and e = fwAjGj = fuA. (() Observe that fwAi = fwAiwn(n i) = fuAivn i , for 1 i n. Therefore, fwA; : : : ; fwAn form a group in L( juj n), and so L is not FO(<; N)-de nable.
To check this criterion, we can use the known PSpace algorithms [
Theorem 3. NC1-hardness of L(A), for an NFA A, can be decided in PSpace. Proof. We follows that steps of the proof above, using the following criterion. The language L(A), for a minimal DFA A, is NC1-hard i there are u; v; w 2 such that, for x 2 fu; v; wg, fxA = fxAfuAvw, fxA 6= fxA2 and fuAvw = fxAix , for some iu; iv; iw 2 N that are pairwise coprime. Indeed, L(A) is NC1-hard i there is a non-solvable group in M (L(A)). By [24, Corollary 3], a group is non-solvable i there are 3 elements with pairwise coprime orders whose product is the identity.
In the PSpace algorithm checking this criterion, we need to compute iu; iv; iw and check that they are pairwise coprime. It is readily seen that those numbers (if exist) are jQjjQj and can be dealt with in PSpace.
Theorem 4. Both FO(<; N)-rewritability and NC1-completeness (in data complexity ) of LTLb2ool OMQs over -ABoxes are decidable in ExpSpace. 4
Theorem 5. Deciding FO(<)- and FO(<; N)-rewritability of LTLhorn OMAQs over -ABoxes is ExpSpace-hard.
Proof. The idea of the proof is as follows. Given a Turing machine M with
exponential tape and an input word x, we construct|in a way similar to [
Let x be a word and M a Turing machine requiring N = 2nc tape cells on an input of size n. Let N 0 be the rst prime after N + 1. We construct a family fAig0 i<N0 of simple star-free minimal DFAs whose intersection represents accepting computations of M on x. We encode computations as words over [ f]; [g of the form ] c1 ] c2 ] : : : ] ck 1 ] ck[, where the ci are con gurations.
The DFA A0 checks that an input starts with an initial and ends with an accepting con guration of M on x. The Ai, for 0 < i N , check that the ith symbol in a con guration `follows' from the (i 1)th, ith, and (i + 1)th symbols in the previous con guration (if A1 is constructed, Ai can skip the rst i 1 symbols and run A1). The rest of the family just accept all the words with the only [ at the very end. We then have TiN=00 L(Ai) = ; i M rejects x. We next construct minimal DFAs A and A0 with the languages (L(A0) : : : L(AN0 1)) and ((L(A0) [ f[g) : : : (L(AN0 1) [ f[g)) . Thus, we obtain: (i) L(A) is star-free i TiN=00 L(Ai) = ; (i M rejects x); (ii) L(A0) is in AC0 i TiN=00 L(Ai) = ;.
Now we de ne LTLhorn ontologies O and O0 simulating A and A0. We name the states in A by triples (i; t; j), where i indicates Ai the state `came from', t is a `type' of the state (say, where the DFA skips the rst i 1 symbols), and j is a counter in t (e.g., saying how many symbols still are to be skipped). The number of types is constant, while i; j 2k, for k = dlog2 N 0e.
The ontology O uses the concepts Aij and Lij, where i = 0; 1 and j = 1; : : : ; k, the symbols in [ f]; [g, Qt, for a type t, X, Y and F . Let 0 = [ f]; [; X; Y g. For any w = w1 : : : wm 2 ( [f]; [g) , let Aw = fX(0); w1(1); : : : wm(m); Y (m+ 1)g: For a binary word c = bk : : : b1, set Ac = Ab1 1 ^ ^ Abkk ;
A<c = _ bi=1
Ai0 ^ ^ Ajbj ; j>i
A>c = _ bi=0
Ai1 ^ ^ Ajbj j>i and let Lc, L<c, and L>c be similar concepts for Li . We represent each triple j (i; t; j) as the conjunction Ai ^ Qt ^ Lj. We de ne O so that, having read a pre x w1 : : : wl of w, the DFA A is in state (i; t; j) i O; Aw j= (Ai ^ Qt ^ Lj)(l + 1). To achieve this, for every transition (i1; t1; j1) !a (i2; t2; j2) of A, we need
O j= Ai1 ^ Qt1 ^ Lj1 ^ a ! F Ai2 ^ F Qt2 ^ F Lj2 : As the structure of A is repetitive, we can ensure this without writing axioms for all transitions. For example, consider the fragment of A corresponding to the part of A0 that, after reading x, checks that the rest of the tape is blank b. All the states in this part have the same type t with a counter j. So, for n + 1 < j < N + 1, there is a transition (0; t; j) !b (0; t; j + 1). We capture all these transitions by one formula
A0 ^ Q0 ^ L>n ^ L<N+1 ^ b ! F A0 ^ F Q0 ^ iL;
k iL = ^
Ll0 ^ Ll1 1 ^ : : : ^ L11 ! F Ll1 ^ F Ll0 1 ^ : : : ^ F L10 ^ where l=1 ^ l1<l2 (Ll01 ^ Ll2 ! F Ll02 ) ^ (Ll01 ^ Ll2 ! F Ll12 ) : 0 1 As a result, O j= (iL ^ Li) ! F Li+1. Similarly, we de ne iA, dL, hA, and LA so that O j= (dL ^ Li) ! F Li 1, O j= (hA ^ Ai) ! F Ai, O j= (LA ^ Ai) ! F Li. This gives us polynomially many horn axioms in O, to which we add a ^ b ! ?; for a; b 2
0; X ! F A0 ^ F Q0 ^ F L0; A0 ^ Q0 ^ L0 ^ Y ! F: The ontology O0 is de ned in the same way for the DFA A0. It follows that the certain answer to (O; F ) over Aw is yes i w 2 L(A), and similarly for (O0; F ). Lemma 1. The LTLhorn OMAQs (O; F ) and (O; F (x)) are FO(<)-rewritable over 0-ABoxes i L(A) is star-free; (O0; F ) and (O0; F (x)) are FO(<; N)rewritable over 0-ABoxes i L(A0) is in AC0.
Proof. We only sketch the proof of the former claim, where ()) is clear. (() Suppose L(A) is star-free and A is a 0-ABox. Then O; A j= F (k) only if (O; A) is inconsistent, and so there are a(i); b(i) 2 A for some a 6= b, or A contains a subset of the form fX(i 1); a1(i); a2(i + 1); a3(i + 2); : : : ; ak i(k 1); Y (k)g such that a1a2 : : : ak i 2 L(A). As L(A) is star-free, it is de nable by an FO(<)sentence [23, Ch. VI], and so (O; F ) and (O; F (x)) are FO(<)-rewritable. Theorem 6. Deciding FO(<)- or FO(<; N)-rewritability of LTLkrom OMPEQs over -ABoxes is ExpSpace-hard.
Proof. Take an LTLhorn OMAQ q = (O; A) and sig(q), assuming that the axioms in O are of the form C ! ? or C ! B, for some C = C1 ^ ^ Cn and atomic B. We construct an LTLkrom OMPEQ q0 = (O0; {) with atomic concepts fB; B j B 2 sig(q)g. Let O0 = fB ^ B ! ?; > ! B _ B j B 2 sig(q)g and { = A _ _
3F 3P C C!? in O
_ _
3F 3P (C ^ B): C!B in O For any -ABox A, the certain answers to q and q0 (and to q(x) and q0(x)) over A coincide. It follows that q0 and q0(x) are FO(<)- or FO(<; N)-rewritable over -ABoxes i q and q(x) are FO(<)- or FO(<; N)-rewritable, respectively. 5
Theorem 7. Deciding FO(<)- or FO(<; N)-rewritability of linear LTLhoPrn OMAQs over -ABoxes is PSpace-complete; NC1-completeness is in PSpace. Proof. One can reduce L-rewritability of linear speci c OMAQs to L-rewritability of linear Boolean OMAQs. Let q = (O; A1) be a linear OMAQ. We transform q to q0 = (O0; A01) such that q0 is L-rewritable over -ABoxes i q is and A 2 idb(O0) only occurs in axioms of the form P`1 C1 ^ ^ P`k Ak ^ P A ! B. For example, O = f P X ! A2; P3Y ^ P A2 ! A1; Z ^ P A1 ! A2; P4W ^ A2 ! A3, V ^ P A3 ! ? g is transformed to an ontology O0 with the following axioms: Let edb(O) = sig(q)nidb(O) and let ext(O) be the set of (maximal) basic concepts
P` A with A 2 edb(O) that occur on the left-hand side of an axiom in O. Thus, ext(O0) = f P X; P3Y; Z; P4W; V; P5W; A1; A2; A3g in the example above.
Let ext (O0) = ext(O0) . De ne an NFA Bq0 over q0 = 2ext (O0), which we illustrate below for the OMAQ q0 = (O0; A01) in our example, assuming that = fX; Y; Z; W; V; A1; A2; A3g and S !e S0 implies S !e0 S0 for all e0 e: f P Xg; fA2g
A02 start ;
A00 f P3Y g; fV; P5W g fZg fA1g
A01 We show that L(q0) is L-de nable over -ABoxes i L(Bq0 ) is L-de nable. The proof uses an FO(<)-reduction maping a 2 to e 2 q0 with a 2 L(q0) i e 2 L(Bq0 ), and the other way round. To show that deciding FO(<)-, FO(< ; N)-de nability, or NC1-completeness of L(Bq0 ) can be done in PSpace is not immediate as neither q0 nor Bq0 is polynomial in jqj. However, the number of states in Bq0 is polynomial in q and one can check whether q !e q0 by a PSpace algorithm, which allows us to use Theorems 2 and 3 for Bq0 without explicitly constructing it. The lower bounds are proved by reduction of FO(<)and FO(<; N)-de nability for regular languages.
Theorem 8. Deciding FO(<)-rewritability of LTLkrom OMAQs q = (O; A) over -ABoxes is coNP-complete.
Proof. Let q0 = (O0; Y ) with O0 = O [ fA ! ?g and fresh Y , and q00 = (O00; Y ) with O00 = O [ fX ^ A ! ?g and fresh X; Y . For any (X; Y -free) ABox A, (O; A) j= 9xA(x) i (O0; A) j= 9x Y (x) i A is inconsistent with O0; similarly, (O; A) j= A(k) i (O00; A[fX(k)g) j= 9xA(x) i A[fX(k)g is inconsistent with O00, for k 2 tem(A). So we only need to consider Boolean OMAQs q = (O; A) with the yes-answer only for ABoxes inconsistent with O.
As O is krom, A is inconsistent with O i (i) there are A(i); B(i) 2 A with
O j= B ^ A ! ?, or (ii) there exist k1 k2, B(k1) 2 A and C(k2) 2nA+1:wCithg
O j= B ! Fk2 k1 :C; cf. [
Proof. We assume that O does not contain disjointness axioms B ^ C ! ? as they can be removed from O and { replaced by { _ WOj=B^C!? 3F 3P (B ^ C); giving an equivalent OMQ. We further assume that all of the other rules have the following forms: A ! B, A ! F B, or A ! P B. As in the proof of Theorem 7, rewritability of speci c OMQs can be reduced to rewritability of Boolean OMQs.
Given O, A, B and k, one can check in polytime whether O; A j= B(k), which, by structural induction, implies that checking O; A j= 9x{(x) is in NP.
Let B = fw1 : : : wk 2 j 8i jw(i)j > 0; Pi jw(i)j < j{jg. With every w 2 B we associate the language Lw = L(; w1; : : : ; wk; ) \ L (q). For -words v and v0, we write v0 v if they are of the same length and vi0 vi, for all i.
As q is an LTLcore OMPEQ, we have O; A j= q i O; A0 j= q, for some
A0 A, jA0j j{j. Then, for every v 2 , we have v 2 L (q) i there is v0 v
such that v0 2 Lw for some w 2 B. It follows that the language L (q) is
FO(<)de nable i Lw is FO(<)-de nable, for every w 2 B. For w = w1 : : : wk 2 B and
I = (i0; : : : ; ik), let vw;I = ;i0 w1;i1 : : : wk;ik . For c 2 N, let I c be I with all
ij > c replaced with c. If Lw is FO(<)-de nable, there is c with vw;I 2 Lw i
vw;I<c 2 Lw. By the properties of the canonical models [
Now, q is not FO(<)-rewritable i we can guess w 2 B and I such that
max(I) < 2c and only one of vw;I and vw;I<c is in Lw. We can check membership
in Lw using an NP-oracle, so FO(<)-rewritability is in coNPNP = 2p. The
matching lower bound is shown by reduction of 893CNF [
i=0 is a rewriting of q'. If 8X9Y '(X; Y ) is false, then there is a 2 2X such that ' is false for any assignment to Y . For w = fBgXa, Xa = fA; x1a(0); : : : ; xan(n)g, the language Lw is L(; fBg(;;) Xa; ), and so q' cannot be FO(<)-rewritable. Acknowledgements This work was supported by EPSRC U.K. EP/S032282.