We investigate the practical feasibility of automated reasoning over temporal DL-Lite (TDL-Lite) knowledge bases (KBs) [1,15,4,2,3]. By `TDL-Lite', we consider here the TF P X DL-LitebNool logic [2], the most expressive decidable language of the DL-Lite family combined with Linear Temporal Logic (LTL). The key idea is to map a TDL-Lite KB|a set of TBox and ABox axioms|into an equisatis able LTL formula by applying the translation described in [2]. TDL-Lite admits both past and future operators interpreted over Z while LTL reasoners often can deal with only future operators interpreted over N. Thus, we present a translation removing past operators that retains formula satis ability (Gabbay [10] showed that past temporal modalities do not add expressive power, and recently Markis [16] presented an algorithm preserving formula equivalence where the obtained pure-future formulas have an exponential blow-up in size). Since we are interested in preserving satis ability, we provide a linear in size translation that removes past operators from a TDL-Lite knowledge base, thus obtaining an equi-satis able pure-future LTL formula. The result is stated in the following theorem, which is more generally formulated in terms of LTL formulas (where LTLP denotes LTL extended with past operators and interpreted over Z). Theorem 1. Let ' be a LTLP formula, then, ' is satis able i its LTL translation 'N is satis able. The size of 'N grows linearly w.r.t j'j.
SAT
pltl (graph) pltl (tree)
reasoners [
Example 1. Let K = (T ; A), where T is a TDL-Lite TBox expressing that, at each point in time, a person has a unique Name which is also global (i.e., does not change over time), but the ABox A (0 and 1 are timestamps denoting when the assertions hold) violates the fact that p1's name is functional and global: T = fPerson v 1 Name; Person v : 2 Nameg
A = fPerson(p1; 0); Name(p1; n1; 0); Name(p1; n2; 1)g
Depending on the di erent sizes of the tested ABoxes, the number of
propositional variables in the resulting LTL formulas translating the TDL-Lite KBs
of the \toy scenario" ranges from 180 to 2336 variables. The results shown in
Fig. 1 in the form of `heat maps' [
Randomly Generated TBoxes. In a second experiment, we investigate the
scalability of the reasoners over synthetic TBoxes (no ABoxes in this experiment)
by extending the random algorithm proposed for LTL [
Lc = 5
Lc = 10
following settings: (i) the average-behaviour analysis which covers TDL-Lite
TBoxes in a uniform way (see the full paper [
For more detail see the full version of the paper [
Conclusions. This work investigate the scalability and robustness of LTL solvers
while checking TDL-Lite KBs for satis ability. Two major culprits in the
runtime of solvers are the size of the ABox and the presence of past operators. The
increase in the number of propositional variables when removing past opertors
penalizes the runtime of the solvers. Concerning ABoxes, the preliminary results
show that a brute force approach makes reasoning in the presence of ABoxes
almost unfeasable. As a future work, we plan to investigate reasoners able to
scale in the presence of ABoxes. We will experiment with rst-order temporal
logic solvers to avoid the step of grounding the translation, making the number
of propositional variables of the resulting LTL encoding not manageable.
Furthermore, we plan to extend to the temporal case the existing ABox abstraction
approaches which are successfully applied over OWL ontologies [