Analysing Temporal Reasoning in Description Logics Using Formal Grammars (IJCAI Extended Abstract)

1 Introduction

Ontology-mediated query answering (OMQA) aims at improving data access by enriching data with domain knowledge. This knowledge, typically expressed in a given description logic (DL) as a set of logical formulas (concept inclusions, in DL parlance), enables comprehensive query answering based not only on facts stored in the data but also on facts deducible through logical reasoning [Poggi et al., 2008; Kontchakov and Zakharyaschev, 2014; Bienvenu and Ortiz, 2015; Baader et al., 2003]. In practical applications, where the focus is on efficiency, many ontologies use DLs from the EL family [Baader et al., 2005; Baader et al., 2008], which allow for tractable reasoning.

Various extensions of the OMQA framework have been proposed to make it applicable to querying temporal data [Artale et al., 2017]. In this setting, facts are associated with timestamps, and concept inclusions may feature some operators from linear temporal logic (LTL). We consider the temporal description logic TEL, which extends EL with the operators ⃝ (next), ⃝- (previous), ♢ (eventually) and ♢- (eventually in the past) [Artale et al., 2007; Guti´errez-Basulto et al., 2016]. For instance, the concept inclusion Prof ⊑ ⃝Prof 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 relations between individuals (called 'roles') are rigid, i.e., they do not change over time.

∗ For the full version, see Bourgaux et al. [2025a; 2025b]

Example 1. Imagine that Alice is a professor in 2026, denoted Prof(Alice, 2026). 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 formalised as follows (using a rigid role advisorOf):

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

Despite both LTL and EL being decidable, Guti´errezBasulto et al. [2016] showed that their combination in TEL quickly leads to undecidability. They exhibited fragments of TEL that allow for decidable query answering by guaranteeing a certain semantic 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. It was shown that the use of the operator ♢ destroys this property, while it is enjoyed by certain 'acyclic' fragments of TEL◦, a sublanguage limited to operators ⃝ and ⃝-. The question of ultimate periodicity, and, in general, of decidability of query answering for the full TEL◦ was left open.

Our main contribution is to link temporal reasoning in TEL◦ to the study of associated formal languages, in particular, conjunctive languages of Okhotin [2013]. This connection allows us to close the open question of Guti´errez-Basulto et al. [2016] and obtain additional results. First, we close negatively the question of whether TEL◦ enjoys ultimate periodicity, and complete the complexity picture of TEL: atomic query answering in TEL◦ is undecidable. Second, we provide results for two new fragments TEL◦fut and TEL◦lin we introduce. As for TEL◦fut , which only allows to derive novel information about the future (or present) and not the past, we prove that atomic query answering is solvable in polynomial time (in combined and data complexity). Regarding TEL◦lin , a temporal extension of linear EL [Dimartino et al., 2016], we prove that TEL◦lin enjoys ultimate periodicity, and derive complexity results for atomic query answering. For details and proofs, we refer the reader to the main paper [Bourgaux et al., 2025a; 2025b]. We also point to a recent continuation of this line of work which generalises our results [Gnatenko and Kontchakov, 2026].

2 Preliminaries

We assume familiarity with formal languages, grammars, and semilinear sets. We recall the definition of TEL◦ from Guti´errez-Basulto et al. [2016]. Let NI, NC, NR be disjoint countably infinite sets of individual names, concept names and role names, respectively, with NR partitioned into rigid role names N rig R and local role names N loc R .

Syntax. A fact is an expression of the form A(a, n) or r(a, b, n), where a, b ∈ NI, A ∈ NC, r ∈ NR, and n ∈ Z. An ABox (data instance) A is a finite set of facts. A TEL◦- TBox (ontology) T is a finite set of concept inclusions of the form

where A,A′ ,B ∈ NC, r ∈ NR, and n ∈ Z. When n = 0, n = 1, or n = -1, we simply write A ⊑ B, A ⊑ ⃝B, and A ⊑ ⃝-B, respectively. A knowledge base (KB) is a pair (T ,A). We denote by NC(T ), NR(T ), N rig R (T ), and N loc R (T ), respectively, the sets of concept names, role names, and rigid and local role names appearing in T . The size |T | of T (resp. |A| of A) is the number of symbols needed to write it down, with integers encoded in unary.

We will further consider two fragments of TEL◦: the future fragment, TEL◦fut , is obtained by setting n ⩾ 0, and the linear fragment, TEL◦lin , disallows concept inclusions of the form A ⊓ A′ ⊑ B. For TEL◦lin , moreover, we distinguish the case where all role names in TBoxes are rigid; the corresponding subfragment is denoted TEL◦lin&rig .

Semantics. An interpretation J is a structure (∆J , (Ii)i∈Z) where each Ii = (∆J , ·Ii ) is a classical DL interpretation with domain ∆J : for every a ∈ NI, aIi = a (standard name assumption, assuming that NI ⊆ ∆J ), for every A ∈ NC, AIi ⊆ ∆J , and for every r ∈ NR, rIi ⊆ ∆J ×∆J . Moreover, for every r ∈ N rig R , rIi = rI0 for every i ∈ Z. The interpretation function ·Ii is often written as ·J,i and is extended to interpret complex concepts as expected:

The interpretation J is a model of a fact A(a, n) (resp. r(a, b, n)) if a ∈ AJ,n (resp. (a, b) ∈ rJ,n ), and of a concept inclusion C ⊑ D if C J,i ⊆ DJ,i for every i ∈ Z. It is a model of an ABox A (resp. a TBox T ) if it is a model of all facts in A (resp. all concept inclusions in T ), and of a KB (T ,A) if it is a model of T and A. We write J |= α to denote that J is a model of α. A TBox T entails a concept inclusion α, written T |= α, if J |= T implies J |= α, and a KB (T ,A) entails a fact α, (T ,A) |= α, if J |= (T ,A) implies J |= α. Note that rigid concept names can be defined in a similar fashion as rigid role names, and can be simulated with A ⊑ ⃝A and A ⊑ ⃝-1A in TEL◦ and TEL◦lin (but not in TEL◦fut ).

Query answering and ultimate periodicity. The temporal atomic query answering (TAQA) problem is that of deciding, given a temporal KB (T , A) and a fact A(a, n), whether (T , A) |= A(a, n). We consider combined complexity, where the size of the input is |T | + |A| + |A(a, n)|, and data complexity, where T is fixed. For the latter, TAQA is PSPACEcomplete when the TBox T is ultimately periodic, i.e. when the sets {n ∈ Z | T |= A ⊑ ⃝nB} are semilinear, for all A, B ∈ NC(T ) [Guti´errez-Basulto et al., 2016].

Conjunctive grammars. To analyse ultimate periodicity of TEL◦-TBoxes, we employ conjunctive grammars. As introduced by Okhotin [2013], a conjunctive grammar is a triple G = (N, Σ, R), where N and Σ are disjoint alphabets of nonterminals and terminals, respectively, and R is a finite set of rules of the form:N → α1 & · · · &αn

with N ∈ N, n ⩾ 1, and αi ∈ (N ∪ Σ)∗ . Several rules with the same left-hand side N can be written as a single rule, with | separating the right-hand sides.

The semantics extends that of context-free grammars with intersection: given a rule of the above form, apply "in parallel" context-free rules N → αi and take the intersection of the generated languages. We write LG(N) for the language generated by the nonterminal N ∈ N. Languages that can be generated in this way, e.g. {an bn cn | n ∈ N}, are called conjunctive. We refer to Okhotin [2013] for details.

The membership problem for conjunctive languages is PTIME-complete, both when the grammar is fixed or is part of input itself [Okhotin, 2003; 2011]. We will focus on unary grammars, where the underlying alphabet contains just one symbol, i.e. Σ = {c}. A unary language L can be seen as a set of natural numbers given in unary: {n ∈ N | cn ∈ L}. While unary context-free grammars can generate only regular languages (i.e., semilinear subsets of N) [Parikh, 1966], conjunctive grammars are more powerful. For example, there is a unary conjunctive language corresponding to the set {4n | n ∈ N} [Je˙z, 2008]. Moreover, emptiness and regularity of the language are both undecidable for unary conjunctive grammars [Je˙z and Okhotin, 2010].

3 FromTBoxes toGrammars, andBackAgain

We present two theorems that establish our key result: the sets of the form {n ∈ N | T |= A ⊑ ⃝nB} for TEL◦fut -TBoxes correspond exactly to unary conjunctive languages. In this extended abstract, we assume that all role names in TBoxes are rigid (all the results hold in the general case).

Theorem 2. For every TEL◦fut -TBox T , one can construct in polynomial time a unary conjunctive grammar GT = (N, {c}, R) such that for any A, B ∈ NC(T ), there is NAB ∈ N such that cn ∈ LGT (NAB) iff T |= A ⊑ ⃝nB.

We sketch the construction. Given a TEL◦fut -TBox T , let GT = (NT , {c},RT ), where NT = {NAB | A,B ∈ NC(T )} and RT contains exactly:

Intuitively, for every pair of concept names A, B ∈ NC(T ), GT encodes every possible way of deriving B(a, n) from A(a, 0) with respect to T : either directly (2, 3), or by obtaining C(a, n) and D(a, n) that together give B(a, n) (4), or by going through a null (5), or through an intermediate point C(a, k), 0 ⩽ k ⩽ n (6). To illustrate, recall the TBox T from Example 1, which is such that T |= Prof ⊑ ⃝3Happy. Figure 2 shows the derivations witnessing c3 ∈ LGT (NProfProf ) and c3 ∈ LGT (NProfProud). We obtain c3 ∈ LGT (NProfHappy) using the rule NProfHappy → NProfProf &NProfProud.

We now turn our attention to the converse translation.

Theorem 3. For every unary conjunctive grammar G = (N, {c}, R), one can construct in polynomial time a TEL◦fut - TBox TG and A ∈ NC(TG), such that for every B ∈ N there is B ∈ NC(TG) such that TG |= A ⊑ ⃝nB iff cn ∈ LG(B).

2

Figure 3: An illustration for TG |= A ⊑ ⃝4B1. The concept inclusion used for each inference is given in superscript (cf. Example 4).

Let G = ({B1, . . . , Bm}, {c},R) be a unary conjunctive grammar. W.l.o.g., we assume that its rules are of the forms

with w ∈ {c}∗ and N,N1,N2 ∈ {B1, . . . , Bm}. Indeed, every unary grammar can be converted to this form in polynomial time. Fix concept names A,B1, . . . ,Bm, and rigid role names r1, . . . , rm. We define TG to contain exactly the following concept inclusions, according to the rules of R. 1

It can be shown that cn ∈ LG(Bi) iff TG |= A ⊑ ⃝nBi. We first illustrate this on an example.

Example 4. Consider the grammar G defined by the following rules and the corresponding concept inclusions of TG:

Then, we have TG |= A ⊑ ⃝4B1, as shown in Figure 3.

More generally, consider a rule of the form Bi → BjBk. It states that cn ∈ LG(Bi) if n = n1 + n2, cn1 ∈ LG(Bj) and cn2 ∈ LG(Bk). This corresponds to the following line of reasoning with respect to TG. Starting from A(a, 0), we derive Bj(a, n1), and then go, by Bj ⊑ ∃rj.A (10), to a new element, b, where the process restarts, recursively, from A(b, n1). When Bk(b, n1 + n2) is inferred, and only at that point, it is lifted up to Bi(a, n1 +n2) by ∃rj.Bk ⊑ Bi (11).

Linear TEL◦ and Context-Free Grammars

If a TBox T belongs to both TEL◦fut and TEL◦lin , the grammar GT provided by Theorem 2 does not contain rules of type (4), and is thus context-free. This connection can be extended to the linear fragment in general.

1 We present here a simplified construction compared to Bourgaux et al. [2025a], assuming a stronger normal form of G.

Theorem 5. For every TEL◦lin -TBox T , there exists a contextfree grammar ΓT = (N, {c, d}, R), of size polynomial in |T |, such that for any A,B ∈ NC(T ), there is NAB ∈ N such that T |= A ⊑ ⃝nB iff there exists w ∈ LΓT (NAB) with #c(w) - #d(w) = n.

In a word w ∈ {c, d}∗ , a symbol c corresponds to a step forwards in time, and a symbol d to a step backwards. Otherwise, the intuition behind ΓT is the same as that given for GT from Theorem 2.

Example 6. Consider a TEL◦lin -TBox T containing the following concept inclusions, with r ∈ N rig R . Figure 4 shows a word witnessing that T |= A ⊑ ⃝2E.

Note that Theorem 5 is not constructive. For a TEL◦lin&rig - TBox, however, one can compute ΓT in polynomial time, just like in Theorem 2.

4 Answering Temporal Atomic Queries

We use Theorems 2, 3, and 5 to analyse ultimate periodicity of TBoxes and derive complexity bounds for TAQA.

First, we close the question of TEL◦ ultimate periodicity.

Theorem 7. The following statements hold.

• (i) There is a TEL◦fut -TBox which is not ultimately periodic.
• (ii) It is undecidable to check if {n ∈ N | T |= A ⊑ ⃝nB} is semilinear for a TEL◦fut -TBox T and A, B ∈ NC.

Proof sketch. Point (i) holds by Theorem 3 and the existence of a non-regular unary conjunctive language [Je˙z, 2008]. For (ii), we give a reduction from the problem of deciding whether LG(B) is regular for a unary conjunctive grammar G and a nonterminal B, which is undecidable [Je˙z and Okhotin, 2010].

Second, by a reduction from the undecidable problem of emptiness checking for unary conjunctive languages [Je˙z and Okhotin, 2010], we obtain undecidability results for TAQA.

Theorem 8. TAQA is undecidable, for combined complexity, with TEL◦-TBoxes and with TEL◦fut -TBoxes extended with rigid concept names.

We obtain positive results as well. First, we show that TAQA is decidable with TEL◦fut -TBoxes.

Theorem 9. TAQA with TEL◦fut -TBoxes is PTIME-complete, both for combined and data complexity.

Proof sketch. The lower bounds hold already for the description logic EL (without temporal operators) [Calvanese et al., 2013]. For the upper bounds, one can provide a polynomial reduction from the problem of deciding whether (T ,A) |= 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 [Okhotin, 2003; 2011].

We note that Theorem 9 can be alternatively proved by a reduction to reasoning with temporally acyclic TBoxes [Guti´errez-Basulto et al., 2016]. However, the connection to grammars allows us to reuse efficient algorithms and tools [Okhotin, 2002; Okhotin and Reitwießner, 2012].

We now turn to the linear fragment. For an ultimately periodic T , let ∥T ∥ denote the largest norm among the (semilinear) sets {n ∈ Z | T |= A ⊑ ⃝nB} [Chistikov and Haase, 2016].

Theorem 10. The following statements hold.

• (i) Every TEL◦lin -TBox T is ultimately periodic, ∥T ∥ ⩽ 2poly(|T |) .
• (ii) TAQA with TEL◦lin -TBoxes is NL-complete, for data complexity.
• (iii) TAQA with TEL◦lin&rig -TBoxes is in EXPSPACE, for combined complexity.

Proof sketch. The point (i) follows from Theorem 5 and results on context-free languages [Parikh, 1966; Esparza et al., 2011]. The lower bound in (ii) follows from the atemporal case [Calvanese et al., 2013]. For the upper bounds, both in (ii) and (iii), one can translate TEL◦lin -TBoxes to programs of linear temporal datalog [Artale et al., 2025], following the general approach of [Guti´errez-Basulto et al., 2016] to ultimately periodic TBoxes.

Following Guti´errez-Basulto et al. [2016], we assume a unary encoding of numbers. For the case of binary encoding, and for the missing bounds (data complexity for TEL◦, combined complexity for TEL◦lin and a lower bound for TEL◦lin&rig ), we refer the reader to Gnatenko and Kontchakov [2026].

5 Conclusions

Connections between temporal logics, such as LTL, and formal languages (in particular, regular languages) are wellknown [Vardi, 1996; Demri et al., 2016]. We establish new ones, between the linear and future fragments of the temporal description logic TEL◦, on the one side, and context-free and unary conjunctive languages, on the other. Using these connections, we obtain several important results on TEL◦, both negative and positive, relying on the formal language theory.

Ethical Statement

There are no ethical issues.

Acknowledgments

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. This work is supported by the ANR project EXPAND - ANR-25-CE23-1215.