=Paper=
{{Paper
|id=Vol-2663/abstract-22
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-2663/abstract-22.pdf
|volume=Vol-2663
|dblpUrl=https://dblp.org/rec/conf/dlog/TahratBAGO20
}}
==None==
https://ceur-ws.org/Vol-2663/abstract-22.pdf
Automated Reasoning in Temporal DL-Lite
(Extended Abstract)?
Sabiha Tahrat1 , German Braun2 ,
Alessandro Artale3 , Marco Gario3 , and Ana Ozaki4
1
Université de Paris, France sabiha.tahrat@parisdescartes.fr
2
Universidad Nacional del Comahue, Argentina german.braun@fi.uncoma.edu.ar
3
Free Univ. of Bolzano, Italy artale@inf.unibz.it, marco.gario@gmail.com
4
University of Bergen, Norway Ana.Ozaki@uib.no
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 con-
sider here the TF P X DL-LiteNbool 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 equisatisfi-
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 trans-
lation 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
LTLP denotes LTL extended with past operators and interpreted over Z).
Theorem 1. Let ϕ be a LTLP formula, then, ϕ is satisfiable iff its LTL trans-
lation ϕ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 propo-
sitional variables, we also introduce the simpler logic, called TN 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 PSpace-
complete [2]. To put these results in practice, we provide a tool, named crowd-ERVT 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
?
Copyright ©
2020 for this paper by its authors. Use permitted under Creative
Commons License Attribution 4.0 International (CC BY 4.0).
5
crowd.fi.uncoma.edu.ar/ervt-gui/erd_editor.php
2 Tahrat et. al
SAT UNSAT
Aalta
pltl (graph)
pltl (tree)
NuXMV-BDD
NuXMV-SBMC 60
NuXMV-SBMC 20
NuXMV-IC3
TRP++(BFS)
TRP++(DFS)
Fig. 1: Heat maps with TBox from Ex. 1. Each rectangle represents the runtime in
CPU seconds of SAT and UNSAT KBs with different ABox sizes on different LTL
solvers. The runtimes colours are as follows:
< 0.01 sec > 0.01 sec, ≤ 0.25 sec > 0.25 sec, ≤ 0.50 sec > 0.50 sec, ≤ 1 sec > 1 sec, ≤ 2 sec
> 2 sec, ≤ 4 sec > 4 sec, ≤ 8 sec > 8 sec, ≤ 16 sec > 16 sec, ≤ 32 sec > 32 sec, ≤ 64 sec
> 64 sec, ≤ 125 sec > 125 sec, ≤ 250 sec > 250 sec, ≤ 500 sec > 500 sec, ≤ 1000 sec T/O, OoM or Fail
reasoners [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 sce-
nario 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 p1 ’s name is functional and global:
T = {Person v≥ 1 Name, Person v ¬ ≥ 2 Name}
A = {Person(p1 , 0), Name(p1 , n1 , 0), Name(p1 , n2 , 1)}
Depending on the different sizes of the tested ABoxes, the number of propo-
sitional 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 satisfia-
bility 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 scal-
ability 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
Automated Reasoning in Temporal DL-Lite (Extended Abstract) 3
1 concept 3 concepts 5 concepts
Lc = 5
NuXMV-SBMC
Lc = 10
Aalta
Aalta + Future
NuXMV-SBMC + Future
NuXMV-IC3 + Future
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 param-
eters: N = 1, 3, 5 (number of concept names), Q = 5 (maximum cardinality),
Lt = 10 (number of TBox axioms). Lc = 5, 10 (length of concept expressions),
and by increasing the probability Pt of generating temporal operators and the
probability Pg 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 Pg = 0.7 and two values for Pt = 0.1, 0.9, while the last two columns
consider Pg = 0.9 and again Pt = 0.1, 0.9. For each solver, the first line is the
case where Lc = 5, while the second has Lc = 10. Due to the increase in the
number of variables when removing the past operators, as expected solvers per-
form better on TBoxes expressed with only future operators (i.e., on TN DL-Lite
TBoxes) as shown on Lines 3, 4 and 5, with the BMC option performing better
than IC3. Increasing Pt 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 run-
time 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. Fur-
thermore, we plan to extend to the temporal case the existing ABox abstraction
approaches which are successfully applied over OWL ontologies [9,11].
4 Tahrat et. al
References
1. A. Artale and E. Franconi. Temporal description logics. In Handbook of Temporal
Reasoning in Artificial Intelligence, pages 375–388. Elsevier, 2005.
2. A. Artale, R. Kontchakov, V. Ryzhikov, and M. Zakharyaschev. A cookbook for
temporal conceptual data modelling with description logics. ACM Trans. Comput.
Log., 15(3):25:1–25:50, 2014.
3. A. Artale, A. Mazzullo, and A. Ozaki. Do you need infinite time? In IJCAI, 2019.
4. F. Baader, S. Ghilardi, and C. Lutz. LTL over description logic axioms. ACM
Trans. Comput. Log., 13(3), 2012.
5. G. A. Braun, L. A. Cecchi, and P. R. Fillottrani. Taking advantages of automated
reasoning in visual ontology engineering environments. In Proc. of the Joint On-
tology Workshops 2019 Episode V: The Styrian Autumn of Ontology (JOWO’19),
2019.
6. G. A. Braun, C. Gimenez, L. A. Cecchi, and P. R. Fillottrani. crowd: A visual tool
for involving stakeholders into ontology engineering tasks. Künstl Intell (2020),
2020.
7. R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover,
M. Roveri, and S. Tonetta. The NuXMV symbolic model checker. In 26th Int.
Conf. on Computer Aided Verification, (CAV), volume 8559 of Lecture Notes in
Computer Science, pages 334–342. Springer, 2014.
8. M. Daniele, F. Giunchiglia, and M. Y. Vardi. Improved automata generation for
linear temporal logic. In CAV, 1999.
9. A. Fokoue, F. Meneguzzi, M. Sensoy, and J. Z. Pan. Querying linked ontological
data through distributed summarization. In J. Hoffmann and B. Selman, editors,
Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence. AAAI
Press, 2012.
10. D. M. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis
of fairness. In Conference Record of the 7th ACM Symposium on Principles of
Programming Languages (POPL’80), page 163–173. ACM Press, 1980.
11. B. Glimm, Y. Kazakov, and T. Tran. Scalable reasoning by abstraction beyond
DL-Lite. In M. Ortiz and S. Schlobach, editors, Web Reasoning and Rule Systems
(RR) - Proceedings of the 10th International Conference, volume 9898 of Lecture
Notes in Computer Science, pages 77–93. Springer, 2016.
12. U. Hustadt and B. Konev. TRP++2.0: A temporal resolution prover. In Automated
Deduction - CADE-19, 19th International Conference on Automated Deduction,
Proceedings, pages 274–278, 2003.
13. U. Hustadt, A. Ozaki, and C. Dixon. Theorem proving for metric temporal logic
over the naturals. In CADE, pages 326–343, 2017.
14. J. Li, S. Zhu, G. Pu, L. Zhang, and M. Y. Vardi. Sat-based explicit LTL reasoning
and its application to satisfiability checking. Formal Methods Syst. Des., 54(2):164–
190, 2019.
15. C. Lutz, F. Wolter, and M. Zakharyaschev. Temporal description logics: A survey.
In Proc. of the 15th Int. Symposium on Temporal Representation and Reasoning,
TIME’08, pages 3–14. IEEE Computer Society, 2008.
16. N. Markey. Temporal logic with past is exponentially more succinct. Bulletin of
the EATCS, 79:122–128, 2003.
17. V. Schuppan. Extracting unsatisfiable cores for LTL via temporal resolution. In
C. Sánchez, K. B. Venable, and E. Zimányi, editors, 2013 20th International Sym-
posium on Temporal Representation and Reasoning, Pensacola, FL, USA, Septem-
ber 26-28, 2013, pages 54–61. IEEE Computer Society, 2013.
Automated Reasoning in Temporal DL-Lite (Extended Abstract) 5
18. S. Schwendimann. A new one-pass tableau calculus for PLTL. In H. de Swart,
editor, Automated Reasoning with Analytic Tableaux and Related Methods, pages
277–291. Springer Berlin Heidelberg, 1998.
19. S. Tahrat, G. Braun, A. Artale, M. Gario, and A. Ozaki. Automated reasoning in
temporal DLite. arXiv, To be done, 2020.