Towards Spatio-Temporal Reasoning in Description Logic f-ALC(D)-LTL

Abstract

With the emergence of fuzzy spatio-temporal knowledge, the representation and reasoning of fuzzy spatio-temporal knowledge have become one of the hot research issues in the elds of visual object tracking and GIS [1] [2]. Description logics (DLs), as a formal language of knowledge representation, have been widely used in the elds of computer science and arti cial intelligence [3]. Hence, how to extend DLs to realize the representation and reasoning of fuzzy spatio-temporal knowledge needs to be solved. In this work, we propose a fuzzy spatio-temporal description logic named f-ALC(D)-LTL that extends spatial fuzzy description logic f-ALC(D) [4] with linear temporal logic LTL [5]. In f-ALC(D)-LTL, vagueness is included through the standard Goedel semantics, space through a concrete domain of RCC-8 spacial operators, and time through a sequence of interpretations in the style of LTL connectives. Let C; R; T; I and O be a disjoint set of concept names, abstract roles names, concrete roles names, abstract individual names and fuzzy spatial regions names. Also, let R2 R be an abstract role and T2 T be a concrete role, d 2 fC, DC, P, PP, EQ, O, DR, PO, EC, NTP, TPP, NTTPg [6]. The f-ALC(D)LTL atomic formulas are given by :: = hC1 v C2 ./ ni j hC1(a) ./ ni j hR(a; b) ./ ni j hT (a; o) ./ ni j hd(o1; o2) ./ ni where C1; D1 2 C, R 2 R, T 2 T, a, b 2 I, o; o1; o2 2 O, ./2 f ; >; <; g, n2 [0, 1]. The f-ALC(D)-LTL formulas ' is the smallest set containing the atomic formulas such that: (i) if is an atomic formula, then is an f-ALC(D)-LTL formula; (ii) if '1; '2 are fALC(D)-LTL formulas, then so are :'1, '1, '1 _ '2, '1 ^ '2 and '1U '2, where temporal operators and U mean that next and until, respectively. The semantic interpretation I of f-ALC(D)-LTL can be de ned as an in nite sequence I(0), I(1), , I(w) of fuzzy interpretations (see Fig. 1 for semantic interpretation). De nition 1 (Truth). Given a temporal model M = h=; Ii and arbitrary time point (or state) w 2 W . At time point w, the truth of f-ALC(D)-LTL formulas ' (denoted by (M; w) ') is de ned inductively as follows: (M; w) hC1 v C2 ./ ni i infa24I (C1I(w)(a) ) CI(w)(a)) 2

-

(M; w)

hC1(a) ./ ni i C1I(w)(a) ./ n ? corresponding author

Haitao Cheng, and Zongmin Ma f LA C ( D ) S e m a n ti c s f LA C ( D ) S e m a n ti c s f LA C ( D ) S e m a n ti c s f LA C ( D ) S e m a n it c s 0 1 2 3 Ă time hR(a; b) ./ ni i RI(w)(a; b) ./ n hT (a; o) ./ ni i T I(w)(a; o) ./ n hd(o1; o2) ./ ni i dI(w)(o1; o2) ./ n :' i (M; w) 2 ' '1 _ '2 i (M; w) '1 _ (M; w) '2 '1 ^ '2 i (M; w) '1 ^ (M; w) '2 '1U '2 i 9v > w, 8k 2 (w, v) s.t (M; v) '2 and (M; k) '1 De nition 2 (Satis ability). Let M = h=; Ii be a temporal model. An fALC(D)-LTL formulas ' is satis able i there is a temporal model M such that (M; w0) ', where w0 2 W is an initial state or an initial time point.

The satis ability problem of f-ALC(D)-LTL formulas ' is a basic reasoning problem. Thus, we propose a tableau-based reasoning algorithm for determining satis ability of f-ALC(D)-LTL formula. Our algorithm is based on the tableau algorithm for PLTL proposed by Wolper [ 7 ]. Similar to [ 8 ], our algorithm consists of two phases: (i) tableau construction, and (ii) tableau elimination. The rst phase can obtain a complete tableau by applying a series of tableau rules for a given formula '. The second phase can eliminate some unsatis able nodes of the complete tableau by repeatedly applying elimination rules. We also show the termination, soundness, and completeness of the tableau algorithm using Hintikka structure [ 9 ]. As a result, the satis ability problem of f-ALC(D)-LTL formula ' is decidable.

Technical details and references to relevant work can be found in the full paper: Haitao Cheng, Zongmin Ma. f-ALC(D)-LTL: A Fuzzy Spatio-Temporal Description Logic, In Proceedings of the 10th International Conference on Knowledge Science, Engineering and Management(KSEM 2017), pages 93-105[ 10 ]. This work is supported by National Key R&D Program of China (No.2018YFB1003201), National Natural Science Foundation of China (No.61672296, No.61602261), Major Natural Science Research Projects in Colleges and Universities of Jiangsu Province (No. 18KJA520008), and NUPTSF(No.NY217133).

Towards Spatio-Temporal Reasoning in Description Logic f-ALC(D)-LTL

References

1. Ribaric , S. , Hrkac , T. : A model of fuzzy spatio-temporal knowledge representation and reasoning based on high-level petri nets . Information Systems 37 ( 3 ), 238 { 256 ( 2012 )

2. Cheng, H., Yan , L. , Ma , Z. , Ribaric , S: Fuzzy spatio-temporal ontologies and formal construction based on fuzzy Petri nets . Computational Intelligence 35 ( 1 ), 204 { 239 ( 2019 )

3. Haarslev , V. , Lutz , C. , Moller , R.: A description logic with concrete domains and a role-forming predicate operator . Journal of Logic and Computation 9 ( 3 ), 351 { 384 ( 1999 )

4. Straccia , U. : Towards spatial reasoning in fuzzy description logics . In: FUZZIEEE , pp. 512 { 517 ( 2009 )

5. Manna , Z. , Pnueli , A. : The temporal logic of reactive and concurrent systems ( 1992 )

6. Randell , D.A. , Cui , Z. , Cohn , A.G. : A spatial logic based on regions and connection . In: KR , pp. 165 { 176 ( 1992 )

7. Wolper , P.: The tableau method for temporal logic: An overview . Logique Et Analyse 110 , 119 { 136 ( 1985 )

8. Goranko , V. , Shkatov , D. : Tableau-based decision procedures for logics of strategic ability in multiagent systems . ACM Transactions on Computational Logic 11 ( 1 ), 1 { 51 ( 2009 )

9. Seylan , I. , Jamroga , W. : Coalition description logic with individuals . Electronic Notes in Theoretical Computer Science 262 , 231 { 248 ( 2010 )

10. Cheng, H.T, Ma, Z.M. f-ALC(D)-LTL: A Fuzzy Spatio-Temporal Description Logic . In: KSEM, pp. 93 { 105 ( 2017 )