# Analysing Temporal Reasoning in Description Logics
Using Formal Grammars

Camille Bourgaux, Anton Gnatenko, Michaël Thomazo

<figure><img src="image_1.png" /></figure>

## To cite this version:

Camille Bourgaux, Anton Gnatenko, Michaël Thomazo. Analysing Temporal Reasoning in Description Logics Using Formal Grammars. ECAI'25 – 28th European Conference on Artificial Intelligence, Oct 2025, Bologna, Italy. hal-05273645

HAL Id: hal-05273645

https://inria.hal.science/hal-05273645v1

Submitted on 23 Sep 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Analysing Temporal Reasoning in Description Logics
Using Formal Grammars

Camille Bourgauxª, Anton Gnatenkoᵇ,\* and Michaël Thomazoª

ªDI ENS, ENS, CNRS, PSL University & Inria, Paris, France

ᵇFree University of Bozen-Bolzano, Italy

**Abstract.** We establish a correspondence between (fragments of) $TEL^○$, a temporal extension of the $EL$ description logic with the LTL operator $○^k$, and some specific kinds of formal grammars, in particular, conjunctive grammars (context-free grammars equipped with the operation of intersection). This connection implies that $TEL^○$ does not possess the property of ultimate periodicity of models, and further leads to undecidability of query answering in $TEL^○$, closing a question left open since the introduction of $TEL^○$. Moreover, it also allows to establish decidability of query answering for some new interesting fragments of $TEL^○$, and to reuse for this purpose existing tools and algorithms for conjunctive grammars.

## 1 Introduction

Ontology-mediated query answering (OMQA) aims at improving data access by enriching data with an ontology that expresses domain knowledge [40, 31, 14]. In this setting, an ontology is a set of logical formulas, typically expressed in a given description logic (DL) [9] or via extensions of Datalog [1, 13, 19]. It provides a formalized vocabulary that allows a user to formulate queries in familiar terms, and to obtain more complete answers to queries, as answers are based not only on facts explicitly stored in the data (or ABox, in DL parlance) but also on facts that can be deduced through logical reasoning using the ontology (TBox). In the large literature on OMQA, special attention has been devoted to the so-called lightweight description logics, such as the DL-Lite family [3] or the $EL$ family [10, 11], which allow for tractable reasoning and underpin the OWL 2 QL and OWL 2 EL profiles of the Semantic Web standard ontology language [32]. In particular, many large real-world ontologies, including the biomedical ontology SNOMED CT, use languages from the $EL$ family.

As many real-world applications require to query temporal data, various extensions of the OMQA framework have been proposed to integrate temporal modelling [6]. In this paper, we consider (fragments of) $TEL$, a temporal extension of the DL language $EL$ introduced by Gutiérrez-Basulto et al. [26]. In $TEL$, the ABox facts are associated with timestamps, and the TBox concept inclusions may feature some operators from linear temporal logic (LTL): $○$ (next), $○^−$ (previous), $◇$ (eventually) and $◇^−$ (eventually in the past). For instance, the concept inclusion $Prof ⊑ ○Prof$ intuitively means that at any moment, someone that is a professor is also a professor at the next instant. Moreover, $TEL$ allows the user to specify that some roles (binary predicates) are rigid, i.e., that the relations they model do not change over time.

<figure><img src="image_3.png" /><figcaption>**Figure 1.** Representation of some inferences for Example 1. Dashed lines represent the temporal evolution of a given element, while dotted lines represent a relation whose existence is known due to role rigidity.</figcaption></figure>

**Example 1.** Imagine that Alice is a professor in 2025, denoted Prof(Alice, 2025). Professorship is permanent and requires advising students, who in three years become doctors. Being an advisor of a doctor makes one proud, and proud professors are happy. This knowledge is formalized as follows (using a rigid role advisorOf):

$$ 
\begin{array}{l}
\text{Prof} \sqsubseteq \circ\text{Prof} \quad \text{Prof} \sqcap \text{Proud} \quad \sqsubseteq \text{Happy} \quad \text{Student} \sqsubseteq \circ^3\text{Dr} \\
\text{Prof} \sqsubseteq \exists\text{advisorOf.Student} \quad \exists\text{advisorOf.Dr} \sqsubseteq \text{Proud}
\end{array}
$$

Figure 1 provides a graphical representation of some information about Alice that can be inferred from Prof(Alice, 2025) and the above $TEL$ TBox. In particular, Alice is happy at year 2028.

Integrating temporal reasoning in OMQA gave rise to a flourishing literature, with a large body of work on the theoretical side as well as some implementations [30, 44, 42], in a wide variety of settings. For example, an alternative way to model fact temporal validity is to use time intervals instead of timestamps [25, 18, 12]. On the ontology-mediated query side, it is also possible to use a standard, atemporal TBox and temporal queries, built from conjunctive queries and LTL operators [15, 16]. Finally, $TEL$ stems from a line of research which studies combinations of various DL languages and LTL operators [2, 4, 7]. For a more in-depth discussion of temporal reasoning within OMQA, we refer the reader to the survey by Artale et al. [6].

Despite both LTL and $EL$ being decidable, Gutiérrez-Basulto et al. [26] showed that their combination in $TEL$ quickly leads to undecidability. However, they exhibited fragments of $TEL$ for which atomic query answering is decidable. Most of such fragments restrict the expressiveness of the temporal modelling, by only allowing operators $○$ and $○^−$, giving rise to the $TEL^○$ language. Gutiérrez-Basulto et al. [26] left open the question of whether that restriction by itself is enough to regain decidability and proposed additional syntactic constraints, based on some form of acyclicity (either on the description

<footnote>* Email: anton.gnatenko@student.unibz.it</footnote>
logics side, or on the temporal side). All these constraints enforce a
crucial property: the existence of models that are ultimately periodic.
In a nutshell, a model is ultimately periodic if the evolution over time
of any given element is, after some initial segment, periodic.

Our main contribution is to link temporal reasoning with TEL ◦ -TBoxes to the study of associated formal languages, which allows us to close the open question of Gutiérrez-Basulto et al. [26] and ob-
tain additional results. We first consider the case of TEL ◦ $_{future}$, where
concept inclusions only allow to derive novel information about the
future (or present) and not the past. For this fragment, we show in
Section 3 that the task of deciding whether a concept inclusion of
the form A ⊑ ◦ $^{n}$B is entailed by a TBox can be reduced to deciding
whether n belongs to the Parikh image [39] of a unary conjunctive
language, and vice-versa. Such languages are defined by conjunc-
tive grammars, introduced by Okhotin [33] as a generalization of
context-free grammars which allows for a conjunction operation in
rules. We then turn our attention to TEL ◦ $_{lin}$, a temporal extension of
linear EL [23], and obtain in Section 4 a similar reduction from rea-
soning in TEL ◦ lin to deciding whether the Parikh image of a context-
free grammar over a binary alphabet fulfils some property. In Sec-
tion 5, we exploit the previous correspondences to obtain results for
TEL ◦ and fragments thereof. First, we close negatively the ques-
tion of whether all TEL ◦ -TBoxes enjoy ultimate periodicity, and
complete the complexity picture of TEL given by Gutiérrez-Basulto
et al. [26]: atomic query answering in TEL ◦ is undecidable. Second,
we provide results for the new fragments TEL ◦ future and TEL ◦ $_{lin}$we
introduce. As for TEL ◦ $_{future}$, we prove that atomic query answering
is solvable in polynomial time (in combined and data complexity),
but becomes undecidable if TEL ◦ future is extended with rigid concept
names or the universal concept $^{⊤}$. Regarding TEL ◦ $_{lin}$, we prove that
TEL ◦ $_{lin}$-TBoxes enjoy ultimate periodicity, and derive complexity re-
sults for atomic query answering. Detailed proofs are provided in
Bourgaux et al. [17].

## 2 Preliminaries

In this section, we introduce TEL ◦ and conjunctive grammars.

2.1 The TEL ◦ temporal description logic

We recall the syntax and semantics of TEL ◦ from Gutiérrez-Basulto
et al. [26]. Let N<sub>i</sub>, N<sub>C</sub>, N<sub>R</sub> be disjoint countably infinite sets of indi-
vidual names, concept names and role names, respectively, with N<sub>R</sub>
partitioned into rigid role names N<sub>R</sub><sup>rig</sup> and local role names N<sub>R</sub><sup>loc</sup>.

**Syntax** A fact is an expression of the form $A(a, n)$ or $r(a, b, n)$, where $a, b \in N_i$, $A \in N_c$, $r \in N_R$, and $n \in \mathbb{Z}$. A (temporal) ABox (data instance) $\mathcal{A}$ is a finite set of facts. A TEL $^\circ$-TBox (ontology) $\mathcal{T}$ is a finite set of concept inclusions of the form

$$
A \sqsubseteq \circ^n B \quad A \sqcap A' \sqsubseteq B \quad \exists r. A \sqsubseteq B \quad A \sqsubseteq \exists r. B \quad (1)
$$

where $A, A', B \in \mathbb{N}_C, r \in \mathbb{N}_R$, and $n \in \mathbb{Z}$. When $n=0, n=1$, or $n=-1$, we simply write $A \sqsubseteq B, A \sqsubseteq \circ B$, and $A \sqsubseteq \circ^{-} B$, respectively. We will further consider two fragments of TEL $^\circ$: the future fragment, TEL $^\circ_{future}$, is obtained by setting $n \ge 0$, and the linear fragment, TEL $^\circ_{lin}$, disallows concept inclusions of the form $A \sqcap A' \sqsubseteq B$. A (temporal) knowledge base (KB) is a pair $(\mathcal{T}, \mathcal{A})$. Note that we consider TEL $^\circ$-TBoxes in normal form [26]. We denote by $\mathbb{N}_C(\mathcal{T})$, $\mathbb{N}_R(\mathcal{T})$, $\mathbb{N}_R^{\text{rig}}(\mathcal{T})$, and $\mathbb{N}_R^{\text{loc}}(\mathcal{T})$, respectively, the sets of concept names, role names, and rigid and local role names appearing in $\mathcal{T}$. The size $|\mathcal{T}|$ of $\mathcal{T}$ (resp. $|\mathcal{A}|$ of $\mathcal{A}$) is the number of symbols needed to write it down, with integers encoded in unary.

**Semantics** An interpretation $\mathfrak{J}$ is a structure $(\Delta^3, (Z_i)_{i \in \mathbb{Z}})$ where each $I_i = (\Delta^3, \mathcal{I}_i)$ is a classical DL interpretation with domain $\Delta^3$: for every $a \in N_i$, $a^{\mathcal{I}_i} = a$ (standard name assumption, assuming that $N_i \subseteq \Delta^3$), for every $A \in \mathbb{N}_C$, $A^{\mathcal{I}_i} \subseteq \Delta^3$, and for every $r \in \mathbb{N}_R$, $r^{\mathcal{I}_i} \subseteq \Delta^3 \times \Delta^3$. Moreover, for every $r \in \mathbb{N}_R^{\text{rig}}$, $r^{\mathcal{I}_i} = r^{\mathbb{I}_0}$ for every $i \in \mathbb{Z}$. The interpretation function $\mathcal{I}_i$ is often written as $\mathfrak{J}^{\mathcal{I}_i}$ and is extended to interpret complex concepts as expected:

$$
\begin{align*}
(\circ^n A)^{\mathfrak{J}, i} &= A^{\mathfrak{J}, i+n} & (A \sqcap B)^{\mathfrak{J}, i} &= A^{\mathfrak{J}, i} \sqcap B^{\mathfrak{J}, i} \\
(\exists r. A)^{\mathfrak{J}, i} &= \{d \mid \exists e \in A^{\mathfrak{J}, i}, (d, e) \in r^{\mathfrak{J}, i}\} & &
\end{align*}
$$

The interpretation $\mathfrak{J}$ is a *model* of a fact $A(a, n)$ (resp. $r(a, b, n)$) if $a \in A^{\mathfrak{J},n}$ (resp. $(a, b) \in r^{\mathfrak{J},n}$), and of a concept inclusion $C \subseteq D$ if $C^{\mathfrak{J},i} \subseteq D^{\mathfrak{J},i}$ for every $i \in \mathbb{Z}$. It is a model of an ABox $\mathcal{A}$ (resp. a TBox $\mathcal{T}$) if it is a model of all facts in $\mathcal{A}$ (resp. all concept inclusions in $\mathcal{T}$), and of a KB $(\mathcal{T}, \mathcal{A})$ if it is a model of $\mathcal{T}$ and $\mathcal{A}$. We write $\mathfrak{J} \models \alpha$ to denote that $\mathfrak{J}$ is a model of $\alpha$. A TBox $\mathcal{T}$ *entails* a concept inclusion $\alpha$, written $\mathcal{T} \models \alpha$, if $\mathfrak{J} \models \mathcal{T}$ implies $\mathfrak{J} \models \alpha$, and a KB $(\mathcal{T}, \mathcal{A})$ entails a fact $\alpha$, $(\mathcal{T}, \mathcal{A}) \models \alpha$, if $\mathfrak{J} \models (\mathcal{T}, \mathcal{A})$ implies $\mathfrak{J} \models \alpha$. Note that *rigid concept names* can be defined in a similar fashion as rigid role names, and can be simulated with $A \sqsubseteq \circ A$ and $A \sqsubseteq \circ^{-1} A$ in TEL $^\circ$ and TEL $^\circ_{lin}$ (but not in TEL $^\circ_{future}$).

**Derivations** We will use the following derivation system for TEL $^\circ$. Let $N_N$ be an infinite countable set of named nulls (constants) disjoint from $N_i$. Given a TEL $^\circ$-TBox $\mathcal{T}$ and ABox $\mathcal{A}$, we write $(\mathcal{T}, \mathcal{A}) \vdash A(a, n)$ if there exists a derivation of $A(a, n)$ from $\mathcal{A} \cup \mathcal{T}$ using rules of the form (2)-(6). Formally, such a derivation is a sequence $(F_0, \dots, F_m)$ with $F_0 = \mathcal{A} \cup \mathcal{T}$, $A(a, n) \in \mathcal{F}_m$, and for $1 \le i \le m$, $F_i$ is obtained from $F_{i-1}$ by choosing a rule such that all formulas in the left-hand side are in $F_{i-1}$ and adding the formulas on the right-hand side.

$$
r(a, b, n), r \in \mathbb{N}_R^{\text{rig}}, k \in \mathbb{Z} \quad \vdash \quad r(a, b, k) \quad (2)
$$

$$
A(a, n), A \sqsubseteq \circ^k B \quad \vdash \quad B(a, n + k) \quad (3)
$$

$$
A(a, n), A'(a, n), A \sqcap A' \sqsubseteq B \quad \vdash \quad B(a, n) \quad (4)
$$

$$
r(a, b, n), A(b, n), \exists r. A \sqsubseteq B \quad \vdash \quad B(a, n) \quad (5)
$$

$$
A(a, n), A \sqsubseteq \exists r. B \quad \vdash \quad r(a, b, n), B(b, n) \quad (6)
$$

where in (6), $b$ is a fresh element from $N_N$. The next proposition is
easily shown using the canonical model of a TEL $^\circ$ KB, defined in
a similar way as in the temporal DL-Lite case [4, 5].

**Proposition 2.** For every TEL $^\circ$-TBox $\mathcal{T}$, ABox $\mathcal{A}$, $A, B \in \mathbb{N}_C$, $a \in N_i$, and $n, k \in \mathbb{Z}$:

• $(\mathcal{T}, \mathcal{A}) \models A(a, n) \text{ iff } (\mathcal{T}, \mathcal{A}) \vdash A(a, n)$, and

• $\mathcal{T} \models A \sqsubseteq \circ^n B \text{ iff } (\mathcal{T}, \{A(a, k)\}) \vdash B(a, k + n)$.

**Example 3** (Example 1 cont’d). Below is a derivation of Happy(Alice, 2028), from the TBox $\mathcal{T}$ that contains the concept inclusions from Example 1 and $\mathcal{A} = \{\text{Prof}(\text{Alice}, 2025)\}$, with advisorOf $\in \mathbb{N}_R^{\text{rig}}$. The form of the rule applied is given as a subscript to $\vdash$ and the left-hand side is left implicit.

$\vdash^{(3)} \text{Prof}(\text{Alice}, 2026)$

$\vdash^{(3)} \text{Prof}(\text{Alice}, 2027)$

$\vdash^{(3)} \text{Prof}(\text{Alice}, 2028)$

$\vdash^{(6)} \text{advisorOf}(\text{Alice}, b, 2025), \text{Student}(b, 2025)$

$\vdash^{(3)} \text{Dr}(b, 2028)$

$\vdash^{(2)} \text{advisorOf}(\text{Alice}, b, 2028)$

$\vdash^{(5)} \text{Proud}(\text{Alice}, 2028)$

$\vdash^{(4)} \text{Happy}(\text{Alice}, 2028)$
By Proposition 2, it holds that $(\mathcal{T}, \mathcal{A}) \models \text{Happy}(\text{Alice}, 2028)$ and $\mathcal{T} \models \text{Prof} \sqsubseteq \textcircled{3}\text{Happy}$.

**Query answering and ultimately periodic TBoxes** The temporal atomic query answering (TAQA) problem is that of deciding, given a temporal KB $(\mathcal{T}, \mathcal{A})$ and a fact $A(a, n)$, whether $(\mathcal{T}, \mathcal{A}) \models A(a, n)$. We consider combined complexity, where the size of the input is $|\mathcal{T}| + |\mathcal{A}| + |A(a, n)|$, and data complexity, where $\mathcal{T}$ is fixed. Gutiérrez-Basulto et al. [26] show that decidability of TAQA is ensured by a property of the TBox, namely, ultimate periodicity, which they define using the canonical quasimodel of the TBox. Since we do not use the notion of quasimodel in this work, we rephrase this property using the sets of numbers $\{n \in \mathbb{Z} \mid \mathcal{T} \models A \sqsubseteq \textcircled{n} B\}$. A set $\mathcal{L} \subseteq \mathbb{Z}^n$ is linear if $\mathcal{L} = \{\vec{b} + k_1\vec{p}_1 + \dots + k_l\vec{p}_l \mid k_1, \dots, k_l \in \mathbb{N}\}$ for some $\vec{b} \in \mathbb{Z}^n$, called offset, and $\vec{p}_1, \dots, \vec{p}_l \in \mathbb{Z}^n$, called periods. A semilinear set is a union of finitely many linear sets. A TBox $\mathcal{T}$ is ultimately periodic if for every $A, B \in \mathbb{N}_c(\mathcal{T})$, the set $\{n \in \mathbb{Z} \mid \mathcal{T} \models A \sqsubseteq \textcircled{n} B\}$ is semilinear.

**Theorem 4** (Gutiérrez-Basulto et al. [26]). TAQA with ultimately periodic $\mathcal{T}\mathcal{E}\mathcal{L}\textcircled{-TBoxes is in PSPACE for data complexity.}$

## 2.2 Conjunctive grammars

To analyse ultimate periodicity of general $\mathcal{T}\mathcal{E}\mathcal{L}\textcircled{-TBoxes, we employ conjunctive grammars over a unary alphabet.

**Syntax** A conjunctive grammar, as introduced by Okhotin [33, 37], is a quadruple $G = (N, \Sigma, S, R)$, where $N$ and $\Sigma$ are disjoint alphabets of nonterminals and terminals, respectively, $S \in N$ is a distinguished start symbol, and $R$ is a finite set of rules of the form:

$$ \mathcal{N} \rightarrow \alpha_1 \& \dots \& \alpha_n \quad (7) $$

with $\mathcal{N} \in N$, $n \ge 1$, and $\alpha_i \in (N \cup \Sigma^*)$. Each $\alpha_i$ is called a conjunct. If a grammar has a unique conjunct in every rule, then it is a context-free grammar, and if further this conjunct has form either $\varepsilon$ or $c\mathcal{N}'$, for $c \in \Sigma$, $\mathcal{N}' \in N$, then it is a regular grammar [21, 27]. When the start symbol is not specified, we write $G = (N, \Sigma, R)$. Several rules with the same left-hand side $\mathcal{N}$ can also be written as a single rule (with $|$ used to separate the right-hand sides):

$$ \mathcal{N} \rightarrow \alpha_1^1 \& \dots \& \alpha_{n_1}^1 \mid \dots \mid \alpha_1^m \& \dots \& \alpha_{n_m}^m \quad (8) $$

The size $|G|$ of $G$ is the number of symbols needed to write it down.

**Semantics** Intuitively, the semantics of conjunctive grammars extends that of context-free grammars with intersection: given rule (7), apply “in parallel” context-free rules $\mathcal{N} \rightarrow \alpha_i$ and take the intersection of the generated languages. Formally, derivations for grammars are defined in a similar way as derivations for knowledge bases. Given $G$, let $\{X(w) \mid X \in N \cup \Sigma, w \in \Sigma^*\}$ be a set of propositions, each meaning “a word $w$ has a property $X$”. The axioms are

$$ c(c) \quad (\text{for every } c \in \Sigma) \quad (8) $$

and the derivation rules are obtained as follows. For every rule of form (7) in $R$, each $\alpha_i$ is of the form $X_1^i \dots X_{k_i}^i$ with $k_i \ge 0$ and $X_j^i \in N \cup \Sigma$. For all words $u_j^i \in \Sigma^*$ with $1 \le i \le n$ and $1 \le j \le k_i$ such that $u_1^1 \dots u_{k_1}^1 = \dots = u_1^n \dots u_{k_n}^n = w$, we have the rule:

$$ X_1^1(u_1^1), \dots, X_{k_1}^1(u_{k_1}^1), \dots, X_1^n(u_1^n), \dots, X_{k_n}^n(u_{k_n}^n) \vdash \mathcal{N}(w) \quad (9) $$

Then we write $G \vdash X(w)$ whenever $X(w)$ can be derived from the axioms using the rules. The language of $X \in N \cup \Sigma$ is $L_G(X) =$

$\{w \in \Sigma^* \mid G \vdash X(w)\}$, and the language of the grammar $G$ is $L(G) = L_G(S)$. We refer to the survey by Okhotin [37] for discussion of alternative equivalent definitions of the semantics.

**Example 5** (Okhotin [37]). The language $\{a^n b^n c^n \mid n \in \mathbb{N}\}$ is generated by $G = (\{S, A, B, C, D\}, \{a, b, c\}, S, R)$ where $R$ contains:

$$ \begin{array}{rcl} S & \rightarrow & AB \ \& \ DC \\ A & \rightarrow & aA \mid \varepsilon & B \rightarrow & bBc \mid \varepsilon \\ C & \rightarrow & cC \mid \varepsilon & D \rightarrow & aDb \mid \varepsilon \end{array} $$

We call a language $L \subseteq \Sigma^*$ conjunctive, (context-free, regular) if $L = L(G)$ for a conjunctive (respectively, context-free or regular) grammar $G$. A language (or a grammar) is called unary when the underlying alphabet contains just one symbol, i.e. $\Sigma = \{c\}$. The membership problem for conjunctive grammars is P-complete.

**Theorem 6** (Okhotin [35, 36]). Checking whether $w \in L(G)$, for a given conjunctive grammar $G$ and $w \in \Sigma^*$, is P-complete.

**Parikh images and expressiveness** Given an alphabet $\Sigma = \{c_1, \dots, c_n\}$ enumerated in a fixed order, let $\#c_i(w)$ denote the number of occurrences of $c_i$ in $w \in \Sigma^*$. The Parikh image $p(w)$ of a word $w$ is a vector $\vec{u} \in \mathbb{Z}^n$ such that $u_i = \#c_i(w)$, for all $1 \le i \le n$. The Parikh image $p(L)$ of a language $L$ is the set $\{p(w) \mid w \in L\}$. It is easy to see that when $L$ is regular, $p(L)$ is semilinear. A deeper result is the following.

**Theorem 7** (Parikh [39]). If $L$ is context-free, then $p(L)$ is semilinear. Moreover, for any semilinear $S \subseteq \mathbb{N}^n$ there exists a regular language $L'$ such that $S = p(L')$.

A unary language $L$ can be seen as a set of numbers given in unary that coincides with its Parikh image: $c^n \in L$ if and only if $n \in p(L)$. Theorem 7 implies that a unary language is regular iff its Parikh image is semilinear, and thus unary context-free languages are regular. However, unary conjunctive languages may not be regular.

**Example 8** (Jeż [28]). For the following grammar $G$, the language $L_G(\mathcal{N}_1) = \{c^{4^n} \mid n \in \mathbb{N}\}$ is not regular:

$$ \begin{array}{rcl} \mathcal{N}_1 & \rightarrow & \mathcal{N}_1 \mathcal{N}_3 \ \& \ \mathcal{N}_2 \mathcal{N}_2 \mid c \\ \mathcal{N}_2 & \rightarrow & \mathcal{N}_1 \mathcal{N}_1 \ \& \ \mathcal{N}_2 \mathcal{N}_6 \mid cc \\ \mathcal{N}_3 & \rightarrow & \mathcal{N}_1 \mathcal{N}_2 \ \& \ \mathcal{N}_6 \mathcal{N}_6 \mid ccc \\ \mathcal{N}_6 & \rightarrow & \mathcal{N}_1 \mathcal{N}_2 \ \& \ \mathcal{N}_3 \mathcal{N}_3 \end{array} $$

To understand the rules above, associate every word $c^n$ with the number $n$, and each $\mathcal{N}_i$ with the set $\{i \cdot 4^n \mid n \in \mathbb{N}\}$. Since $c^n c^k = c^{n+k}$, concatenation of words corresponds to the summation of the respective numbers. The expression $\mathcal{N}_1 \mathcal{N}_3 \ \& \ \mathcal{N}_2 \mathcal{N}_2$ encodes the equation $4^m+3 \cdot 4^k = 2 \cdot 4^l+2 \cdot 4^s$, which holds if and only if $m = k = l = s$, when both sides become equal to $4^{k+1}$. This newly obtained number is assigned, by the first rule, to the set of $\mathcal{N}_1$.

Building on the idea behind Example 8, Jeż and Okhotin [29] devised grammars encoding Turing machine computations, leading to:

**Theorem 9** (Jeż and Okhotin [29]). Given a unary conjunctive grammar $G$, it is undecidable (and co-r.e.-complete) whether $L(G)$ is (i) empty, (ii) finite, or (iii) regular.
### 3 Future $\mathcal{TEL}^{\circ}$ and unary conjunctive grammars

In this section, we prove two theorems that establish our key result: $\{\{n \in \mathbb{N} | T \models A \sqsubseteq \circ^n B\} | T \mathcal{TEL}^{\circ}_{\text{future}}\text{-TBox}, A, B \in \mathcal{N}_C\}$ is the set of Parikh images of unary conjunctive languages. This will allow us to apply Theorems 7 and 9 to analyse ultimate periodicity of $\mathcal{TEL}^{\circ}$-TBoxes.

**Theorem 10** (TBoxes to Grammars). For every $\mathcal{TEL}^{\circ}_{\text{future}}$-TBox $\mathcal{T}$, one can construct in polynomial time a unary conjunctive grammar $G_{\mathcal{T}} = (N, \{c\}, R)$ such that for any $A, B \in \mathcal{N}_C(\mathcal{T})$, there is $\mathcal{N}_{AB} \in N$ such that $c^n \in L_{G_{\mathcal{T}}}(\mathcal{N}_{AB})$ iff $T \models A \sqsubseteq \circ^n B$.

Given a $\mathcal{TEL}^{\circ}_{\text{future}}$-TBox $\mathcal{T}$, we sketch the construction of $G_{\mathcal{T}}$. The first step is to ensure that every role name in $\mathcal{T}$ can be treated as rigid. For each $C \in \mathcal{N}_C(\mathcal{T})$, $r \in \mathcal{N}^{\text{rc}}_R(\mathcal{T})$, introduce a pair of fresh concept names $C_r, C'_r$, and let $T_{\text{rig}}$ be obtained from $\mathcal{T}$ as follows:

1. for each $r \in \mathcal{N}^{\text{rc}}_R(\mathcal{T})$, substitute every $A \sqsubseteq \exists r.B \in \mathcal{T}$ with

$$A \sqsubseteq \exists r.B_r \qquad B_r \sqsubseteq B \qquad (10)$$

2. for each $C_r$, substitute every $\exists r.A \sqsubseteq B \in \mathcal{T}$ with

$$A \sqcap C_r \sqsubseteq A'_r \qquad \exists r.A'_r \sqsubseteq B \qquad (11)$$

3. substitute each $r \in \mathcal{N}^{\text{rc}}_R(\mathcal{T})$ with a fresh $r' \in \mathcal{N}^{\text{rig}}_R$.

Intuitively, in a derivation using $T_{\text{rig}}$, a fact $B_r(b, n)$ created from some $A(a, n)$ and $A \sqsubseteq \exists r.B_r$ guards the "locality" of $r(a, b, n)$ at time $n$. Any application of a derivation rule of form (5) using a fact of the form $r(a, b, k)$, and hence any effect of $b$ on $a$, is only possible using some $\exists r.A'_r \sqsubseteq C$ and $A'_r(b, k)$, and thus is limited to $k = n$, since $A'_r(b, k)$ can only be derived using $A \sqcap B_r \sqsubseteq A'_r$ and $B_r(b, n)$. The translation from $\mathcal{T}$ to $T_{\text{rig}}$ is polynomial, and it is not hard to prove the following lemma.

**Lemma 11.** Let $\mathcal{T}$ be a $\mathcal{TEL}^{\circ}$-TBox. For any $A, B \in \mathcal{N}_C(\mathcal{T})$ and $n \in \mathbb{Z}$, $T \models A \sqsubseteq \circ^n B$ if and only if $T_{\text{rig}} \models A \sqsubseteq \circ^n B$.

**Definition 12.** Given a $\mathcal{TEL}^{\circ}_{\text{future}}$-TBox $\mathcal{T}$, $G_{\mathcal{T}} = (N_{\mathcal{T}}, \{c\}, R_{\mathcal{T}})$, where $N_{\mathcal{T}} = \{\mathcal{N}_{AB} | A, B \in \mathcal{N}_C(T_{\text{rig}})\}$ and $R_{\mathcal{T}}$ contains exactly:

$$\mathcal{N}_{AB} \rightarrow \varepsilon, \qquad \text{for } A \sqsubseteq B \in T_{\text{rig}} \text{ or } A = B \qquad (12)$$

$$\mathcal{N}_{AB} \rightarrow c^n, \qquad \text{for } A \sqsubseteq \circ^n B \in T_{\text{rig}}, n > 0 \qquad (13)$$

$$\mathcal{N}_{AB} \rightarrow \mathcal{N}_{AC} \& \mathcal{N}_{AD}, \qquad \text{for } \begin{array}{l} A \in \mathcal{N}_C(T_{\text{rig}}), \\ C \sqcap D \sqsubseteq B \in T_{\text{rig}} \end{array} \qquad (14)$$

$$\mathcal{N}_{AB} \rightarrow \mathcal{N}_{CD}, \qquad \text{for } \left\{ \begin{array}{l} A \sqsubseteq \exists r.C, \\ \exists r.D \sqsubseteq B \end{array} \right\} \sqsubseteq T_{\text{rig}} \qquad (15)$$

$$\mathcal{N}_{AB} \rightarrow \mathcal{N}_{AC} \mathcal{N}_{CB}, \qquad \text{for } A, B, C \in \mathcal{N}_C(T_{\text{rig}}) \qquad (16)$$

Intuitively, for every pair of concept names $A, B \in \mathcal{N}_C(T_{\text{rig}})$, $G_{\mathcal{T}}$ encodes every possible way of deriving $B(a, n)$ from $\{A(a, 0)\} \cup T_{\text{rig}}$: either directly (12, 13), or by obtaining $C(a, n)$ and $D(a, n)$ that together give $B(a, n)$ (14), or by going through a null (15), or through an intermediate point $C(a, k)$, $0 \le k \le n$ (16). One can show that a derivation witnessing $(\mathcal{T}, \{A(a, 0)\}) \vdash B(a, n)$ using rules of the form (2)–(6) corresponds to a derivation for $G_{\mathcal{T}} \vdash \mathcal{N}_{AB}(c^n)$ from axiom (8) using rules (9), and vice versa. Theorem 10 follows by Lemma 11, Proposition 2 and definition of $L_{G_{\mathcal{T}}}(\mathcal{N}_{AB})$.

**Example 13** (Ex. 3 cont'd). Recall that $T \models \text{Prof} \sqsubseteq \circ^3 \text{Happy}$. Figure 2 illustrates the derivations witnessing $G_{\mathcal{T}} \vdash \mathcal{N}_{\text{ProfProf}}(c^3)$ and $G_{\mathcal{T}} \vdash \mathcal{N}_{\text{ProfProud}}(c^3)$. We obtain $G_{\mathcal{T}} \vdash \mathcal{N}_{\text{ProfHappy}}(c^3)$ using the rule $\mathcal{N}_{\text{ProfHappy}} \rightarrow \mathcal{N}_{\text{ProfProf}} \& \mathcal{N}_{\text{ProfProud}}$. One can further check that $L_{G_{\mathcal{T}}}(\mathcal{N}_{\text{ProfHappy}}) = \{c^{3+n} | n \in \mathbb{N}\}$, since $\mathcal{N}_{\text{ProfHappy}} \rightarrow \mathcal{N}_{\text{ProfProf}} \mathcal{N}_{\text{ProfHappy}}$ is in $R_{\mathcal{T}}$ and $G_{\mathcal{T}} \vdash \mathcal{N}_{\text{ProfProf}}(c^n)$ for every $n$.

$R_2: \mathcal{N}_{\text{ProfProf}}(ccc)$

$R_2: \mathcal{N}_{\text{ProfProf}}(cc)$

$R_1: \mathcal{N}_{\text{ProfProf}}(c)$

<figure><img src="image_4.png" /></figure>

$R_3: \mathcal{N}_{\text{StudentDr}}(ccc)$

$R_4: \mathcal{N}_{\text{ProfProud}}(ccc)$

**Figure 2.** Derivations witnessing $G_{\mathcal{T}} \vdash \mathcal{N}_{\text{ProfProf}}(c^3)$, in the upper part, and $G_{\mathcal{T}} \vdash \mathcal{N}_{\text{ProfProud}}(c^3)$, in the lower part. Intuitively, each symbol $c$ stands for a step forward in time (cf. Figure 1). The grammar rule of $G_{\mathcal{T}}$ used to obtain each proposition through (9) is given in the following

$$\begin{align*} \text{denotation: } R_1: \mathcal{N}_{\text{ProfProf}} \rightarrow c, & \quad R_2: \mathcal{N}_{\text{ProfProf}} \rightarrow \mathcal{N}_{\text{ProfProf}} \mathcal{N}_{\text{ProfProf}}, \\ R_3: \mathcal{N}_{\text{StudentDr}} \rightarrow c^3, & \quad R_4: \mathcal{N}_{\text{ProfProud}} \rightarrow \mathcal{N}_{\text{StudentDr}}. \end{align*}$$

We now turn our attention to the converse translation.

**Theorem 14** (Grammars to TBoxes). For every unary conjunctive grammar $G = (N, \{c\}, R)$, one can construct in polynomial time a $\mathcal{TEL}^{\circ}_{\text{future}}$-TBox $T_G$ and $A \in \mathcal{N}_C(T_G)$, such that for every $B \in N$ there is $B \in \mathcal{N}_C(T_G)$ such that $T_G \models A \sqsubseteq \circ^n B$ iff $c^n \in L_G(B)$.

Let $G$ be a unary conjunctive grammar with nonterminals $N = \{B_1, \dots, B_m\}$. W.l.o.g., we assume that its rules are of the forms

$$B_i \rightarrow \varepsilon \qquad (17)$$

$$B_i \rightarrow c^n, \quad n > 0 \qquad (18)$$

$$B_i \rightarrow \alpha_1 \qquad (19)$$

$$B_i \rightarrow \alpha_1 \& \alpha_2 \qquad (20)$$

where $\alpha_1, \alpha_2$ are nonempty strings of nonterminals. Indeed, every unary grammar can be converted to this form in polynomial time.

Fix concept names $A, B_1, \dots, B_m$, and, for each $\alpha_l = B_{i_1} \dots B_{i_k}$ that occurs in the rules of $G$, introduce concept names $C_{i_j \dots i_k}$ and rigid role names $r_{i_j \dots i_k}$, for $1 \le j < k$. Let $\mathcal{J}$ denote the set of number sequences $i_j \dots i_k$ appearing in the subscripts of these symbols. We use the symbol $\iota$ to denote the elements of $\mathcal{J}$, and write $i\iota$ to mean the sequence obtained from $\iota$ by appending $i$ in the beginning. Moreover, let $\iota(\alpha_l)$ denote exactly the sequence $i_1 \dots i_k$.

**Definition 15.** Given $G = (N, \{c\}, R)$, with $N = \{B_1, \dots, B_m\}$ and rules of the forms (17)–(20), $T_G$ contains exactly the following concept inclusions.

$$A \sqsubseteq B_i, \qquad \text{for each rule of the form } (17) \qquad (17^*)$$

$$A \sqsubseteq \circ^n B_i, \qquad \text{for each rule of the form } (18) \qquad (18^*)$$

$$C_{i(\alpha_1)} \sqsubseteq B_i, \qquad \text{for each rule of the form } (19) \qquad (19^*)$$

$$C_{i(\alpha_1)} \sqcap C_{i(\alpha_2)} \sqsubseteq B_i, \qquad \text{for each rule of the form } (20) \qquad (20^*)$$

$$B_i \sqsubseteq \exists r_{i\iota} \cdot A, \qquad \text{for } i\iota \in \mathcal{J} \qquad (21^*)$$

$$\exists r_{i\iota} \cdot C_i \sqsubseteq C_{i\iota} \qquad \text{for } i\iota \in \mathcal{J} \qquad (22^*)$$

$$B_i \sqsubseteq C_i \qquad \text{for } i \in \{1, \dots, m\} \text{ s. t. } i \in \mathcal{J} \qquad (23^*)$$

We show that $c^n \in L_G(B_i)$ iff $T \models A \sqsubseteq \circ^n B_i$. We first illustrate this on an example.

**Example 16.** Consider the grammar $G$ defined by the following rules (subset of those presented in Example 8 such that $L_G(B_1) =$
<figure><img src="image_5.png" /><figcaption>**Figure 3.** Derivation witnessing ($\mathcal{T}_G$, {$A(a, 0)$}) $\vdash$ $B_1(a, 4)$. The concept inclusions used to obtain facts are given in superscripts.</figcaption></figure>

$(c, c^4))$ and the corresponding concept inclusions of $\mathcal{T}_G$:

$$ B_1 \to B_1 B_3 \text{ & } B_2 B_2 \qquad C_{13} \sqcap C_{22} \sqsubseteq B_1 \quad (I_1) $$

$$ B_1 \to c \qquad A \sqsubseteq \circ B_1 \quad (I_2) $$

$$ B_2 \to cc \qquad A \sqsubseteq \circ^2 B_2 \quad (I_3) $$

$$ B_3 \to ccc \qquad A \sqsubseteq \circ^3 B_3 \quad (I_4) $$

Additionally, $\mathcal{T}_G$ contains:

$$ B_1 \sqsubseteq \exists r_{13} \cdot A \quad (i) \quad B_3 \sqsubseteq C_3 \quad (ii) \quad \exists r_{13} \cdot C_3 \sqsubseteq C_{13} \quad (iii) \quad (I_5) $$

$$ B_2 \sqsubseteq \exists r_{22} \cdot A \quad (i) \quad B_2 \sqsubseteq C_2 \quad (ii) \quad \exists r_{22} \cdot C_2 \sqsubseteq C_{22} \quad (iii) \quad (I_6) $$

Then, we derive $B_1(a, 4)$ from $\mathcal{T}_G \cup \{A(a, 0)\}$ as shown in Figure 3.

More generally, consider a rule of the form (19): $B_i \to B_{i_1} \dots B_{i_k}$. It states that $c^n \in L(B_i)$ if $n = n_1 + \dots + n_k$ and $c^{n_j} \in L(B_{i_j})$, $1 \le j \le k$. The right-hand side of the rule is represented in $\mathcal{T}_G$ by $C_{i_1 \dots i_k}$, and whenever $C_{i_1 \dots i_k}(e, \ell)$ is derived, $B_i(e, \ell)$ follows by the corresponding concept inclusion (19*). The derivation is performed in steps. Starting from $A(a, 0)$, we derive $B_{i_1}(a, n_1)$, and then go, by $B_{i_1} \sqsubseteq \exists r_{i_1 \dots i_k} \cdot A$ (21*), to a new null, $b$, where the process restarts, recursively, from $A(b, n_1)$ targeting $C_{i_2 \dots i_k}$. This fact is stored in the index of the role name $r_{i_1 \dots i_k}$, so when $C_{i_2 \dots i_k}(b, n_1 + n')$ is inferred, and only at that point, it is lifted up to $C_{i_1 \dots i_k}(a, n_1 + n')$ by $\exists r_{i_1 \dots i_k} \cdot C_{i_2 \dots i_k} \sqsubseteq C_{i_1 \dots i_k}$ (22*). The inclusion $B_i \sqsubseteq C_i$ (23*) ends the recursion. Lemma 17 formalizes this intuition and is proved by induction on $k$.

**Lemma 17.** For $\iota = i_1 \dots i_k \in \mathcal{J}$, $\mathcal{T}_G \models A \sqsubseteq \circ^n C_i$ if and only if $n = n_1 + \dots + n_k$, such that $\mathcal{T}_G \models A \sqsubseteq \circ^{n_j} B_{i_j}$ for $1 \le j \le k$.

Concept inclusions of form (20*) just generalize this to the case of conjunction. We prove the next lemma by showing that the existence of a derivation witnessing $\mathcal{T}_G \vdash A \sqsubseteq \circ^n B_i$ implies the existence of a derivation witnessing $G \vdash B_i(c^n)$, and vice versa, by induction on the derivation length. This finalizes the proof of Theorem 14.

**Lemma 18.** $\mathcal{T}_G \models A \sqsubseteq \circ^n B_i$ if and only if $G \vdash B_i(c^n)$, for $i \in \{1, \dots, m\}$.

# 4 Linear $\mathcal{TEL}^\circ$ and context-free grammars

If a TBox $\mathcal{T}$ belongs to both $\mathcal{TEL}_{\text{future}}$ and $\mathcal{TEL}_{\text{lin}}$, the grammar $\mathcal{G}_{\mathcal{T}}$ provided by Definition 12 in the proof of Theorem 10 does not contain rules of type (14), and is thus context-free. In this section, we prove a similar result about the linear fragment in general, which is used later in Section 5 for TAQA with $\mathcal{TEL}_{\text{lin}}$-TBoxes.

**Theorem 19.** For every $\mathcal{TEL}_{\text{lin}}$-TBox $\mathcal{T}$, there exists a context-free grammar $\Gamma_{\mathcal{T}} = (N, \{c, d\}, R)$, of size polynomial in $|\mathcal{T}|$, such that for any $A, B \in \mathcal{N}_C(\mathcal{T})$, there is $\mathcal{N}_{AB} \in N$ such that $\mathcal{T} \models A \sqsubseteq \circ^n B$ iff there exists $w \in L_{\Gamma_{\mathcal{T}}} (\mathcal{N}_{AB})$ with $\#c(w) - \#d(w) = n$.

<figure><img src="image_6.png" /><figcaption>**Figure 4.** A derivation witnessing $(\mathcal{T}, \{A(a, 0)\}) \vdash E(a, 2)$ and the corresponding word $ddcccc$ can be read along the dotted line.</figcaption></figure>

To reuse the ideas of the proof of Theorem 10, we would need to get rid of local role names that occur in $\mathcal{T}$. However, we cannot rely on the construction of $\mathcal{T}_{rig}$ as in Section 3, since it introduces concept inclusions of the form $A \sqcap C_r \sqsubseteq A'_r$, so that $\mathcal{T}_{rig}$ does not belong to $\mathcal{TEL}_{\text{lin}}$ even if $\mathcal{T}$ does. We treat separately the case where $\mathcal{T}$ does not feature any local role name and the case where it does.

## 4.1 The case of rigid role names only

Suppose $\mathcal{T}$ is a $\mathcal{TEL}_{\text{lin}}$-TBox such that all role names in $\mathcal{T}$ are rigid. We construct a grammar $\Gamma_{\mathcal{T}} = (N, \{c, d\}, R)$ in a similar way as $G_{\mathcal{T}}$ in Section 3.

**Definition 20.** Given a $\mathcal{TEL}_{\text{lin}}$-TBox $\mathcal{T}$ such that $\mathcal{N}_R(\mathcal{T}) \subseteq \mathcal{N}_R^{\text{rig}}$, $\Gamma_{\mathcal{T}} = (N_{\mathcal{T}}, \{c, d\}, R_{\mathcal{T}})$, where $N_{\mathcal{T}} = \{\mathcal{N}_{AB} | A, B \in \mathcal{N}_C(\mathcal{T})\}$ and $R_{\mathcal{T}}$ contains exactly the rules defined by (12), (13), (15), (16) with $\mathcal{T}_{rig} = \mathcal{T}$, as well as the following rules.

$$ \mathcal{N}_{AB} \to d^{|n|}, \quad \text{for } A \sqsubseteq \circ^n B \in \mathcal{T}, n < 0 \quad (13^*) $$

In a word $w \in \{c, d\}^*$, a symbol $c$ corresponds to a step forwards in time, and a symbol $d$ to a step backwards. Otherwise, the intuition behind $\Gamma_{\mathcal{T}}$ is the same as that given for $G_{\mathcal{T}}$ in Section 3. For every derivation witnessing $\Gamma_{\mathcal{T}} \vdash \mathcal{N}_{AB}(w)$, we can construct a corresponding derivation of $B(a, \#c(w) - \#d(w))$ from $\mathcal{T} \cup \{A(a, 0)\}$. Conversely, from a derivation witnessing $(\mathcal{T}, \{A(a, 0)\}) \vdash B(a, n)$, we obtain a word $w$ such that $\Gamma_{\mathcal{T}} \vdash \mathcal{N}_{AB}(w)$ as follows: whenever a derivation rule uses a concept inclusion of the form $A' \sqsubseteq \circ^k B'$, we write $c^k$ if $k \ge 0$, and $d^{|k|}$ when $k < 0$.

**Lemma 21.** If $\mathcal{N}_R(\mathcal{T}) \subseteq \mathcal{N}_R^{\text{rig}}$, for any $A, B \in \mathcal{N}_C(\mathcal{T})$, $\mathcal{T} \models A \sqsubseteq \circ^n B$ iff there exists $w \in L_{\Gamma_{\mathcal{T}}} (\mathcal{N}_{AB})$ with $\#c(w) - \#d(w) = n$.

**Example 22.** Consider a $\mathcal{TEL}_{\text{lin}}$-TBox $\mathcal{T}$ containing the following concept inclusions, with $r \in \mathcal{N}_R^{\text{rig}}$. Figure 4 shows a derivation witnessing $(\mathcal{T}, \{A(a, 0)\}) \vdash E(a, 2)$ and the corresponding word.

$$ A \sqsubseteq \exists r \cdot B \quad B \sqsubseteq \circ^{-2} C \quad C \sqsubseteq \circ^4 D \quad \exists r \cdot D \sqsubseteq E $$

Lemma 21 cannot be extended beyond $\mathcal{TEL}_{\text{lin}}^\circ$ because different words, say $ddcccc$ and $cdcccd$, correspond to the same “shift” in time (here, 2), but the semantics of rules of type (14) treats them as different: if $N \to ddcccc$ and $M \to cdcccd$, then $N \& M$ generates an empty language.

## 4.2 The case of both rigid and local role names

For this case, we provide a translation from $\mathcal{T}$ to $\Gamma_{\mathcal{T}}$ which is not constructive but nevertheless guarantees the existence of $\Gamma_{\mathcal{T}}$ and the bound on its size stated by Theorem 19. To actually build $\Gamma_{\mathcal{T}}$, one needs to compute the set $\{A \sqsubseteq B | \mathcal{T} \models A \sqsubseteq B\}$, and we do not provide any recipe for that when $\mathcal{T}$ features local role names. However, Theorem 19 is enough to show ultimate periodicity of $\mathcal{TEL}_{\text{lin}}$-TBoxes, as we do in the next section.
<figure><img src="image_7.png" /><figcaption>**Figure 5.** A derivation of $G(a, 2)$ from $\{A(a, 0)\}$ and the TBox $\mathcal{T}$ of Example 23 goes along the dotted line. A derivation with $\mathcal{T}_{\text{rig}}^{\text{lin}}$ uses $B \sqsubseteq F$ and skips the part in the grey box, passing along the dash-dotted line.</figcaption></figure>

Consider a $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{rig}}^{\circ}$-TBox $\mathcal{T}$ and let $\mathcal{T}_0$ be obtained from $\mathcal{T}$ by removing all concept inclusions that use local role names. Then, let

$$ \mathcal{T}_{\text{rig}}^{\text{lin}} = \mathcal{T}_0 \cup \{A \sqsubseteq B \mid \mathcal{T} \models A \sqsubseteq B\}. \quad (24) $$

Intuitively, in a derivation using $\mathcal{T}$, if a rule of form (6) produces a fact $r(a, b, n)$ with some $r \in \mathbb{N}_{\mathbb{R}}^{\text{loc}}$, and later a rule of form (5) uses $r(a, b, n')$ to “propagate back” the consequences of facts derived about $b$ on $a$, the locality of $r$ implies that $n = n'$. A derivation that uses $\mathcal{T}_{\text{rig}}^{\text{lin}}$ “skips” the derivation between these two rule applications, immediately inferring a new fact for $a$ at time $n$.

**Example 23.** Let $r \in \mathbb{N}_{\mathbb{R}}^{\text{loc}}$ and $\mathcal{T}$ contain the concept inclusions:

$$ \begin{array}{l@{\quad}l@{\quad}l@{\quad}l} A \sqsubseteq O & F \sqsubseteq O & C \sqsubseteq O^{-3} & D \sqsubseteq O^{3} \\ B \sqsupseteq \exists r. C & \exists r. E \sqsubseteq F & & \end{array} $$

Then $\mathcal{T} \models B \sqsubseteq F$, and $\mathcal{T}_{\text{rig}}^{\text{lin}}$ contains the concept inclusions in the first line and $B \sqsubseteq F$. Figure 5 illustrates two derivations of $G(a, 2)$: one from $\{A(a, 0)\} \cup \mathcal{T}$, and one from $\{A(a, 0)\} \cup \mathcal{T}_{\text{rig}}^{\text{lin}}$.

In general, the following lemma holds.

**Lemma 24.** Let $\mathcal{T}$ be a $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{rig}}^{\circ}$-TBox. For any $A, B \in \mathbb{N}_{\mathbb{C}}(\mathcal{T})$ and $n \in \mathbb{Z}$, $\mathcal{T} \models A \sqsubseteq \circ^n B$ if and only if $\mathcal{T}_{\text{rig}}^{\text{lin}} \models A \sqsubseteq \circ^n B$.

The proof of Theorem 19 uses Lemma 24 and the facts that $\mathbb{N}_{\mathbb{R}}(\mathcal{T}_{\text{rig}}^{\text{lin}}) \subseteq \mathbb{N}_{\mathbb{R}}^{\text{rig}}$ and that $|\mathcal{T}_{\text{rig}}^{\text{lin}}|$ is polynomial in $|\mathcal{T}|$ to assume that $\mathcal{T}$ uses only rigid roles, and concludes via Lemma 21 and the polynomial time construction of $\Gamma_{\mathcal{T}}$ in Definition 20.

# 5 Answering temporal atomic queries

We now draw the consequences of the correspondences between $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^{\circ}$ or $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{rig}}^{\circ}$-TBoxes and grammars for TAQA.

## 5.1 Undecidability results

First, we close negatively the question of $\mathcal{T}\mathcal{E}\mathcal{L}^{\circ}$ ultimate periodicity.

**Theorem 25.** The following statements hold.

(i) There exists a $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^{\circ}$-TBox which is not ultimately periodic.

(ii) It is undecidable to check if the set $\{n \in \mathbb{N} \mid \mathcal{T} \models A \sqsubseteq \circ^n B\}$ is semilinear for a $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^{\circ}$-TBox $\mathcal{T}$ and $A, B \in \mathbb{N}_{\mathbb{C}}(\mathcal{T})$.

*Proof.* (i) Let $G$ be the grammar of Example 8. By Theorem 14, there exists a $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^{\circ}$-TBox $\mathcal{T}_G$ and $A, B \in \mathbb{N}_{\mathbb{C}}(\mathcal{T}_G)$ such that $\mathcal{T}_G \models A \sqsubseteq \circ^n B$ iff $c^n \in L_G(\mathbb{N}_1)$. Hence, $\{n \in \mathbb{N} \mid \mathcal{T}_G \models A \sqsubseteq \circ^n B\} = \{4^k \mid k \in \mathbb{N}\}$, which is not semilinear.

(ii) We proceed by a reduction to the problem of deciding whether $L(G)$ is regular for a unary conjunctive grammar $G$, which is undecidable by point (iii) of Theorem 9. Given a unary conjunctive grammar $G$, by Theorem 14, one can construct a $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^{\circ}$-TBox $\mathcal{T}_G$ and

$A, B \in \mathbb{N}_{\mathbb{C}}(\mathcal{T}_G)$ such that $\mathcal{T}_G \models A \sqsubseteq \circ^n B$ iff $c^n \in L_G(S)$, where $S$ is the start symbol of $G$, so that $L(G) = L_G(S)$. Hence, $\{(n) \in \mathbb{N} \mid \mathcal{T}_G \models A \sqsubseteq \circ^n B\}$ is the Parikh image of $L(G)$. Thus, by Theorem 7, $L(G)$ is regular iff this set is semilinear. $\square$

Second, we obtain some undecidability results for TAQA.

**Theorem 26.** TAQA is undecidable, for combined complexity, with $\mathcal{T}\mathcal{E}\mathcal{L}^{\circ}$-TBoxes and with $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^{\circ}$-TBoxes extended with rigid concept names.

*Proof.* By Theorem 9 (i), checking if $L(G) = \emptyset$ for a given unary conjunctive grammar $G$ is undecidable. We reduce this problem to TAQA. As in the proof of Theorem 25 (ii), given a unary conjunctive grammar $G$, one can construct a $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^{\circ}$-TBox $\mathcal{T}_G$ and $A, B \in \mathbb{N}_{\mathbb{C}}(\mathcal{T}_G)$ such that $\mathcal{T}_G \models A \sqsubseteq \circ^n B$ iff $c^n \in L(G)$. Let $C$ be a fresh concept name. We construct $\mathcal{T}'_G$ such that $L(G) \neq \emptyset$ iff $(\mathcal{T}'_G, \{A(a, 0)\}) \models C(a, 0)$ as follows. For the $\mathcal{T}\mathcal{E}\mathcal{L}^{\circ}$ case, let $\mathcal{T}'_G = \mathcal{T}_G \cup \{B \sqsubseteq C, C \sqsubseteq \circ^{-1}C\}$, and for $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^{\circ}$ with rigid concept names, let $C$ be rigid and $\mathcal{T}'_G = \mathcal{T}_G \cup \{B \sqsubseteq C\}$. $\square$

It is known that rigid concept names can be simulated with rigid role names if the language allows for the concept $\top$ (which is such that $\top^{\mathcal{I}}_i = \Delta^\top$ for every $\mathcal{J} = (\Delta^\top, (\mathcal{I}_i)_{i \in \mathcal{Z}})$ and $i \in \mathbb{Z}$, and is not allowed in the original definition of $\mathcal{T}\mathcal{E}\mathcal{L}^{\circ}$ by Gutiérrez-Basulto et al. [26]): adding $C \equiv \exists r. \top$ for a fresh $r \in \mathbb{N}_{\mathbb{R}}^{\text{rig}}$ to the TBox makes $C$ rigid. It thus follows from Theorem 26 that TAQA is undecidable also if one extends $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^{\circ}$ with $\top$. Note that Theorem 26 does not imply undecidability for data complexity. However, it implies that even having fixed a TBox $\mathcal{T}$, there is no “computational” way to obtain an algorithm for TAQA with that $\mathcal{T}$.

## 5.2 Decidability results

We first show that TAQA is decidable with $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^{\circ}$-TBoxes.

**Theorem 27.** TAQA with $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^{\circ}$-TBoxes is P-complete, both for combined and data complexity.

*Proof sketch.* The lower bounds hold already for the description logic $\mathcal{E}\mathcal{L}$ (without temporal operators) [20]. For the upper bounds, we provide a polynomial reduction from the problem of deciding whether $(\mathcal{T}, A) \models A(a, n)$ to that of checking whether a word belongs to the language of a conjunctive grammar, which can be tested in polynomial time (Theorem 6). Our reduction builds a $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^{\circ}$-TBox $\mathcal{T}' \cup \mathcal{T}_A$, an assertion $C_a(a, l)$ and a concept name $A_n$ such that $(\mathcal{T}, A) \models A(a, n)$ iff $(\mathcal{T}' \cup \mathcal{T}_A, \{C_a(a, l)\}) \models A_n(a, n)$, then use Proposition 2 and Theorem 10 to conclude. The idea is to encode all information about $a$ in $A$ into $C_a(a, l)$ thanks to $\mathcal{T}_A$.

Let $\mathbb{N}_1(A)$ be the set of individual names that occur in $A$, and $l, m \in \mathbb{Z}$ be the least and the greatest timestamps appearing in $A$. We introduce fresh concept names $\{C_a \mid a \in \mathbb{N}_1(A)\}$ and $\{A_k \mid A \in \mathbb{N}_{\mathbb{C}}(\mathcal{T}), l \le k \le m+1\}$, and role names $\{\rho_r^{ab} \mid a, b \in \mathbb{N}_1(A), r \in \mathbb{N}_{\mathbb{R}}(\mathcal{T})\}$. For the convenience of notation, we write $A_k$ for all $k \ge l$, assuming that $A_k = A_{m+1}$ when $k > m$. The TBox $\mathcal{T}'$ contains the following inclusions, for all $k \in \{l, \dots, m+1\}$.

$$ A_k \sqsubseteq \circ^s B_{k+s} \qquad \text{for } A \sqsubseteq \circ^s B \in \mathcal{T} \quad (25) $$

$$ A_k \sqcap A'_k \sqsubseteq B_k \qquad \text{for } A \sqcap A' \sqsubseteq B \in \mathcal{T} \quad (26) $$

$$ A_k \sqsubseteq \exists r. B_k \qquad \text{for } A \sqsubseteq \exists r. B \in \mathcal{T} \quad (27) $$

$$ \exists r. A_k \sqsubseteq B_k \qquad \text{for } \exists r. A \sqsubseteq B \in \mathcal{T} \quad (28) $$
Additionally, the TBox $\mathcal{T}_A$ contains the following inclusions.

$$C_a \sqsubseteq \circ^{k-l} A_k \quad \text{for } A(a, k) \in \mathcal{A} \qquad (29)$$

$$C_a \sqsubseteq \exists \rho_{ab}^r \cdot C_b \quad \text{for } r(a, b, \ell) \in \mathcal{A} \qquad (30)$$

$$\exists \rho_{ab}^r \cdot A_k \sqsubseteq B_k \quad \text{for } \exists r.A \sqsubseteq B \in \mathcal{T}, r(a, b, \ell) \in \mathcal{A}, \quad (31)$$
$$\text{where } r \in \mathbb{N}_R^{\text{rig}} \text{ or } \ell = k.$$

Both $\mathcal{T}'$ and $\mathcal{T}_A$ can be constructed in polynomial time w.r.t. $|\mathcal{T}| + |\mathcal{A}|$ and are expressed in $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^\circ$ (since $\mathcal{T}$ is a $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^\circ$-TBox and $k-l \ge 0$ for every $A(a, k) \in \mathcal{A}$ by definition of $l$) and we show that $(\mathcal{T}, \mathcal{A}) \models A(a, n)$ iff $(\mathcal{T}' \cup \mathcal{T}_A, \{C_a(a, l)\}) \models A_n(a, n). \square$

One could prove Theorem 27 without using grammars. Given $(\mathcal{T}, \mathcal{A})$, and $A(a, n)$, construct $(\mathcal{T}_n, \mathcal{A}')$ with $\mathcal{T}_n$ defined as $\mathcal{T}'$ above except that we use $k \in \{l, \dots, n\}$ in the concept inclusions, and $\mathcal{A}' = \{A_k(b, k) \mid A(b, k) \in \mathcal{A}\} \cup \{r(b, c, k) \in \mathcal{A}\}$. Using the inability of $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^\circ$ to reason backwards, one can show that $(\mathcal{T}, \mathcal{A}) \models A(a, n)$ iff $(\mathcal{T}_n, \mathcal{A}') \models A_n(a, n)$. Then, $\mathcal{T}_n$ is temporally acyclic, in the terminology of Gutiérrez-Basulto et al. [26], who prove that TAQA with such TBoxes is in P, even with rigid concept names (this is not a contradiction with Theorem 26, since $\mathcal{T}_n$ is constructed for a fixed $n$, while in the proof of Theorem 26 rigid concept names are used to simulate an existential query of the form $\exists n.A(a, n)$). On the other hand, the technique we present here allows us to reuse existing algorithms and tools for conjunctive grammars: a parser generator *Whale Calf* [34] and an efficient parsing method tailored to *unary* conjunctive grammars [38].

We also obtain positive results for the linear fragment. In the next theorem, we use the following measure for the “size” of semilinear sets. Let $\|u\| = |u_1| + \dots + |u_n|$ for $\vec{u} \in \mathbb{Z}^n$. We define $\|\mathcal{L}\|$ as the least number $\|\vec{b}\| + \|\vec{p}_1\| + \dots + \|\vec{p}_l\|$ among all representations of a linear set $\mathcal{L}$ by an offset $\vec{b}$ and periods $\vec{p}_1, \dots, \vec{p}_l$, and $\|S\|$ as the least sum $\|\mathcal{L}_1\| + \dots + \|\mathcal{L}_m\|$ among all representations of a semilinear set $S$ as a union of linear sets. For an ultimately periodic TBox $\mathcal{T}$, we set $\|\mathcal{T}\| = \max_{A,B \in \mathbb{N}_c(\mathcal{T})}(\|\{n \in \mathbb{Z} \mid \mathcal{T} \models A \sqsubseteq \circ^n B\}\|)$.

**Theorem 28.** *The following statements hold.*

(i) Every $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{lin}}^\circ$-TBox $\mathcal{T}$ is ultimately periodic, $\|\mathcal{T}\| \le 2^{\text{poly}(|\mathcal{T}|)}$.

(ii) TAQA with $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{lin}}^\circ$-TBoxes is NL-complete, for data complexity.

(iii) TAQA with $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{lin}}^\circ$-TBoxes without local role names is in EX-PSPACE, for combined complexity.

*Proof sketch.* For (i), let $\mathcal{T}$ be a $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{lin}}^\circ$-TBox. By Theorem 19, there exists a context-free grammar $\Gamma_\tau = (N, \{c, d\}, R)$ such that for any $A, B \in \mathbb{N}_c(\mathcal{T})$, there is $\mathcal{N}_{AB} \in N$ such that $\mathcal{T} \models A \sqsubseteq \circ^n B$ iff there exists $w \in L_{\Gamma_\tau}(\mathcal{N}_{AB})$ with $\#c(w) - \#d(w) = n$. Let $L = L_{\Gamma_\tau}(\mathcal{N}_{AB})$. By Theorem 7, since $\Gamma_\tau$ is context-free, the Parikh image $p(L) \subseteq \mathbb{N}^2$ of $L$ (with alphabet ordered as $c, d$) is semilinear. Hence, for every $A, B \in \mathbb{N}_c(\mathcal{T})$, $\{n \in \mathbb{Z} \mid \mathcal{T} \models A \sqsubseteq \circ^n B\} = \{n \in \mathbb{Z} \mid n = \#c(w) - \#d(w), w \in L\} = \{u_1 - u_2 \mid \vec{u} \in p(L)\}$ is semilinear, since it is the image of the semilinear set $p(L)$ under the linear mapping $\vec{u} \mapsto u_1 - u_2$. For the bound on $\|\mathcal{T}\|$, we use the methods introduced by Esparza et al. [24] to establish that $\|p(L)\| = 2^{\text{poly}(|\Gamma_\tau|)}$, and further observe that $\|\{u_1 - u_2 \mid \vec{u} \in p(L)\}\| \le 2\|p(L)\|$.

The lower bound in (ii) follows from the atemporal case [20]. For the upper bounds, both in (ii) and (iii), we provide a translation of $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{lin}}^\circ$-TBoxes to programs of linear Datalog $\diamond\diamond$ that extends linear Datalog with operators $\circ/\circ^-$ and $\diamond/\diamond^-$ (cf. proof of [26, Th. 5]).

Given a $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{lin}}^\circ$ TBox $\mathcal{T}$, let $\Phi_\tau$ be a (linear) Datalog $\diamond\diamond$ program defined as follows. For each $\exists r.A \sqsubseteq B \in \mathcal{T}$, it contains $B(x) \leftarrow r(x, y), A(y)$, and, if $r \in \mathbb{N}_R^{\text{rig}}$, also $B(x) \leftarrow$

$\diamond r(x, y), A(y)$ and $B(x) \leftarrow \diamond r(x, y), A(y)$. If $r(a, b, k) \in \mathcal{A}$ for $r \in \mathbb{N}_R^{\text{rig}}$, the facts $r(a, b, m)$, $m \in \mathbb{Z}$, are not derived explicitly, but are simulated by the latter two rules. Further, for every $A, B \in \mathbb{N}_c(\mathcal{T})$, we take a representation of the semilinear set $\{n \in \mathbb{Z} \mid \mathcal{T} \models A \sqsubseteq \circ^n B\}$ as a union of linear sets $\mathcal{L}_1 \cup \dots \cup \mathcal{L}_m$, $\mathcal{L}_i = \{b^i + k_1 p_i^+ + \dots + k_l p_i^+ \mid k_1, \dots, k_l \in \mathbb{N}\}$. Then, $\Phi_\tau$ contains the rules $F_i^{AB}(x) \leftarrow \circ^{-b^i} A(x)$, $F_i^{AB}(x) \leftarrow \circ^{-p_i^j} F_i^{AB}(x)$, $B(x) \leftarrow F_i^{AB}(x)$, for all $i \in \{1, \dots, m\}$. Thus, if $A(a, k) \in \mathcal{A}$, the fact $F_i^{AB}(a, m)$, and therefore $B(a, m)$ is derived for all $m$ such that $m - k \in \mathcal{L}_i$. It can be shown that $(\mathcal{T}, \mathcal{A}) \models A(a, n)$ iff $(\Phi_\tau, \mathcal{A}) \models A(a, n)$ and that $|\Phi_\tau| \le 2^{\text{poly}(|\mathcal{T}|)}$.

Moreover, if $\mathbb{N}_R(\mathcal{T}) \subseteq \mathbb{N}_R^{\text{rig}}$, $\Phi_\tau$ can be built from $\mathcal{T}$ using the automata-theoretic construction of Esparza et al. [24]. Points (ii) and (iii) then follow from the results on Datalog $\diamond\diamond$ [8]. $\square$

**Remark 29.** Following Gutiérrez-Basulto et al. [26], we assume a unary encoding of numbers. If sequences $\circ \cdots \circ$ were written as $\circ^n$ with $n$ encoded in binary, translating a TBox into a grammar would cause an exponential blow-up (since $c^n$ is actually a word of length $n$), making our algorithms exponentially slower w.r.t. $|\mathcal{T}|$.

# 6 Discussion

Connections between temporal logics, such as *LTL*, and formal languages (in particular, regular languages) are well-known [43, 22]. This paper makes new ones, between the fragments $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{lin}}^\circ$ and $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^\circ$ of the temporal description logic $\mathcal{T}\mathcal{E}\mathcal{L}^\circ$, on the one side, and context-free and unary conjunctive languages, on the other. Using these connections, we obtain several important results on $\mathcal{T}\mathcal{E}\mathcal{L}^\circ$, both negative and positive, from the formal language theory.

In particular, $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^\circ$-TBoxes are in a one-to-one correspondence with unary conjunctive grammars (Theorems 10 and 14). Therefore, $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^\circ$ is not ultimately periodic (Theorem 25), which is arguably unexpected, as its temporal component, *LTL*, is ultimately periodic [41], and its DL component, $\mathcal{EL}$, is such that every KB possesses a canonical model which has, informally speaking, a regular structure [31]. Moreover, TAQA with $\mathcal{T}\mathcal{E}\mathcal{L}^\circ$-TBoxes is undecidable (Theorem 26). On the other hand, the same correspondence allows us to use parsing algorithms for conjunctive grammars as tools for TAQA with $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^\circ$-TBoxes, leading to a drastic decrease of complexity, from undecidability to polynomial time, owed to a mere removal of the temporal operator $\circ^-$ (previous). Despite the partial undecidability result of Theorem 25, it remains open if ultimate periodicity of $\mathcal{T}\mathcal{E}\mathcal{L}^\circ$-TBoxes is decidable, since for the corresponding problem—given a unary conjunctive grammar tell if all its nonterminals generate regular languages—no result is known.

The linear fragment, $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{lin}}^\circ$, is connected to context-free grammars (Theorem 19). As a result, it is ultimately periodic, and enjoys considerably low data complexity of query answering (Theorem 28).

Language theorists may find interesting that every unary conjunctive grammar is transformable, in polynomial time, to the “normal form” of Definition 12, by applying first Theorem 14, then Theorem 10. Moreover, the grammars that correspond to “pure *LTL*” TBoxes (i.e., do not have any rule of form (15) in this normal form) are guaranteed to generate regular languages. This is, to the best of our knowledge, the first nontrivial sufficient condition for this property.

On the more theoretical side, it is possible that the TBox-grammar correspondence can be lifted to more expressive temporal description logics and more general classes of formal grammars (e.g. Boolean grammars [37]). On the applications side, we hope to employ this correspondence to develop a practical reasoner for $\mathcal{T}\mathcal{E}\mathcal{L}_{\text{future}}^\circ$.
Acknowledgements

Many thanks to Roman Kontchakov for introducing us to the problem of ultimate periodicity from the perspective of semilinear sets. We would also like to thank Alexander Okhotin for providing us with the code of *Whale Calf* and valuable suggestions on the implementation.

References

[1] S. Abiteboul, R. Hull, and V. Vianu. *Foundations of Databases*. Addison-Wesley, 1995. URL http://webdam.inria.fr/Alice/.

[2] A. Artale, R. Kontchakov, C. Lutz, F. Wolter, and M. Zakharyaschev. Temporalising tractable description logics. In *TIME*, 2007. doi: 10.1109/TIME.2007.62.

[3] A. Artale, D. Calvanese, R. Kontchakov, and M. Zakharyaschev. The DL-Lite family and relations. *J. Artif. Intell. Res.*, 36:1–69, 2009. doi: 10.1613/JAIR.2820.

[4] A. Artale, R. Kontchakov, F. Wolter, and M. Zakharyaschev. Temporal description logic for ontology-based data access. In *IJCAI*, 2013. URL http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6824.

[5] A. Artale, R. Kontchakov, A. Kovtunova, V. Ryzhikov, F. Wolter, and M. Zakharyaschev. First-order rewritability of temporal ontology-mediated queries. In *IJCAI*, 2015. URL http://ijcai.org/Abstract/15/383.

[6] A. Artale, R. Kontchakov, A. Kovtunova, V. Ryzhikov, F. Wolter, and M. Zakharyaschev. Ontology-mediated query answering over temporal data: A survey (invited talk). In *TIME*, 2017. doi: 10.4230/LIPICS TIME.2017.1.

[7] A. Artale, R. Kontchakov, A. Kovtunova, V. Ryzhikov, F. Wolter, and M. Zakharyaschev. First-order rewritability and complexity of two-dimensional temporal ontology-mediated queries. *J. Artif. Intell. Res.*, 2022. doi: 10.1613/JAIR.1.13511.

[8] A. Artale, A. R. Gnatenko, V. Ryzhikov, and M. Zakharyaschev. On deciding the data complexity of answering linear monadic datalog queries with LTL operators. In *ICDT*, 2025. doi: 10.4230/LIPICS.ICDT.2025.31.

[9] F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, and P. F. Patel-Schneider, editors, *The Description Logic Handbook: Theory, Implementation, and Applications*. Cambridge University Press, 2003.

[10] F. Baader, S. Brandt, and C. Lutz. Pushing the EL envelope. In *IJCAI*, 2005. URL http://ijcai.org/Proceedings/05/Papers/0372.pdf.

[11] F. Baader, C. Lutz, and S. Brandt. Pushing the EL envelope further. In *OWLED*, 2008. URL https://ceur-ws.org/Vol-496/owled2008dc\_paper_3.pdf.

[12] F. Baader, S. Borgwardt, P. Koopmann, A. Ozaki, and V. Thost. Metric temporal description logics with interval-rigid names. *ACM Trans. Comput. Log.*, 21(4):30:1–30:46, 2020. doi: 10.1145/3399443.

[13] J. Baget, M. Leclère, M. Mugnier, and E. Salvat. On rules with existential variables: Walking the decidability line. *Artif. Intell.*, 175(9-10): 1620–1654, 2011. doi: 10.1016/J.ARTINT.2011.03.002.

[14] M. Bienvenu and M. Ortiz. Ontology-mediated query answering with data-tractable description logics. In *RW*, 2015. doi: 10.1007/978-3-319-21768-0_9.

[15] S. Borgwardt and V. Thost. Temporal query answering in the description logic EL. In *IJCAI*, 2015. URL http://ijcai.org/Abstract/15/399.

[16] S. Borgwardt, M. Lippmann, and V. Thost. Temporalizing rewritable query languages over knowledge bases. *J. Web Semant.*, 33:50–70, 2015. doi: 10.1016/J.WEBSEM.2014.11.007.

[17] C. Bourgaux, A. Gnatenko, and M. Thomazo. Analysing temporal reasoning in description logics using formal grammars (arXiv preprint), 2025. URL https://arxiv.org/abs/2508.00575.

[18] S. Brandt, E. G. Kalayci, V. Ryzhikov, G. Xiao, and M. Zakharyaschev. Querying log data with metric temporal logic. *J. Artif. Intell. Res.*, 62: 829–877, 2018. doi: 10.1613/JAIR.1.11229.

[19] A. Calì, G. Gottlob, and T. Lukasiewicz. A general datalog-based framework for tractable query answering over ontologies. *J. Web Semant.*, 14:57–83, 2012. doi: 10.1016/J.WEBSEM.2012.03.001.

[20] D. Calvanese, G. D. Giacomo, D. Lembo, M. Lenzerini, and R. Rosati. Data complexity of query answering in description logics. *Artif. Intell.*, 195:335–360, 2013. doi: 10.1016/J.ARTINT.2012.10.003.

[21] N. Chomsky. Three models for the description of language. *IRE Trans. Inf. Theory*, 2(3):113–124, 1956. doi: 10.1109/TIT.1956.1056813.

[22] S. Demri, V. Goranko, and M. Lange. *Temporal Logics in Computer Science: Finite-State Systems*. 2016.

[23] M. M. Dimartino, A. Calì, A. Poulovassilis, and P. T. Wood. Query rewriting under linear EL knowledge bases. In *RR*, 2016. doi: 10.1007/978-3-319-45276-0_6.

[24] J. Esparza, P. Ganty, S. Kiefer, and M. Luttenberger. Parikh's theorem: A simple and direct automaton construction. *Inf. Process. Lett.*, 111 (12):614–619, 2011. doi: https://doi.org/10.1016/j.ipl.2011.03.019.

[25] V. Gutiérrez-Basulto and S. Klarman. Towards a unifying approach to representing and querying temporal data in description logics. In *RR*, 2012. doi: 10.1007/978-3-642-33203-6_8.

[26] V. Gutiérrez-Basulto, J. C. Jung, and R. Kontchakov. Temporalized EL ontologies for accessing temporal data: Complexity of atomic queries. In *IJCAI*, 2016. URL http://www.ijcai.org/Abstract/16/160.

[27] J. E. Hopcroft, R. Motwani, and J. D. Ullman. *Introduction to Automata Theory, Languages, and Computation (3rd Edition)*. Addison-Wesley Longman Publishing Co., Inc., USA, 2006.

[28] A. Jeż. Conjunctive grammars generate non-regular unary languages. *Int. J. Found. Comput. Sci.*, 19(3):597–615, 2008. doi: 10.1142/ S012905410800584X.

[29] A. Jeż and A. Okhotin. Conjunctive grammars over a unary alphabet: Undecidability and unbounded growth. *Theory Comput. Syst.*, 46(1): 27–58, 2010. doi: 10.1007/s00224-008-9139-5.

[30] E. G. Kalayci, S. Brandt, D. Calvanese, V. Ryzhikov, G. Xiao, and M. Zakharyaschev. Ontology-based access to temporal data with on-top: A framework proposal. *Int. J. Appl. Math. Comput. Sci.*, 29(1): 17–30, 2019. doi: 10.2478/AMCS-2019-0002.

[31] R. Kontchakov and M. Zakharyaschev. An introduction to description logics and query rewriting. In *RW*, 2014. doi: 10.1007/978-3-319-10587-1_5.

[32] B. Motik, B. Cuenca Grau, I. Horrocks, Z. Wu, A. Fokoue, and C. Lutz. OWL 2 Web Ontology Language profiles. W3C Recommendation, 11 December 2012. Available at http://www.w3.org/TR/owl2-profiles/.

[33] A. Okhotin. Conjunctive grammars. *J. Autom. Lang. Comb.*, 6(4):519–535, 2001. doi: 10.25596/JALC-2001-519.

[34] A. Okhotin. Whale calf, a parser generator for conjunctive grammars. In *CIAA*, 2002.

[35] A. Okhotin. A recognition and parsing algorithm for arbitrary conjunctive grammars. *Theor. Comput. Sci.*, 302(1):365–399, 2003. doi: https://doi.org/10.1016/S0304-3975(02)00853-8.

[36] A. Okhotin. A simple P-complete problem and its language-theoretic representations. *Theor. Comput. Sci.*, 412(1):68–82, 2011. doi: https://doi.org/10.1016/j.tcs.2010.09.015.

[37] A. Okhotin. Conjunctive and Boolean grammars: The true general case of the context-free grammars. *Comput. Sci. Rev.*, 9:27–59, 2013. doi: 10.1016/j.cosrev.2013.06.001.

[38] A. Okhotin and C. Reitwießner. Parsing Boolean grammars over a one-letter alphabet using online convolution. *Theor. Comput. Sci.*, 2012. doi: https://doi.org/10.1016/j.tcs.2012.06.032.

[39] R. J. Parikh. On context-free languages. *J. ACM*, 13(4):570–581, Oct. 1966. doi: 10.1145/321356.321364.

[40] A. Poggi, D. Lembo, D. Calvanese, G. D. Giacomo, M. Lenzerini, and R. Rosati. Linking data to ontologies. *J. Data Semant.*, 10:133–173, 2008. doi: 10.1007/978-3-540-77688-8_5.

[41] A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. *J. ACM*, 32(3):733–749, July 1985. ISSN 0004-5411. doi: 10.1145/382838.3837.

[42] V. Thost, J. Holste, and Ö. L. Özçep. On implementing temporal query answering in DL-Lite (extended abstract). In *DL*, 2015. URL https://ceur-ws.org/Vol-1350/paper-63.pdf.

[43] M. Y. Vardi. An automata-theoretic approach to linear temporal logic. In *Logics for Concurrency: Structure versus Automata*. 1996. doi: 10.1007/3-540-60915-6_6.

[44] D. Wang, P. Hu, P. A. Walega, and B. C. Grau. Meteor: Practical reasoning in datalog with metric temporal operators. In *AAAI*, 2022. doi: 10.1609/AAAI.V36I5.20535.