We report on our initial results regarding the data complexity of answering atomic queries mediated by ontologies given in a Horn fragment of the metric temporal logic MTL. We adopt the pointwise semantics for MTL over dense time. The complexity classes involved are AC0, NC1, L, NL, and P. Our general concern is detecting events in a complex asynchronous system based on qualitative sensor measurements. More precisely, the system in question has a number of sensors that from time to time and asynchronously send their readings to a database. We may think of such readings as pairs of the form (A; t), where A is a concept name and t a timestamp given as a non-negative nite binary fraction such as 101.011. As a formalism to dene events we use propositional Horn clauses with operators of the metric temporal logic MTL [14,2]. For example, according to Siemens, a gas turbine has a normal stop if the rotor speed coasts down from 1500 to 200, which was preceded by another coast down from 6600 to 1500 some time in the previous 9 minutes, at most 2 minutes before which the main ame was o, while the active power was o earlier within another 2 minutes. The event 'normal stop' can be encoded by the following hornMTL rule, where (n;m]' is assumed to hold true at a timestamp t if ' holds at some previous timestamp t0 with n < t t0 m: CoastDown1500to200 ^ (0;9m] CoastDown6600to1500 ^ (the concepts on the right-hand side can be dened by similar rules). The use of hornMTL and datalogMTL ontologies (with both diamond and box operators in rule bodies and only box operators in rule heads) for querying temporal log data was advocated in [9], which also demonstrated experimentally feasibility and eciency of ontology-based data access (OBDA) with nonrecursive datalogMTL queries. An extension of the OBDA platform Ontop to support such queries was suggested in [8]. For a recent survey of temporal OBDA we refer the reader to [5]; surveys of early developments in temporal deductive databases
NormalStop
are given in [
In this paper, we start investigating the data complexity of answering
ontology-mediated queries (OMQs) with MTL operators. As the problem turns out
to be quite involved, we restrict ourselves to atomic queries and ontologies in
the fragment hornMTL of hornMTL where only past diamond operators are
allowed in rule bodies and no temporal operators can be used in rule heads. We
distinguish between arbitrary, linear and core (or binary) rules and consider, in
particular, the following types of the range % in %: hr; 1), h0; ri, and [r; r] where
h is one of [ or (, while i is one of ] or ). The underlying timeline is (R; ) as
we cannot assume that sensor readings come at regular time intervals. There
are two standard semantics for MTL over (R; ): continuous and pointwise ;
see, e.g., [
below, where ‘range-uniform’ means that all the % operators before intensional concept names in a given hornMTL program have the same range %: rules n ranges
linear core any hr; 1) = P = NL in AC0
NL h0; ri
L
NC1 in AC0(range-uniform) [r; r]
L NC1 L 2
Q2; the set of non-negative dyadic rationals is denoted by Q2 0. As well-known,
the form [t1; t2], [t1; t2), (t1; t2] or (t1; t2), where t1; t2 2 Q2 [ f 1; 1g and t1 t2, excluding t1 = t2 2 f 1; 1g. We identify (t; 1] with (t; 1), [ 1; t] with ( 1; t], etc. A range, %, is an interval with non-negative endpoints.
operators indexed by ranges, say (0;60], which is interpreted over (R; <) as ‘at every time instant within the previous minute’, its future counterpart (0;60], and their dual diamond operators (0;60] and (0;60]. In this paper, we only consider a fragment of MTL that is called hornMTL .
where k
A
B1 ^
^ Bk; B ::= A j > j %B; (1) with A being a concept name or ?. As usual, A is called the head of the rule, and B1 ^ : : : ^ Bk its body. A hornMTL program is linear if, in each of its rules, at most one of the concepts in the body occurs as a head in . A hornMTL program is core if all of its rules are of the form A B or ? B1 ^ B2. A hornMTL (ontology-mediated) query takes the form ( ; A(x)).
D = f(A1; t1); : : : ; (An; tn)g, where the Ai are concept names from some xed alphabet and the ti are (not necessarily ordered) timestamps from Q2 0. When proving some complexity results, we assume that D is given as the FO-structure D = ( ; <; ; bitin ; bitfr ; A1; : : : ; Ap); (2) in which
= f0; : : : ; `g N, where ` is the maximum of the number of distinct timestamps in D and the number of bits in the longest binary fraction in D (excluding the binary point), and < is the usual order on ;
is a set of timestamps ; for every n 2 , we set n = b` b0:c0 c` such that bitin (i; n; bi) and bitfr (i; n; ci) hold, for i = 0; : : : ; `; thus, bitin and bitfr are ternary relations on such that, for any n 2 and i 2 , there is a unique bi 2 f0; 1g and a unique ci 2 f0; 1g with bitin (i; n; bi) and bitfr (i; n; ci);
Ai , for i = 1; : : : ; p; intuitively, Ai(n) holds i Ai(n) 2 D.
For any d 2 Q2 0, one can readily dene FO-formulas: dist<d(x; y) that holds in D i x; y 2 and 0 dist>d(x; y) that holds in D i x; y 2 and x their modications dist d(x; y) and dist d(x; y). x y < d; y > d; It will be convenient to assume that these predicates are also given by D for the relevant d. In Theorem 5, we also make the following assumption: (ord) = f0; : : : ; kg, for some k `, and n < m k implies n < m.
I = (T; A1I ; A2I ; : : : ); where T 6= ; is a nite subset of Q2 0 (timestamps) and AI i if B = A, BI = T if B = >, BI = ; if B = ?, and T. We set BI = AI ( %B)I = ft 2 T j 9t0 2 BI (t t0 2 %)g: I is a model of a data instance D if t 2 AI for any (A; t) 2 D; I is a model of a hornMTL program if, for any rule (1) in and any t 2 T, we have t 2 AI whenever t 2 BiI for 1 i k. We say that D and are consistent if there is a model of D and . We also say that a timestamp t from D is a certain answer to a query ( ; A(x)) over D if t 2 AI , for every model I of D and . The query answering problem for ( ; A(x)) is to decide, given a data instance
a continuous interpretation is dened over the reals: I = (R; A1I ; A2I ; : : : ) with AiI R and ( %B)I = ft 2 R j 9t0 2 BI (t t0 2 %)g. To illustrate, suppose that = fA (0;1] (0;1]Bg and D = f(B; 0); (C; 2)g. Then ( ; A) has no answers over D under the former semantics (because 1 is not a timestamp in D), but 2 is an answer under the latter one.
P0 P0 %01 P10 ^ %1 P1 ^ ^ %0` P m0; ^ %k Pk ^ %01 P10 ^ ^ %0` P m0; (3) (4) where the Pi0 are from the data alphabet , the Pi do not belong to (and so cannot occur in data instances), and 0 2= %i for any i (although there may be, say %0i = [0; 0]). Every hornMTL program can be transformed to a program in normal form with the same answers. We illustrate this claim by an example. Example 1. Let = fP10 [0;d]P00 ^ Q00; P00 (0;e)P10 ^ [0;f]Q01g, where the
P1 [0;d]P0 ^ Q00; P0 (0;e)P1 ^ [0;f]Q01; P0 P00; P1
P 0: 1
P1
P0 ^Q00; P1 (0;d]P0 ^Q00; P0 (0;e)P1 ^ [0;f]Q01; P0
P00; P1
P 0: 1 Now, P0 in the rst rule is not in the scope of % (Q00 can be regarded as a shorthand for [0;0]Q00). So we transform the rule using obvious derivations to obtain the following program in normal form:
P1
P00 ^ Q00; P1 (0;e)P1 ^ [0;f]Q01 ^ Q00; P1
(0;d]P0 ^ Q00; P0 (0;e)P1 ^ [0;f]Q01; P0
P00; P1
P 0: 1
A 2= . Clearly, every query can be converted to a one in normal form and having the same answers. 3
It is not hard to see that consistency checking and answering hornMTL queries can be reduced to consistency checking and answering monadic datalog queries over D. For example, the rule A datalog rule
(r;s]B can be replaced with the monadic A(x)
B(y) ^ dist>r(x; y) ^ dist s(x; y);
where dist>r and dist s are extensional predicates given by the data instance. It
follows that consistency checking and answering hornMTL queries can be done
in polynomial time for data complexity; for linear hornMTL queries, this can
be done in NL. The next theorem establishes a matching lower bound, which is
in sharp contrast to hornLTL queries that are in NC 1 for data complexity [
(ii) Consistency checking and answering linear hornMTL queries is NLcomplete for data complexity.
Proof. We only show the lower bound in (ii); the construction in (i) is similar.
G = (V; E) be such a digraph with a set V = fv0; : : : ; vn 1g of vertices and a set E V V of edges such that whenever (vi; vj ) 2 E then i < j (we can always represent G in this way due to its acyclicity). Suppose that the task is to check whether vt 2 V is reachable from vs 2 V in G.
We construct a data instance DG with concepts V , Er, El, I, O, which encodes G on a linear order. Namely, DG contains the following pairs (i; j; k 2 N): (V; 2k + 2in ), for 0 k < n and 1 i (Er; 2i + i2+n1 ), for (vi; vj ) 2 E; (El; 2i + j2+n1 ), for (vi; vj ) 2 E; (I; 2k + i2+n1 ), for 0 k < n and vs = vi; (O; 2k + i2+n1 ), for 0 k < n and vt = vi. n;
vs = v0
G: by
: DG :
R R I O Er El
V V V V 0 116126136146 1 V : v0v1v2v3
R R I O
Er El V V V V
be a linear hornMTL program with the following rules: R
I; R
El ^ [0;1](Er ^ R); R
V ^ [2;2]R; P
R ^ O; ?
P: Note that all numbers occurring in DG and belong to Q2. For the atoms implied by , see the previous picture. One can show that and DG are consistent i vt is not reachable from vs. 4 hornMTL
hr;1) In this section, we show that if all temporal operators in a hornMTL program are of the form hr;1), then answering ( ; A(x)) can be done in AC0; in other words, ( ; A(x)) is FO-rewritable. To this end, we require the canonical models for hornMTL programs, which can be dened as follows.
Suppose we are given a hornMTL program and a data instance D. Dene a set C ;D of pairs of the form (B; t) that contains all answers to queries with over D. We start by setting C = D and denote by cl(C) the result of applying exhaustively and non-recursively the following rules to C: (horn) if A B1 ^ : : : ^ Bk is in and (Bi; t) 2 C, for i = 1; : : : ; k, then we add (A; t) to C; ( %) if %B occurs in , (B; t0) 2 C, and t t0 2 %, for a timestamp t in D, then we add ( %B; t) to C.
D) such that clN (C) = clN+1(C). We then set C ;D = clN (D). and
(A; t) 2 C ;D.
hornMTL programs, then all such queries are FO-rewritable and in AC0 for data complexity. In fact, almost the same argument shows the following: Theorem 3. Consistency checking and answering hornMTL queries with temporal operators of the form hr;1) are in AC0 for data complexity. Proof. Let ( ; A(x)) be a hornMTL query with temporal operators of the form hr;1). It is easy to see that constructing Cp ;D needs at most j j2 applications of the cl operator to D (because each rule ( hr;1)) needs to be applied at most once). Thus, we can construct an FO-rewriting of ( ; A(x)) using iteratively the standard FO-translation of, say, [r;1)B into 9t0 (dist r(t; t0) ^ B(t0)).
prising two rules A [2;1)C, C [1;1)A looks as follows: com9y A(x) _ C(y) ^ dist 2(x; y) _ A(y) ^ dist 3(x; y) :
not work any more and the complexity landscape changes signicantly.
Our technical tool for studying the data complexity of linear hornMTL queries
is automata with metric constraints that are dened for programs in normal
form. These automata can be viewed as a primitive version of standard timed
automata for MTL [
A (nondeterministic) metric automaton is a quadruple A = (S; S0; ; ), where S 6= ; is a set of states, a tape alphabet, a transition relation , and S0 is a nonempty set of pairs of the form (q; e), where e 2 , q 2 S. The transition relation is a set of instructions of the form q !%e q0 with q; q0 2 S, e 2 and a range %. The automaton A takes as input timed words = (e0; t0); : : : ; (en; tn), where the ti are timestamps with ti 1 < ti. A run over is a sequence q0; : : : ; qm such that (q0; e0) 2 S0, qi 1 %!iei qi is in and ti ti 1 2 %i, for 0 < i n.
Let be a linear hornMTL program in normal form. We denote the conjunctions %01 P10 ^ : : : ^ %0` P m0 (with data concept names Pi0) that occur in by ", possibly with subscripts. Thus, since is linear, rules (4) in are of the form P " ^ %Q. Let E = f"1; : : : ; "qg be the set of all such " occurring in . We dene a metric automaton A for as follows. The set S of its states comprises the head concept names in , and = 2E . The transition relation comprises Q !%E P such that P " ^ %Q is in and " 2 E. Finally, S0 is the set of all pairs (P; ") such that a rule P " of the form (3) is in . E1 = f [0;1]P00g, E2 = fP10; [0;1]P00g, and S0 = f(P0; [0;1]P00)g.
Example 3. For = fP0 the metric automaton A
[0;1]P00; P1 (1;2)P0 ^ P10; P0 is depicted below, where P00; P10 2 (1;3)P1g, , E0 = fP10g, P0
P1 E2 (1; 2) E0 (1; 2)
in D, let E(ti) be the maximal set of " from that hold at ti in D, and let D = (E(t1); t1); : : : ; (E(tn); tn) . The corresponding FO-structure from
D = ( ; <; ; bitin ; bitfr ; E1; : : : ; Ek); (5) where fE1; : : : ; Ekg = 2E . It is not hard to see that there is an FO-translation of (2) to (5). Theorem 4. For any linear hornMTL query ( ; A(x)), a timestamp ti is a tcheertalaisnt atinms wesetramovpertiaadnadtaa irnusntaonfceA D oivtehrereD0etxhisatt aensdusbwwoitrhd A. D0 of D with
D 3 (E1; 1); (E0; 2 ); (;; 4); (E2; 5); and so 5 is a certain answer to the query over D from Example 4.
Theorem 4 does not use them in the standard way as it requires runs on subwords. Whether and how such runs can be captured by timed automata remains to be claried. We now use the obtained automaton characterisation of certain answers to linear queries to give better complexity bounds for two classes of linear programs with restricted temporal ranges than the NL bound of Theorem 1 (ii). 6 hornMTL
h0;ri We say that a hornMTL program in normal form is range-uniform if every (intensional) concept name P 2= occurs in in the scope of %, for some xed range %. By a coreMTL program we mean a core hornMTL program in normal form. Rules (4) in such a program take the form P %Q. 6.1
h0;ri
Let be a range-uniform coreMTL program and A = (S; S0; ; ) the
corresponding metric automaton. For each (q0; e0) in S0, we dene a classical nite
automaton AqA0;e0 = (S; ; fq0g; ; fAg), where S; , and are as in A (note
tnhaal tsatalltetrsa,nrseistpioenctsivtaelkye. tThheufos,rmAqqA0h;0e;0r!iis; aq0)u,naanrdy q(0i.ae.n,dovAerarseinugnleiqtoune ianliptihaalbaentd)
automaton. It is known that each such automaton has an equivalent automaton
in normal form [
= fS0
B; S1 (0;d)S0; S2 (0;d)S1; S3 (0;d)S2; S1 (0;d)S3g: The automaton AS0;B (which is in normal form) is shown in the picture below on the right. Using it, we construct the following FO-rewriting '(x) of ( ; S1(x)): '(x) = 9x0 B(x0) ^ 8y (x0 < y x) ! 9y0 dist<d(y; y0) ^ ('1(x0; x) _ '2(x0; x) _ '3(x0; x)) ; where '1(x0; x) = (x x0) 2 1 + 3N; '2(x0; x) = (x x0) 2 2 + 3N ^ 9x1 ((x0 < x1 x) ^ '+1(x1; x0)); '3(x0; x) = (x x0) 2 3 + 3N ^ '1+1+1(x0; x) _ '1+2(x0; x); '1+2(x0; x) = 9x1 ((x0 < x1 x) ^ '+2(x1; x0)); '1+1+1(x0; x) = 9x1; x2 ((x0 < x1 < x2 x) ^ '+1(x1; x0) ^ '+1(x2; x0) ^ ((x2 x1) > 1)); '+k(z; x0) = dist<d(z; z k k 1) x0), for k = 1; 2.
1) ^ ((z Intuitively, to derive S1 at x, we need a point x0 with B(x0) in the data and a sequence of points y between x0 and x without gaps of length d. An example of such a data instance is given below.
S0
S1
S3 S2 S3 S1
S1 S2
S2 S3
S0
S1
Note how we maintain the ‘stack of states’ with the elements at its bottom
alternating in a cycle between S1; S2, and S3. Note also that the states go in
decreasing order when we scan the stack from bottom to top. So we use the
formulas 'k(x0; x) to express that S1 is inferred at x on level k of the stack.
The formula '+k(z; x0) says that the height of the stack increases by k because
of a cluster of k + 2 points within the segment of size < d ending with z. The
formulas '1+2(x0; x) and '1+1+1(x0; x) express two ways of increasing the height
of the stack from 1 to 3. It is to be emphasised that properties of x and x0
such as (x x0) 2 1 + 3N can be expressed by FO-formulas using the predicate
PLUS(num1; num2; sum) or BIT(num; bit), which gives a binary representation
of every object num in the domain of an FO-structure [
h0;ri with ranges % of the form h0; ri.
Theorem 6. Consistency checking and answering hornMTL queries with temporal operators of the form h0;ri are in L for data complexity.
Example 7. We illustrate the log-space algorithm used in the proof of Theorem 6 by means of a program with the following rules:
P2 (0;2]P2 ^ (0;1]P1;
P1 (0;3]P2;
P2
P 0: 2 For this , we can scan an input word D with the help of three pointers , 1 and 2. Intuitively, will point to the last processed timestamp and 1 ( 2) to the last timestamp where P1 (respectively, P2) holds. Consider the word D shown in the picture below. Before the algorithm starts, we assume that , 1, and 2 do not point anywhere. First, we set to the rst point t0 (with the timestamp 0) and read P20. Because P2 holds there by the last rule in , we set 2 to t0. Next, we move to t1 where we read Q0 (not present in ). Here, we check whether t0 pointed to by 2 and t1 pointed to by are such that t1 t0 3 (which can be done in L using any subtraction algorithm). Since it is the case, we set 1 to t1 to reect the meaning of the second rule in , and we do not need to update 2. Next, we move to t2. We check that the dierence between the timestamps pointed to by and 1 does not exceed 3 to verify whether the second rule in applies. Similarly, we check that the dierence between and
verify whether the rst rule in applies. As a result, we set both 1 and 2 to t2. A complete run of our algorithm on D is shown below.
D : run: derived: 0 P 0 2 2 P2 1 Q0
1 P1 2 Q0 1; 2 P1; P2 To decide whether, say, t5 is a certain answer to ( ; P1(x)), we only need to check whether we move 2 to t5 when we move there.
form h0; ri. Intuitively, resetting i to every time a rule with Pi in the head applies does not provide correct answers for other forms of ranges.
The exact complexity for the queries in Theorem 6 remains open. At the
moment, we only have the following result, which is proved by reduction of
hornLTL queries with rules of the form Q P P ^ P 0, where P is the ‘previous
moment of time’ operator, that were shown to be NC 1-complete in [
Theorem 7. Consistency checking and answering hornMTL queries with temporal operators of the form h0;ri are NC1-hard for data complexity. 7 hornMTL Theorem 8. Consistency checking and answering hornMTL queries with temporal operators of the form [r;r] are in L for data complexity.
= fP1 [1;1]P1; A
P1 ^ [1:5;1:5]P2g and D = f(P1; 1); (P1; 1:25); (P1; 1:5); (P2; 2); (P1; 2:375); (P2; 2:5); (P2; 3); (P1; 3:5); (P2; 3:625); (P2; 4)g: Let num( ) be the set of numbers in . To check whether 4 is a certain answer to ( ; A(x)), we compute d = gcd(num( )) = 0:5 and k = max(num( )) = 3. d Observe rst that the algorithm can ignore those facts in D with a timestamp t for which 4 t is not divisible by d, that is, we can omit (P1; 1:25), (P1; 2:375), and (P2; 3:625) as they have no inuence on the facts derived at 4. Next, notice that to derive a fact at some t, it suces to check what facts hold at the instants t; t d; : : : ; t kd. Hence, for each concept name in , it suces to use k + 1 = 4 pointers storing the last 4 timestamps where this concept holds. The consecutive steps of our algorithm are shown below, where symbols in boxes represent facts derived by the rules in :
D : step 1: step 2: step 3: step 4: step 5: step 6: step 7:
Z P1 PZ1 P1 The algorithm uses k + 1-many log-space pointers for each concept name in , where k only depends on , and a single pointer indicating the currently processed timestamp. As a result, the algorithm is in L for data complexity.
can be shown using a reduction similar to that in the proof of Theorem 7. The algorithm illustrated above cannot be used to show an NC 1 upper bound because it must ignore some facts in D.
This work was supported by the NCN grant 2016/23/N/HS1/02168 and the