Analysing Temporal Reasoning in Description Logics Using Formal Grammars

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.

Authors

• Camille Bourgaux
• Anton R. Gnatenko
• Michaël Thomazo

Keywords

No keywords are indexed for this paper.