Analysing Temporal Reasoning in Description Logics Using Formal Grammars

TL;DR

This paper links a temporal description logic to formal grammars, revealing undecidability in general but identifying decidable fragments and enabling the use of existing grammar tools.

Contribution

It establishes a formal correspondence between a temporal description logic and conjunctive grammars, leading to new decidability results and insights into model properties.

Findings

Proves undecidability of query answering in the full logic.

Identifies decidable fragments of the logic.

Enables reuse of existing grammar algorithms.

Abstract

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