Interval Temporal Logic

Menu Menu

ITLは時区間によって論理式の真理値が異なる論理である。この論理の意味論(Semantics)の定義には、M(P) meaning fucntion を使う。これによって式の論理値を決めることができる。σ₀は時刻を表し、σ₀...σ_nは時区間を表す。

Mσ0σ1...σn(p)	=	T/F (p は命題変数) 通常はさらに M σ0...σn(p) = M σ0(p) を要求する (変数は時刻にのみ依存する(Locality))
M σ0σ1...σn(P&Q)	=	0≦∃i≦n∧ M σ0...σi(P)∧ M σi...σn(Q), (P,Q は、任意の式)
M σ0σ1...σn(@ P)	=	Mσ1...σn(P) (もしn=0だったF)
M σ0σ...σn(empty)	=	T iff n=0
Mσ0σ1...σn(*P)	=	∃i, 0≦i≦n, Mσ0...σi(P) ∧ (M σi...σn(*P ∨ empty)),
その他、普通の論理の記号(¬,∧,⇒,⇔)を使う。例えば
Mσ0σ1...σn(P ∧ Q)	=	Mσ0...σn(P) ∧ Mσ0...σn(Q)

---

例題

• ◇P ≡ T & P
• □P ≡ ~◇~P
• more ≡ ~ empty
• ○P ≡ @P ∨ empty
• fin(P) ≡T & (P ∧ empty)
• keep(P) ≡□P & @empty
• ◇□P ⇔ □◇P ⇔ fin(P)

---

Tableau expansion of ITL

このtableau methoでは、式を現在時刻と未来の時刻に分割する

T	→	empty∧ T
		more ∧ @T
P&Q	→	empty∧ P∧Q
		(more ∧ more(P)&Q) ∨ ((empty(P)∧empty)&Q)
@P	→	empty∧ F
		more ∧ P

more(P)などは既に分割された式のmore partを指す。

Disjunction を決定的に展開する。それにより、tableu全体を決定的に展開することができる。こうしないと、否定を計算する際に、一旦、tableau のdisjuctive normal formを再計算する必要がある。

P∨Q ⇔ (P)∨(~P∧Q)

また、こうすることにより全体をBDD(2進決定図)で表現することができる。

でも、今の実装は、Prolog baseなのでBDDの利点を真に生かしているとはいいがたい。⇒ C で書き換える? そのためには、すべてのoperation をBDD operation (=論理演算)に書き換える必要がある。