Analysing Temporal Reasoning in Description Logics Using Formal Grammars

Abstract

We establish a correspondence between (fragments of) ${\mathcal{T}\mathcal{E}\mathcal{L}}^{◯}$, a temporal extension of the $\mathcal{E}\mathcal{L}$ 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 ${\mathcal{T}\mathcal{E}\mathcal{L}}^{◯}$ does not possess the property of ultimate periodicity of models, and further leads to undecidability of query answering in ${\mathcal{T}\mathcal{E}\mathcal{L}}^{◯}$, closing a question left open since the introduction of ${\mathcal{T}\mathcal{E}\mathcal{L}}^{◯}$. Moreover, it also allows to establish decidability of query answering for some new interesting fragments of ${\mathcal{T}\mathcal{E}\mathcal{L}}^{◯}$, and to reuse for this purpose existing tools and algorithms for conjunctive grammars.

This is an extended version of a paper appearing at the 28th European Conference on Artificial Intelligence (ECAI 2025). 20 pages