多维模态逻辑的应用 ——时空推理及其判定性问题

Presentation on theme: "多维模态逻辑的应用 ——时空推理及其判定性问题"— Presentation transcript:

1 多维模态逻辑的应用 ——时空推理及其判定性问题
徐召清

2 目录 一、简介 二、基于区域的空间逻辑 三、基于时间点的时空逻辑 四、基于时间区间的时空逻辑 五、参考文献

3 一、简介

4 时空逻辑 时空逻辑=时间逻辑+空间逻辑 基于区域的空间逻辑 基于时间点和空间区域的时空逻辑 基于时间区间和空间区域的时空逻辑

5 二、基于区域的空间逻辑

6 二、基于区域的空间逻辑 1、区域连接演算：RCC C(X,Y), 其直观意思是“区域X和区域Y相连”。

7 定义谓词

8 定义谓词（续）

9 RCC-拓扑语义

10 2、RCC-8

11 RCC-8拓扑语义

12 3、 BRCC-8 RCC-8的扩张，允许对区域变元进行布尔运算：⊔，⊓，¬。

13 区域项的定义及解释

14 4、模态逻辑S4u 基本模态语言+全局算子■，◆。 其中， ■ φ=¬◆¬φ。

15 S4u-语义

16

17 约定： 以下，分别用I和C代表□和◇，∀和∃代表■和◆。

18 5、将BRCC-8嵌入S4u 定义BRCC-8公式到S4u的翻译·Δ如下：

19

20

21 S4u的两个例子：

22 6、BRCC-8的判定性问题 利用前面的定理4，可以得到： 推论1：BRCC-8公式的可满足性问题是可判定的。 推论2：RCC-8公式的可满足性问题是可判定的。

23 7、BRCC-8和RCC-8的计算复杂性 通过进一步将BRCC-8嵌入S5，可以证明BRCC-8和RCC-8都是NP-完全的。

24

25

26 定理6：任给BRCC-8公式φ，φΔ在类锯上可满足当且仅当φ⊙是S5-可满足的。

27 定理7：SAT(BRCC-8)是NP-完全的。
定理8：SAT(RCC-8)是NP-完全的。

28 三、基于时间点的时空逻辑

29 三、基于时间点的时空逻辑 1、线性时间逻辑PTL 语言：U，S。 模型：𝔐=(ℕ ,<,V)。真值定义：
𝔐,n|=φUψ当且仅当存在m>n使得𝔐,m|=ψ，并且对任意k，如果n<k<m，则𝔐,k|=φ； 𝔐,n|=φSψ当且仅当存在m<n使得𝔐,m|=ψ，并且对任意k，如果m<k<n，则𝔐,k|=φ。

30 定义算子o, F, G, P, H, 𝒲如下： oφ= ⊥Uφ; Fφ=ΤUφ; Gφ=¬F¬φ; Pφ=ТSφ; Hφ=¬P¬φ; φ𝒲ψ=Gφ∨(φUψ).

31 定理9：PTL是可判定的。 定理10：PTL是PSPACE-完全的(Sistla and Clarke, 1985)。

32 2、时空逻辑 时空逻辑=时间逻辑+空间逻辑 RCC-8+PTL：ST0⊆ST1⊆ST2； BRCC-8+PTL：ST0+⊆ST1+⊆ST2+。

33 (1) ST0 语言：RCC-8的语言加U，S算子。 公式： 所有RCC-8公式都是ST0公式； 如果φ，ψ是ST0公式，则φUψ，φSψ，¬φ，φ∧ψ也是。 可以如常定义F，G，P，H，o，𝒲等。

34 ST0-语义 定义10：拓扑时间模型（topological temporal model，tt-model）是三元组(𝔗, 𝔑, 𝔞)，其中𝔗 =(U,𝕀)是拓扑空间，𝔑=(ℕ,<)是时间框架，𝔞是赋值，对每个区域变元X和时间点n∈ℕ，𝔞(X,n)非空且是U的正规封闭子集。对每个的n，记函数𝔞n(X)=𝔞(X,n)为𝔞n。

35 ST0-语义（续） 定义11：任给tt-模型𝔐=(𝔗, 𝔑, 𝔞)，ST0公式φ，和n∈ℕ，递归定义满足关系如下：
如φ不含时间算子，则(𝔐,n)|=φ 当且仅当𝔗|= 𝔞n φ； 𝔐,n|=φUψ 当且仅当存在m>n，使得𝔐,m|=ψ，且对所有k，如果n<k<m，则𝔐,k|=φ； 𝔐,n|=φSψ 当且仅当存在m<n，使得𝔐,m|=ψ，且对所有k，如果n<k<m，则𝔐,k|=φ。

36 （2）ST1 ST0的扩张，允许区域项加o算子： 其语义解释是：𝔞(ot,n)= 𝔞(t,n+1)。

37 （3）ST2 ST1的扩张，允许区域项加任意时间算子： 其语义解释是： 𝔞(Gt,n)=ℂ𝕀(⋂k>n 𝔞(t, k)); 𝔞(Ft,n)=ℂ𝕀(⋃k>n 𝔞(t, k)); 𝔞(Ht,n)=ℂ𝕀(⋂k<n 𝔞(t, k)); 𝔞(Pt,n)=ℂ𝕀(⋃k<n 𝔞(t, k)); 𝔞(t1Ut2,n)=ℂ𝕀{x|∃m>n(x∈𝔞(t2,m)∧∀k(n<k<m →x∈𝔞(t1,k)))}; 𝔞(t1St2,n)=ℂ𝕀{x|∃m<n(x∈𝔞(t2,m)∧∀k(m<k<n →x∈𝔞(t1,k)))}; 𝔞(t1𝒲t2,n)= ℂ𝕀(⋂k>n 𝔞(t, k))∪ℂ𝕀{x|∃m>n(x∈𝔞(t2,m)∧∀l(n<l<m →x∈𝔞(t1,l)))}.

38 （4）STi+ STi+= STi —RCC-8+BRCC-8，其中i=0，1，2； 相应的语义解释只需增加： 𝔞(t1⊔t2)=ℂ𝕀(𝔞(t1)∪𝔞(t2))= 𝔞(t1)∪𝔞(t2); 𝔞(t1⊓t2)=ℂ𝕀(𝔞(t1)∩𝔞(t2)); 𝔞(¬t)=ℂ𝕀(U- 𝔞(t)).

39 ⋃n=1→∞[1/n,1-1/n]=(1,0); ⋂n=1→∞[-1/n,1/n]=(1,0)。 FCA： 没有区域无限次地变化其空间轮廓。 FSA： 每个区域都只有有穷多的可能状态（虽然可以无限次改变其状态）。

40 3、将ST2+嵌入PSTL （1）PSTL PSTL=S4u×PTL。 语言：U，S，C，I，∀，∃。

41 PSTL-Kripke语义

42 PSTL-拓扑语义

43 定理11：任意PSTL-公式φ，φ在克里普克模型(𝔉,ℕ,𝔙)中可满足，则φ在拓扑模型中可满足。
FCp↔CFp。

44 定理12：任意PSTL-公式φ，φ在满足FSA的克里普克模型(𝔉,ℕ,𝔙)中可满足，当且仅当φ在满足FSA的拓扑模型中可满足。

45 (ot)Δ=CIotΔ, (Ft)Δ=CIFtΔ, (Gt)Δ=CIGtΔ .
（2）将ST2+嵌入PSTL 定义14：只需对带时间算子的项t定义翻译如下： (t1Ut2)Δ=CI(t1ΔUt2Δ); (t1St2)Δ=CI(t1ΔSt2Δ). 对定义算子，也有： (ot)Δ=CIotΔ, (Ft)Δ=CIFtΔ, (Gt)Δ=CIGtΔ .

46 定理13： ST2+公式φ在满足FSA条件的tt-模型上可满足，当且仅当φΔ在PSTL的克里普克模型（也满足FSA条件）上可满足，其基于的S4-框架是类锯（即，深度≤1，宽度≤2）； ST1+公式φ在tt-模型上可满足，当且仅当φΔ在PSTL的克里普克模型上可满足，其基于的S4-框架是类锯（即，深度≤1，宽度≤2）。

47 STi和STi+的计算复杂性 SAT(ST0)是PSPACE-完全的（与PTL相同）；
SAT(ST1)是EXPSPACE可判定的。如果只有时间算子o，则是NP-完全的； 如果将模型限制为满足FSA条件的模型，SAT(ST2)也是EXPSPACE可判定的； STi+和相应的STi计算复杂性一样。

48 四、基于时间区间的时空逻辑

49 四、基于时间区间的时空逻辑 1、All-13

50 ∀x,y∈𝔞(i)∀z∈W(x<z<y →z∈𝔞(i)).
All-13的语义 令𝔉=(W,<)为严格线序，实际应用中的严格线序往往是(ℕ,<)，(ℚ,<)，(ℝ,<)。赋值𝔞将每个变元i，映射到𝔉上的时间区间（任意非空凸集），即𝔞(i)是W的非空子集，且 ∀x,y∈𝔞(i)∀z∈W(x<z<y →z∈𝔞(i)).

51 All-13的语义（续）

52 对All-13进行扩充，可以得到表达力更强的语言，比如：
Holds(P, i)，性质P在区间i中保持； OCCURS(E,i)，事件E发生在区间i中。

53 (2)将All-13嵌入GH 首先，为了简便，定义记号□p=Hp∨p∨GH; ◇p=Pp∨p∨Fp。 定义All-13公式φ到GH公式φ#的翻译·#如下：

54

55 All-13的判定性问题 定理14：任意严格线序上的All-13公式的可满足性问题是NP-完全的。

56 2、ARCC-8（BRCC-8+All-13） （1）ARCC-8 语法：BRCC-8+All-13，加Holds(φ,i)，其中，φ是BRCC-8公式。

57 𝔐|= Holds(φ,i)当且仅当对所有的u∈𝔞(i)，𝔗|=αu φ。
ARCC-8语义 定义16：it-模型（interval topological model）是三元组𝔐=(𝔉,𝔗,𝔞)，其中𝔉=(W,<)是严格线序，𝔗=(U,𝕀)是拓扑空间，𝔞是赋值，对每个区间变元i，𝔞(i)是𝔉中的非空凸集，对每个区域变元X和每个时间点u，𝔞(X,u)是𝔗的正规闭集。 对Holds(φ,i)的定义如下： 𝔐|= Holds(φ,i)当且仅当对所有的u∈𝔞(i)，𝔗|=αu φ。

58 （2）将ARCC-8嵌入PSTL 结合·Δ和·#可以将ARCC-8嵌入PSTL。通过组合All-13和BRCC-8的可满足性的算法，进一步可以证明： 定理15：SAT(ARCC-8)是NP-完全的。

59 五、参考文献 [1] Gabbay D.M, Kurucz A, Wolter F, Zakharyaschev. Many-dimensional modal logics: Theory and Applications, Elsevier, North-Holland, 2003. [2] Bennett B, Cohn G, Wolter F, Zakharyaschev. M. “Multi-Dimensional modal logic as a framework for spatio-temporal reasoning”, Applied Intelligence, 2002,3(4):239~251. [3] Wolter F, Zakharyaschev F. Spatio-Temporal representation and reasoning based on RCC-8. In: Cohn AG, Giunchiglia F, Selman B, eds. Proc. of the 7th Conf. on Principles of Knowledge Representation and Reasoning. Breckenridge: Morgan Kaufmann, ~14. [4] I. Hodkinson, F. Woter, and M. Zakaryaschev. “Decidable fragments of first-order temporal logics”, Annals of Pure and Applied Logic, vol. 106, pp. 85–134, 2000. [5] 刘大有，胡鹤，王生生，谢琦：《时空推理研究进展》，《软件学报》vol.15，No.8，2004。

60 Thank You !