Data Complexity and Rewritability of Ontology-Mediated Queries in Metric Temporal Logic under the Event-Based Semantics (Full Version)

TL;DR

This paper explores the data complexity of answering ontology-mediated queries in metric temporal logic under event-based semantics, providing complexity classifications, rewritings, and lower bounds.

Contribution

It introduces complexity classifications, rewritings to first-order logic, and establishes lower bounds for ontology-mediated query answering in metric temporal logic.

Findings

Queries can be answered in AC0, NC1, L, NL, P, and coNP depending on the class.

Rewritings to first-order logic and extensions are provided.

Lower bounds for data complexity are established.

Abstract

We investigate the data complexity of answering queries mediated by metric temporal logic ontologies under the event-based semantics assuming that data instances are finite timed words timestamped with binary fractions. We identify classes of ontology-mediated queries answering which can be done in AC0, NC1, L, NL, P, and coNP for data complexity, provide their rewritings to first-order logic and its extensions with primitive recursion, transitive closure or datalog, and establish lower complexity bounds.

Equations

$${\boxminus }_{(0,30s]}{\mathsf{speed}}_{<1500}\wedge {}_{(0,2m]}{\boxminus }_{(0,30s]}{\mathsf{speed}}_{>6600}\to \mathsf{cdown}.$$

$${\vartheta }_1\wedge \cdots \wedge {\vartheta }_k\to {\vartheta }_{k+1}\vee \cdots \vee {\vartheta }_{k+l},$$

$$\mathcal{D}\text{leavevmode}=\text{leavevmode}(\Delta ,<,\Theta ,{\mathsf{bit}}_{in},{\mathsf{bit}}_{fr},A_1^{\mathcal{D}},\dots ,A_p^{\mathcal{D}}),$$

$$\mathcal{I}\text{leavevmode}=\text{leavevmode}(\Delta ,<,\Theta ,{\mathsf{bit}}_{in},{\mathsf{bit}}_{fr},A_1^{\mathcal{I}},\dots ,A_p^{\mathcal{I}}),\text{AiD⊆AiI⊆Θ,}$$

$$({}_{\varrho }A{)}^{\mathcal{I}}$$

$$({\boxminus }_{\varrho }A{)}^{\mathcal{I}}$$

$$X\to T\vee F,{}_{[2,2]}T\to T,{}_{[2,2]}F\to F,$$

$$N\wedge {}_{[0,1]}(I_0\wedge T)\to F,N\wedge {}_{[0,1]}(I_0\wedge F)\to T,$$

$$D\wedge {}_{[0,1]}(I_1\wedge T)\to T,D\wedge {}_{[0,1]}(I_2\wedge T)\to T,$$

$$C\wedge {}_{[0,1]}(I_1\wedge F)\to F,C\wedge {}_{[0,1]}(I_2\wedge F)\to F,$$

$$D\wedge {}_{[0,1]}(I_1\wedge F)\wedge {}_{[0,1]}(I_2\wedge F)\to F,$$

$$C\wedge {}_{[0,1]}(I_1\wedge T)\wedge {}_{[0,1]}(I_2\wedge T)\to T.$$

$$B^{\prime }(w,z)\wedge {\mathsf{dist}}_{\ge r}(x,w)\wedge {\mathsf{dist}}_{\le s}(x,z)$$

$$B^{\prime }(w,z)\wedge {\mathsf{dist}}_{\ge s}(x,w)\wedge {\mathsf{dist}}_{\le r}(x,z)\wedge {\mathsf{dist}}_{\ge (s-r)}(z,w)$$

$$A^{\prime }(y,z)\wedge (y\le x\le z)\to G(x),$$

$$B^{\prime }(x,y)\wedge B^{\prime }(z,z)\wedge \mathsf{suc}(y,z)\to B^{\prime }(x,z).$$

$${\boxminus }_{[2,2]}R\to R^{\prime },{\boxminus }_{(0,1]}{R}^{\prime }\to R^{\prime \prime },{\boxminus }_{[2,2]}{R}^{\prime \prime }\to R,{\boxminus }_{[4,4]}R\to R.$$

$${}_{[2,2]}R\to R^{\prime },{}_{(0,1]}{R}^{\prime }\to R^{\prime \prime },{}_{[2,2]}{R}^{\prime \prime }\to R,{}_{[4,4]}R\to R.$$

$$\Phi_{\Pi}\leavevmode\nobreak\ =\leavevmode\nobreak\ \bigvee_{\bar{\boldsymbol{t}}\in\mathfrak{O}_{\Pi}}\exists x_{1},\dots,x_{n}\big{[}(x_{1}=\min)\land\bigwedge_{1\leq i\leq n}\delta_{{\boldsymbol{t}}_{i}}(x_{i})\land{}\\ \bigwedge_{{\it wit}({\boldsymbol{t}}_{i},{\boldsymbol{t}}_{j},\varrho)}\mathsf{in}_{\varrho}(x_{i},x_{j})\land\bigwedge_{\overline{\it wit}({\boldsymbol{t}}_{i},{\boldsymbol{t}}_{j},\varrho)}\neg\mathsf{in}_{\varrho}(x_{i},x_{j})\land{}\\ \forall y\bigwedge_{1\leq i\leq n}\big{(}(x_{i}\prec y)\to\bigvee_{{\boldsymbol{t}}\in\mathfrak{F}^{i}_{\bar{\boldsymbol{t}}}}(\delta_{\boldsymbol{t}}(y)\land{}\bigwedge_{\overline{\it wit}({\boldsymbol{t}}_{i},{\boldsymbol{t}}_{j},\varrho)}\neg\mathsf{in}_{\varrho}(y,x_{j}))\big{)}\big{]},$$

$$P^{\mathcal{I}}=\{t\in \mathsf{ts}(\mathcal{D})\mid P\in \mathbf{t}(t)\},$$

$${}_{\varrho}\sigma\in{\boldsymbol{t}}(t)\quad\Longleftrightarrow\quad\exists t^{\prime}\,\big{(}\mathsf{in}_{\varrho}(t,t^{\prime})\leavevmode\nobreak\ \land\leavevmode\nobreak\ \sigma\in{\boldsymbol{t}}(t^{\prime})\big{)}.$$

$${}_{{\varrho }_1^{\prime }}{P}_1^{\prime }\wedge \cdots \wedge {}_{{\varrho }_{\ell }^{\prime }}{P}_m^{\prime }\to P_0,$$

$${}_{{\varrho }_1}{P}_1\wedge \cdots \wedge {}_{{\varrho }_k}{P}_k\wedge {}_{{\varrho }_1^{\prime }}{P}_1^{\prime }\wedge \cdots \wedge {}_{{\varrho }_{\ell }^{\prime }}{P}_m^{\prime }\to P_0,$$

$${}_{[0,d]}{P}_0\wedge Q_0^{\prime }\to P_1,{}_{(0,e)}{P}_1\wedge {}_{[0,f]}{Q}_1^{\prime }\to P_0,P_0^{\prime }\to P_0,P_1^{\prime }\to P_1.$$

$$P_0\wedge Q_0^{\prime }\to P_1,{}_{(0,d]}{P}_0\wedge Q_0^{\prime }\to P_1,{}_{(0,e)}{P}_1\wedge {}_{[0,f]}{Q}_1^{\prime }\to P_0,P_0^{\prime }\to P_0,P_1^{\prime }\to P_1.$$

$$\begin{gathered} P_0^{\prime }\wedge Q_0^{\prime }\to P_1,{}_{(0,e)}{P}_1\wedge {}_{[0,f]}{Q}_1^{\prime }\wedge Q_0^{\prime }\to P_1,{}_{(0,d)}{P}_0\wedge Q_0^{\prime }\to P_1, \\ {}_{(0,e)}{P}_1\wedge {}_{[0,f]}{Q}_1^{\prime }\to P_0,P_0^{\prime }\to P_0,P_1^{\prime }\to P_1. \end{gathered}$$

$$(E_1,1),(E_0,\frac{3}{2}),(\varnothing ,4),(E_2,5),$$

$$\Pi =\{S_0\leftarrow B,S_1\leftarrow {}_{(0,d)}{S}_0,S_2\leftarrow {}_{(0,d)}{S}_1,S_3\leftarrow {}_{(0,d)}{S}_2,S_1\leftarrow {}_{(0,d)}{S}_3\}.$$

$$\exists x^{\prime}\,\big{[}B(x^{\prime})\land\forall y\,\big{(}(x^{\prime}<y\leq x)\to\exists y^{\prime}\,\mathsf{dist}_{<d}(y,y^{\prime})\land{}(\varphi_{1}(x^{\prime},x)\lor\varphi_{2}(x^{\prime},x)\lor\varphi_{3}(x^{\prime},x))\big{)}\big{]},$$

$$\varphi_{1}(x^{\prime},x)\leavevmode\nobreak\ =\leavevmode\nobreak\ \exists z,z^{\prime},z^{\prime\prime},y\,\big{(}(x=y+1)\land{}\\ \text{PLUS}(z,z,z^{\prime})\land{}\text{PLUS}(z^{\prime},z,z^{\prime\prime})\land\text{PLUS}(x^{\prime},z^{\prime\prime},y)\big{)}.$$

$$\displaystyle\left[\begin{array}[]{l}R_{{\boldsymbol{s}}_{1}}(x,z)\equiv\vartheta_{{\boldsymbol{s}}_{1}}\\ \dots\\ R_{{\boldsymbol{s}}_{n}}(x,z)\equiv\vartheta_{{\boldsymbol{s}}_{n}}\end{array}\right]\bigvee_{\neg A\in{\boldsymbol{s}}\in Q}R_{{\boldsymbol{s}}}(x,y)\leavevmode\nobreak\ \land\leavevmode\nobreak\ \mathsf{div}_{\boldsymbol{1}}(y,x),$$

$$(x=z)\wedge {\delta }_{\mathbf{s}}(z),$$

$$\neg {\mathsf{div}}_1(z,x)\wedge \exists z^{\prime }({\mathsf{dist}}_{<\mathbf{m}}(z,z^{\prime })\wedge {\mathsf{div}}_1(z^{\prime },x))\wedge R_{\mathbf{s}}(x,z-1),$$

$${\mathsf{div}}_1(z,x)\wedge \underset{\begin{array}{c}\mathbf{i}\in \{1,\dots ,\mathbf{m}\}\\ {\mathbf{s}}^{\prime }{\to }_{\mathbf{i}}\mathbf{s}\end{array}}{\bigvee }({\delta }_{\mathbf{s}}(z)\wedge {\mathsf{last}}_{\mathbf{i}}(z)\wedge R_{{\mathbf{s}}^{\prime }}(x,z-1)),$$

$$\{\neg {}_{1}P,\neg {}_{2}P,\neg {}_{3}P,P,Q\},\{\neg {}_{1}P,\neg {}_{2}P,\neg {}_{3}P,P,\neg Q\}.$$

Full text

1 Introduction

In this paper, we are concerned with the following problem: given a formula $\Pi$ of metric temporal logic MTL and an atomic proposition $A$, is it possible to construct a query ${\boldsymbol{Q}}(x)$ in some standard query language such that, for any data instance $\mathcal{D}$ of atoms timestamped with binary fractions and any timestamp $t$ from $\mathcal{D}$, we have $\Pi,\mathcal{D}\models A(t)$ iff ${\boldsymbol{Q}}(t)$ is true in $\mathcal{D}$?

MTL was originally designed for modelling and reasoning about real-time systems [24, 2]; for a survey see [12]. Recently, combinations of MTL with description logics have been suggested as temporal ontology languages [22, 7]. Datalog with MTL-operators was used by [13, 27] for practical ontology-based access to temporal log data aiming to facilitate detection and monitoring complex events in asynchronous systems based on sensor measurements. For example, a Siemens turbine has a coast down if the rotor speed was below 1500 in the previous 30 seconds, while no more than 2 minutes before that the speed was above 6600 for 30 seconds. The event ‘coast down’ can be encoded by the following MTL-formula, where ${}_{(r,s]}\varphi$ ($\boxminus_{(r,s]}\varphi$) is true at a timestamp $t$ if $\varphi$ holds at some (respectively, all) $t^{\prime}$ with $r<t-t^{\prime}\leq s$:

[TABLE]

To find when a coast down occurred, a Siemens engineer can now simply execute the query $\mathsf{cdown}(x)$ mediated by an MTL-ontology with formulas such as the one above, whose atoms are related to sensor data by appropriate mappings. Answering datalogMTL queries in the streaming setting was considered by [32].

The underpinning idea of classical ontology-based data access (OBDA) [15, 33] is a reduction of ontology-mediated query (OMQ) answering to standard database query evaluation. As known from descriptive complexity [23], the existence of such reductions, or rewritings, is closely related to the data complexity of OMQ answering, which is by now well understood for atemporal OMQs both uniformly (for all OMQs in a given language) and non-uniformly (for individual OMQs) [19, 10, 11, 26].

Temporal ontology and query languages have attracted attention of datalog and description logic communities since the 1990s; see [8, 17, 25, 5] for surveys. In recent years, the proliferation of temporal data from various sources and its importance for analysing the behaviour of complex systems and decision making in all economic sectors have intensified research into formalisms that can be used for querying temporal databases and streaming data [31, 9, 30]. OBDA with atemporal ontologies and query languages with linear temporal logic LTL operators has been in use since [6, 29]. Rewritability and data complexity of OMQs in the description logics DL-Lite and $\mathcal{EL}$ extended with LTL operators were considered in [4, 21].

Here, we investigate the (uniform) rewritability and data complexity problems for basic OMQs given in metric temporal logic MTL, assuming that data instances are finite sets of atoms timestamped by dyadic rationals and that MTL is interpreted under the event-based semantics where atoms refer to events (state changes) rather than to states themselves [28]. MTL is more succinct, expressive, and versatile compared to LTL, being able to model both synchronous (discrete) and asynchronous (real-time) settings.

First, we observe that answering arbitrary MTL-OMQs is coNP-complete for data complexity (in contrast to $\textsc{NC}^{1}$-completeness for LTL-OMQs). OMQs in the Horn fragment hornMTL are P-complete and rewritable to datalog(FO), which extends datalog with FO-formulas built from EDB predicates; in fact, we establish P-hardness already for the fragment $\textsl{coreMTL}\!^{\boxminus}$ of hornMTL with binary rules (like in OWL 2 QL) and box operators only. OMQs in coreMTL turn out to be FO(TC)-rewritable (FO with transitive closure) and NL-hard. We then classify MTL-OMQs by the type of ranges $\varrho$ constraining their temporal operators ϱ and $\boxminus_{\varrho}$: infinite $(r,\infty)$ and $[r,\infty)$, punctual $[r,r]$, and arbitrary non-punctual $\varrho$. We show that OMQs of the first type are FO-rewritable and can be answered in ${\textsc{AC}^{0}}$. OMQs of the second type are FO(RPR)-rewritable (FO with relational primitive recursion) and ${\textsc{NC}^{1}}$-complete. For the third type, we obtain an NL upper bound with rewritability to FO(TC) and ${\textsc{NC}^{1}}$ lower bound; for hornMTL-OMQs of this type, the results are improved to L with rewritability to FO(DTC) (FO with deterministic closure).

2 MTL Ontology-Mediated Queries

In the context of event monitoring, we consider a ‘past’ variant of MTL, which is a propositional modal logic with constrained operators ϱ ‘sometime in the past within range $\varrho$’ and $\boxminus_{\varrho}$ ‘always in the past within range $\varrho$,​’ interpreted over finite timed words under the event-based semantics. We assume that timestamps in timed words are given as non-negative dyadic rational numbers (finite binary fractions), the set of which is denoted by $\mathbb{Q}_{2}^{\geq 0}$. The ranges $\varrho$ in ϱ and $\boxminus_{\varrho}$ are non-empty intervals with end-points in $\mathbb{Q}_{2}^{\geq 0}\cup\{\infty\}$.

An MTL-program, $\Pi$, is a finite set of rules of the form

[TABLE]

where each $\vartheta_{i}$ takes the form $A$, ${}_{\varrho}A$, or $\boxminus_{\varrho}A$, for an atomic proposition $A$. We denote the empty $\land$ by $\top$ (truth) and empty $\lor$ by $\bot$ (falsehood). Using fresh atoms, every MTL-formula can be transformed to an equivalent (in the sense of giving the same answers to queries) MTL-program.

An MTL-program is called a hornMTL-program if, in all of its rules (1), $l\leq 1$ and $\vartheta_{k+1}$ is an atom. As usual, $\vartheta_{k+1}$ is called the head of the rule and $\vartheta_{1}\land\dots\land\vartheta_{k}$ its body. A hornMTL-program is a coreMTL-program if $k+l\leq 2$. An MTL- (hornMTL- or coreMTL-) ontology-mediated query (OMQ) takes the form ${\boldsymbol{q}}=(\Pi,A)$, where $\Pi$ is an MTL- (resp., hornMTL- or coreMTL-) program and $A$ an atom.

Intuitively, a data instance, $\mathcal{D}$, can be thought of as a word $\boldsymbol{A}_{0}(\bar{0}),\dots,\boldsymbol{A}_{k}(\bar{k})$ with timestamps $\bar{0}<\dots<\bar{k}$, $\bar{i}\in\mathbb{Q}^{\geq 0}_{2}$, where each $\boldsymbol{A}_{i}$ is the set of atoms that are true at $\bar{i}$. Formally, we represent $\mathcal{D}$ as the FO-structure

[TABLE]

with domain $\varDelta=\{0,\dots,\ell\}$ ordered by $<$, timestamps $\varTheta=\{0,\dots,k\}$, $1\leq k\leq\ell$, and subsets $A^{\mathcal{D}}_{i}\subseteq\varTheta$. The ternary predicates $\mathsf{bit}_{\it in}$ and $\mathsf{bit}_{\it fr}$ are such that, for any $n\in\varTheta$ and $i\in\varDelta$, there are unique $b_{i},c_{i}\in\{0,1\}$ with $\mathsf{bit}_{\it{in}}(n,i,b_{i})$ and $\mathsf{bit}_{\it{fr}}(n,i,c_{i})$. These predicates give the value $\bar{n}\in\mathbb{Q}_{2}^{\geq 0}$ of every timestamp $n\in\varTheta$: $\bar{n}=b_{\ell}\dots b_{0}.c_{\ell}\dots c_{0}$ iff $\mathsf{bit}_{\it{in}}(n,i,b_{i})$ and $\mathsf{bit}_{\it{fr}}(n,i,c_{i})$ hold for all $i\leq\ell$. We assume that $\bar{n}<\bar{m}$ if $n<m$. For any $r\in\mathbb{Q}^{\geq 0}_{2}$, we can define an FO-formula $\mathsf{dist}_{<r}(x,y)$ that holds in $\mathcal{D}$ iff $x,y\in\varTheta$ and $0\leq\bar{x}-\bar{y}<r$, its variants $\mathsf{dist}_{>r}(x,y)$, $\mathsf{dist}_{=r}(x,y)$, etc.; see Appendix A for details. Using these, we can further define FO-formulas $\mathsf{in}_{\varrho}(x,y)$ for $\bar{x}-\bar{y}\in\varrho$, $\mathsf{suc}(x,y)$ for ‘$x$ is an immediate successor of $y$ in $\mathcal{D}$’​, and FO-expressible constants $\min=0$ and $\max=k$.

An event-based interpretation over $\mathcal{D}$ is a structure

[TABLE]

where the Boolean connectives are interpreted as usual and

[TABLE]

An interpretation $\mathcal{I}$ over $\mathcal{D}$ is a model of an MTL-program $\Pi$ and $\mathcal{D}$ if, for any rule (1) in $\Pi$ and any $t\in\varTheta$, whenever $t\in\vartheta_{i}^{\mathcal{I}}$ for all $i$, $1\leq i\leq k$, then $t\in\vartheta_{k+j}^{\mathcal{I}}$ for some $j$, $1\leq j\leq l$. We call $\mathcal{D}$ and $\Pi$ consistent if there is a model of $\Pi$ and $\mathcal{D}$.

Henceforth, we write ${\mathsf{ts}}(\mathcal{D})$ for the set $\varTheta$ of timestamps in (2) and often informally identify $t\in{\mathsf{ts}}(\mathcal{D})$ with its value $\bar{t}$. We call $t\in{\mathsf{ts}}(\mathcal{D})$ (and so $\bar{t}$) a certain answer to ${\boldsymbol{q}}=(\Pi,A)$ over $\mathcal{D}$ if $t\in A^{\mathcal{I}}$ for every model $\mathcal{I}$ of $\mathcal{D}$ and $\Pi$. The OMQ answering problem for ${\boldsymbol{q}}$ is to decide, given $\mathcal{D}$ and $t\in{\mathsf{ts}}(\mathcal{D})$, whether $t$ is a certain answer to ${\boldsymbol{q}}$ over $\mathcal{D}$. To illustrate, consider $\Pi=\{\boxminus_{[0,2)}B\to B^{\prime},\ {}_{[1,1]}B^{\prime}\to A\}$, $\mathcal{D}_{1}=\{B(0),B(1/2),C(3/2)\}$ and $\mathcal{D}_{2}=\{B(0),C(3/2)\}$. Then $3/2$ is a certain answer to $(\Pi,A)$ over $\mathcal{D}_{1}$, but there are no certain answers to $(\Pi,A)$ over $\mathcal{D}_{2}$:

B\ {\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}B^{\prime}}[math]B\ {\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}B^{\prime}}$$\frac{1}{2}$$C\ {\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}A}$$\frac{3}{2}

We are interested in the data complexity of OMQ answering, that is, regard $\mathcal{D}$ as the only input to the problem and assume ${\boldsymbol{q}}$ to be fixed.

Let $\mathcal{L}$ be a query language over FO-structures (2). An OMQ ${\boldsymbol{q}}$ is said to be $\mathcal{L}$-rewritable if there is an $\mathcal{L}$-query ${\boldsymbol{Q}}(x)$, called an $\mathcal{L}$-rewriting of ${\boldsymbol{q}}$, such that, for any data instance $\mathcal{D}$, a timestamp $t\in{\mathsf{ts}}(\mathcal{D})$ is a certain answer to ${\boldsymbol{q}}$ over $\mathcal{D}$ iff $\mathcal{D}\models{\boldsymbol{Q}}(t)$. Our target query languages $\mathcal{L}$ include:

• –

FO$(<)$ and its extension FO$(<,+)$ with the predicate PLUS (e.g., $\exists x\,\text{PLUS}(x,x,\max)$ says that $|\varTheta|$ is odd); evaluating such queries is in $\textsc{AC}^{0}$ for data complexity;

• –

FO(RPR), i.e., FO$(<)$ with relational primitive recursion, which is in $\textsc{NC}^{1}$ [18];

• –

FO(TC) and FO(DTC), i.e., FO$(<)$ with transitive and deterministic transitive closure, which are in NL and L, respectively [23];

• –

datalog(FO), i.e., datalog queries with additional FO-formulas built from EDB predicates in their rule bodies, which are in P [20].

All of them save datalog(FO) can be implemented in SQL. $\mathcal{L}$-rewritability of an OMQ ${\boldsymbol{q}}$ means that answering ${\boldsymbol{q}}$ is in the same data-complexity class as evaluation of $\mathcal{L}$-queries.

Given a hornMTL-program $\Pi$ and a data instance $\mathcal{D}$, we define a set $\mathfrak{C}_{\Pi,\mathcal{D}}$ of pairs of the form $(\vartheta,t)$ that contains all answers to OMQs with $\Pi$ over $\mathcal{D}$. We start by setting $\mathfrak{C}=\mathcal{D}$ and denote by $\mathsf{cl}(\mathfrak{C})$ the result of applying exhaustively and non-recursively the following rules to $\mathfrak{C}$:

• –

if $\vartheta_{1}\land\dots\land\vartheta_{k}\to\vartheta$ is in $\Pi$ and $(\vartheta_{i},t)\in\mathfrak{C}$, for all $i$, $1\leq i\leq k$, then we add $(\vartheta,t)$ to $\mathfrak{C}$;

• –

if ${}_{\varrho}B$ occurs in $\Pi$, $(B,t^{\prime})\in\mathfrak{C}$, and $\mathsf{in}_{\varrho}(t,t^{\prime})$ holds for some $t\in{\mathsf{ts}}(\mathcal{D})$, then we add $({}_{\varrho}B,t)$ to $\mathfrak{C}$;

• –

if $\boxminus_{\varrho}B$ occurs in $\Pi$, $t\in{\mathsf{ts}}(\mathcal{D})$ and $(B,t^{\prime})\in\mathfrak{C}$ for all $t^{\prime}\in{\mathsf{ts}}(\mathcal{D})$ with $\mathsf{in}_{\varrho}(t,t^{\prime})$, then we add $(\boxminus_{\varrho}B,t)$ to $\mathfrak{C}$.

It should be clear that there is some $N<\omega$ polynomially depending on $\Pi$ and $\mathcal{D}$ such that $\mathsf{cl}^{N}(\mathfrak{C})=\mathsf{cl}^{N+1}(\mathfrak{C})$. We then set $\mathfrak{C}_{\Pi,\mathcal{D}}=\mathsf{cl}^{N}(\mathcal{D})$. We can regard $\mathfrak{C}_{\Pi,\mathcal{D}}$ as a (minimal) model of $\Pi$ and $\mathcal{D}$ with domain ${\mathsf{ts}}(\mathcal{D})$ in which $t\in B^{\mathfrak{C}_{\Pi,\mathcal{D}}}$ iff $(B,t)\in\mathfrak{C}_{\Pi,\mathcal{D}}$ The proof of the following is standard:

Theorem 1**.**

For a hornMTL-OMQ $(\Pi,A)$, $(i)$ $\Pi$ is inconsistent with $\mathcal{D}$ iff $(\bot,t)\in\mathfrak{C}_{\Pi,\mathcal{D}}$; $(ii)$ a timestamp $t\in{\mathsf{ts}}(\mathcal{D})$ is a certain answer to a hornMTL-OMQ $(\Pi,A)$ over $\mathcal{D}$ iff either $\mathfrak{C}_{\Pi,\mathcal{D}}\models A[t]$ or $\Pi$ is inconsistent with $\mathcal{D}$.

Note in passing that, as a consequence, we obtain the following reduction of $\mathcal{L}$-rewritability of more general hornMTL-OMQs $(\Pi,\varphi)$ with positive FO-queries $\varphi$ (built from atoms, $\land$, $\lor$, $\forall$, and $\exists$) to $\mathcal{L}$-rewritability of atomic OMQs we deal with in this paper:

Corollary 2**.**

Let $(\Pi,\varphi)$ be a hornMTL-OMQ with a positive FO-query $\varphi$. If $(\Pi,A)$ has an $\mathcal{L}$-rewriting ${\boldsymbol{Q}}_{A}(x)$, for every atom $A$, then ${\boldsymbol{Q}}_{\varphi}=\varphi[A_{1}/{\boldsymbol{Q}}_{A_{1}},\dots,A_{n}/{\boldsymbol{Q}}_{A_{n}}]\lor\exists x\,{\boldsymbol{Q}}_{B}(x)$ is an $\mathcal{L}$-rewriting of $(\Pi,\varphi)$, where $B$ is an atom not occurring in $\Pi$ and any data instance and $\varphi[A_{1}/{\boldsymbol{Q}}_{A_{1}},\dots,A_{n}/{\boldsymbol{Q}}_{A_{n}}]$ is the result of replacing every atom of the form $A_{i}(x)$ in $\varphi$ with ${\boldsymbol{Q}}_{A_{i}}(x)$.

Proof.

Observe first that, since $\varphi(\vec{x})$ is positive, we have, for any consistent $\Pi$ and $\mathcal{D}$ and any $\vec{a}\subseteq{\mathsf{ts}}(\mathcal{D})$, that $\mathfrak{C}_{\Pi,\mathcal{D}}\models\varphi(\vec{a})$ iff $\mathcal{I}\models\varphi(\vec{a})$ for all models $\mathcal{I}$ of $\Pi$ and $\mathcal{D}$. Indeed, to show $(\Rightarrow)$, we use the fact that there is a homomorphism from $\mathfrak{C}_{\Pi,\mathcal{D}}$ onto $\mathcal{I}$ (as $\mathfrak{C}_{\Pi,\mathcal{D}}$ is a minimal model of $\Pi$ and $\mathcal{D}$), and positive formulas are preserved under homomorphic images [16]. On the other hand, one can show by induction on the construction of $\varphi$ that $\mathfrak{C}_{\Pi,\mathcal{D}}\models\varphi(\vec{a})$ iff $\mathcal{D}\models\varphi[A_{1}/{\boldsymbol{Q}}_{A_{1}},\dots,A_{n}/{\boldsymbol{Q}}_{A_{n}}](\vec{a})$. It remains to observe that $\Pi$ and $\mathcal{D}$ are inconsistent iff $\mathcal{D}\models\exists x\,{\boldsymbol{Q}}_{B}(x)$. ∎

3 OMQs with Arbitrary Ranges

We begin by establishing (non-)rewritability and data complexity of answering OMQs in various classes where arbitrary ranges in temporal operators are allowed. We denote by $\textsl{coreMTL}\!^{\boxminus}$ (coreMTL) the restriction of coreMTL to the language with operators $\boxminus_{\varrho}$ (respectively, ϱ) only.

Theorem 3**.**

$(i)$* Answering MTL-OMQs is coNP-complete for data complexity; $(ii)$ hornMTL-OMQs are datalog(FO)-rewritable, with $\textsl{coreMTL}\!^{\boxminus}$-OMQs being P-hard; $(iii)$ coreMTL-OMQs are FO(TC)-rewritable and NL-hard.*

Proof.

$(i)$ The membership in coNP is trivial. We establish coNP-hardness by reduction of NP-complete circuit satisfiability [3]. Let $\boldsymbol{C}$ be a Boolean circuit with $N_{0}$-many (two-input) AND, OR and (one-input) NOT gates enumerated by consecutive numbers starting from 0 so that if there is an edge from $n$ to $m$, then $n<m$. Take the minimal $N=2^{k}\geq N_{0}$ and a data instance $\mathcal{D}_{\boldsymbol{C}}$ with the facts

• –

$A(2n+i/N)$, if $n$ is a gate and $0\leq i<N_{0}$;

• –

$X(2n+n/N)$, if $n$ is an input gate;

• –

$N(2n+n/N)$, if $n$ is a NOT gate;

• –

$D(2n+n/N)$, if $n$ is an OR gate;

• –

$C(2n+n/N)$, if $n$ is an AND gate;

• –

$I_{0}(2n+m/N)$, if $n$ is a NOT gate with input gate $m$;

• –

$I_{1}(2n+m/N)$ and $I_{2}(2n+k/N)$, if $n$ is an OR or AND gate with input gates $m$ and $k$.

Let $\Pi_{\boldsymbol{C}}$ be an MTL-program with the following rules:

[TABLE]

Then $\mathbf{C}$ is satisfiable iff the maximal number in ${\mathsf{ts}}(\mathcal{D})$ is not a certain answer to $(\Pi_{\boldsymbol{C}},F)$ over $\mathcal{D}_{\boldsymbol{C}}$. An example of $\boldsymbol{C}$ and an initial part of a model of $\Pi_{\boldsymbol{C}}$, $\mathcal{D}_{\boldsymbol{C}}$ is shown below:

$\lor$2$\land$3$\neg$4$X$​1$X$​0A$$A$$A$$A$$A$$A$$A$$A$$A$$A$$A$$A$$A$$A$$A$$A$$A$$A$$A$$A$$\frac{0}{8}$$\frac{1}{8}$$\frac{2}{8}$$\frac{3}{8}$$\frac{4}{8}$$\frac{16}{8}$$\frac{17}{8}$$\frac{18}{8}$$\frac{19}{8}$$\frac{20}{8}$$\frac{32}{8}$$\frac{33}{8}$$\frac{34}{8}$$\frac{35}{8}$$\frac{36}{8}$$\frac{48}{8}$$\frac{49}{8}$$\frac{50}{8}$$\frac{51}{8}$$\frac{52}{8}$$X$$X$$I_{1}$$I_{2}$$D$$I_{1}$$I_{2}$$C$$T$$T$$F$$T$$F$$T$$T$$F$$T$$F

$(ii)$ We construct a datalog(FO) rewriting $(\Pi^{\prime},G(x))$ of a hornMTL-OMQ ${\boldsymbol{q}}=(\Pi,A)$. To begin with, we add to $\Pi$ the rule $P(x)\to P^{\prime}(x,x)$ for each $P$ in $\Pi$. The other rules in $\Pi^{\prime}$ are obtained from the rules in $\Pi$ by the following transformations. We replace every atom $B$ not under the scope of a temporal operator with $B^{\prime}(x,x)$ and every ${}_{[r,s]}B$ with

[TABLE]

and similarly for other types of ranges $\varrho$ in ${}_{\varrho}B$. Intuitively, $\Pi^{\prime},\mathcal{D}\models B^{\prime}(x,y)$ iff $(B,t)\in\mathfrak{C}_{\Pi,\mathcal{D}}$, for each $t\in[x,y]$ from ${\mathsf{ts}}(\mathcal{D})$. We replace every $\boxminus_{[r,s]}B$ in the body of a rule with

[TABLE]

and similarly for other types of ranges. Finally, we add the following rules to the resulting program:

[TABLE]

Note that the obtained datalog program $\Pi^{\prime}$ contains FO-definable EDB predicates such as $\mathsf{dist}_{\geq r}(x,w)$ and $\mathsf{suc}(y,z)$ in rule bodies. Clearly, $t$ is a certain answer to ${\boldsymbol{q}}$ over any given data instance $\mathcal{D}$ iff $t$ is an answer to $(\Pi^{\prime},G(x))$ over $\mathcal{D}$.

We show P hardness of $\textsl{coreMTL}\!^{\boxminus}$-OMQs by reduction of path system accessibility (PSA). Let $G$ be a hypergraph with $N_{0}$ vertices enumerated by consecutive natural numbers starting from 0 so that if $(m,n,o)$ is a hyperedge, then $m<n<o$. Let $e_{0},\dots,e_{k-1}$ be the lexicographical order of hyperedges. Suppose the problem is to check whether a vertex $t$ is accessible from a set of vertices $S$, i.e., whether $t\in S$ or there are vertices $u,w$ accessible from $S$ and $(u,w,t)$ is a hyperedge. Let $\mathcal{D}_{G}$ comprise the atoms $A(4i+n/N)$, for $0\leq i\leq k$ and a vertex $n$, together with

• –

$A(2+4i+m/N)$, $A(2+4i+n/N)$, $A(2+4i+o/N)$, and $A(2+4i+n/N-1)$, for a hyperedge $e_{i}=(m,n,o)$;

• –

$R(4i+n/N)$, for $0\leq i\leq m$ and $n\in S$.

For example, for the vertices $0,1,2,3$, hyperedge $(0,1,2)$, $S=\{0,1\}$, and $t=3$, $\mathcal{D}_{G}$ looks as follows:

A$$A$$A$$A$$A$$A$$A$$A$$A$$\frac{5}{4}$$A$$A$$A$$\frac{0}{4}$$\frac{1}{4}$$\frac{2}{4}$$\frac{3}{4}$$\frac{8}{4}$$\frac{9}{4}$$\frac{10}{4}$$\frac{16}{4}$$\frac{17}{4}$$\frac{18}{4}$$\frac{19}{4}$$R$$R$$R$$R$$R^{\prime}$$R^{\prime}$$R^{\prime\prime}$$Rby $\Pi$:$\mathcal{D}_{G}:$hyperedge $(v_{0},v_{1},v_{2})$

Let $\Pi$ be a $\textsl{coreMTL}\!^{\boxminus}$ program with the rules:

[TABLE]

Then $4k+t/N$ is a certain answer to $(\Pi,R)$ over $\mathcal{D}_{G}$ iff $t$ is accessible from $S$ in $G$.

$(iii)$ The upper bound can be shown by reduction to FO(TC) via linear datalog(FO). Without loss of generality, we assume that, in the disjointness constraints $\vartheta_{1}\land\vartheta_{2}\to\bot$ occurring in the given coreMTL-OMQ ${\boldsymbol{q}}=(\Pi,A)$, the $\vartheta_{i}$ are atomic. First, we straightforwardly translate ${\boldsymbol{q}}$ with the disjointness constraints removed from $\Pi$ to linear datalog(FO). Then, we transform the result into an FO(TC)-query $\varPsi_{A}(x)$ [20]. Now, for every disjointness constraint $B_{1}\land B_{2}\to\bot$ in $\Pi$, we take the sentence $\exists x(\varPsi_{B_{1}}(x)\land\varPsi_{B_{2}}(x))$ and, finally, form a disjunction of $\varPsi_{A}(x)$ with those sentences, which is obviously an FO(TC)-rewriting of ${\boldsymbol{q}}$.

We prove NL-hardness by reduction of the reachability problem in acyclic digraphs. Let $G$ be such a digraph with $N_{0}$ vertices enumerated by consecutive natural numbers starting from 0 so that, if there is an edge from $n$ to $m$, then $n<m$. Let $e_{0},\dots,e_{k-1}$ be the lexicographical order of edges. Take the minimal $N=2^{i}\geq N_{0}$ for $i\in\mathbb{N}$. Suppose we want to check whether a vertex $t$ is accessible from $s$. Let $\mathcal{D}_{G}$ consist of the atoms $A(4i+n/N)$, for $0\leq i\leq k$ and a vertex $n$; $A(2+4i+n/N)$, $A(2+4i+m/N)$, for every edge $e_{i}=(n,m)$; $R(4i+s/N)$, for $0\leq i\leq k$. An example of $G$ and an initial part of $\mathcal{D}_{G}$ is shown below:

•$s=0$•$1$•$2$•3=t$$A$$A$$A$$A$$A$$A$$A$$A$$A$$A$$\frac{0}{4}$$\frac{1}{4}$$\frac{2}{4}$$\frac{3}{4}$$\frac{8}{4}$$\frac{10}{4}$$\frac{16}{4}$$\frac{17}{4}$$\frac{18}{4}$$\frac{19}{4}$$R$$R$$R^{\prime}$$R^{\prime\prime}$$R$$G:by $\Pi$:$\mathcal{D}_{G}:$edge $e_{0}=(0,2)$

Let $\Pi$ be a coreMTL program with the following rules:

[TABLE]

Then $4k+t/N$ is a certain answer to $(\Pi,R)$ over $\mathcal{D}_{G}$ iff $t$ is reachable from $s$ in $G$. ∎

To obtain finer complexity results, we classify MTL-OMQs by the type of ranges $\varrho$ in their operators ϱ and $\boxminus_{\varrho}$: infinite, punctual, and non-punctual. Let $\langle$ be one of $($ or $[$, and let $\rangle$ be one of $)$ or $]$.

4 OMQs with Ranges $\langle r,\infty)$

First, consider OMQs with ⟨r,∞) and $\boxminus_{\langle r,\infty)}$, which resemble LTL-operators ‘sometime’ and ‘always in the past’​. Using partially-ordered automata, it was shown in [4] that LTL-OMQs with these operators are FO-rewritable. Although such automata are not applicable now, we establish the same complexity by characterising the structure of models. In the constructions below, it will be convenient to regard $\boxminus_{\varrho}$ as an abbreviation for $\neg{}_{\varrho}\neg$ with Boolean negation $\neg$ and only consider, without loss of generality, OMQs $(\Pi,A)$ with $A$ occurring in $\Pi$.

Theorem 4**.**

MTL*-OMQs with temporal operators of the form ⟨r,∞) and $\boxminus_{\langle r,\infty)}$ only are $\textup{FO}(<)$-rewritable.*

Proof.

Let ${\boldsymbol{q}}=(\Pi,A)$ be an MTL-OMQ as specified above. A simple literal, $\sigma$, for $\Pi$ takes the form $P$ or $\neg P$, where $P$ is an atom in $\Pi$; a temporal literal, $\tau$, for $\Pi$ is of the form ${}_{\varrho}\sigma$ or $\neg{}_{\varrho}\sigma$ provided that ${}_{\varrho}P$ or $\boxminus_{\varrho}P$ occurs in $\Pi$ and $P$ is the atom in $\sigma$. Let $\varSigma_{\Pi}$ and $\varXi_{\Pi}$ be the sets of simple and temporal literals for $\Pi$, respectively. A type for $\Pi$ is any maximal set ${\boldsymbol{t}}\subseteq\varSigma_{\Pi}\cup\varXi_{\Pi}$ consistent with $\Pi$. The number of different types is $N_{\Pi}=2^{O(|\Pi|)}$.

Given a model $\mathcal{I}$ of $\Pi$ and some $\mathcal{D}$ with $s\in{\mathsf{ts}}(\mathcal{D})$, denote by ${\boldsymbol{t}}(s)$ the type of $s$ in $\mathcal{I}$. As the ranges in $\Pi$ are of the form $\langle r,\infty)$, the model $\mathcal{I}$ has the following monotonicity property:

• –

${}_{\varrho}\sigma\in{\boldsymbol{t}}(s)$ implies ${}_{\varrho}\sigma\in{\boldsymbol{t}}(s^{\prime})$ for all $s^{\prime}>s$ in $\mathcal{I}$;

• –

$\neg{}_{\varrho}\sigma\in{\boldsymbol{t}}(s)$ implies $\neg{}_{\varrho}\sigma\in{\boldsymbol{t}}(s^{\prime})$ for all $s^{\prime}<s$ in $\mathcal{I}$.

We call ${\boldsymbol{t}}(s)$ in $\mathcal{I}$ an osteo-type if there is $\lambda\in{\boldsymbol{t}}(s)$ such that $\lambda\notin{\boldsymbol{t}}(s^{\prime})$, for all $s^{\prime}<s$. Thus, if ${}_{\varrho}\sigma\in{\boldsymbol{t}}(s^{\prime})$ in $\mathcal{I}$, there is an osteo-type ${\boldsymbol{t}}(s)\ni\sigma$ with $\mathsf{in}_{\varrho}(s^{\prime},s)$. All osteo-types in $\mathcal{I}$ are pairwise distinct, so the number of them does not exceed $N_{\Pi}$. Non-osteo-types are called fluff-types. By monotonicity, any fluff-type ${\boldsymbol{t}}(s^{\prime})$ has the same temporal literals as its nearest osteo-type ${\boldsymbol{t}}(s)$, for $s<s^{\prime}$. For example, in the model of the program $\Pi=\{\boxminus_{\varrho}P\land{}_{\varrho}P\land P\to\bot\}$, $\varrho=[1,\infty)$, shown below, there are three fluff-types: ${\boldsymbol{t}}(3/4)$, ${\boldsymbol{t}}(9/8)$, and ${\boldsymbol{t}}(5/4)$.

[math]\neg{}_{\varrho}P$$\neg{}_{\varrho}\neg P$$\neg P$$\frac{1}{2}$$\neg{}_{\varrho}P$$\neg{}_{\varrho}\neg P$$P$$\frac{3}{4}$$\neg{}_{\varrho}P$$\neg{}_{\varrho}\neg P$$\neg P$$1$$\neg{}_{\varrho}P$${}_{\varrho}\neg P$$\neg P$$\frac{9}{8}$$\neg{}_{\varrho}P$${}_{\varrho}\neg P$$P$$\frac{5}{4}$$\neg{}_{\varrho}P$${}_{\varrho}\neg P$$P$$\frac{3}{2}$${}_{\varrho}P$${}_{\varrho}\neg P$$\neg Pfluff-types fluff-type

We now define an FO-sentence $\Phi_{\Pi}$ such that any given data instance $\mathcal{D}$ is consistent with $\Pi$ iff $\Phi_{\Pi}$ holds in the FO-structure $\mathcal{D}$. Let $\mathfrak{O}_{\Pi}$ be the set of sequences $\bar{\boldsymbol{t}}=({\boldsymbol{t}}_{1},\dots,{\boldsymbol{t}}_{n})$, $1\leq n\leq N_{\Pi}$, of distinct types for $\Pi$ that satisfy the monotonicity property and such that ${}_{\varrho}\sigma\in{\boldsymbol{t}}_{i}$ implies $\sigma\in{\boldsymbol{t}}_{j}$ for some $j\leq i$; for minimal such $j$, we write $\textit{wit}({\boldsymbol{t}}_{i},{\boldsymbol{t}}_{j},\varrho)$. We write $\overline{\textit{wit}}({\boldsymbol{t}}_{i},{\boldsymbol{t}}_{j},\varrho)$ if $j\leq i$, $\neg{}_{\varrho}\sigma\in{\boldsymbol{t}}(s_{i})$ and $\sigma\in{\boldsymbol{t}}(s_{j})$, for some ${}_{\varrho}\sigma$. Denote by $\mathfrak{F}^{i}_{\bar{\boldsymbol{t}}}$ the set of types ${\boldsymbol{t}}$ for $\Pi$ sharing the same temporal literals with ${\boldsymbol{t}}_{i}$ and such that, for every $\sigma\in{\boldsymbol{t}}$, there is ${\boldsymbol{t}}_{j}\ni\sigma$ with $j\leq i$. Finally, for any type ${\boldsymbol{t}}$, let $\delta_{\boldsymbol{t}}(x)=\bigwedge_{\neg P\in{\boldsymbol{t}}}\neg P(x)$ (which is true at $t$ in $\mathcal{D}$ iff, for every $P$ in $\Pi$, whenever $P(t)\in\mathcal{D}$ then $P(t)\in{\boldsymbol{t}}$). Now, we set

[TABLE]

where $x_{i}\prec y$ says that $x_{i}$ is the nearest predecessor of $y$, which is different from $x_{1},\dots,x_{n}$.

Suppose $\mathcal{I}$ is a model of $\Pi$, $\mathcal{D}$ and $\bar{\boldsymbol{t}}=({\boldsymbol{t}}(t_{1}),\dots,{\boldsymbol{t}}(t_{n}))$, for $t_{1}<\dots<t_{n}$, are all the osteo-types in $\mathcal{I}$. This $n$-tuple of types is in $\mathfrak{O}_{\Pi}$ and the $\delta_{{\boldsymbol{t}}(t_{i})}(t_{i})$ are true in $\mathcal{I}$ by definition. The $\mathsf{in}_{\varrho}(t_{i},t_{j})$ also hold for ${\it wit}({\boldsymbol{t}}(t_{i}),{\boldsymbol{t}}(t_{j}),\varrho)$ because ${\boldsymbol{t}}(t_{i})$ is the first type in $\mathcal{I}$ witnessing the relevant ${}_{\varrho}\sigma$. Similarly, $\mathsf{in}_{\varrho}(t_{i},t_{j})$ does not hold in $\mathcal{I}$ for $\overline{\it wit}({\boldsymbol{t}}(t_{i}),{\boldsymbol{t}}(t_{j}),\varrho)$. Finally, let $t$ be any timestamp in $\mathcal{I}$ with $t_{i}\prec t$. By construction, ${\boldsymbol{t}}(t)$ is a fluff-type in $\mathfrak{F}^{i}_{\bar{\boldsymbol{t}}}$ and $\delta_{{\boldsymbol{t}}(t)}(t)$ holds in $\mathcal{I}$. If $\overline{\it wit}({\boldsymbol{t}}(t_{i}),{\boldsymbol{t}}(t_{j}),\varrho)$, we have $\neg{}_{\varrho}\sigma\in{\boldsymbol{t}}(t_{i})\cap{\boldsymbol{t}}(t)$ and $\sigma\in{\boldsymbol{t}}(t_{j})$, and so $\mathsf{in}_{\varrho}(t,t_{j})$ cannot hold in $\mathcal{I}$. Thus, $\mathcal{D}\models\Phi_{\Pi}$.

Conversely, suppose $\Phi_{\Pi}$ holds in $\mathcal{D}$, assigning timestamps $t_{i}$ to the $x_{i}$ and associating types ${\boldsymbol{t}}(t)$ with every $t\in{\mathsf{ts}}(\mathcal{D})$. Define an interpretation $\mathcal{I}$ by setting

[TABLE]

for every atom $P$. We prove that $\mathcal{I}$ is a model of $\Pi$ and $\mathcal{D}$. As all the ${\boldsymbol{t}}(t)$ are types for ${\boldsymbol{q}}$, it suffices to show that

[TABLE]

Suppose ${}_{\varrho}\sigma\in{\boldsymbol{t}}(t)$. If $t=t_{i}$, for some $i$, then $\textit{wit}({\boldsymbol{t}}_{i},{\boldsymbol{t}}_{j},\varrho)$, for some $j\leq i$, and so $\sigma\in{\boldsymbol{t}}(t_{j})$ and $\mathsf{in}_{\varrho}(t_{i},t_{j})$ holds in $\mathcal{I}$. If $t_{i}\prec t$, then ${}_{\varrho}\sigma\in{\boldsymbol{t}}(t_{i})$, and we can use the previous argument as $\mathsf{in}_{\varrho}(t_{i},t_{j})$ implies $\mathsf{in}_{\varrho}(t,t_{j})$.

Conversely, suppose ${}_{\varrho}\sigma\notin{\boldsymbol{t}}(t)$. Then $\neg{}_{\varrho}\sigma\in{\boldsymbol{t}}(t)$. Consider first the case $t=t_{i}$. Suppose $t^{\prime}\leq t_{i}$ with $\sigma\in{\boldsymbol{t}}(t^{\prime})$. Then $\sigma\in{\boldsymbol{t}}(t_{j})$ for some $t_{j}\leq t^{\prime}$, and so $\overline{\it wit}({\boldsymbol{t}}_{i},{\boldsymbol{t}}_{j},\varrho)$ and $\neg\mathsf{in}_{\varrho}(t_{i},t_{j})$, whence $\neg\mathsf{in}_{\varrho}(t,t_{j})$ and $\neg\mathsf{in}_{\varrho}(t,t^{\prime})$. Now, let $t\notin\{t_{1},\dots,t_{n}\}$. Then $t_{i}\prec t$ for some $i$ (because of $\min x_{1}$). Suppose $t^{\prime}\leq t$ with $\sigma\in{\boldsymbol{t}}(t^{\prime})$. If $t^{\prime}<t_{i}$, then $\sigma\in{\boldsymbol{t}}(t_{j})$ for some $t_{j}\leq t^{\prime}$, and so $\overline{\it wit}({\boldsymbol{t}}_{i},{\boldsymbol{t}}_{j},\varrho)$ and $\neg\mathsf{in}_{\varrho}(t,t_{j})$, whence $\neg\mathsf{in}_{\varrho}(t,t^{\prime})$. If $t^{\prime}=t_{i}$, then, by the last conjunct of $\Phi_{\Pi}$, we have $\neg\mathsf{in}_{\varrho}(t,t_{i})$. Finally, if $t_{i}<t^{\prime}\leq t$, then $\sigma\in{\boldsymbol{t}}(t_{j})$, for some $t_{j}\leq t_{i}$, and we are done again.

An FO$(<)$-rewriting of ${\boldsymbol{q}}$ is the FO formula $\neg\Phi_{\neg A}(x)$, where $\Phi_{\neg A}(x)$ is obtained from $\Phi_{\Pi}$ by replacing $\delta_{\boldsymbol{t}}(z)$ with $\delta_{\boldsymbol{t}}(z,x)$, which is $\delta_{\boldsymbol{t}}(z)$ if $\neg A\in{\boldsymbol{t}}$ and $\delta_{\boldsymbol{t}}(z)\land(x\neq z)$ otherwise. Clearly, $\Phi_{\neg A}(x)$ holds in $\mathcal{D}$ iff there is a model of $\Pi$ and $\mathcal{D}$ satisfying $\neg A$ in $x$. ∎

We also mention in passing one more FO-rewritability result (which does not fit our classification). To formulate it, we require a few definitions.

Normal form. Until the end of this section, we assume that our MTL programs and OMQs are in normal form. Namely, a program is said to be in normal form if its rules have one of the forms:

[TABLE]

where the $P^{\prime}_{i}$ are from the data alphabet (like EDB predicates in datalog) and do not occur in the rule heads, while the $P_{i}$ do not occur in data instances, and $0\notin\varrho_{i}$ for any $i$ (although there may be $\varrho^{\prime}_{i}=[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 5**.**

Let $\Pi=\{{}_{[0,d]}P_{0}^{\prime}\land Q_{0}^{\prime}\to P_{1}^{\prime},\ {}_{(0,e)}P_{1}^{\prime}\land{}_{[0,f]}Q_{1}^{\prime}\to P_{0}^{\prime}\}$, where the $P_{i}^{\prime}$ are in the data alphaet. By introducing fresh atoms $P_{0}$, $P_{1}$, we convert $\Pi$ to

[TABLE]

To get rid of $[0,d]$, we further transform the program to

[TABLE]

Now, $P_{0}$ in the first rule is not in the scope of ϱ ($Q_{0}^{\prime}$ can be regarded as a shorthand for ${}_{[0,0]}Q_{0}^{\prime}$). So we transform the rule using obvious derivations to obtain the following program in normal form:

[TABLE]

A hornMTL query $(\Pi,A(x))$ is in normal form if $\Pi$ is in normal form and $A$ is not in the data alphabet. Clearly, every query can be converted to a one in normal form and having the same answers.

Metric automata for hornMTL. Our technical tool for studying the data complexity of linear hornMTL queries is automata with metric constraints that are defined for programs in normal form. These automata can be viewed as a primitive version of standard timed automata for MTL [1] as we only have one clock $c$, the clock reset $c:=0$ happens at every transition, and the clock constraints are of the simple form $c\in\varrho$.

A (nondeterministic) metric automaton is a quadruple $\mathcal{A}=(S,S_{0},\Sigma,\delta)$, where $S\neq\emptyset$ is a set of states, $\Sigma$ a tape alphabet, $\delta$ a transition relation, and $S_{0}$ is a nonempty set of pairs of the form $(q,e)$, where $e\in\Sigma$, $q\in S$. The transition relation $\delta$ is a set of instructions of the form $q\xrightarrow{\varrho}_{e}q^{\prime}$ with $q,q^{\prime}\in S$, $e\in\Sigma$ and a range $\varrho$. The automaton $\mathcal{A}$ takes as input timed words $\sigma=(e_{0},t_{0}),\dots,(e_{n},t_{n})$, where the $t_{i}$ are timestamps with $t_{i-1}<t_{i}$. A run over $\sigma$ is a sequence $q_{0},\dots,q_{m}$ such that $(q_{0},e_{0})\in S_{0}$, $q_{i-1}\xrightarrow{\varrho_{i}}_{e_{i}}q_{i}$ is in $\delta$ and $t_{i}-t_{i-1}\in\varrho_{i}$, for $0<i\leq n$.

Let $\Pi$ be a linear hornMTL program in normal form. We denote the conjunctions ${}_{\varrho_{1}^{\prime}}P^{\prime}_{1}\land\ldots\land{}_{\varrho_{\ell}^{\prime}}P^{\prime}_{m}$ (with data atoms $P_{i}^{\prime}$) that occur in $\Pi$ by $\varepsilon$, possibly with subscripts. Thus, since $\Pi$ is linear, rules (4) in $\Pi$ are of the form $\varepsilon\land{}_{\varrho}Q\to P$. Let $E_{\Pi}=\{\varepsilon_{1},\dots,\varepsilon_{q}\}$ be the set of all such $\varepsilon$ occurring in $\Pi$. We define a metric automaton $\mathcal{A}_{\Pi}$ for $\Pi$ as follows. The set $S$ of its states comprises the head concept names in $\Pi$, and $\Sigma=2^{E_{\Pi}}$. The transition relation $\delta$ comprises $Q\xrightarrow{\varrho}_{E}P$ such that $\varepsilon\land{}_{\varrho}Q\to P$ is in $\Pi$ and $\varepsilon\in E$. Finally, $S_{0}$ is the set of all pairs $(P,\varepsilon)$ such that a rule $\varepsilon\to P$ of the form (3) is in $\Pi$.

Example 6**.**

For $\Pi=\{{}_{[0,1]}P_{0}^{\prime}\to P_{0},\ {}_{(1,2)}P_{0}\land P_{1}^{\prime}\to P_{1},\ {}_{(1,3)}P_{1}\to P_{0}\}$, the metric automaton $\mathcal{A}_{\Pi}$ is depicted below, where $P_{0}^{\prime},P_{1}^{\prime}\in\Lambda$, $E_{0}=\{P_{1}^{\prime}\}$, $E_{1}=\{{}_{[0,1]}P_{0}^{\prime}\}$, $E_{2}=\{P_{1}^{\prime},{}_{[0,1]}P_{0}^{\prime}\}$, and $S_{0}=\{(P_{0},{}_{[0,1]}P_{0}^{\prime})\}$.

P_{0}$$P_{1}$$E_{0}\ (1,2)$$E_{2}\ (1,2)$$\emptyset\ (1,3)$$E_{0}\ (1,3)$$E_{1}\ (1,3)$$E_{2}\ (1,3)

We represent any data instance $\mathcal{D}$ as a timed word $\sigma_{\mathcal{D}}$. For $t_{i}$ occurring in $\mathcal{D}$, let $E(t_{i})$ be the maximal set of $\varepsilon$ from $\Pi$ that hold at $t_{i}$ in $\mathcal{D}$, and let \sigma_{\mathcal{D}}=\big{(}(E(t_{1}),t_{1}),\dots,(E(t_{n}),t_{n})\big{)}.

Example 7**.**

A data instance $\mathcal{D}$ and its representation as $\sigma_{\mathcal{D}}$ are shown below:

$P_{0}^{\prime}$[math]Q^{\prime}$$1$$P_{1}^{\prime}$$1.5$$P_{0}^{\prime}$$4$$P_{1}^{\prime}$$4.5$$P_{1}^{\prime}$$5$$Q^{\prime}$$6.5$$\mathcal{D}:$$\emptyset$$E_{1}$$E_{0}$$\emptyset$$E_{2}$$E_{2}$$\emptyset$$\sigma_{\mathcal{D}}:

Theorem 8**.**

For any linear hornMTL OMQ $(\Pi,A(x))$, a timestamp $t_{i}$ is a certain answer over a data instance $\mathcal{D}$ iff there exist a subword $\sigma_{\mathcal{D}}^{\prime}$ of $\sigma_{\mathcal{D}}$ with the last timestamp $t_{i}$ and a run of $\mathcal{A}_{\Pi}$ over $\sigma_{\mathcal{D}}^{\prime}$ that ends with $A$.

Example 9**.**

Let $(\Pi,P_{1}(x))$ be an OMQ with $\Pi$ from Example 6. Then, for $\sigma_{\mathcal{D}}$ from Example 7, we have the run $P_{0},P_{1},P_{0},P_{1}$ on

[TABLE]

and so $5$ is a certain answer to the query over $\mathcal{D}$ from Example 7.

One could define metric automata as classical timed automata; however, Theorem 8 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 clarified. We now use the obtained automaton characterisation of certain answers for linear queries to give better complexity bounds for the case of restricted temporal ranges than the NL bound of Theorem 3 $(iii)$.

Call an MTL-program range-uniform if all of its temporal operators have the same constraining range.

Theorem 10**.**

Range-uniform coreMTL-OMQs with ranges of the form ⟨0,r⟩ are FO$(<,+)$-rewritable.

Proof.

We illustrate the proof by a concrete example. Consider the OMQ $(\Pi,S_{1})$ with

[TABLE]

For such a $\Pi$ the automaton $\mathcal{A}_{\Pi}$ is shown in the picture below on the right-hand side. Using it, we construct the following FO-rewriting ${\boldsymbol{Q}}(x)$ of $(\Pi,S_{1})$:

[TABLE]

where

• –

$\varphi_{1}(x^{\prime},x)=(x-x^{\prime})\in 1+3\mathbb{N}$;

• –

$\varphi_{2}(x^{\prime},x)=(x-x^{\prime})\in 2+3\mathbb{N}\land\exists x_{1}\,((x^{\prime}<x_{1}\leq x)\land\varphi_{+1}(x_{1},x^{\prime}))$;

• –

$\varphi_{3}(x^{\prime},x)=(x-x^{\prime})\in 3+3\mathbb{N}\land\varphi_{1+1+1}(x^{\prime},x)\lor\varphi_{1+2}(x^{\prime},x)$;

• –

$\varphi_{1+2}(x^{\prime},x)=\exists x_{1}\,((x^{\prime}<x_{1}\leq x)\land\varphi_{+2}(x_{1},x^{\prime}))$;

• –

$\varphi_{1+1+1}(x^{\prime},x)=\exists x_{1},x_{2}\,((x^{\prime}<x_{1}<x_{2}\leq x)\land\varphi_{+1}(x_{1},x^{\prime})\land\varphi_{+1}(x_{2},x^{\prime})\land{}((x_{2}-x_{1})>1))$;

• –

$\varphi_{+k}(z,x^{\prime})=\mathsf{dist}_{<d}(z,z-k-1)\land((z-k-1)\geq x^{\prime})$, for $k=1,2$.

Intuitively, to derive $S_{1}$ at $x$, we need a point $x^{\prime}$ with $B(x^{\prime})$ in the data and a sequence of points $y$ between $x^{\prime}$ and $x$ without gaps of length $\geq d$. An example of such a data instance is given below.

Note how we maintain the ‘stack of states’ with the elements at its bottom alternating in a cycle between $S_{1},S_{2}$, and $S_{3}$. Note also that the states go in decreasing order when we scan the stack from bottom to top. So we use the formulas $\varphi_{k}(x^{\prime},x)$ to express that $S_{1}$ is inferred at $x$ on level $k$ of the stack. The formula $\varphi_{+k}(z,x^{\prime})$ 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 $\varphi_{1+2}(x^{\prime},x)$ and $\varphi_{1+1+1}(x^{\prime},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 $x^{\prime}$ such as $(x-x^{\prime})\in 1+3\mathbb{N}$ can be expressed by FO-formulas using the predicate $\text{PLUS}(\textit{num}1,\textit{num}2,\textit{sum})$ or $\text{BIT}(\textit{num},\textit{bit})$, which gives a binary representation of every object $num$ in the domain of an FO-structure [23], whereas FO with $<$ only is not enough. For example, $(x-x^{\prime})\in 1+3\mathbb{N}$ is expressed by the formula

[TABLE]

We leave further details to the reader. ∎

5 OMQs with Punctual Ranges $[r,r]$

Operators of the form [r,r] resemble the LTL previous time operator $\ominus$. To illustrate an essential difference, consider the program $\Pi=\{{}_{[1,1]}P\to Q,\ {}_{[1.5,1.5]}P\land Q\to P\}$ and the data instance $\mathcal{D}$ below. In LTL, we always derive $\ominus P$ at $n+1$

$P$[math]P$$\frac{1}{4}$$P$$\frac{3}{4}$$P$$\frac{7}{8}$$P\ Q$$\frac{7}{4}$$Q$$\frac{15}{8}$$3$${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}P}\ Q$$\frac{13}{4}

if $P$ holds at $n$. In our example, $P$ at $3/4$ implies $Q$ at $7/4$, which together with $P$ at $1/4$ imply $P$ at $7/4$, and eventually the latter $P$ with $Q$ at $13/4$ implies $P$ at $13/4$; independently, $P$ at $7/8$ implies $Q$ at $15/8$.

Theorem 11**.**

MTL*-OMQs with temporal operators of the form [r,r] and $\boxminus_{[r,r]}$ only are FO(RPR)-rewritable; answering such OMQs is $\textsc{NC}^{1}$-complete for data complexity.*

Proof.

$\textsc{NC}^{1}$-hardness is proved by reduction of hornMTL-OMQs with rules of the form $\ominus P\land P^{\prime}\to Q$, answering which is NC1-complete [4].

To show FO(RPR)-rewritability of a given OMQ ${\boldsymbol{q}}=(\Pi,A)$, we assume w.l.o.g. that $\Pi$ does not contain ranges $[0,0]$. Let $R_{\Pi}$ be the set of numbers occurring as endpoints of ranges in $\Pi$. We set $\boldsymbol{1}=\text{gcd}(R_{\Pi})$, $\boldsymbol{n}=\boldsymbol{1}\cdot n$, for $n\in\mathbb{N}$, $\boldsymbol{m}=\max(R_{\Pi})$. Thus, in our example above, $\boldsymbol{1}=1/2$, $\boldsymbol{2}=1$, $\boldsymbol{3}=3/2$. We define ${\it cl}(\Pi)$ to be the set of simple and temporal literals with atoms from $\Pi$ and operators i such that $\boldsymbol{i}\in\{\boldsymbol{1},\dots,\boldsymbol{n}\}$ and n occurs in $\Pi$. By a type ${\boldsymbol{s}}$ for $\Pi$ we now mean any maximal subset of ${\it cl}(\Pi)$ consistent with $\Pi$. For types ${\boldsymbol{s}}$, ${\boldsymbol{s}}^{\prime}$ and $\boldsymbol{i}\in\{\boldsymbol{1},\dots,\boldsymbol{m}\}$, we write ${\boldsymbol{s}}\rightarrow_{\boldsymbol{i}}{\boldsymbol{s}}^{\prime}$ if

• –

$\sigma\in{\boldsymbol{s}}$ iff ${}_{\boldsymbol{i}}\sigma\in{\boldsymbol{s}}^{\prime}$, for any ${}_{\boldsymbol{i}}\sigma\in{\it cl}(\Pi)$;

• –

${}_{\boldsymbol{j}}\sigma\in{\boldsymbol{s}}$ iff ${}_{\boldsymbol{j+i}}\sigma\in{\boldsymbol{s}}^{\prime}$, for ${}_{\boldsymbol{j+i}}\sigma\in{\it cl}(\Pi)$, $\boldsymbol{j}\geq\boldsymbol{1}$.

We say that $({\boldsymbol{s}}_{0},t_{0}),\dots,({\boldsymbol{s}}_{n},t_{n})$ is a run from $t_{0}$ to $t_{n}$ on a data instance $\mathcal{D}$ of the form (2) if $t_{i}\in{\mathsf{ts}}(\mathcal{D})$, for $i\leq n$, and

• –

$\{P\in\varSigma_{\Pi}\mid t_{0}\in P^{\mathcal{D}}\}\subseteq{\boldsymbol{s}}_{0}$;

• –

$\neg{}_{\boldsymbol{j}}\sigma\in{\boldsymbol{s}}_{0}$ for all ${}_{\boldsymbol{j}}\sigma\in cl(\Pi)$;

• –

$\bar{t}_{i+1}-\bar{t}_{i}\in\{\boldsymbol{1},\dots,\boldsymbol{m}\}$ and if $t_{i+1}>t>t_{i}$ then $\bar{t}-\bar{t}_{i}\not\in\{\boldsymbol{1},\dots,\boldsymbol{m}\}$, for any $t\in{\mathsf{ts}}(\mathcal{D})$;

• –

${\boldsymbol{s}}_{i}\rightarrow_{(\bar{t}_{i+1}-\bar{t}_{i})}{\boldsymbol{s}}_{i+1}$ and $\{P\!\in\!\varSigma_{\Pi}\mid t_{i+1}\in P^{\mathcal{D}}\}\subseteq{\boldsymbol{s}}_{i+1}$.

Call $t\in{\mathsf{ts}}(\mathcal{D})$ initial if $\bar{t}-\bar{t}^{\prime}\not\in\{\boldsymbol{1},\dots,\boldsymbol{m}\}$, for all $t^{\prime}\in{\mathsf{ts}}(\mathcal{D})$. The next lemma follows directly from the given definitions:

Lemma 12**.**

$(i)$* $(\Pi,\mathcal{D})$ is consistent iff, for every $t\in{\mathsf{ts}}(\mathcal{D})$, there exists a run on $\mathcal{D}$ from some initial $t^{\prime}\leq t$ to $t$; $(ii)$ A timestamp $t\in{\mathsf{ts}}(\mathcal{D})$ is not a certain answer to ${\boldsymbol{q}}$ over $\mathcal{D}$ iff $(\Pi,\mathcal{D})$ is consistent and there is a run $({\boldsymbol{s}}_{0},t_{0}),\dots,({\boldsymbol{s}}_{n},t_{n})$ from initial $t_{0}$ to $t=t_{n}$ on $\mathcal{D}$ and $\neg A\in{\boldsymbol{s}}_{n}$.*

We first show how to express the existence of a run from $x$ to $y$ specified in $(ii)$ by an FO(RPR)-formula $\mathsf{run}_{\boldsymbol{q}}(x,y)$ over $\mathcal{D}$. First, as divisibility of binary integers by a given number is recognisable by a finite automaton, we can define an FO(RPR)-formula $\mathsf{div}_{\boldsymbol{1}}(u,v)$ that is true iff $\bar{u}-\bar{v}=n\boldsymbol{1}$, for some $n\in\mathbb{N}$ (see Appendix B). We also have an FO-formula $\mathsf{last}_{\boldsymbol{i}}(u)$ saying that $\boldsymbol{i}$ is minimal among $\{\boldsymbol{1},\dots,\boldsymbol{m}\}$ with $\bar{u}-\boldsymbol{i}=\bar{v}$, for some $v\in{\mathsf{ts}}(\mathcal{D})$. Let $Q=\{{\boldsymbol{s}}_{1},\dots,{\boldsymbol{s}}_{n}\}$ be the set of all types for $\Pi$, and let $Q_{0}\subseteq Q$ comprise ${\boldsymbol{s}}$ with $\neg{}_{\boldsymbol{j}}\sigma\in{\boldsymbol{s}}$, for all ${}_{\boldsymbol{j}}\sigma\in{\it cl}(\Pi)$. We define $\mathsf{run}_{\boldsymbol{q}}(x,y)$ as the FO(RPR)-formula

[TABLE]

where $R_{{\boldsymbol{s}}}(x,z)$, for ${\boldsymbol{s}}\in Q$, is a relation variable and the formula $\vartheta_{\boldsymbol{s}}(x,z,R_{{\boldsymbol{s}}_{1}}(x,z-1),\dots,R_{{\boldsymbol{s}}_{n}}(x,z-1))$ is a disjunction of the three formulas below if ${\boldsymbol{s}}\in Q_{0}$ and a disjunction of the last two of them if ${\boldsymbol{s}}\notin Q_{0}$:

[TABLE]

where $z-1$ is the immediate predecessor of $z$ in ${\mathsf{ts}}(\mathcal{D})$.

To illustrate, in the context of the example above, the formulas $R_{\boldsymbol{s}}\equiv\vartheta_{\boldsymbol{s}}$ say that $R_{{\boldsymbol{s}}}(1/4,1/4)$ holds for the types

[TABLE]

Then $R_{{\boldsymbol{s}}}(1/4,3/4)$ holds for

[TABLE]

$R_{{\boldsymbol{s}}}(1/4,7/8)$ for the same ${\boldsymbol{s}}$ as $R_{{\boldsymbol{s}}}(1/4,3/4)$, $R_{{\boldsymbol{s}}}(1/4,7/4)$ for ${\boldsymbol{s}}=\{\neg{}_{\boldsymbol{1}}P,{}_{\boldsymbol{2}}P,{}_{\boldsymbol{3}}P,P,Q\}$, and so on.

Thus, we obtain the following FO(RPR)-rewriting of ${\boldsymbol{q}}$

[TABLE]

where $\Phi_{\Pi}$ checks the consistency condition of Lemma 12 $(i)$ and can be constructed similarly to $\mathsf{run}_{\boldsymbol{q}}$. ∎

6 OMQs with Non-Punctual Ranges

Unlike the proof of Theorem 11, where the derived facts at $t$ were determined by the data $\mathcal{D}$ at $t$ and the derived facts at the nearest $t^{\prime}\in{\mathsf{ts}}(\mathcal{D})$ with $\bar{t}^{\prime}=\bar{t}-\boldsymbol{i}$, for non-punctual ranges the derived facts at $t$ depend on an unbounded number of timestamps $t^{\prime}<t$. In the proof of Theorem 13 below, we show that to construct derivations in this case, we can actually keep track of a fixed number (depending only on the given OMQ) of moments $t_{P}^{\prime}<t$ where each $P$ was derived.

Theorem 13**.**

$(i)$* MTL-OMQs whose operators ϱ and $\boxminus_{\varrho}$ have non-punctual $\varrho$ are FO(TC)-rewritable; answering them is in NL and ${\textsc{NC}^{1}}$-hard; $(ii)$ hornMTL-OMQs of this kind are FO(DTC)-rewritable; answering them is in L and ${\textsc{NC}^{1}}$-hard.*

Proof.

In both cases, ${\textsc{NC}^{1}}$-hardness can be established as in the proof of Theorem 11 by encoding $\ominus$ with (0,1].

$(i)$ Let ${\boldsymbol{q}}=(\Pi,A)$ be the given OMQ. For $\varrho=\langle r,q\rangle$ with $q\neq\infty$, let $\varrho^{-}=\langle 0,q-r\rangle$ and $\varrho^{+}=\langle 0,q\rangle$; if $q=\infty$, $\varrho^{-}$ and $\varrho^{+}$ are undefined. Let $\Sigma_{\Pi}$ be the set of all $\sigma$ with ${}_{\varrho}\sigma$ in $\Pi$, for some $\varrho$. For $\sigma\in\Sigma_{\Pi}$, let $\varrho_{\sigma}^{-}$ ($\varrho_{\sigma}^{+}$) be the intersection (union) of the defined $\varrho^{-}$ ($\varrho^{+}$) with ${}_{\varrho}\sigma$ in $\Pi$; if there are no such ${}_{\varrho}\sigma$, $\varrho_{\sigma}^{-}$ and $\varrho_{\sigma}^{+}$ are undefined. To illustrate, consider the hornMTL-program $\Pi$ with the rules

[TABLE]

Then $\varrho_{P}^{-}=(0,1)$, $\varrho_{P}^{+}=[0,4]$, and $\varrho_{Q}^{-}$, $\varrho_{Q}^{+}$ are undefined.

For a data instance $\mathcal{D}$, a trace of length $\ell$ for $t\in{\mathsf{ts}}(\mathcal{D})$ is a sequence of intervals $[u_{0},s_{0}],\dots,[u_{\ell},s_{\ell}]$ where either $[u_{i},s_{i}]=[*,*]$ (meaning that this interval is undefined) or $u_{i},s_{i}\in{\mathsf{ts}}(\mathcal{D})$, $u_{0}=s_{0}$, and $u_{1}\leq s_{1}<u_{2}\leq s_{2}<\dots<u_{\ell}\leq s_{\ell}\leq t$, assuming that $*<u$, for any $u$. Thus, for the data instance $\mathcal{D}$ below,

P$$\frac{1}{2}$$P$$\frac{5}{4}$$Q$$\frac{5}{2}$$\frac{15}{4}$$5$$\frac{25}{4}$$10

$([{\textstyle\frac{1}{2}},{\textstyle\frac{1}{2}}],[*,*],[*,*],[{\textstyle\frac{1}{2}},{\textstyle\frac{5}{4}]},[{\textstyle\frac{5}{2}},{\textstyle\frac{5}{2}}])$ is a trace for $t=5/2$. Intuitively, such a trace stores the most recent $\ell$ intervals preceding $t$ where a simple literal holds at some point, with $[u_{0},s_{0}]$ storing the very first point where the literal holds. A tuple $(\boldsymbol{t},(\boldsymbol{tr}_{\sigma})_{\sigma\in\Sigma_{\Pi}},t)$ is an extended type for $t\in{\mathsf{ts}}(\mathcal{D})$ if

• –

$\boldsymbol{t}$ is a type for $\Pi$ (as in the proof of Theorem 4);

• –

$\boldsymbol{tr}_{\sigma}$ is a trace for $t$ of length $\ell_{\sigma}=\lceil|\varrho_{\sigma}^{+}|/|\varrho_{\sigma}^{-}|\rceil$, where $|\varrho_{\sigma}^{+}|$ and $|\varrho_{\sigma}^{-}|$ denote the end-points of these intervals; if one of the intervals is undefined, $\ell_{\sigma}=0$;

• –

${}_{\varrho}\sigma\in\boldsymbol{t}$ iff $\mathsf{int}_{\varrho}(t,u_{i},s_{i})$, for some $[u_{i},s_{i}]$ in $\boldsymbol{tr}_{\sigma}$,

where $\mathsf{int}_{\varrho}(t,u,s)$ is true iff $\{\bar{t}-k\mid k\in\varrho\}\cap[\bar{u},\bar{s}]\neq\emptyset$ and $u,s\neq*$. In our example, $\ell_{P}=4$, $\ell_{Q}=0$, and the following triples $(\boldsymbol{t}_{i},(\boldsymbol{tr}^{i}_{\sigma})_{\sigma\in\Sigma_{\Pi}},t_{i})$ are extended types for $t_{i}$:

[TABLE]

Intuitively, an extended type records the simple and temporal literals that hold at $t$ (the type ${\boldsymbol{t}}$) and also some history of the validity of $\sigma$ (the traces) justifying the presence of ${}_{\varrho}\sigma$ in ${\boldsymbol{t}}$. As follows from Lemma 14 below, to make correct derivations, this history should keep $\ell_{\sigma}+1$ intervals. Note that this bound does not apply if punctual intervals are present in $\Pi$, which explains the increase of complexity in Theorem 3.

Lemma 14**.**

Let $t_{0}<\dots<t_{m}$ be all the timestamps in $\mathcal{D}$. Then $\Pi$ and $\mathcal{D}$ are consistent iff there exists a sequence $(\boldsymbol{t}_{i},(\boldsymbol{tr}^{i}_{\sigma})_{\sigma\in\Sigma_{\Pi}},t_{i})$ of extended types for $t_{i}$, $0\leq i\leq m$, satisfying the following conditions for $\sigma\in\Sigma_{\Pi}$:**

• –

$\{P\in\varSigma_{\Pi}\mid t_{i}\in P^{\mathcal{D}}\}\subseteq{\boldsymbol{t}}_{i}$;

• –

*if $\sigma\notin\boldsymbol{t}_{0}$, all $[u_{j},s_{j}]$ in $\boldsymbol{tr}^{0}_{\sigma}$ are $[*,*]$; if $\sigma\in\boldsymbol{t}_{0}$, then $[u_{0},s_{0}]=[u_{\ell_{\sigma}},s_{\ell_{\sigma}}]=[t_{0},t_{0}]$ and $[u_{j},s_{j}]=[*,*]$ for $0<j<\ell_{\sigma}$; *

• –

if $\sigma\not\in\boldsymbol{t}_{i}$ and $i>0$, then $\boldsymbol{tr}^{i}_{\sigma}=\boldsymbol{tr}^{i-1}_{\sigma}$; if $\sigma\in\boldsymbol{t}_{i}$, $\boldsymbol{tr}^{i-1}_{\sigma}=([u_{0},s_{0}],\dots,[u_{\ell_{\sigma}},s_{\ell_{\sigma}}])$ and $[u,s]=[u_{0},s_{0}]$ when $u_{0}\neq*$ and $[u,s]=[t_{i},t_{i}]$ otherwise, then $\boldsymbol{tr}^{i}_{\sigma}=([u,s],[u_{1},s_{1}],\dots,[u_{\ell_{\sigma}},t_{i}])$ if $\bar{t}_{i}-\bar{s}_{\ell_{\sigma}}\in\varrho^{-}_{\sigma}$, else $\boldsymbol{tr}^{i}_{\sigma}=([u,s],[u_{2},s_{2}],\dots,[u_{\ell_{\sigma}},s_{\ell_{\sigma}}],[t_{i},t_{i}])$.

Proof.

$(\Rightarrow)$ For a model $\mathcal{I}$ of $\Pi$ and $\mathcal{D}$, we define $(\boldsymbol{t}_{i},(\boldsymbol{tr}^{i}_{\sigma})_{\sigma\in\Sigma_{\Pi}},t_{i})$ with $\boldsymbol{t}_{i}=\boldsymbol{t}(t_{i})$ as follows. If there is a minimal $t_{j}\leq t_{i}$ with $\sigma\in{\boldsymbol{t}}(t_{j})$, we set $[u_{0},s_{0}]=[t_{j},t_{j}]$ in $\boldsymbol{tr}^{i}_{\sigma}$; otherwise $[u_{0},s_{0}]=[*,*]$. Consider a maximal interval $[u,s]$, $s\leq t_{i}$, such that $\sigma\in{\boldsymbol{t}}(u)\cap{\boldsymbol{t}}(s)$ and, for any $t\in[u,s)$, there is $t^{\prime}\in{\mathsf{ts}}(\mathcal{D})$ with $\sigma\in{\boldsymbol{t}}(t^{\prime})$ and $\bar{t}^{\prime}-\bar{t}\in\varrho_{\sigma}^{-}$. Suppose there are $k$ such intervals. Let $k^{\prime}=\min\{k,\ell_{\sigma}\}$. We define $\boldsymbol{tr}^{i}_{\sigma}$ by making its last intervals equal to $[u_{\ell_{\sigma}-k^{\prime}+1},s_{\ell_{\sigma}-k^{\prime}+1}],\dots,[u_{\ell_{\sigma}},s_{\ell_{\sigma}}]$, making its [math]-th interval equal to $[u_{0},s_{0}]$, and making all the remaining intervals equal to $[*,*]$. One can check that $(\boldsymbol{t}_{i},(\boldsymbol{tr}^{i}_{\sigma})_{\sigma\in\Sigma_{\Pi}},t_{i})$ are as required.

($\Leftarrow$) Given a sequence $(\boldsymbol{t}_{i},(\boldsymbol{tr}^{i}_{\sigma})_{\sigma\in\Sigma_{\Pi}},t_{i})$, $1\leq i\leq m$, we construct an interpretation $\mathcal{I}$ by making $\sigma$ true at $t_{i}$ in $\mathcal{I}$ iff $\sigma\in{\boldsymbol{t}}_{i}$ for each simple literal $\sigma$ from ${\boldsymbol{q}}$. The conditions on these extended types ensure that $\mathcal{I}$ is a model of $\Pi$ and $\mathcal{D}$. ∎

We use the characterisation of Lemma 14 to construct an FO(TC)-sentence $\Phi_{\Pi}$ that is true in $\mathcal{D}$ iff $\Pi$ and $\mathcal{D}$ are consistent, for any data instance $\mathcal{D}$. $\Phi_{\Pi}$ contains tuples of variables $\boldsymbol{x}=\boldsymbol{x}_{\sigma_{1}},\dots,\boldsymbol{x}_{\sigma_{n}}$, for $\{\sigma_{1},\dots,\sigma_{n}\}=\Sigma_{\Pi}$, where $\boldsymbol{x}_{\sigma}=\boldsymbol{x}_{0\sigma},\dots,\boldsymbol{x}_{\ell_{\sigma}\sigma}$ and $\boldsymbol{x}_{i\sigma}=u_{i\sigma},s_{i\sigma}$ for intervals in traces ${\boldsymbol{tr}}_{\sigma}$; $\boldsymbol{x}^{\prime}$ is the same as $\boldsymbol{x}$ but with primed variables:

[TABLE]

Here, $\mathsf{first}_{\boldsymbol{t}}(\boldsymbol{x})$ is an FO-formula saying that ${\boldsymbol{t}}$ holds in the first timestamp ($\min$) of $\mathcal{D}$ and $\boldsymbol{x}$ represents $\boldsymbol{tr}^{0}_{\sigma}$ for all $\sigma$ by encoding $[*,*]$ as the empty interval $[\max,\min]$. The formula $\xi(t,\boldsymbol{x},t^{\prime},\boldsymbol{x}^{\prime})$ under the transitive closure TC says that there is an extended type for $t$ with the trace given by $\boldsymbol{x}$, that $t^{\prime}$ is the immediate successor of $t$ in ${\mathsf{ts}}(\mathcal{D})$, and there is an extended type for $t^{\prime}$ whose trace is given by $\boldsymbol{x}^{\prime}$. We define it as

[TABLE]

with $\xi_{{\boldsymbol{t}}^{\prime}}(t,\boldsymbol{x},t^{\prime},\boldsymbol{x}^{\prime})$ saying that if $({\boldsymbol{t}},(\boldsymbol{tr}_{\sigma})_{\sigma\in\varSigma_{\Pi}},t)$ is an extended type for $t$ with $(\boldsymbol{tr}_{\sigma})_{\sigma\in\varSigma_{\Pi}}$ given by $\boldsymbol{x}$, then $({\boldsymbol{t}}^{\prime},(\boldsymbol{tr}^{\prime}_{\sigma})_{\sigma\in\varSigma_{\Pi}},t^{\prime})$ can be the next extended type with $(\boldsymbol{tr}^{\prime}_{\sigma})_{\sigma\in\varSigma_{\Pi}}$ given by $\boldsymbol{x}^{\prime}$:

[TABLE]

The formula $\mathsf{ext}_{\boldsymbol{t}}(t,\boldsymbol{x})$ defines an extended type for $t$ in $\mathcal{D}$:

[TABLE]

Finally, $\mathsf{first}_{\boldsymbol{t}}(\boldsymbol{x})$ is $\bot$ if there is ${}_{\varrho}\sigma\in{\boldsymbol{t}}$ and otherwise it is

[TABLE]

saying that the intervals in the initial extended type are set correctly. That $\Phi_{\Pi}$ is as required follows from Lemma 14.

One can now modify $\Phi_{\Pi}$ to obtain an FO(TC)-rewriting of ${\boldsymbol{q}}$. As before, to obtain a rewriting $\Phi_{\boldsymbol{q}}(x)$, we need a formula $\Phi_{\neg A}(x)$ that holds true on $\mathcal{D}$ iff there exists a model of $(\Pi,\mathcal{D})$ such that $\neg A$ is true at $x$ in this model. We define $\Phi_{\neg A}(x)$ as a conjunction of $\Phi_{\Pi}$ and

[TABLE]

The negation of $\Phi_{\neg A}(x)$ is the required rewriting $\Phi_{\boldsymbol{q}}(x)$.

$(ii)$ It will be convenient to assume a restricted version of our normal form (1), where ϱ operators do not occur with $\varrho=[0,r\rangle$. Every hornMTL program $\Pi$ can be converted to this form by replacing ${}_{[0,r\rangle}A$ by $A\lor{}_{(0,r\rangle}A$ and then expressing, e.g., $A\lor{}_{(0,r\rangle}A\to B$ by a pair of rules $A\to B,\,{}_{(0,r\rangle}A\to B$. (For each $\neg{}_{[0,r\rangle}\neg A$ we substitute it by $A\land\neg{}_{(0,r\rangle}\neg A$.) Let $(\boldsymbol{tr}_{\sigma})_{\sigma\in\Sigma_{\Pi}}$ be a trace for $t^{\prime}\in{\mathsf{ts}}(\mathcal{D})$ and $\Lambda$ be the set ${}_{\varrho}\sigma$ from $\Pi$ such that $int_{\varrho}(t,u_{i},s_{i})$, for some $[u_{i},s_{i}]$ in $\boldsymbol{tr}_{\sigma}$. Let $\varDelta$ be a set of $P$ from $\Pi$. We call a type ${\boldsymbol{t}}$ for $\Pi$ minimal for $t$ with respect to $\varDelta$ and $(\boldsymbol{tr}_{\sigma})_{\sigma\in\Sigma_{\Pi}}$ if every $\vartheta$ from $\Pi$ is in ${\boldsymbol{t}}$ iff $\vartheta$ is in the closure of $\Lambda$ and $\varDelta$ under rules (1). We say that a type ${\boldsymbol{t}}$ is minimal initial with respect to $\varDelta$ if it is minimal for some (every) $t$ with respect to an empty trace with all $[u_{j},s_{j}]$ in $\boldsymbol{tr}_{\sigma}$ are $[*,*]$ for all $\sigma\in\Sigma_{\Pi}$.

Lemma 15**.**

Let $t_{0}<\dots<t_{m}$ be the timestamps in $\mathcal{D}$. Then $\Pi$ and $\mathcal{D}$ are consistent iff there exists a sequence $(\boldsymbol{t}_{i},(\boldsymbol{tr}^{i}_{\sigma})_{\sigma\in\Sigma_{\Pi}},t_{i})$ of extended types for $t_{i}$, $0\leq i\leq m$, satisfying the conditions of Lemma 14 and such that: $(i)$ ${\boldsymbol{t}}_{0}$ is minimal initial w.r.t. $\mathcal{D}(t_{0})$, $(ii)$ ${\boldsymbol{t}}_{i}$ is the minimal for $t_{i}$ w.r.t. $\mathcal{D}(t_{i})$ and $(\boldsymbol{tr}^{i-1}_{\sigma})_{\sigma\in\Sigma_{\Pi}}$.

Note that each type ${\boldsymbol{t}}_{0}$ in the lemma above is uniquely determined by $\mathcal{D}$ and so is the trace $(\boldsymbol{tr}^{0}_{\sigma})_{\sigma\in\Sigma_{\Pi}}$. Then type ${\boldsymbol{t}}_{1}$ is uniquely determined by $(\boldsymbol{tr}^{0}_{\sigma})_{\sigma\in\Sigma_{\Pi}}$ and $\mathcal{D}$ and so is $(\boldsymbol{tr}^{1}_{\sigma})_{\sigma\in\Sigma_{\Pi}}$, etc. Therefore, we can replace in $\Phi_{\Pi}$ the formula $\xi(t,\boldsymbol{x},t^{\prime},\boldsymbol{x}^{\prime})$ by $\xi^{\prime}(t,\boldsymbol{x},t^{\prime},\boldsymbol{x}^{\prime})$ such that for given values of $t$ and $\boldsymbol{x}$, there are unique values of $t^{\prime}$ and $\boldsymbol{x}^{\prime}$ for which $\xi^{\prime}(t,\boldsymbol{x},t^{\prime},\boldsymbol{x}^{\prime})$ holds. ∎

7 Conclusion

In this paper, we made a first step towards understanding the data complexity of answering queries mediated by ontologies with MTL operators and their rewritability into standard database query languages. By imposing natural restrictions on the ranges $\varrho$ constraining the operators ϱ and $\boxminus_{\varrho}$, and by distinguishing between arbitrary, Horn and core ontologies, we identified classes of MTL-OMQs that are rewritable to FO$(<)$, FO$(<,+)$, FO(RPR), FO(DTC), FO(TC), and datalog(FO). Unrestricted MTL-OMQs were shown to be coNP-hard. The rewritability results look encouraging, though much remains to be done to make our rewritings practical, especially in the presence of more expressive atemporal (description logic or datalog) ontologies.

We can extend our language with constrained operators since $\mathcal{S}_{\varrho}$. In this case, hornMTL remains P-complete (but coreMTL becomes P-hard) and Theorem 13 holds, too. We believe that our hornMTL can also be extended with $\boxminus_{\varrho}$ in the rule heads (cf. [14]): Theorems 3 $(ii)$ and  13 $(i)$ also hold in this case, but so far we have not managed to prove Theorem 13 $(ii)$ for such rules. Extending MTL with future-time operators is also interesting, in which case Theorems 3 and 4 remain to hold. Finally, we are looking into MTL-OMQs under the continuous (state-based) semantics, where the techniques developed above do not apply directly.

Acknowledgements This work was supported by EPSRC UK grant EP/S032282, NCN Poland grant 2016/23/N/HS1/ 02168, and the Foundation for Polish Science (FNP). We would like to thank Stanislav Kikot for his help with the proof of Theorem 5.

Appendix A $\mathsf{dist}_{=r}(x,y)$ and Related Formulas

We show that for every $r\in\mathbb{Q}^{\geq 0}_{2}$ we can define an FO-formula $\mathsf{dist}_{=r}(x,y)$ that holds in $\mathcal{D}$ iff $x,y\in\varTheta$ and $\bar{x}-\bar{y}=r$. Let $r\in\mathbb{Q}^{\geq 0}_{2}$ and $h,k\in\mathbb{N}$ be such that $r=h/2^{k}$. Then, we define:

[TABLE]

where $\mathsf{bit}_{\it in}^{+h/2^{k}}(y,j,v)$ states that $v$ is the $j$-th bit of the integer part of $\bar{y}+h/2^{k}$, and $\mathsf{bit}_{\it fr}^{+h/2^{k}}(y,j,v)$ states that $v$ is the $j$-th bit of the fractional part of $\bar{y}+h/2^{k}$. We define $\mathsf{bit}_{\it in}^{+h/2^{k}}(y,j,v)$ and $\mathsf{bit}_{\it fr}^{+h/2^{k}}(y,j,v)$ inductively by means of the following FO($<$)-formulas, where $\ell$ is the last (maximal) element of the domain $\Delta$ of $\mathcal{D}$, $d\in\mathbb{Q}^{\geq 0}_{2}$, and $u=\ell-k$ (which can can be easily defined using $<$):

[TABLE]

[TABLE]

The formulas $\mathsf{dist}_{<r}(x,y)$ for $r\in Q_{2}^{\geq 0}\cup\{\infty\}$ and $\mathsf{dist}_{>r}(x,y)$ are defined by modifications of $\mathsf{dist}_{=r}(x,y)$. Using these, we can further define FO-formulas $\mathsf{in}_{\varrho}(x,y)$ and $\mathsf{int}_{\varrho}(t,u,s)$.

Appendix B Divisibility and $\mathsf{div}_{d}$

We will show how to define an FO(RPR)-formula $\mathsf{div}_{d}(x,y)$ that is true in $\mathcal{D}$ iff $u,v\in\varTheta$ and $\bar{x}-\bar{y}=d$.

Let $\mathcal{D}$ be an arbitrary FO-structure. First, we will define FO-formulas $b_{fr}(x,y,i)$, $b_{in}(x,y,i)$, $\mathsf{dif}_{fr}(i,x,y)$, and $\mathsf{dif}_{in}(i,x,y)$ such that:

• –

$b_{fr}(x,y,i)$ is true in $\mathcal{D}$ iff when using the column method to subtract $\bar{y}$ from $\bar{x}$, the $i$-th bit from the fractional part of $\bar{x}$ is borrowed;

• –

$b_{in}(x,y,i)$ is true in $\mathcal{D}$ iff when using the column method to subtract $\bar{y}$ from $\bar{x}$, the $i$-th bit from the integral part of $\bar{x}$ is borrowed;

• –

$\mathsf{dif}_{fr}(i,x,y)$ is true in $\mathcal{D}$ iff the $i$-th bit of the fractional part of $\bar{x}-\bar{y}$ is $1$;

• –

$\mathsf{dif}_{in}(i,x,y)$ is true in $\mathcal{D}$ iff the $i$-th bit of the integral part of $\bar{x}-\bar{y}$ is $1$.

Let the binary representations of fractional parts of $\bar{x}$ and $\bar{y}$, be $x_{\ell}\dots x_{0}$ and $y_{\ell}\dots y_{0}$, respectively. Let $b_{i}\in\{0,1\}$ indicate whether a bit is borrowed from $x_{i}$ when subtracting $y$ from $x$ using the column method. Clearly, $b_{0}=0$ and the value of $b_{i}$ for $i\neq 0$ can be determined as follows:

[TABLE]

Using the equivalence above, we define $b_{fr}(x,y,i)$ as follows:

[TABLE]

In what follows we will denote the binary representation of the fractional part of $x-y$ as $z_{\ell}\dots z_{0}$, which can be defined as follows (for [math] and $1$ treated as truth-values):

[TABLE]

Thus, we can define $\mathsf{dif}_{fr}(i,x,y)$ as:

[TABLE]

In a similar way we can define the formulas $b_{in}(x,y,i)$ and $\mathsf{dif}_{in}(i,x,y)$ which are about the integral parts of $x$ and $y$. In particular, we define $b_{in}(x,y,i)$ as:

[TABLE]

where $\ell$ is (a constant for) the last element of $\varDelta$. The formula $\mathsf{dif}_{in}(i,x,y)$ is defined analogously to $\mathsf{dif}_{fr}(i,x,y)$.

Next, we will make use of the integer divisibility automaton $\mathcal{A}_{k}=(Q,\{0,1\},q_{0},q_{a},\delta)$, which is an NFA taking as an input an inverted binary representation $z_{0}z_{1}\dots z_{n}$ of an integer number $z$ and reaching the accepting state $q_{a}$ iff $z$ is divisible by $k$. It is known that for any integer $k$ we can construct such an automaton. Recall that $z_{\ell}\dots z_{0}$ is the fractional part of $\bar{x}-\bar{y}$, i.e., $z_{i}=1$ iff $\mathsf{dif}_{fr}(i,x,y)$ is true in $\mathcal{D}$. Analogously, we denote the integral part of $\bar{x}-\bar{y}$ by $w_{\ell}w_{\ell-1}\dots w_{0}$, i.e., $w_{i}=1$ iff $\mathsf{dif}_{in}(i,x,y)$ is true in $\mathcal{D}$.

Next, we claim that for any $n\in\mathbb{N}$, $k\in\mathbb{Z}$, and a state $q$ of the divisibility automaton $\mathcal{A}_{k}$, we can construct an FO-formula $reach_{q,\mathcal{A}_{k}}^{n}(x,y)$ which is true in $\mathcal{D}$ iff $x,y\in\varTheta$ and either:

• –

$\ell\geq n$, $z_{i}=0$ for $i<\ell-n$, and $\mathcal{A}_{k}$ has a run from $q_{0}$ to $q$ on $z_{\ell-n}\dots z_{\ell-1}z_{\ell}$; or

• –

$\ell<n$ and $\mathcal{A}_{k}$ has a run from $q_{0}$ to $q$ on $\underbrace{0\dots 0}_{n-\ell}z_{0}\dots z_{\ell}.$

To construct $reach_{q,\mathcal{A}_{k}}^{n}$ one needs to consider paths of length bounded by $n$ in $\mathcal{A}_{k}$, whose number is finite, and therefore the formula is constructible in FO (we leave details to the reader).

Let $f_{d}$ be the number of significant bits in the fractional part of the binary representation of $d$ (e.g., $f_{d}=3$ for $d=10001.101$). Then, we can prove the following result:

Lemma 16**.**

Let $d\in\mathbb{Q}_{2}^{\geq 0}$, $D=d2^{f_{d}}$, and let $\mathcal{A}_{D}=(Q,\{0,1\},q_{0},q_{a},\delta)$ be the divisibility automaton for $D$. Then, for any data instance $\mathcal{D}$ and $x,y\in\Theta$, the value of $\bar{x}-\bar{y}$ is divisible by $d$ iff there exists $q\in Q$ such that $reach_{q,\mathcal{A}_{D}}^{f_{d}}(x,y)$ is true in $\mathcal{D}$, and $\mathcal{A}_{D}$ has a run from $q$ to $q_{a}$ on $w_{0}w_{1}\dots w_{\ell}$, where $w_{l},\dots w_{1}w_{0}$ is the binary representation of the integral part of $\bar{x}-\bar{y}$.

Now, let $d$, $D$, and $\mathcal{A}_{D}=(Q,\{0,1\},q_{0},q_{a},\delta)$ be as stated in the lemma. For every $q\in Q$ we will introduce an FO(RPR)-formula expressing that $R_{q}(i,x,y)$ is true in $\mathcal{D}$ iff either:

• –

$i=0$ and there exists $q^{\prime}\in Q$ such that $reach_{q^{\prime},\mathcal{A}_{D}}^{f_{d}}(x,y)$ and $q\in\delta(q^{\prime},w_{0})$; or

• –

$i>0$ and there exists $q^{\prime}\in Q$ such that $R_{q^{\prime}}(i-1,x,y)$ is true in $\mathcal{D}$ and $q\in\delta(q^{\prime},w_{i})$.

This formula, denoted by $\alpha_{q}$, is as follows:

[TABLE]

Finally, we define $\mathsf{div}_{d}(x,y)$ by means of the following FO(RPR)-formula, where $q_{0},\ldots,q_{n}$ are all states in $Q$:

[TABLE]

Intuitively, the formula uses simultaneous recursion to check whether the accepting state is reached on the input $w_{0}w_{1}\dots w_{\ell}$.