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 AC 0 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 ACC 0 , in which case it is FO(<, MOD)-rewritable, or NC 1complete, 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-, Π p 2 -and coNP-complete.
Classical ontology-based data access (OBDA) [8,20] was launched by identifying ontology and query languages that uniformly guarantee FO-rewritability of all ontology-mediated queries (OMQs) given in those languages. Thus, by design, OBDA ontologies are rather inexpressive. An alternative, non-uniform approach to OBDA would be-at least in theory-to develop algorithms that, given any OMQ in some expressive languages, could recognise the data complexity of answering that OMQ and construct its rewriting of optimal type. The datalog community has been investigating FO-and linear-datalog-rewritability (aka boundedness and linearisability) of datalog programs since the 1980s [26,25,11,19]. The data complexity and rewritability of individual OMQs in various description logics have become an active research area in the past decade [17,7,16,18,15].
Here we take first steps towards extending the non-uniform analysis to OBDA over temporal data (see [3] for a survey of results in uniform temporal OBDA). We consider OMQs given in linear temporal logic LTL, which were uniformly classified in [2,4] according to their data complexity and rewritability type.
Example 1. Let O be an LTL ontology with the following axioms containing the temporal operators 3 F (eventually) and F / P (next/previous minute):
Malfunction ∧ P Malfunction ∧2 P Malfunction → ¬ F InOperation. (3) We query temporal data, say the ABox A = {Malfunction(2), Malfunction (5), Malfunction (6), Fixed (6), Malfunction(7)} using LTL-formulas such as
which can be understood as a Boolean query asking whether there was a malfunction that was fixed 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 [4], every LTL OMQ is rewritable to an FO(<)-formula extended with relational primitive recursion (or to a monadic second-order formula), whose evaluation over data instances is in the complexity class NC 1 . Here, we first establish a connection between LTL OMQs and regular languages, and then use it to prove that deciding FO(<)-rewritability of such OMQs is ExpSpace-complete, with the lower bound shown for Horn LTL ontologies with the next-time operator F and atomic queries, and also for Krom ontologies with positive LTL queries. For atomic OMQs (OMAQs, for short) with linear Horn LTL ontologies that contain P only, deciding FO(<)-rewritability turns out to be PSpace-complete; the complexity goes down to coNP for OMAQs with Krom ontologies and the nextand previous-time operators. On the other hand, deciding FO(<)-rewritability becomes Π p 2 -complete for core (that is, both Horn and Krom) ontologies and positive existential temporal queries, which do not contain negation and the operators always in the future/past, since and until. OMQs with such queries are referred to as OMPEQs.
Using the connection with regular languages and the seminal results of [5], we show that OMQ answering in AC 0 coincides with rewritability to FO(<, ≡ N )formulas, which admit unary predicates x ≡ 0 (mod n), and that deciding FO(< , ≡ N )-rewritiability of LTL OMQs is ExpSpace-complete. We further observe that answering any OMQ is either in ACC 0 , in which case it is FO(<, MOD)rewritable, or NC 1 -complete, and prove that distinguishing between these two cases can be done in ExpSpace. For OMAQs with linear Horn LTL ontologies with P only, these problems become decidable in PSpace. All our complexity results for circuit complexity and rewritability of OMQs are summarised below:
In our setting, the alphabet of linear temporal logic LTL comprises a set of atomic concepts A i , i < ω. Basic temporal concepts, C, are defined by the grammar
with the operators 2 F /2 P (always in the future/past) and F / P (at the next/ previous moment). A temporal ontology, O, is a finite set of axioms of the form
where k, m ≥ 0, the C i are basic temporal concepts, the empty ∧ is , and the empty ∨ is ⊥. Following the DL-Lite convention [1,2], we classify ontologies by the shape of their axioms and the temporal operators that can occur in them. Suppose c ∈ {horn, krom, core, bool} and o ∈ {2, , 2 }. The axioms of an LTL o c -ontology may only contain occurrences of the (future and past) temporal operators in o and satisfy the following restrictions on k and m in (4) indicated by c: horn requires m ≤ 1, krom requires k + m ≤ 2, core both k + m ≤ 2 and m ≤ 1, while bool imposes no restrictions. For example, axiom (2) from Example 1 is allowed in all of these fragments, (3) is equivalent to a horn axiom (with ⊥ on the right-hand side), and (1) can be expressed in krom as explained in Remark 1. A basic concept is called an IDB (intensional database) concept in an ontology O if its atomic concept occurs on the right-hand side of an axiom in O. The set of IDB atomic concepts in O is denoted by idb(O). An LTL o hornontology is called linear if each of its axioms
An ABox is a finite set A of atoms A i ( ), for ∈ Z, together with a finite interval tem(A) = [min A, max A] of integers such that min A < max A and whenever A i ( ) ∈ 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 specified explicitly, it is assumed to be [0, m], where m is the maximal timestamp in A. By a signature, Ξ, we mean any finite set of atomic concepts. An ABox A is said to be a
We query ABoxes by means of temporal concepts, κ, which are LTL-formulas built from the atoms A i , Booleans ∧, ∨, ¬, temporal operators F , 2 F , 3 F (eventually), U (until), and their past-time counterparts P , 2 P , 3 P (some time in the past) and S (since). If κ does not contain ¬, 2 F , 2 P , U and S, we call it a positive existential temporal concept.
A (temporal) interpretation is a structure I = (Z, A I 0 , A I 1 , . . . ) with A I i ⊆ Z, for every i < ω. The extension κ I of a temporal concept κ in I is defined inductively as usual in LTL under the 'strict semantics' [14,12]:
and symmetrically for the past operators. An axiom ( 4) is true in I if we have
i . An LTL o c ontology-mediated query (OMQ) is a pair of the form q = (O, κ), where O is an LTL o c 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 specific 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
. By the evaluation (or answering) problems for q and q(x) we understand the decision problems '(O, A) |= ? ∃xκ(x)' and '(O, A) |= ? κ(k)' with input A and, resp., A and k ∈ tem(A). We say that q or q(x) is in a complexity class C if the corresponding evaluation problem is in C.
} it is yes. There are no answers to q 2 (x) = (O 1 , C(x)) over A 1 , while over A 2 there are two of them: 0 and 1. (iii
The answer to q 3 = (O 3 , B 0 ∧ E) over A e is yes iff the number of 1s in e is even. (iv) Let O 4 = {A → F B} and q 4 = (O 4 , B). Then, the answer to q 4 over A = {A(0)} is yes; however, there are no certain answers to q 4 (x) = (O 4 , B(x)) over A. (v) Let O 5 = {A → B ∨ F B}. The certain answer to q 5 = (O 5 , B) over A = {A(0), C(1)} is yes; however, there are no certain answers to q 5 (x) over A.
Remark 1. Let O be as in Example 1 and let O be the result of replacing (1) in O by Malfunction ∧ 2 F X → ⊥ and → X ∨ Fixed, for a fresh concept name X. Then the OMQ q = (O, κ) in Example 1 is 'equivalent' to q = (O , κ) in the sense that q and q have the same certain answers over any sig(q)-ABox A.
Let L be a class of FO-formulas that can be interpreted over finite 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 iff S A |= Q. Here, S A is a structure with domain tem(A) ordered by <, in which
with one free variable x such that, for any Ξ-ABox A, k is a certain answer to q over A iff S A |= Q(k). The sentence Q and the formula Q(x) are called L-rewritings of the Boolean and specific OMQ q, respectively.
We require four languages L for rewriting LTL OMQs: FO(<) (monadic) first-order formulas with the built-in predicate < for order; Example 3. (i) An FO(<)-rewriting of q 1 (x) is
where odd(x, y) = x ≡ 0 (mod 2) ↔ y ≡ 0 (mod 2) implies that the distance between x and y is odd, and an FO(<, ≡ N )-rewriting of q 2 is ∃xϕ 2 (x). (iii) The OMQ q 3 is not rewritable to an FO-formula with any numeric predicates as PARITY is not in AC 0 [13]; the following is an FO(<, MOD)-rewriting of q 3 :
(iv) An FO(<)-rewriting of q 4 (x) is ϕ 4 (x) = B(x)∨A(x−1); an FO(<)-rewriting of q 4 is ϕ 4 = ∃x(A(x) ∨ B(x)). (v) The same ϕ 4 is an FO(<)-rewriting of q 5 , and B(x) is a rewriting of q 5 (x).
A uniform classification of specific LTL OMQs by their rewritability type has been obtained in [4]. Here, we only mention in passing that all (Boolean and specific) LTL OMQs are FO(RPR)-rewritable and can be answered in NC 1 . In this paper, we take a non-uniform approach to rewritability, aiming to understand how (complex it is) to decide the optimal type of FO-rewritability for a given LTL OMQ q over Ξ-ABoxes. Clearly, we can always assume that Ξ ⊆ sig(q).
For any q and Ξ ⊆ sig(q), we regard the set Σ Ξ = 2 Ξ as an alphabet. A Ξ-ABox A can be given as a Σ Ξ -word w A = a 0 . . . a n with a i = {A | A(i) ∈ A}. Conversely, any Σ Ξ -word w = a 0 . . . a n can be understood as an ABox A w with tem(A w ) = [0, n] and A(i) ∈ A w iff A ∈ a i . The language L Ξ (q) of the Boolean OMQ q is the set of Σ Ξ -words w A such that the certain answer to q over A is yes. For a specific q(x), we take Γ Ξ = Σ Ξ ∪ Σ Ξ , for a disjoint copy Σ Ξ of Σ Ξ , and represent a pair (A, i) with a Ξ-ABox A and i ∈ tem(A) as a Γ Ξword w A,i = a 0 . . . a i . . . a n , where a j = {A | A(j) ∈ A} ∈ Σ Ξ for j = i, and a i = {A | A(i) ∈ A} ∈ Σ Ξ . The language L Ξ (q(x)) is the set of Γ Ξ -words w A,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.
) is L-definable. Both L Ξ (q) and L Ξ (q(x)) are regular for any Ξ.
Proof. We only show that L Ξ (q) is regular. Let sub q be the set of temporal concepts in q and their negations. A type is any maximal subset τ of sub q that is consistent with O. The set of all types is denoted by T . We define an NFA A over Σ Ξ whose language is Σ * Ξ \ L Ξ (q). The states in A comprise the set
The transition relation → a , for a ∈ Σ Ξ , is defined by setting τ 1 → a τ 2 if the following conditions hold (assuming that the temporal operators are expressed via U and S): The following table summarises known results connecting definability of regular languages L with properties of their syntactic monoids M (L) and syntactic morphisms η L (see Section 3 and [5] for details) and with their circuit complexity (under a reasonable binary encoding of L's alphabet):
all groups in M (L) are solvable in ACC 0 FO(RPR)
arbitrary
The statement in the table that all groups in M (L) are solvable iff L is in ACC 0 holds unless ACC 0 = NC 1 . Using Proposition 1, these results can be extended to rewritability and data complexity of Boolean and specific LTL OMQs: (a) an OMQ is FO(<, ≡ N )-rewritable iff it can be answered in AC 0 , (b) an OMQ is FO(<, MOD)-rewritable iff it can be answered in ACC 0 (unless ACC 0 = NC 1 ), (c) an OMQ is FO(<, RPR)-rewritable iff it can be answered in NC 1 .
Since deciding FO(<)-definability of regular languages given by NFAs is PSpacecomplete [9,6], we obtain by Proposition 1:
The exact complexity of deciding FO(<, ≡ N )-definability and NC 1 -hardness of regular languages seems to be open (their decidability was shown in [5].) So our first aim is to settle these issues. Given an NFA A = (Q, Σ, δ, Q 0 , F ), states q, q ∈ Q, and w = a 0 . . . a n ∈ Σ * , we write q → w q if there is a run of A on w that starts with (q 0 , 0) and ends with (q , n + 1). We say that a state q ∈ Q is accessible if q → w q, for some q ∈ Q 0 and w ∈ Σ * . Two states q 1 , q 2 ∈ Q are equivalent if, for each w ∈ Σ * , we have q 1 → w q for some q ∈ F iff q 2 → w q for some q ∈ F . A DFA is minimal if each of its states is accessible and it has no distinct equivalent states. Every DFA A = (Q, Σ, δ, q 0 , F ) can be converted to a minimal DFA A = (Q , Σ, δ , q 0 , F ) with L(A) = L(A ) in the following way [23]. Let R = {q ∈ Q | q is accessible in A} and let ∼ be a relation on R defined by taking q ∼ q iff q and q are equivalent. Clearly, ∼ is an equivalence relation; we denote by q/ ∼ the equivalence class of q ∈ R. Now, we set Q = {q/ ∼ | q ∈ R} and define δ by taking q/ ∼ → a q / ∼ , where {q } = δ(a, q), for all q ∈ R and a ∈ Σ (which is obviously well-defined). Finally, we set q 0 = q 0 / ∼ and F = {q/ ∼ | q ∈ R ∩ F }. It is known that, for any regular language L, all minimal DFAs A with L(A ) = L are isomorphic; we call each such A a minimal DFA of L.
A monoid M = (B, •, e) has an associative binary operation • and an identity e with a • e = e • a = a, for all a ∈ B. We shorten a • b to ab. Given a DFA A = (Q, Σ, δ, q 0 , F ) and w ∈ Σ * , define a map
, where ε is the empty word and
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 defined by η L (w) = f A w is called a syntactic morphism of L. Given a set W ⊆ Σ * , we set η L (W ) = {η L (w) | w ∈ W }. 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 )-definability 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, finally, to an NFA. Let A = (Q, Σ, δ, q 0 , F ) be minimal. We use the following criterion: L(A) is not FO(<, ≡ N )-definable iff there are w and
for some u and v with |v| = |u|. 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 = e, a ∈ G. We have a |G| = e, a |G|+1 = ae = a and, since a, e ∈ η L (Σ t ), there are w, u ∈ Σ t such that a = f A w and e
form a group in η L (Σ |u|•n ), and so L is not FO(<, ≡ N )-definable.
To check this criterion, we can use the known PSpace algorithms [9,6] for checking FO(<)-definability of L(A). We now show how to extend this result to any DFA A. Let Q r be the set of accessible states in A. We call words w, v ∈ Σ * equivalent in A and write w ≡ A v if whenever q → w q then there is q ∈ Q r such that q ∼ q and q → v q , and the other way round. Let A * be a minimal
This implies that, in the criterion above, we can replace every f A x = f A y by x ≡ A y and obtain the same criterion for an arbitrary DFA, which is checkable in PSpace. We can finally obtain a criterion of FO(<, ≡ N )-definability of a language given by an NFA by replacing every f A x = f A y by x ≡ A y, where A is the powerset automaton of A. To show that the latter criterion can be checked in PSpace, we observe that each state of A can be stored using polynomial space and then adjust the algorithm for DFAs without increasing its complexity.
Theorem 3. NC 1 -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 NC 1 -hard iff there are u, v, w ∈ Σ * such that, for x ∈ {u, v, w}, f
, for some i u , i v , i w ∈ N that are pairwise coprime. Indeed, L(A) is NC 1 -hard iff there is a non-solvable group in M (L(A)). By [24, Corollary 3], a group is non-solvable iff there are 3 elements with pairwise coprime orders whose product is the identity.
In the PSpace algorithm checking this criterion, we need to compute i u , i v , i w and check that they are pairwise coprime. It is readily seen that those numbers (if exist) are ≤ |Q| |Q| and can be dealt with in PSpace.
Using Theorems 2, 3 and Proposition 1, we obtain: 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 [9]two DFAs A and A of exponential size whose language is FO(<)-definable (starfree) and, respectively, FO(<, ≡ N )-definable (in AC 0 ) iff M rejects x. Then we simulate those DFAs by LTL horn ontologies of polynomial size. Let x be a word and M a Turing machine requiring N = 2 n c tape cells on an input of size n. Let N be the first prime after N + 1. We construct a family {A i } 0≤i<N of simple star-free minimal DFAs whose intersection represents accepting computations of M on x. We encode computations as words over Σ ∪ { , } of the form c 1 c 2 . . . c k−1 c k , where the c i are configurations.
The DFA A 0 checks that an input starts with an initial and ends with an accepting configuration of M on x. The A i , for 0 < i ≤ N , check that the ith symbol in a configuration 'follows' from the (i − 1)th, ith, and (i + 1)th symbols in the previous configuration (if A 1 is constructed, A i can skip the first i − 1 symbols and run A 1 ). The rest of the family just accept all the words with the only at the very end. We then have N i=0 L(A i ) = ∅ iff M rejects x. We next construct minimal DFAs A and A with the languages (L(A 0 ) . . . L(A N −1 )) * and ((L(A 0 ) ∪ { }) . . . (L(A N −1 ) ∪ { })) * . Thus, we obtain:
Now we define LTL horn ontologies O and O simulating A and A . We name the states in A by triples (i, t, j), where i indicates A i the state 'came from', t is a 'type' of the state (say, where the DFA skips the first 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 ≤ 2 k , for k = log 2 N .
The ontology O uses the concepts A i j and L i j , where i = 0, 1 and j = 1, . . . , k, the symbols in Σ ∪ { , }, Q t , for a type t, X, Y and F . Let Σ = Σ ∪ { , , X, Y }.
and let L c , L <c , and L >c be similar concepts for L i j . We represent each triple (i, t, j) as the conjunction A i ∧ Q t ∧ L j . We define O so that, having read a prefix w 1 . . . w l of w, the DFA A is in state (i, t, j) iff O, A w |= (A i ∧ Q t ∧ L j )(l + 1). To achieve this, for every transition (i 1 , t 1 , j 1 ) → a (i 2 , t 2 , j 2 ) of A, we need
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 A 0 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
As a result, O |= (i L ∧ L i ) → F L i+1 . Similarly, we define i A , d L , h A , and
This gives us polynomially many horn axioms in O, to which we add
The ontology O is defined in the same way for the DFA A . It follows that the certain answer to (O, F ) over A w is yes iff w ∈ L(A), and similarly for (O , F ).
Acknowledgements This work was supported by EPSRC U.K. EP/S032282.
Lemma 1. The LTL horn OMAQs (O, F ) and (O, F (x)) are FO(<)-rewritable over Σ -ABoxes iff L(A) is star-free; (O , F ) and (O , F (x)) are FO(<, ≡ N )rewritable over Σ -ABoxes iff L(A ) is in AC 0 .
Proof. We only sketch the proof of the former claim, where (⇒) is clear. (⇐) Suppose L(A) is star-free and A is a Σ -ABox. Then O, A |= F (k) only if (O, A) is inconsistent, and so there are a(i), b(i) ∈ A for some a = b, or A contains a subset of the form {X(i − 1), a 1 (i), a 2 (i + 1), a 3 (i + 2), . . . , a k−i (k − 1), Y (k)} such that a 1 a 2 . . . a k−i ∈ L(A). As L(A) is star-free, it is definable 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 LTL krom OMPEQs over Ξ-ABoxes is ExpSpace-hard.
Proof. Take an LTL horn OMAQ q = (O, A) and Ξ ⊆ sig(q), assuming that the axioms in O are of the form
For any Ξ-ABox A, the certain answers to q and q (and to q(x) and q (x)) over A coincide. It follows that q and q (x) are FO(<)-or FO(<, ≡ N )-rewritable over Ξ-ABoxes iff q and q(x) are FO(<)-or FO(<, ≡ N )-rewritable, respectively.
5 Linear, Krom and core OMAQs and OMPEQs Theorem 7. Deciding FO(<)-or FO(<, ≡ N )-rewritability of linear LTL P horn OMAQs over Ξ-ABoxes is PSpace-complete; NC 1 -completeness is in PSpace.
Proof. One can reduce L-rewritability of linear specific OMAQs to L-rewritability of linear Boolean OMAQs. Let q = (O, A 1 ) be a linear OMAQ. We transform q to q = (O , A 1 ) such that q is L-rewritable over Ξ-ABoxes iff q is and A ∈ idb(O ) only occurs in axioms of the form
is transformed to an ontology O with the following axioms:
and let ext(O) be the set of (maximal) basic concepts P A with A ∈ edb(O) that occur on the left-hand side of an axiom in O. Thus,
, which we illustrate below for the OMAQ q = (O , A 1 ) in our example, assuming that Ξ = {X, Y, Z, W, V, A 1 , A 2 , A 3 } and S → e S implies S → e S for all e ⊇ e:
The proof uses an FO(<)-reduction maping a ∈ Ξ * to e ∈ Γ * q with a ∈ L(q ) iff e ∈ L(B q ), and the other way round. To show that deciding FO(<)-, FO(< , ≡ N )-definability, or NC 1 -completeness of L(B q ) can be done in PSpace is not immediate as neither q nor B q is polynomial in |q|. However, the number of states in B q is polynomial in q and one can check whether q → e q by a PSpace algorithm, which allows us to use Theorems 2 and 3 for B q without explicitly constructing it. The lower bounds are proved by reduction of FO(<)and FO(<, ≡ N )-definability for regular languages. As O is krom, A is inconsistent with O iff (i) there are
are FO(<)-definable for any B, C ∈ Ξ, then L Ξ (q) is FO(<)-definable and q is FO(<)-rewritable over Ξ-ABoxes. For any B, C, we construct an NFA A BC over the alphabet {∅} of size O(|q|) that accepts L BC [4]. Using [22, Theorem 6.1], we show that deciding FO(<)-rewritability of the language of a unary NFA is coNP-complete, obtaining the required upper bound. To show the matching lower bound, for any unary NFA A = (Q, {a}, δ, I, F ), we define an LTL core ontology O A with the axioms X → I, q ∧ Y → ⊥ and p → F r, for all q ∈ F and transitions p → a r in δ. The OMAQ (O A , A) is FO(<)-rewritable over {X, Y }-ABoxes iff L(A) is FO(<)-definable, as the answer to the OMAQ over an {X, Y }-ABox A can only be yes iff there are X(i), Y (j) ∈ A with a j−i−1 ∈ L(A). Theorem 9. Deciding FO(<)-rewritability of LTL core OMPEQs q = (O, κ) over Ξ-ABoxes is Π p 2 -complete.
Proof. We assume that O does not contain disjointness axioms B ∧ C → ⊥ as they can be removed from O and κ replaced by κ ∨ O|=B∧C→⊥ 3 F 3 P (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 specific OMQs can be reduced to rewritability of Boolean OMQs. Given O, A, B and k, one can check in polytime whether O, A |= B(k), which, by structural induction, implies that checking O, A |= ∃xκ(x) is in NP.
Ξ -words v and v , we write v ≤ v if they are of the same length and v i ⊆ v i , for all i.
As q is an LTL core OMPEQ, we have O, A |= q iff O, A |= q, for some A ⊆ A, |A | ≤ |κ|. Then, for every v ∈ Σ * Ξ , we have v ∈ L Ξ (q) iff there is v ≤ v such that v ∈ L w for some w ∈ B. It follows that the language L Ξ (q) is FO(<)definable iff L w is FO(<)-definable, for every w ∈ B. For w = w 1 . . . w k ∈ B and I = (i 0 , . . . , i k ), let v w,I = ∅ i0 w 1 ∅ i1 . . . w k ∅ i k . For c ∈ N, let I ≤c be I with all i j > c replaced with c. If L w is FO(<)-definable, there is c with v w,I ∈ L w iff v w,I<c ∈ L w . By the properties of the canonical models [4], there is a suitable c with c < 2 |sig(q)|+|κ| + 1. Now, q is not FO(<)-rewritable iff we can guess w ∈ B and I such that max(I) < 2c and only one of v w,I and v w,I<c is in L w . We can check membership in L w using an NP-oracle, so FO(<)-rewritability is in coNP NP = Π p 2 . The matching lower bound is shown by reduction of ∀∃3CNF [21]. Given a QBF ∀X∃Y ϕ with a 3CNF ϕ, X = {x 1 , . . . , x n } and Y = {y 1 , . . . , y m }, we construct an LTL core OMPEQ q ϕ = (O ϕ , κ ϕ ) that is FO(<)-rewritable iff ∀X∃Y ϕ(X, Y ) is true. We use atomic concepts x 0 i and x 1 i for x i ∈ X, y j i for y i ∈ Y and 0 ≤ j < p i , where p i is the i-th prime number, A and B. O ϕ has the axioms
Let ϕ result from ϕ by replacing all x i with x 1 i , all ¬x i with x 0 i , and similarly for the y j . We set κ
, and so, for every i, there is x 0 i (s) or x 1 i (s) in A, for some s ≤ t. There is an assignment a 1 ∈ 2 X such that O ϕ , A |= x a1(i) i (s) for all s > t. Take a corresponding assignment a 2 ∈ 2 Y that makes ϕ true. There exists a number r such that r mod p i = a 2 (i) for all i ≤ m. Therefore O ϕ , A |= ϕ (t + r), and so O ϕ , A |= 3 F ϕ (t). Thus, the sentence
is a rewriting of q ϕ . If ∀X∃Y ϕ(X, Y ) is false, then there is a ∈ 2 X such that ϕ is false for any assignment to Y . For w = {B}X a , X a = {A, x a(0) 1 , . . . , x a(n) n }, the language L w is L(∅ * {B}(∅∅) * X a ∅ * ), and so q ϕ cannot be FO(<)-rewritable.