null

第4章時相論理
4～4,1,1
H28.07.07
荒木研M1 綿貫凌
1
導入
• 時相論理とは、時間との関連で問題を表現するための規
則と表記法の体系である。
• 様相論理と呼ばれる論理体系に属する。様相論理とは、
基本的な論理体系に、必然性･可能性、義務、時間と
いった命題の真偽の様相にかかわる構成要素を付け加え
て拡張した論理体系である。
• 非時相論理では、時間変化によって真偽値が変化しない
文しか扱えない。すなわち、静的な性質、動作中の個々
の時刻における状態に関する性質しか記述できない。
• →時間変化によって真偽値が変化する文、動的な性質、
動作中に刻々と変化するシステムの状態に対し、時間に
応じた静的な性質の成否を記述できる必要がある。
2
導入
• 扱う時間モデルについて
・離散時間を扱う。=各時刻について直前と直後の時刻が
存在し、整数値で表現できる時間パラメータに基づく。
・時間を区間ではなく、点として取り扱い、各瞬間の命題
の真偽を扱う。
・未来に関する時間のみを扱う。
• 次時刻での命題の真偽値が、決定的に決まる線形時間モ
デルと、非決定的に決まる分岐時間モデルがある。
3
4,1 命題線形時相論理PLTL
• 命題線形時相論理(Propositional Linear Temporal Logic)
• ∧,∨,￢,→等の論理演算子と、時間に関する性質を表現
する基本演算子、F(将来いつか、Finally),G(今後常に、
Globally),X(次の時刻で、neXt),U(ある時間まで、Until)から
構成される。
• 命題変数、命題定数は論理式(原子論理式)である。
• φ,ψが論理式のとき、(￢φ),(φ∧ψ),(φ∨ψ),(φ→ψ),(φ↔ψ),
(Xφ),(Gφ),(Fφ),(φUψ),(φRψ)は論理式である。
• 以上がPLTLの論理式の全てである。
• 結合順序はGとFが￢と同じ、UとRが∨や∧と同じである。
• 例:GA∧Bとは、(GA)∧Bであり、G(A∧B)
4
4,1 命題線形時相論理PLTL
• p:「私は空腹である」
文の意味自体は一定であるが、真偽は時間経過によって
変化する。同時に真であり偽でもあるということは無い。
• Xp:次の時刻でpが必ず成立する。next time p
「私は次の時刻で空腹になる」
• Fp:将来いつか必ずpが成立する。sometimes p,eventually p
「私はそのうち空腹になる」
• Gp:今後常にpが成立する。always p,globally p
「私はいつも空腹である」
• pUq:qがいつか必ず成立し、その前までの間pが成立する。
qが最初から成立している場合は、pの成否にかかわらず、
成立する。p until q
「私はドーナツを食べるまで空腹である」
5
4,1 命題線形時相論理PLTL
t
Xp
t+1
p
pUq
t+3
t+4
t+5
p
p
Fp
Gp
t+2
p
p
p
p
p
p
p
p
p
q
p
p
p
q
p
t+9
p
t+10
q
FGp
p
G(p→Fq)
t+6
t+7
q
t+8
p
t+11
FGp:「私はいつか空腹になり、以降ずっと空腹である」
G(p→Fq):「私はいつも、一旦空腹になると、いつかドーナツ
を食べる」(※注意良い例思いつかず)
6
4,1 PLTLの意味論
• PLTLの意味論を定義するために、原子論理式の真偽の時
間的変化を表現する、クリプキ構造(Kripke structure)と呼
ばれる数学的構造を定義する。クリプキ構造は以下の３
つの要素の組M=〈S,R,L〉で定義される。
• S:非空な状態の有限集合
• R⊆S×S:状態集合上の二項関係
• L:S→2PV:PV(Proposition Variable)を命題変数の集合としたと
き、各状態で真になる命題変数の集合を与える。=ラベ
リング関数
• 任意の状態s∈Sに対して、R(s,s’)となるようなs’∈Sが存在
するとき、sからs’への遷移が存在すると考える。
• 二項関係Rにおいて、常に∀s∃s’R(s,s’)が成立するとき、
Rを「全域的(total)」であるという。以降では、二項関係
Rは全域的なもののみを扱う。
7
4,1 例4.1
getParts
composing
finished
shipping
removed
1,部品を用意(getParts)
2,組み立て(composing)
3,完成(finished)
4,出荷準備(shipping)
1と3では検査を実施し、不合格の場合、取り除く。
8
4,1 例4.1
• 命題変数の集合をPV={productExists,composingProduct}と
する。
productExists:完成した製品が存在する。
composingProduct:製品を組み立て中である。
• L(getParts)=L(removed)={}
• L(composing)={composingProduct}
• L(finished)=L(shipping)={productExists}
• (この例は例4.6にも登場する)
9
4,1 PLTLの意味論
• クリプキ構造の状態s0から始まる無限長の経路を
σ=s0s1...sisi+1... ∀i(si,si+1)∈R
とし、ここで、σ(i)はσにおけるi番目の状態を表す。
• クリプキ構造Mの経路σの状態iについてPLTL式iが成り立
つことを、M,σ,i⊨φと表す。(Mが明らかなときは省略可)
• 本意味論の特徴は、(複数の)初期状態が存在し、(計算の)
経路は無限(繰り返しを含む)、というものである。
10
4,1 PLTLの意味論
• PLTLの意味論は、クリプキ構造M=〈S,R,L〉を用いて次の
ように表される。
• ①p∈PVのとき、M,σ,i⊨p⇔p∈L(σ(i))
• ②M,σ,i⊨￢φ⇔M,σ,i⊭φ
(cf.トートロジー)
• ③M,σ,i⊨φ∧ψ⇔M,σ,i⊨φかつM,σ,i⊨ψ
(∧の定義)
(∨、→は省略)
• ④M,σ,i⊨Xφ⇔M,σ,i+1⊨φ
• ⑤M,σ,i⊨Gφ⇔任意の整数jに対しi≦jならばM,σ,j⊨φ
• ⑥M,σ,i⊨Fφ⇔ある整数kが存在しi≦kかつM,σ,k⊨φ
• ⑦M,σ,i⊨φUψ⇔ある整数kが存在しi≦kかつM,σ,k⊨ψかつ、
任意の整数jに対しi≦j<kならばM,σ,j⊨φ
• ④～⑦は時間演算子の説明に他ならない。
11
4,1 例4.2
• 例4.1において、3つの経路
σ1:getParts composing finished shippedの繰り返し
σ2:getParts composing finished removedの繰り返し
σ3:getParts removedの繰り返し
繰り返しとは、σ1については、σ1(4i)=getParts,
σ1(4i+1)=composing,σ1(4i+2)=finishd,σ1(4i+3)=shipped
(i=0,1,2,...)
• このとき、φ1:F productExists,
φ2:￢productExists U composingProduct,
φ3:G(productExists→F(composingProduct))に対して、
M,σ1,0⊨φ1, M,σ1,0⊨φ2, M,σ1,0⊨φ3, M,σ2,0⊨φ1,
M,σ2,0⊨φ2, M,σ2,0⊨φ3, M,σ3,0⊨φ3が成り立つ。
M,σ3,0⊨φ1, M,σ3,0⊨φ2は成り立たない。
12
(※テキストでは、M,σ1,0⊨φ2がふたつ存在する。おそらく
誤植である。
4,1 例4.2
• M,σ1,0⊨φ1 M,σ1,0⊨φ2 M,σ2,0⊨φ1 M,σ2,0⊨φ2は自明。
M,σ1,0⊨φ3 M,σ2,0⊨φ3,は繰り返しであることから。
M,σ3,0⊨φ3,は→の定義より。
• M,σ3,0⊨φ1,M,σ1,0⊨φ1は背理法より。状態iについて命題論
理が成立すると仮定する。
13
4,1 PLTLの意味論
• PLTLの論理式が、あるクリプキ構造M、経路σ、非負整数
iに対してM,σ,i⊨φが成立する場合、φは充足可能である。
全てのM,σ,iに対してM,σ,i⊨φが成立する場合、φは恒真で
あるといい、⊨φと書く。
• 恒真な式
⊨G(p∧q)→Gp∧Gq
⊨Gp→GGp
⊨Fp↔trueUp
⊨Gp↔￢F￢p
⊨Gp→p
⊨Gp→Fp
⊨Xp→Fp
⊨Gp→XGp
14

Download Report