We establish a correspondence between (fragments of) ℰℒ ○ , a temporal extension of ℰℒ with the LTL operator ○ , and conjunctive grammars (context-free grammars equipped with the operation of intersection). This connection implies that ℰℒ ○ does not enjoy ultimate periodicity of models, and further leads to undecidability of query answering in ℰℒ ○ , closing a question left open since the introduction of ℰℒ ○ . It also allows to establish decidability of query answering for some new fragments of ℰℒ ○ , and to reuse for this purpose existing tools and algorithms for conjunctive grammars.
Alice
Prof advisorOf
Happy
Dr
ProfProf ProfProf ProfProf
ProfProf ProfProf
StudentDr ProfProud (a) Some inferences for Example 1. Dashed lines repre- (b) An illustration for the facts that 3 ∈ sent the temporal evolution of a given element, while 3 (ProfProf ), in the upper part, and dotted lines represent a relation whose existence is ∈ (ProfProud), in the lower part. Each known due to role rigidity. symbol stands for a step forward in time.
Gutiérrez-Basulto et al. [
Our contribution is to link temporal reasoning with ℰ ℒ ○ -TBoxes to the study of associated formal languages, which allows us to close (negatively) these open questions and obtain additional results. We work with ℰ ℒ ○ -TBoxes in normal form, whose concept inclusions are of the form ⊑ ○ ⊓ ′ ⊑ ∃. ⊑ ⊑ ∃. (1) with ∈ Z encoded in unary. We will further consider two fragments of ℰ ℒ ○ : the future fragment, ℰ ℒf○ uture, is obtained by setting ⩾ 0, and the linear fragment, ℰ ℒl○in, disallows concept inclusions of the form ⊓ ′ ⊑ . For simplicity, in this extended abstract we assume that all roles are rigid (all the results hold without this assumption).
Conjunctive grammars as introduced by Okhotin [
The membership problem for conjunctive grammars is P-complete [
TBoxes and grammars. We establish a correspondence between TBoxes of ℰ ℒf○ uture and ℰ ℒl○in and unary grammars.
Theorem 2. For every ℰ ℒf○ uture-TBox , one can construct in polynomial time a unary conjunctive
grammar = ( , {}, ) such that for any , ∈ NC( ), there is ∈ such that
∈ () if |= ⊑ ○ .
1Gutiérrez-Basulto et al. [
We sketch the construction. Set = { | , ∈ NC( )} and let contain exactly the following rules.
→ → → → → , , & , , , for ⊑ ∈ or = for ⊑ ○ ∈ , > 0 for ∈ NC( ), ⊓ ⊑ ∈ for ⊑ ∃., ∃. ⊑ ∈ for , , ∈ NC( ) (2) (3) (4) (5) (6)
Intuitively, for every pair of concept names , ∈ NC( ), encodes every possible way of deriving (, ) from (, 0) with : either directly (using (2) when = 0 or (3) when = > 0), or by obtaining (, ) and (, ) that together give (, ) (4), or by going through an anonymous object (5), or through an intermediate point (, ), 0 ⩽ ⩽ (6). See Figure 1b for an illustration.
Interestingly, a converse translation is also possible.
Theorem 3. For every unary conjunctive grammar = (, {}, ), one can construct in polynomial time a ℰ ℒf○ uture-TBox and ∈ NC(), such that for every ℬ ∈ there is ∈ NC() such that |= ⊑ ○ if ∈ (ℬ).
When considering the linear fragment, a similar connection can be built using only context-free grammars (over a two-symbol alphabet).
Theorem 4. For every ℰ ℒl○in-TBox , there exists a context-free grammar Γ = ( , {, }, ′ ), of size polynomial in | |, such that for any , ∈ NC( ), there is ∈ such that |= ⊑ ○ if there exists ∈ Γ ( ) with #() − #() = .
Here, = { | , ∈ NC( )} is as in Theorem 2, and ′ contains exactly the rules defined by (2), (3), (5), (6), as well as the following rules. → ||, for ⊑ ○ ∈ , < 0 (3* ) In a word ∈ {, }* , a symbol corresponds to a step forwards in time, and a symbol to a step backwards. Otherwise, the intuition behind Γ is the same as that given for .
Note that Theorem 4 is not constructive: although Γ can be computed when all roles in are rigid, in the general case we could only prove that it exists.
Consequences for temporal atomic query answering. Using Theorem 2, we show that TAQ
answering with ℰ ℒf○ uture-TBoxes is decidable in polynomial time2. It also follows that one can use
tools that have been developed for conjunctive grammars, such as Whale Calf [
On the other hand, by Theorem 3 and results on unary conjunctive grammars [
The fact that ℰ ℒf○ uture is not ultimately periodic is arguably unexpected, as its temporal component,
LTL, is ultimately periodic [
We hope to employ the TBox-grammar correspondence to develop a practical reasoner for ℰℒf○ uture.
On the more theoretical side, it is possible that this correspondence can be lifted to more expressive
temporal description logics and more general classes of formal grammars (e.g. Boolean grammars [
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.
The authors have not employed any Generative AI tools. [16] R. Kontchakov, M. Zakharyaschev, An introduction to description logics and query rewriting, in: RW, 2014. doi:10.1007/978-3-319-10587-1\_5.