=Paper=
{{Paper
|id=Vol-2663/paper-19
|storemode=property
|title=Recognising FO-rewritability of Ontology-Mediated Queries in Linear Temporal Logic
|pdfUrl=https://ceur-ws.org/Vol-2663/paper-19.pdf
|volume=Vol-2663
|authors=Vladislav Ryzhikov,Yury Savateev,Michael Zakharyaschev
|dblpUrl=https://dblp.org/rec/conf/dlog/RyzhikovSZ20
}}
==Recognising FO-rewritability of Ontology-Mediated Queries in Linear Temporal Logic==
https://ceur-ws.org/Vol-2663/paper-19.pdf
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