=Paper=
{{Paper
|id=Vol-2954/abstract-25
|storemode=property
|title=Abstracting Temporal ABoxes in TDL-Lite (Extended Abstract)
|pdfUrl=https://ceur-ws.org/Vol-2954/abstract-25.pdf
|volume=Vol-2954
|authors=Sabiha Tahrat,German Braun,Alessandro Artale,Ana Ozaki
|dblpUrl=https://dblp.org/rec/conf/dlog/TahratBAO21
}}
==Abstracting Temporal ABoxes in TDL-Lite (Extended Abstract)==
https://ceur-ws.org/Vol-2954/abstract-25.pdf
Abstracting Temporal ABoxes in TDL-Lite
(Extended Abstract)? ??
Sabiha Tahrat1 , German Braun2 , Alessandro Artale3 , and Ana Ozaki4
1
Université de Paris, France sa.tahrat@gmail.com
2
Universidad Nacional del Comahue, Argentina german.braun@fi.uncoma.edu.ar
3
Free Univ. of Bolzano, Italy artale@inf.unibz.it
4
University of Bergen, Norway ana.ozaki@uib.no
We propose an approach for abstracting temporal ABoxes over temporal DL-
Lite knowledge bases (KBs) [2,3,1,4,12] to improve the reasoning performance
when dealing with large ABoxes. We consider here the logic TDL-Lite(N), i.e.,
N
the fragment of the logic TF P X DL-LiteN bool [3], combining DL-Litebool with LTL,
but with just future temporal operators and thus interpreted over the natural
numbers. Let NC , NI , NG , NL be sets of concept, individual, global role, and local
role names, respectively. The union NG ∪NL is the set NR of role names. TDL-Lite
roles R, basic concepts B, and (temporal) concepts C are given by the following
grammar where L ∈ NL , G ∈ NG , A ∈ NC , and q ∈ N:
R ::= L | L− | G | G− , B ::= ⊥ | A | ≥ qR,
C ::= B | ¬C | C1 u C2 | 3F C | #F C.
A TBox, T , is a set of general concept inclusions (GCI) of the form C1 v C2 ,
where C1 , C2 ∈ NC . An ABox. A, is a set of concept assertions of the form
#n A(a) or #n ¬A(a), or role assertions of the form #n R(a, b) or #n ¬R(a, b),
where a, b ∈ NI , and n ∈ N (with, #0 A(a) = A(a), #n+1 A(a) = # #n A(a)). A
TDL-Lite KB is a pair, K = (T , A). The key idea is to map a TDL-Lite KB into
an equisatisfiable LTL formula by applying the translation described in [3], and
then abstracting large temporal ABoxes by adapting the technique presented
in [9]. Given a TDL-Lite ABox we first shift all role assertions associated to
global roles to time point 0, and call the resulting ABox AG . We then map AG
into A†G a first-order temporal formula with unary predicates, QT L1 (N):
^
A†G = ΦAG ∧ n
(Eq R)(a), (1)
R∈roleT , n R(a,b)∈A
G
where roleT is the set of (global and local) role names occurring in T including
their inverses, ΦAG is the conjunction of all concept assertions in AG , and the
unary predicates Eq R(x), Eq R− (x), for R ∈ NR , capture domain and range
of role R, respectively, with q encoding the number of R-successors of a given
individual. We abstract individuals according to their types. For each individual
a ∈ A†G , its type τ (a) = {#n P | #n P (a) ∈ A†G }. With each type, τ , we associate
a fresh new individual, vτ , the representative of all the individuals in A†G with
type τ , and denote with ΓA† the set of all such representatives. Thus, by using
G
?
Extended version published as arXiv:2008.07463
??
Copyright c 2021 for this paper by its authors. Use permitted under Creative Com-
mons License Attribution 4.0 International (CC BY 4.0).
2 Sabiha Tahrat, German Braun, Alessandro Artale, and Ana Ozaki
TDL-Lite(N) ABox QT L1 (N) ABox Gain
Global Abs.
ABox # Concept # Role ABox Abs. Abs. ABox
Roles ABox
(Sample) Assert. Assert. size Ind. ABox size
Gain size
3 677 052
23 481 3 653 571 1 346 369 80 881 80 881 100 0% 97,8%
(7 027 000)
4 241 783
24 617 4 217 166 1 621 779 82 017 80 369 98 2% 98,1%
(10 500 000)
4 587 504
24 955 4 562 549 1 790 413 82 355 27 150 33 67,03% 99,4%
(15 500 000)
Table 1: Abstraction results for randomly generated ABoxes with number of indi-
viduals, I = 100, time span, T = 5 and N = 50. Each row represents ABox sizes
ranging from 70% up to 90% of the whole ABox space (i.e., 5 025 000 distinct possible
assertions). The first column corresponds to the number of distinct assertions generated
from a sample size counting repetitions written below in parentheses. Global Roles Gain
captures the number of gained assertions due to the shift of global role assertions to
time point 0. The QT L1 (N) ABox columns include the size of the resulting QT L1 (N)
ABox, the size of the abstracted ABox and the number of abstracted individuals. The
last two columns report the percentages of the abstraction gain, and the global gain
considering both the translation and the abstraction of the ABox.
just one representative for each type, we finally generate the (equisatisfiable)
abstraction BG of A†G :
[
BG = Bτ , with Bτ = {#n P (vτ ) | τ = τ (a), #n P ∈ τ } (2)
vτ ∈Γ †
A
G
Experiments on Randomly Generated ABoxes. To evaluate the gain in size of
the ABox after the abstraction, we randomly generate temporal ABoxes from
a space of I individual names, N concept names, N global and N local role
names, while the time point n is chosen within the time interval [0, T − 1] in
accordance with the uniform distribution over the space of N · T · I · (1 + 2I)
possible assertions. Table 1 reports abstraction results on sampled ABoxes with
size varying from 70% up to 90% over the whole ABox space.
We observe a gain of more than 95% in the number of QT L1 (N) ABoxes
assertions compared to the original TDL-Lite(N) ABoxes. This is due to the
translation of roles into pairs of unary predicates, together with the shifting of
global role assertions to the initial time point. Moreover, there is a clear gain
in the number of individuals, specially when the ABox size is close to the ABox
space, confirming experimental results obtained for non-temporal DLs [6,8,9].
Experiments on Randomly Generated TBoxes and ABoxes. To evaluate the run-
time efficiency of reasoning over KBs with an abstracted ABox, we pair a ran-
domly generated TDL-Lite(N) TBox with each of the ABoxes in Table 1. To
generate random TBoxes, we extend the test method proposed by [5] in the con-
text of propositional temporal logic to our case. We guess a TBox given a fixed
number of N concept names, N global role names, and N local role names; a
fixed maximum Q for the value q in basic concepts of the form ≥ qR; a fixed
Abstracting Temporal ABoxes in TDL-Lite (Extended Abstract) 3
TDL-Lite(N) ABox LTL BLACK
abs.
# # abs SAT
ABox tr. abs. SAT
Space abs. abs. tr. time
(Sample) time time time
prop. ind. time (runtime)
(runtime)
3 675 455 546,2 546,2
110 150 100 484,01 62,02 546,03
Prop.Var. (7 027 000) (1 030,21) (1 092,23)
110 150 4 241 783 541,12 546,81
109 334 98 400,08 56,27 457,38
(10 500 000) (941,2) (1 004,19)
ABox Space 4 588 504 545,35 273,3
82 814 33 432,68 3,1 79,65
5 025 000 (15 500 000) (978,03) (352,95)
Table 2: Reasoning results over KBs randomly generated with I = 100, T = 5 and
N = 50, and with abstracted ABoxes. Each row represents ABox sizes ranging from
70% up to 90% of the whole ABox space. LTL columns include the resulting number
of propositional variables after the abstraction, the size of the abstracted individuals,
the translation time (from the original TDL-Lite(N) KB to LTL), the time spent to
calculate the abstraction, and the translation time on the abstracted KB. The last two
columns show the runtime efficiency by comparing the runtime of BLACK on KBs with-
out or with ABox abstraction. Time is in seconds and ‘runtime’ includes translation.
number Lt of GCIs in a TBox; and a fixed value Lc of the length of concept. The
guessed TBox for Table 2 has the following parameters: N = 50, Lc = 5, Q = 3,
while the value of Lt is set close to 3 · N so that all concept and role names are
considered in guessing the TBox (when Lc = 5 three names are at most chosen
from a space of 3 · N and we have at most 2 · 3 = 6 names considering both
the right and left hand sides of each GCI). The resulting KB is translated into
LTL resulting in a formula with 110 150 propositional variables (this number
depends only on the size of the TBox and on the number of individuals). Table 2
reports reasoning results on such abstracted KBs using the tableaux based LTL
solver BLACK [7]. We can observe that there is a notable gain in the number of
propositional variables after the abstraction (# abs. prop.), in particular when
the gain on individuals is high. The total runtime, indicated in parentheses, and
including both the translation and the satisfiability checking time, is around 10
minutes for each satisfiability check. The abstraction improves sensibly the rea-
soner performances. The translation time for processing the largest instance was
reduced from 432 to 79 seconds due to the 67% gain on individuals, while the
satisfiability checking time reduced from 545 to 273 seconds. For more details,
see the full version of the paper [11].
Conclusions. We proposed an approach for abstracting temporal ABoxes which
shows good results when increasing the number of ABox assertions in randomly
generated KB to values close to the ones observed in realistic (static) ontologies,
being able to process temporal KBs with millions of assertions. We confirmed the
results of this approach by comparing the runtimes of reasoning with ABoxes
vs abstracted ABoxes by showing significant savings. As a future work, one
can consider the feasibility of pairing the abstraction technique with parallelised
reasoning algorithms, splitting the parallel processes according to the abstracted
individuals, in the lines of what has already been experimented in [10].
4 Sabiha Tahrat, German Braun, Alessandro Artale, and Ana Ozaki
References
1. A. Artale, R. Kontchakov, A. Kovtunova, V. Ryzhikov, F. Wolter, and M. Za-
kharyaschev. Temporal ontology-mediated querying: A survey. In 24th Interna-
tional Symposium on Temporal Representation and Reasoning (TIME17), Mons,
Belgium, October 2017.
2. A. Artale, R. Kontchakov, A. Kovtunova, F. Wolter, and M. Zakharyaschev. First-
order rewritability of temporal ontology-mediated queries. In Proc. of the 24th Int.
Joint Conference on Artificial Intelligence (IJCAI-15), Buenos Aires, Argentina,
25-31 July, 2015. AAAI Press.
3. 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.
4. A. Artale, A. Mazzullo, and A. Ozaki. Temporal DL-Lite over finite traces (pre-
liminary results). In 32nd Int. Workshop on Description Logics, (DL’19), Oslo,
Norway, 18-21 June, 2019.
5. M. Daniele, F. Giunchiglia, and M. Y. Vardi. Improved automata generation for
linear temporal logic. In CAV, 1999.
6. A. Fokoue, A. Kershenbaum, L. Ma, E. Schonberg, and K. Srinivas. The summary
ABox: Cutting ontologies down to size. In Proc. of the 5th Int. Semantic Web
Conference, ISWC-06, volume 4273 of Lecture Notes in Computer Science, pages
343–356. Springer, 2006.
7. L. Geatti, N. Gigante, and A. Montanari. A sat-based encoding of the one-pass
and tree-shaped tableau system for LTL. In Automated Reasoning with Analytic
Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019,
Proceedings, volume 11714 of Lecture Notes in Computer Science, pages 3–20.
Springer, 2019.
8. B. Glimm, Y. Kazakov, T. Liebig, T. Tran, and V. Vialard. Abstraction refine-
ment for ontology materialization. In Proceedings of the International Semantic
Web Conference (ISWC’14), volume 8797 of Lecture Notes in Computer Science.
Springer, 2014.
9. 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.
10. A. Steigmiller and B. Glimm. Parallelised ABox reasoning and query answer-
ing with expressive description logics (extended abstract). In S. Borgwardt and
T. Meyer, editors, Proc. of the 33rd Int. Workshop on Description Logics (DL
2020), volume 2663 of CEUR Workshop Proceedings. CEUR-WS.org, 2020.
11. S. Tahrat, G. Braun, A. Artale, M. Gario, and A. Ozaki. Automated reasoning in
temporal DLite. arXiv, arXiv:2008.07463, 2020.
12. S. Tahrat, G. A. Braun, A. Artale, M. Gario, and A. Ozaki. Automated reasoning
in temporal DL-Lite (extended abstract). In Proceedings of the 33rd International
Workshop on Description Logics (DL 2020), volume 2663 of CEUR Workshop
Proceedings. CEUR-WS.org, 2020.