Deciding FO-rewritability of Ontology-Mediated Queries in Linear Temporal Logic Vladislav Ryzhikov1 , Yury Savateev1,2 , and Michael Zakharyaschev1 1 Department of Computer Science, Birkbeck, University of London, U.K. 2 National Research University Higher School of Economics, Moscow, Russia Abstract. 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 NC1 - complete, 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. 1 Introduction 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 an- swering that OMQ and construct its rewriting of optimal type. The datalog com- munity has been investigating FO- and linear-datalog-rewritability (aka bound- edness and linearisability) of datalog programs since the 1980s [26,25,11,19]. The data complexity and rewritability of individual OMQs in various description log- ics 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 3F (eventually) and F / P (next/previous minute): Malfunction → 3F Fixed, (1) Fixed → F InOperation, (2) Copyright © 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). 2 Malfunction ∧ P Malfunction ∧ 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 _ _ i ¬ Fj InOperation ,  κ = Malfunction ∧ F Fixed ∧ 1≤i≤5 1≤j≤5 which can be understood as a Boolean query asking whether there was a mal- function 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 prim- itive recursion (or to a monadic second-order formula), whose evaluation over data instances is in the complexity class NC1 . Here, we first establish a con- nection 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 con- tain P only, deciding FO(<)-rewritability turns out to be PSpace-complete; the complexity goes down to coNP for OMAQs with Krom ontologies and the next- and previous-time operators. On the other hand, deciding FO(<)-rewritability becomes Π2p -complete for core (that is, both Horn and Krom) ontologies and positive existential temporal queries, which do not contain negation and the op- erators 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 AC0 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 ACC0 , in which case it is FO(<, MOD)- rewritable, or NC1 -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: class of OMQs in AC0 in ACC0 / NC1 -comp. FO(<) FO(<, ≡N ) FO(<, MOD)/FO(RPR) LTL OMQs LTLhorn P OMAQs ExpSpace [Th.1,5,6] ExpSpace [Th.4,5,6] ≤ ExpSpace [Th.4] LTLkrom OMPEQs lin. LTLhorn P OMAQs PSpace [Th. 7] PSpace [Th. 7] ≤ PSpace [Th. 7] LTLkrom OMAQs coNP [Th. 8] all in AC0 [4] – p LTLcore OMPEQs Π2 [Th. 9] all in AC0 [4] – 2 Preliminaries In our setting, the alphabet of linear temporal logic LTL comprises a set of atomic concepts Ai , i < ω. Basic temporal concepts, C, are defined by the grammar C ::= Ai | 2F C | 2P C | F C | 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 finite 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 [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 LTLoc -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 LTLohorn - ontology is called linear if each of its axioms C1 ∧ · · · ∧ Ck → B is such that B is either ⊥ or atomic and at most one Ci , 1 ≤ i ≤ k, is an IDB concept. An ABox is a finite set A of atoms Ai (`), for ` ∈ Z, together with a finite interval tem(A) = [min A, max A] of integers such that min A < max A and whenever Ai (`) ∈ 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 Ξ-ABox if Ai (`) ∈ A implies Ai ∈ Ξ. 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, AI0 , AI1 , . . . ) with AIi ⊆ 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]: ( F κ)I = n ∈ Z | n + 1 ∈ κ I , (2F κ)I = n ∈ Z | k ∈ κ I , for all k > n ,   (3F κ)I = n ∈ Z | there is k > n with k ∈ κ I ,  (κ1 U κ2 )I = n ∈ Z | there is k > n with k ∈ κ2I and m ∈ κ1I for n < m < k ,  and symmetrically for the past operators. An axiom (4) is true in I if we have C1I ∩ · · · ∩ CkI ⊆ Ck+1 I I ∪ · · · ∪ Ck+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 (`) ∈ A implies ` ∈ AIi . An LTLoc ontology-mediated query (OMQ) is a pair of the form q = (O, κ), where O is an LTLoc 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 I of O and A, there is k ∈ Z such that k ∈ κ I , in which case we write (O, A) |= ∃xκ(x). If (O, A) 6|= ∃xκ(x), the certain answer to q over A is no. We write (O, A) |= κ(k), for k ∈ Z, if k ∈ κ I in all models I of O and A. A certain answer to a specific OMQ q(x) = (O, κ(x)) over A is any k ∈ tem(A) with (O, A) |= κ(k). 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. Example 2. (i) Let q 1 = (O1 , C ∧ D) with O1 = {3P A → B, 2F B → C}. The certain answer to q 1 over A1 = {D(0), B(1), A(1)} is yes, but  over A2 = {D(0), A(1)} it is no. The only answer to q 1 (x) = O1 , (C ∧ D)(x) over A1 is 0. (ii) Let O2 = { P A → B, P B → A, A∧B → ⊥ }. The answer to q 2 = (O2 , C) over A1 = {A(0)} is no, but over A2 = {A(0), A(1)} it is yes. There are no answers to q 2 (x) = (O1 , C(x)) over A1 , while over A2 there are two of them: 0 and 1. (iii) Let O3 = { P Bk ∧A0 → Bk , P B1−k ∧A1 → Bk | k = 0, 1}. For any word e = e1 . . . en ∈ {0, 1}n , let Ae = {B0 (0)} ∪ {Aei (i) | 0 < i ≤ n} ∪ {E(n)}. The answer to q 3 = (O3 , B0 ∧ E) over Ae is yes iff the number of 1s in e is even. (iv) Let O4 = {A → F B} and q 4 = (O4 , B). Then, the answer to q 4 over A = {A(0)} is yes; however, there are no certain answers to q 4 (x) = (O4 , B(x)) over A. (v) Let O5 = {A → B ∨ F B}. The certain answer to q 5 = (O5 , 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 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 q 0 = (O0 , κ) in the sense that q and q 0 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 or- ders. 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 SA |= Q. Here, SA is a structure with domain tem(A) ordered by <, in which SA |= Ai (`) iff Ai (`) ∈ A. A specific 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 iff SA |= 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; FO(<, ≡N ) FO(<)-formulas with predicates x ≡ 0 (mod N ), for any N > 1; FO(<, MOD) FO(<)-formulas with quantifiers ∃N , for N > 1, defined by taking SA |= ∃Nx ψ(x) iff the cardinality of the set {n ∈ tem(A) | SA |= ψ(n)} is divisible by N (x ≡ 0 (mod N ) can obviously be defined as ∃Ny (y < x)); FO(RPR) FO(<) with relational primitive recursion [10]. Example 3. (i) An FO(<)-rewriting of q 01 (x) is ϕ1 (x) = D(x) ∧ [C(x) ∨ ∃y(A(y) ∧ ∀z ((x < z ≤ y) → B(z)))], ∃xϕ1 (x) is an FO(<)-rewriting of q 1 . (ii) An FO(<, ≡N )-rewriting of q 2 (x) is ϕ2 (x) = C(x) ∨ ∃x, 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 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 AC0 [13]; the following is an FO(<, MOD)-rewriting of q 3 : ϕ3 = ∃x, y E(x) ∧ (x ≤ y) ∧ ∀z((y < z ≤ x) → (A0 (z) ∨ A1 (z))) ∧ ((B0 (y) ∧ ∃2 z ((y < z ≤ x) ∧ A1 (z))) ∨ (B1 (y) ∧ ¬∃2 z ((y < z ≤ x) ∧ A1 (z)))). (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 spe- cific) LTL OMQs are FO(RPR)-rewritable and can be answered in NC1 . 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 wA = a0 . . . an with ai = {A | A(i) ∈ A}. Conversely, any ΣΞ -word w = a0 . . . an can be understood as an ABox Aw with tem(Aw ) = [0, n] and A(i) ∈ Aw iff A ∈ 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 0 0 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 wA,i = a0 . . . a0i . . . an , where aj = {A | A(j) ∈ A} ∈ ΣΞ for j 6= i, and a0i = {A | A(i) ∈ A} ∈ ΣΞ 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 iff LΞ (q) is L- definable. (ii) A specific OMQ q(x) = (O, κ(x)) is L-rewritable over Ξ-ABoxes iff LΞ (q(x)) is L-definable. 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 define an NFA ∗ A over ΣΞ whose language is ΣΞ \ LΞ (q). The states in A comprise the set Q¬κ = {τ ∈ T | ¬κ ∈ τ }. 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): a ⊆ τ2 , C1 U C2 ∈ τ1 iff C2 ∈ τ2 or C1 U C2 ∈ τ2 and C1 ∈ τ2 , and symmetrically for S. The set of initial states comprises τ ∈ Q¬κ with τ ∪ {2P ¬κ} is consistent with O; the set of accepting states comprises those τ ∈ Q¬κ for which τ ∪ {2F ¬κ} is consistent with O. It ∗ is readily seen that, for every a ∈ ΣΞ we have a ∈ L(A) iff (O, Aa ) 6|= ∃xκ(x). The number of states in A does not exceed O(2|q| ). Since LTL-satisfiability is in PSpace, the NFA A can be constructed in exponential time in |q|. The following table summarises known results connecting definability of reg- ular 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 complex- ity (under a reasonable binary encoding of L’s alphabet): definability of L algebraic characterisation of L circuit complexity FO(<) M (L) is aperiodic FO(<, ≡N ) ηL is quasi-aperiodic in AC0 FO(<, MOD) all groups in M (L) are solvable in ACC0 FO(RPR) arbitrary M (L) in NC1 – M (L) contains unsolvable group NC1 -hard The statement in the table that all groups in M (L) are solvable iff L is in ACC0 holds unless ACC0 = NC1 . 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 AC0 , (b) an OMQ is FO(<, MOD)-rewritable iff it can be answered in ACC0 (unless ACC0 = NC1 ), (c) an OMQ is FO(<, RPR)-rewritable iff it can be answered in NC1 . 3 Deciding FO-Rewritability: Upper Bounds Since deciding FO(<)-definability of regular languages given by NFAs is PSpace- complete [9,6], we obtain by Proposition 1: Theorem 1. Deciding FO(<)-rewritability of LTL2 bool OMQs over Ξ-ABoxes is in ExpSpace. The exact complexity of deciding FO(<, ≡N )-definability and NC1 -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, Σ, δ, Q0 , F ), states q, q 0 ∈ Q, and w = a0 . . . an ∈ Σ ∗ , we write q →w q 0 if there is a run of A on w that starts with (q0 , 0) and ends with (q 0 , n + 1). We say that a state q ∈ Q is accessible if q 0 →w q, for some q 0 ∈ Q0 and w ∈ Σ ∗ . Two states q1 , q2 ∈ Q are equivalent if, for each w ∈ Σ ∗ , we have q1 →w q 0 for some q 0 ∈ F iff q2 →w q 00 for some q 00 ∈ F . A DFA is minimal if each of its states is accessible and it has no distinct equivalent states. Every DFA A = (Q, Σ, δ, q0 , F ) can be converted to a minimal DFA A0 = (Q0 , Σ, δ 0 , q00 , F 0 ) with L(A) = L(A0 ) 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 0 iff q and q 0 are equivalent. Clearly, ∼ is an equivalence relation; we denote by q/∼ the equivalence class of q ∈ R. Now, we set Q0 = {q/∼ | q ∈ R} and define δ 0 by taking q/∼ →a q 0 /∼ , where {q 0 } = δ(a, q), for all q ∈ R and a ∈ Σ (which is obviously well-defined). Finally, we set q00 = q0 /∼ and F 0 = {q/∼ | q ∈ R ∩ F }. It is known that, for any regular language L, all minimal DFAs A0 with L(A0 ) = L are isomorphic; we call each such A0 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, Σ, δ, q0 , F ) and w ∈ Σ ∗ , define a map fwA : Q → Q by setting fwA (q) = q 0 iff q →w q 0 . The transition monoid of A takes the form M = ({fwA | w ∈ Σ ∗ }, ·, fεA ), where ε is the empty word and fwA fvA = fwv A , 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 defined by ηL (w) = fwA 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, Σ, δ, q0 , F ) be minimal. We use the following criterion: L(A) is not FO(<, ≡N )-definable iff there are w and n ∈ N such that fwA 6= fwA2 , fwA = fwAn , and fwA = fvA , fwA2 = fuA , 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 6= 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 = fwA and e = fwA|G| = fuA . (⇐) Observe that fwAi = fwAi wn(n−i) = fuAi vn−i , for 1 ≤ i ≤ n. Therefore, fwA , . . . , fwAn 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 Qr 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 0 then there is q 00 ∈ Qr such that q 00 ∼ q 0 and q →v q 00 , and the other way round. Let A∗ be a minimal ∗ ∗ DFA of L(A). One can show that w ≡A v iff fwA = fvA . This implies that, in the criterion above, we can replace every fxA = fyA 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 fxA = fyA by x ≡A0 y, where A0 is the powerset automaton of A. To show that the latter criterion can be checked in PSpace, we observe that each state of A0 can be stored using polynomial space and then adjust the algorithm for DFAs without increasing its complexity. 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 iff there are u, v, w ∈ Σ ∗ such that, for x ∈ {u, v, w}, fxA = fxA fuvw A , fxA 6= fxA2 and fuvw A = fxAix , for some 1 iu , iv , iw ∈ N that are pairwise coprime. Indeed, L(A) is NC -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 iu , iv , iw 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: Theorem 4. Both FO(<, ≡N )-rewritability and NC1 -completeness (in data com- plexity) of LTL2 bool OMQs over Ξ-ABoxes are decidable in ExpSpace. 4 Deciding FO-Rewritability: Lower Bounds 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 [9]— two DFAs A and A0 of exponential size whose language is FO(<)-definable (star- free) and, respectively, FO(<, ≡N )-definable (in AC0 ) iff M rejects x. Then we simulate those DFAs by LTLhorn ontologies of polynomial size. c Let x be a word and M a Turing machine requiring N = 2n tape cells 0 on an input of size n. Let N be the first prime after N + 1. We construct a family {Ai }0≤ic = A1i ∧ Aj j bi =1 j>i bi =0 j>i and let Lc , Lc be similar concepts for Lij . We represent each triple (i, t, j) as the conjunction Ai ∧ Qt ∧ Lj . We define O so that, having read a prefix w1 . . . wl of w, the DFA A is in state (i, t, j) iff O, Aw |= (Ai ∧ Qt ∧ Lj )(l + 1). To achieve this, for every transition (i1 , t1 , j1 ) →a (i2 , t2 , j2 ) of A, we need O |= Ai1 ∧ Qt1 ∧ Lj1 ∧ a → F Ai 2 ∧ 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 → B ∨ B̄ | B ∈ sig(q)} and _ _ κ = A ∨ 3F 3P C ∨ 3F 3P (C ∧ B̄). C→⊥ in O C→B in O For any Ξ-ABox A, the certain answers to q and q 0 (and to q(x) and q 0 (x)) over A coincide. It follows that q 0 and q 0 (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 LTLhorn P 1 OMAQs over Ξ-ABoxes is PSpace-complete; NC -completeness is in PSpace. Proof. One can reduce L-rewritability of linear specific OMAQs to L-rewritability of linear Boolean OMAQs. Let q = (O, A1 ) be a linear OMAQ. We transform q to q 0 = (O0 , A01 ) such that q 0 is L-rewritable over Ξ-ABoxes iff q is and A ∈ idb(O0 ) only occurs in axioms of the form P`1 C1 ∧ · · · ∧ P`k Ak ∧ P A → B. For example, O = { P X → A2 , P3 Y ∧ P A2 → A1 , Z ∧ P A1 → A2 , P4 W ∧ A2 → A3 , V ∧ P A3 → ⊥ } is transformed to an ontology O0 with the following axioms: A1 → A01 , A2 → A02 , A3 → A03 , P X → A02 , P 4 W∧ P X → A03 , 4 P W ∧ A2 → A03 , 3 P Y ∧ P A02 → A01 , Z ∧ P A01 → A02 , 4 P W∧ 0 0 P A2 → A3 , V ∧ 0 P A3 → ⊥, 4 0 0 5 0 P W ∧Z ∧ P A1 → A3 , V ∧ PW ∧ P A2 → ⊥. Let edb(O) = sig(q)\idb(O) 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, ext(O0 ) = { P X, P3 Y, Z, P4 W, V, P5 W, A1 , A2 , A3 } in the example above. 0 Let extΞ (O0 ) = ext(O0 )  Ξ. Define an NFA Bq0 over Γq0 = 2extΞ (O ) , which 0 0 0 we illustrate below for the OMAQ q = (O , A1 ) in our example, assuming that Ξ = {X, Y, Z, W, V, A1 , A2 , A3 } and S →e S 0 implies S →e0 S 0 for all e0 ⊇ e: ∅ start A00 { P4 W, P X}, { P4 W, A2 } { P X}, {A2 } {A1 } { P3 Y }, {V, 5 P W} { P4 W, Z} A02 A01 A03 {Z} {V } ∅ { P4 W } We show that L(q 0 ) is L-definable over Ξ-ABoxes iff L(Bq0 ) is L-definable. The proof uses an FO(<)-reduction maping a ∈ Ξ ∗ to e ∈ Γq∗0 with a ∈ L(q 0 ) iff e ∈ L(Bq0 ), and the other way round. To show that deciding FO(<)-, FO(< , ≡N )-definability, or NC1 -completeness of L(Bq0 ) can be done in PSpace is not immediate as neither q 0 nor Bq0 is polynomial in |q|. However, the number of states in Bq0 is polynomial in q and one can check whether q →e q 0 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 )-definability for regular languages. Theorem 8. Deciding FO(<)-rewritability of LTLkrom OMAQs q = (O, A) over Ξ-ABoxes is coNP-complete. Proof. Let q 0 = (O0 , Y ) with O0 = O ∪ {A → ⊥} and fresh Y , and q 00 = (O00 , Y ) with O00 = O ∪ {X ∧ A → ⊥} and fresh X, Y . For any (X, Y -free) ABox A, (O, A) |= ∃xA(x) iff (O0 , A) |= ∃x Y (x) iff A is inconsistent with O0 ; similarly, (O, A) |= A(k) iff (O00 , A∪{X(k)}) |= ∃xA(x) iff A∪{X(k)} is inconsistent with O00 , for k ∈ 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 iff (i) there are A(i), B(i) ∈ A with O |= B ∧ A → ⊥, or (ii) there exist k1 ≤ k2 , B(k1 ) ∈ A and C(k2 ) ∈ A with O |= B → Fk2 −k1 ¬C; cf. [4]. So if all LBC = {∅n | O |= B → Fn+1 ¬C} 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 ABC over the alphabet {∅} of size O(|q|) that accepts LBC [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 LTLcore ontology OA with the axioms X → I, q ∧ Y → ⊥ and p → F r, for all q ∈ F and transitions p →a r in δ. The OMAQ (OA , 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 aj−i−1 ∈ L(A). Theorem 9. Deciding FO(<)-rewritability of LTLcore OMPEQs q = (O, κ) over Ξ-ABoxes is Π2p -complete. Proof. We assume that O does not contain disjointness W axioms B ∧ C → ⊥ as they can be removed from O and κ replaced by κ ∨ O|=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 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 P checking O, A |= ∃xκ(x) is in NP. ∗ Let B = {w1 . . . wk ∈ ΣΞ | ∀i |w(i)| > 0, i |w(i)| < |κ|}. With every w ∈ B we associate the language Lw = L(∅∗ w1 ∅∗ . . . ∅∗ wk ∅∗ ) ∩ LΞ (q). For ΣΞ ∗ -words v 0 0 0 and v , we write v ≤ v if they are of the same length and vi ⊆ vi , for all i. As q is an LTLcore OMPEQ, we have O, A |= q iff O, A0 |= q, for some A ⊆ A, |A0 | ≤ |κ|. Then, for every v ∈ ΣΞ 0 ∗ , we have v ∈ LΞ (q) iff there is v 0 ≤ v 0 such that v ∈ Lw for some w ∈ B. It follows that the language LΞ (q) is FO(<)- definable iff Lw is FO(<)-definable, for every w ∈ B. For w = w1 . . . wk ∈ B and I = (i0 , . . . , ik ), let vw,I = ∅i0 w1 ∅i1 . . . wk ∅ik . For c ∈ N, let I≤c be I with all ij > c replaced with c. If Lw is FO(<)-definable, there is c with vw,I ∈ Lw iff vw,I t. Take a corresponding assignment a2 ∈ 2Y that makes ϕ true. There exists a number r such that r mod pi = a2 (i) for all i ≤ m. Therefore Oϕ , A |= ϕ0 (t + r), and so Oϕ , A |= 3F ϕ0 (t). Thus, the sentence n ^ ∃s (s 6 t) ∧ (x0i (s) ∨ x1i (s))   ∃t A(t) ∧ i=0 is a rewriting of q ϕ . If ∀X∃Y ϕ(X, Y ) is false, then there is a ∈ 2X such that ϕ is a(0) a(n) false for any assignment to Y . For w = {B}Xa , Xa = {A, x1 , . . . , xn }, the language Lw is L(∅∗ {B}(∅∅)∗ Xa ∅∗ ), and so q ϕ cannot be FO(<)-rewritable. Acknowledgements This work was supported by EPSRC U.K. EP/S032282. References 1. Artale, A., Calvanese, D., Kontchakov, R., Zakharyaschev, M.: The DL-Lite family and relations. Journal of Artificial Intelligence Research (JAIR) 36, 1–69 (2009) 2. Artale, A., Kontchakov, R., Kovtunova, A., Ryzhikov, V., Wolter, F., Za- kharyaschev, M.: First-order rewritability of temporal ontology-mediated queries. In: Yang, Q., Wooldridge, M. (eds.) Proceedings of the Twenty-Fourth Interna- tional Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Ar- gentina, July 25-31, 2015. pp. 2706–2712. AAAI Press (2015), http://ijcai.org/ Abstract/15/383 3. Artale, A., Kontchakov, R., Kovtunova, A., Ryzhikov, V., Wolter, F., Za- kharyaschev, M.: Ontology-mediated query answering over temporal data: A survey (invited talk). In: Schewe, S., Schneider, T., Wijsen, J. (eds.) 24th International Symposium on Temporal Representation and Reasoning, TIME 2017, October 16- 18, 2017, Mons, Belgium. LIPIcs, vol. 90, pp. 1:1–1:37. Schloss Dagstuhl - Leibniz- Zentrum für Informatik (2017), https://doi.org/10.4230/LIPIcs.TIME.2017.1 4. Artale, A., Kontchakov, R., Kovtunova, A., Ryzhikov, V., Wolter, F., Za- kharyaschev, M.: First-order rewritability of ontology-mediated queries in lin- ear temporal logic. CoRR abs/2004.07221 (2020), https://arxiv.org/abs/2004. 07221 5. Barrington, D.A.M., Compton, K.J., Straubing, H., Thérien, D.: Regular languages in NC1 . J. Comput. Syst. Sci. 44(3), 478–499 (1992), https://doi.org/10.1016/ 0022-0000(92)90014-A 6. Bernátsky, L.: Regular expression star-freeness is PSPACE-complete. Acta Cy- bern. 13(1), 1–21 (1997), http://www.inf.u-szeged.hu/actacybernetica/edb/ vol13n1/Bernatsky_1997_ActaCybernetica.xml 7. Bienvenu, M., ten Cate, B., Lutz, C., Wolter, F.: Ontology-based data access: A study through disjunctive datalog, CSP, and MMSNP. ACM Transactions on Database Systems 39(4), 33:1–44 (2014) 8. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: Tractable reasoning and efficient query answering in description logics: the DL-Lite family. Journal of Automated Reasoning 39(3), 385–429 (2007) 9. Cho, S., Huynh, D.T.: Finite-automaton aperiodicity is PSPACE-complete. Theor. Comp. Sci. 88(1), 99–116 (1991), https://core.ac.uk/download/pdf/82662203. pdf 10. Compton, K.J., Laflamme, C.: An algebra and a logic for NC1 . Inf. Comput. 87(1/2), 240–262 (1990) 11. Cosmadakis, S.S., Gaifman, H., Kanellakis, P.C., Vardi, M.Y.: Decidable opti- mization problems for database logic programs (preliminary report). In: STOC. pp. 477–490 (1988) 12. Demri, S., Goranko, V., Lange, M.: Temporal Logics in Computer Science. Cam- bridge Tracts in Theoretical Computer Science, Cambridge University Press (2016) 13. Furst, M.L., Saxe, J.B., Sipser, M.: Parity, circuits, and the polynomial-time hier- archy. Mathematical Systems Theory 17(1), 13–27 (1984) 14. Gabbay, D., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-Dimensional Modal Logics: Theory and Applications, Studies in Logic, vol. 148. Elsevier (2003) 15. Gerasimova, O., Kikot, S., Kurucz, A., Podolskii, V., Zakharyaschev, M.: A data complexity and rewritability tetrachotomy of ontology-mediated queries with a covering axiom. In: Proceedings of KR (2020) 16. Hernich, A., Lutz, C., Ozaki, A., Wolter, F.: Schema.org as a description logic. In: Yang, Q., Wooldridge, M.J. (eds.) Proceedings of the Twenty-Fourth Inter- national Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015. pp. 3048–3054. AAAI Press (2015), http://ijcai. org/Abstract/15/430 17. Lutz, C., Wolter, F.: Non-uniform data complexity of query answering in descrip- tion logics. In: Proc. of the 13th Int. Conference on Principles of Knowledge Rep- resentation and Reasoning (KR 2012). pp. 297–307. AAAI (2012) 18. Lutz, C., Sabellek, L.: Ontology-mediated querying with the description logic EL: trichotomy and linear datalog rewritability. In: Sierra, C. (ed.) Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017. pp. 1181–1187. ijcai.org (2017), https://doi.org/10.24963/ijcai.2017/164 19. Marcinkowski, J.: DATALOG sirups uniform boundedness is undecidable. In: Pro- ceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996. pp. 13–24. IEEE Computer So- ciety (1996), https://doi.org/10.1109/LICS.1996.561299 20. Poggi, A., Lembo, D., Calvanese, D., De Giacomo, G., Lenzerini, M., Rosati, R.: Linking data to ontologies. Journal on Data Semantics X, 133–173 (2008) 21. Stockmeyer, L.J.: The polynomial-time hierarchy. Theor. Comput. Sci. 3(1), 1–22 (1976), https://doi.org/10.1016/0304-3975(76)90061-X 22. Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: Prelim- inary report. In: Aho, A.V., Borodin, A., Constable, R.L., Floyd, R.W., Harrison, M.A., Karp, R.M., Strong, H.R. (eds.) Proceedings of the 5th Annual ACM Sym- posium on Theory of Computing, April 30 - May 2, 1973, Austin, Texas, USA. pp. 1–9. ACM (1973), https://doi.org/10.1145/800125.804029 23. Straubing, H.: Finite Automata, Formal Logic, and Circuit Complexity. Birkhauser Verlag (1994) 24. Thompson, J.G.: Nonsolvable finite groups all of whose local subgroups are solv- able. Bull. Amer. Math. Soc. 74(3), 383–437 (05 1968), https://projecteuclid. org:443/euclid.bams/1183529612 25. Ullman, J.D., Gelder, A.V.: Parallel complexity of logical query programs. Algo- rithmica 3, 5–42 (1988), https://doi.org/10.1007/BF01762108 26. Vardi, M.Y.: Decidability and undecidability results for boundedness of linear re- cursive queries. In: Edmondson-Yurkanan, C., Yannakakis, M. (eds.) Proceedings of the Seventh ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, March 21-23, 1988, Austin, Texas, USA. pp. 341–351. ACM (1988), http://doi.acm.org/10.1145/308386.308470