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 T F P X DL-Lite N bool 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 equisatisfiable 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 satisfiability (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 satisfiability, we provide a linear in size translation that removes past operators from a TDL-Lite knowledge base, thus obtaining an equi-satisfiable pure-future LTL formula. The result is stated in the following theorem, which is more generally formulated in terms of LTL formulas (where LTL P denotes LTL extended with past operators and interpreted over Z).
Theorem 1. Let ϕ be a LTL P formula, then, ϕ is satisfiable iff its LTL translation ϕ N is satisfiable. The size of ϕ N grows linearly w.r.t |ϕ|.
Since the above translation comes at the cost of increasing the number of propositional variables, we also introduce the simpler logic, called T N DL-Lite, that allows for temporal formulas with only future temporal operators, interpreted over N. Using such a weaker language allows us to evaluate the impact of past operators on the runtime efficiency of reasoners when checking for satisfiability.
The complexity of reasoning over TDL-Lite KBs is known to be PSpacecomplete [2]. To put these results in practice, we provide a tool, named crowd-ER VT 5 , which is a non-trivial extension of crowd [5,6]. Our tool allows users to draw temporal conceptual schemas and populate them with timestamped instances, which are translated into TDL-Lite KBs and, ultimately, into LTL formulas that can be checked for satisfiability and entailment using existing off-the-shelf LTL [18,7,12,14,17]. We conduct experiments to evaluate the scalability of reasoners by randomly generating TDL-Lite TBoxes. We also devise a toy scenario to evaluate the performance of reasoners with ABoxes of increasing size.
Toy Scenario Experiment. In the chosen "toy scenario" a TDL-Lite TBox is paired with various ABoxes of different sizes varying from 20 to 50 assertions (distributed over different time points), which may yield either satisfiable (SAT) or unsatisfiable (UNSAT) KBs. The following example illustrates such a scenario with an ABox that is unsatisfiable w.r.t. the given TBox. 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 p 1 's name is functional and global:
Depending on the different 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' [13] represent the runtime of the KB satisfiability checking for increasing ABox sizes (in columns) and different solvers (in lines). Solvers had better performances over SAT instances compared to UN-SAT ones, except TRP ++ and pltl, which fail to scale already over small ABoxes. Moreover, NuXMV-SBMC fails regardless the size of the model in UNSAT cases. Overall, the best options for SAT and UNSAT cases were NuXMV with BMC and IC3, respectively. Aalta performs well but only when the LTL input formula does not exceed 1200 propositional variables.
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 [8]. We benchmarked our tool against TBoxes (mostly SAT) generated randomly according to the Fig. 2: Heat map of the runtimes on randomly generated TBoxes (colors as in Fig. 1).
following settings: (i) the average-behaviour analysis which covers TDL-Lite TBoxes in a uniform way (see the full paper [19] for more details); and (ii) the temporal-behaviour analysis which increases the chance of generating TBoxes with temporal operators and global roles. For the temporal-behaviour analysis (see Fig. 2), we create batches of 20 random TBoxes with the following parameters: N = 1, 3, 5 (number of concept names), Q = 5 (maximum cardinality), L t = 10 (number of TBox axioms). L c = 5, 10 (length of concept expressions), and by increasing the probability P t of generating temporal operators and the probability P g of generating global roles. Fig. 2 shows the runtime for different values of N against LTL solvers that performed well in the toy scenario, namely, NuXMV-SBMC, Aalta, and NuXMV-IC3. For each value of N , the first two columns consider P g = 0.7 and two values for P t = 0.1, 0.9, while the last two columns consider P g = 0.9 and again P t = 0.1, 0.9. For each solver, the first line is the case where L c = 5, while the second has L c = 10. Due to the increase in the number of variables when removing the past operators, as expected solvers perform better on TBoxes expressed with only future operators (i.e., on T N DL-Lite TBoxes) as shown on Lines 3, 4 and 5, with the BMC option performing better than IC3. Increasing P t does not significantly impact the runtime values. This indicates that LTL solvers are less affected by the number of temporal operators than by the number of variables in the formula. For more detail see the full version of the paper [19]. Conclusions. This work investigate the scalability and robustness of LTL solvers while checking TDL-Lite KBs for satisfiability. 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 first-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 [9,11].