様相論理と時相論理
Kripke 構造 K = S, R, L S: 状態の集合 ( 無限かもしれない ) R: 状態間の遷移関係 R S S L: 状態から命題記号の集合への写像 L(s) は 状態 s S において成り立つ命題記号の集合を与える
Kripke 構造 K = S, R, L G = S, R 有向グラフ
Kripke 構造 K = S, R, L L : S 2 Atom Atom : 命題記号の全体 P Atom = {P, } P, P
様々な Kripke 構造 木 P 森 無限木 P, P, P
様相論理式 ϕ, ψ ::= P 命題記号 ϕ 否定 ϕ ψ 連言 ϕ ψ 選言 ϕ 必然 ϕ 可能
意味論 s = P iff P L(s) s = ϕ iff not s = ϕ s = ϕ ψ iff s = ϕ and s = ψ s = ϕ ψ iff s = ϕ or s = ψ s = ϕ iff t = ϕ for any t s.t. R(s, t) s = ϕ iff t = ϕ for some t s.t. R(s, t) ϕ は ϕ に同値
意味論 (P ) P P P, P
で成り立っているのは? 1. 2. (P ) 3. P P P, P
で成り立っているのは? 1. 2. (P ) 3. P P P, P
で は成り立っている? 1. Yes 2. No P Yes 0% 0% No P, P
様々な様相論理 以上は最小様相論理 K 遷移関係を限定 反射的 T / 推移的 K4 再帰的な命題 計算木論理 様相 µ 計算 多重の様相 様相 ( 遷移関係 ) の演算 ブール論理 動的論理 グラフ上の経路による解釈 線形時間時相論理 グラフを木に限定
充足可能性と有限モデル性 様相論理式 ϕ が充足可能 あるKripke 構造 K とその状態 s が存在して s = ϕ K を ϕ のモデルという 最小論理においては 充足可能な論理式は有限モデルを持つ しかも 有限の木モデルを持つ
様相論理の木モデル性 一般に Kripke 構造 ( グラフ ) をノード s から展開すると ( 無限の ) 木が得られる s において論理式が充足可能ならば 展開した木の根においても充足可能 P s s P P, P, P, P P
時相論理 (Temporal Logic) 状態の遷移や時間の経過の観点よりシステムの性質を記述するための論理体系 線形時間時相論理 LTL(Linear Time Temporal Logic) 分岐時間時相論理 CTL(Computation Tree Logic) μ 計算 (µ-calculus) モデル検査 時相論理で表現された性質をシステムが満たすかどうかを検査すること
例 :Peterson のアルゴリズム me = 0, 1 you = 1, 0 for (;;) { flags[me] = true; turn = you; while (flags[you] == true) { if (turn!= you) break; } // the critical section flags[me] = false; // the idle part }
Peterson のアルゴリズム 0: flags[me] = true; 1: turn = you; 2: if (flags[you]!= true) goto 4; 3: if (turn!= you) goto 4; else goto 2; 4: critical section; 5: flags[me] = false; 6: either goto 6 or goto 0; 状態 :(pc0, pc1, flags[0], flags[1], turn) pc0, pc1: 0..6 flags[0], flags[1]: {true, false} turn: {0, 1}
(pc0, pc1, flags[0], flags[1], turn) = (2,2,t,t,1) から遷移可能な状態は? 1. (2,4,t,t,1) 2. (3,2,t,t,1) 3. (4,2,t,t,1) 0: flags[me] = true; 1: turn = you; 2: if (flags[you]!= true) goto 4; 3: if (turn!= you) goto 4; else goto0% 2; 4: critical section; 5: flags[me] = false; 6: either goto 6 or goto 0; 0% 0% (2,4,t,t,1) (3,2,t,t,1) (4,2,t,t,1)
(pc0, pc1, flags[0], flags[1], turn) = (3,2,t,t,1) から遷移可能な状態は? 1. (2,2,t,t,1) 2. (3,4,t,t,1) 3. (4,2,t,t,1) 0: flags[me] = true; 1: turn = you; 2: if (flags[you]!= true) goto 4; 3: if (turn!= you) goto 4; else goto0% 2; 4: critical section; 5: flags[me] = false; 6: either goto 6 or goto 0; 0% 0% (2,2,t,t,1) (3,4,t,t,1) (4,2,t,t,1)
状態遷移系について検証すべき性質 安全性 (safety) 好ましくないことが決して起こらないこと 活性 (liveness) 好ましいことが必ず起こること 活性が成り立つためには公平性が必要 公平性が成り立たないと 特定のプロセスばかり実行されてしまう 公平性 (fairness) の仮定 無条件の公平性 (unconditional fairness) 弱い公平性 (weak fairness) 強い公平性 (strong fairness)
次のうち活性はどれか? 1. デッドロックが起こらない 2. 開こうとするファイルは必ず存在する 3. 開いたファイルは必ず閉じられる 4. 配列のインデックスは常にその範囲内に納まっている 0% 0% 0% 0% デッドロックが起こらない 開こうとするファイル... 開いたファイルは必ず... 配列のインデックスは...
Peterson のアルゴリズムの場合 安全性 二つのプロセスが同時にはcritical sectionに入らない pc0=pc1=4にはならない 活性 ( 飢餓が起きないこと ) プロセスがヘッダ部に入ったら 必ずいつかはcritical sectionに入ることができる 活性が成り立つためには公平性が必要 どちらのプロセスも必ず進んでいなければならない ここでは,critical sectionで無限ループに陥らないと仮定 公平性 (fairness) の仮定 どちらのプロセスも無限回実行される 無条件の公平性
Petersonのアルゴリズムの正当性の時相論理による表現 安全性 LTL(Linear Time Temporal Logic) G( (pc0=4 pc1=4)) CTL(Computation Tree Logic) AG( (pc0=4 pc1=4)) 活性 ( 飢餓が起きないこと ) LTL G(pc0=0 F(pc0=4)) CTL AG(pc0=0 AF(pc0=4)) 公平性 (fairness) の仮定 LTL G(pc0=0 F(pc0=1))... LTLならば書けるが CTLでは書けない
公平性 (fairness) の仮定 無条件の公平性 (unconditional fairness) どのプロセスもいつかは必ず実行される 弱い公平性 (weak fairness) 実行可能であり続けるプロセスは いつかは必ず実行される 実行されないにもかかわらず 連続的に実行可能で有り続けることはない 強い公平性 (strong fairness) 実行されないにもかかわらず 断続的にも実行可能で有り続けることはない
Java の場合 public class LockTest extends Thread { static Object lock = new Object (); public void run () { while ( true ) { requestlock (); synchronized ( lock ) { acquirelock (); }}}} public static void main ( String [] args ) { LockTest th1 = new LockTest (); LockTest th2 = new LockTest (); th1. start (); th2. start (); } static public void requestlock () {} static public void acquirelock () {}}
どちらのスレッドも ackquirelock を 呼べるためには? 1. 弱い公平性で十分である 2. 強い公平性が必要である 3. 無条件の公平性が要請される 0% 0% 0% 弱い公平性で十分である 強い公平性が必要である 無条件の公平性が要...
計算木論理 (Computation Tree Logic) 分岐時間時相論理 (branching-time temporal logic) の一種 ϕ, ψ ::=... AGϕ globally on any path AFϕ finally on any path EGϕ globally on some path EFϕ finally on some path は AX は EX と書く
経路 (path) について 計算木論理では 無限の経路を考える 行き止まりの状態があると面倒なので どの状態からも次の状態があると仮定 たとえば 終了状態には 便宜上 自分自身への遷移を付加する
意味論 s = AGϕ iff s から到達できる任意の状態 t において t = ϕ s = AFϕ iff s から始まる任意の経路上に t = ϕ を満たす状態 t が存在する
で成り立っているのは? 1. AG P 2. AG P 3. AF 4. AF P P, P,
意味論 s = EFϕ iff s から到達できる状態 t が存在して t = ϕ s = EGϕ iff s から始まる経路が存在して その経路上の任意の状態 t において t = ϕ
で成り立っているのは? 1. EF (P ) 2. EF AG P 3. EG 4. EG P P, P,
で AF AG は成り立っている? 1. Yes 2. No P Yes 0% 0% No P, P,
状態集合の計算 大域的なモデル検査 [[φ]] = {s S s = φ } とおく [[P]] = { s S P L(s) } [[ ϕ]] = S [[ϕ]] [[ϕ ψ]] = [[ϕ]] [[ψ]] [[ϕ ψ]] = [[ϕ]] [[ψ]] [[ ϕ]] = { s S 任意の t S に対して R(s,t) ならば t [[φ]] } [[ ϕ]] = { s S ある t S が存在して R(s,t) かつ t [[φ]] }
[[EFφ]] の計算 状態集合の計算 X := loop Y := [[φ]] { s S ある t S が存在し R(s,t) かつ t X } if Y==X then break X := Y end Y := の右辺を f(x) とおいたとき X = f(x) を満たす最小の X を求めている
EF P P P, P,
EF P P P, P,
EF P P P, P,
[[EGφ]] の計算 状態集合の計算 X := S loop Y := [[φ]] { s S ある t S が存在し R(s,t) かつ t X } if Y==X then break X := Y end Y := の右辺を f(x) とおいたとき X = f(x) を満たす最大の X を求めている
EG P P, P,
EG P P, P,
[[AGφ]] の計算 状態集合の計算 X := S loop Y := [[φ]] { s S 任意の t S は R(s,t) ならば t X } if Y==X then break X := Y end Y := の右辺を f(x) とおいたとき X = f(x) を満たす最大の X を求めている
AG P P, P,
AG P P, P,
AG P P, P,
[[AFφ]] の計算 状態集合の計算 X := loop Y := [[φ]] { s S 任意の t S は R(s,t) ならば t X } if Y==X then break X := Y end Y := の右辺を f(x) とおいたとき X = f(x) を満たす最小の X を求めている
AF AG P P, P,
AF AG P P, P,
AF AG P P, P,
AF AG P P, P,
まとめ [[EFφ]] = [[φ EFφ]] 最小 [[EGφ]] = [[φ EGφ]] 最大 [[AGφ]] = [[φ AGφ]] 最大 [[AFφ]] = [[φ AFφ]] 最小
まとめ [[EFφ]] = [[φ EFφ]] 最小 [[EGφ]] = [[φ EGφ]] 最大 [[AGφ]] = [[φ AGφ]] 最大 [[AFφ]] = [[φ AFφ]] 最小
まとめ [[EFφ]] = [[φ EFφ]] 最小 [[EGφ]] = [[φ EGφ]] 最大 [[AGφ]] = [[φ AGφ]] 最大 [[AFφ]] = [[φ AFφ]] 最小
様相 µ 計算 (modal µ-calculus) 命題変数に対する再帰的定義が可能 X = ϕ X 最小不動点か最大不動点か? 最小不動点の場合 µx. ϕ X EFϕ に一致 最小不動点の場合恒真になってしまう 最大不動点の例 νx. ϕ X AGϕ に一致
AFφ を表すのは? 1. µx. ϕ X 2. µx. ϕ X 3. νx. ϕ X 4. νx. ϕ X 5. µx. ϕ X 6. µx. ϕ X 7. νx. ϕ X 8. νx. ϕ X
線形時間時相論理 (linear-time temporal logic) Kripke 構造上の経路において論理式を解釈する 計算木論理においても 部分的に経路の概念が入っている ここから先はずっと線形時間時相論理の話
Kripke 構造 K = S, R, L S: 状態の集合 R: 状態間の遷移関係 R S S L: 状態から原子論理式の集合への写像 L(s) は 状態 s S において成り立つ原子論理式の集合を与える
状態の無限列 --- 実行経路 π=π 0,π 1,π 2, π i S ( i 0) suffix R(π i, π i+1 ) ( i 0) π i =π i,π i+1,π i+2,
論理式 ϕ, ψ ::= P 命題記号 ϕ 否定 ϕ ψ 連言 ϕ ψ 選言 ϕ (Xϕ) ϕ (Gϕ) ϕ (Fϕ) until は ここでは 考えない
意味論 π = P iff P L(π 0 ) π = ϕ iff not π = ϕ π = ϕ ψ iff π = ϕ and π = ψ π = ϕ ψ iff π = ϕ or π = ψ π = ϕ iff π 1 = ϕ π = ϕ iff π i = ϕ for any i 0 π = ϕ iff π i = ϕ for some i 0 と の意味が これまでと違うことに注意 ϕ は π において成り立つ π = ϕ --- π は ϕ のモデルである
この経路で成り立っているのは? 1. P 2. P 3. (P ) 4. (P ) P P, P,
は成り立っているか? 1. Yes 2. No P Yes 0% 0% No P, P,
P は成り立っているか? 1. Yes 2. No P Yes 0% 0% No P, P,
P は成り立っているか? 1. Yes 2. No P Yes 0% 0% No P, P,
P π = P が成り立っていると π = P なので π i = P を満たす i が存在 π = P なので π i+1 = P が成り立ち π j = P を満たす j>i が存在 同様にして π i = P を満たす無限個の i が存在することがわかる 逆に π i = P を満たす無限個の i が存在すれば π = P が成り立つ
公平性の表現 E をあるプロセスが実行可能であること R をそのプロセスが実行されていることを表す 無条件の公平性 R 弱い公平性 ( Ε R) (Ε R) 強い公平性 Ε R Ε R
と と π = ϕ iff π = ϕ π = ϕ iff π = ϕ
論理式 ( 正形式 ) ϕ, ψ ::= P P ϕ ψ ϕ ψ ϕ ϕ ϕ 任意の論理式に対して それと同値な正形式が存在する
(a b) と同値な正形式は? 1. (a b) 2. (a b) 3. (a b) 4. (a b) 5. ( a b) 6. ( a b) 7. ( a b) 8. ( a b)
と と π = ϕ iff π = ϕ iff π = ϕ ϕ π = ϕ ϕ
cl(ϕ 0 ): ϕ 0 の閉包 以下の性質を満たす最小の ( 論理式の ) 集合 ϕ 0 cl(ϕ 0 ) ϕ 1 ϕ 2 cl(ϕ 0 ) ならば ϕ 1 cl(ϕ 0 ) かつ ϕ 2 cl(ϕ 0 ) ϕ 1 ϕ 2 cl(ϕ 0 ) ならば ϕ 1 cl(ϕ 0 ) かつ ϕ 2 cl(ϕ 0 ) ϕ cl(ϕ 0 ) ならば ϕ cl(ϕ 0 ) ϕ cl(ϕ 0 ) ならば ϕ ϕ cl(ϕ 0 ) ϕ cl(ϕ 0 ) ならば ϕ ϕ cl(ϕ 0 ) P cl(ϕ 0 ) ならば P cl(ϕ 0 ) という条件はなくてもよい
ϕ = 0 (a b) cl(ϕ 0 ) : (a b) (a b) (a b) a b (a b) a b b b b b
ϕ 0 型 Γ cl(ϕ 0 ) ϕ 1 ϕ 2 Γ ならば ϕ 1 Γ かつ ϕ 2 Γ ϕ 1 ϕ 2 Γ ならば ϕ 1 Γ または ϕ 2 Γ P Γ かつ P Γ となることはない ϕ Γ ならば ϕ ϕ Γ ϕ Γ ならば ϕ ϕ Γ
ϕ 0 型の選択と ϕ 0 型間の遷移 ϕ 0 を含む極小のϕ 0 型をすべて選ぶ ϕ 0 型 Γ cl(ϕ 0 ) が選ばれたら {ϕ cl(ϕ 0 ) ϕ Γ} を含む極小のϕ 0 型 Γ をすべて選ぶ Γ Γ とおく ( 遷移 ) 以上の繰り返し
Γ ア : (a b)
Γ ア : (a b) (a b) (a b)
Γ ア : (a b) (a b) (a b) a b Γ イ : (a b) (a b) (a b) (a b)
Γ ア : (a b) (a b) (a b) a b a b Γ イ : (a b) (a b) (a b) (a b)
Γ ア : (a b) (a b) (a b) a b a b b b Γ イ : (a b) (a b) (a b) (a b)
Γ ア : (a b) (a b) (a b) a b a b b b b Γ b イ : (a b) (a b) (a b) (a b)
Γ アからの遷移先に含まれるのは? Γ ア : (a b) (a b) (a b) a b a b b b b b 1. a 2. b 3. b 4. a b 5. (a b)
Γ ア : (a b) (a b) (a b) a b a b b b b Γ ウ : Γ b イ : b (a b) (a b) (a b) (a b)
Γ ア : (a b) (a b) (a b) a b a b b b b Γ ウ : Γ b イ : b (a b) (a b) (a b) b b (a b)
Γ ア : (a b) (a b) (a b) a b a b b b b Γ ウ : Γ b イ : b (a b) (a b) (a b) b b (a b) b b
アから遷移可能なのは? 1. ない 2. ア 3. アとイ 4. アとウ 5. アとイとウ 6. イ 7. イとウ 8. ウ イ : ア : (a b) (a b) (a b) a b a b b b b b (a b) (a b) (a b) (a b) ウ : b b b b b 0% 0% 0% 0% 0% 0% 0% 0% ない ア アとイ アとウ アとイとウ イ イとウ ウ
イから遷移可能なのは? 1. ない 2. ア 3. アとイ 4. アとウ 5. アとイとウ 6. イ 7. イとウ 8. ウ イ : ア : (a b) (a b) (a b) a b a b b b b b (a b) (a b) (a b) (a b) ウ : b b b b b 0% 0% 0% 0% 0% 0% 0% 0% ない ア アとイ アとウ アとイとウ イ イとウ ウ
ウから遷移可能なのは? 1. ない 2. ア 3. アとイ 4. アとウ 5. アとイとウ 6. イ 7. イとウ 8. ウ イ : ア : (a b) (a b) (a b) a b a b b b b b (a b) (a b) (a b) (a b) ウ : b b b b b 0% 0% 0% 0% 0% 0% 0% 0% ない ア アとイ アとウ アとイとウ イ イとウ ウ
ア : (a b) (a b) (a b) a b a b b b b b イ : (a b) (a b) (a b) (a b) ウ : b b b b b
ア : (a b) (a b) (a b) a b a b b b b b イ : (a b) (a b) (a b) (a b) ウ : b b b b b
ア : (a b) (a b) (a b) a b a b b b b b イ : (a b) (a b) (a b) (a b) ウ : b b b b b
ア イ ウ
モデルの 記号 化 π=π 0,π 1,π 2, を ϕ 0 のモデルとしたとき 以下の条件を満たす ϕ 0 型の無限列 Π = Γ 0, Γ 1, Γ 2, が存在する ϕ 0 Γ 0 任意の ϕ Γ i に対して π i = ϕ を満たす Γ i Γ i+1 ϕ Γ i ならば ある j i が存在して ϕ Γ j
π = π 0, π 1, π 2, π 3, π 4, π 5, π 6, π 7, π 1 = π 1, π 2, π 3, π 4, π 5, π 6, π 7, π 2 = π 2, π 3, π 4, π 5, π 6, π 7, π 3 = π 3, π 4, π 5, π 6, π 7, π 4 = π 4, π 5, π 6, π 7, = ϕ 0 = ψ = ψ = θ Π = Γ 0, Γ 1, Γ 2, Γ 3, Γ 4, Γ 5, π 5 = π 5, π 6, π 7, = θ
ア イ ウ
逆に ϕ 0 型 Γ i cl(ϕ 0 ) から成る無限列 Π=Γ 0,Γ 1,Γ 2, が以上の条件を満たし さらに以下の条件を満たせば 任意の ϕ Γ i に対して π i = ϕ が成り立つ ( 特に π = ϕ 0 ) P Γ i ならば P L(π i ) である P Γ i ならば P L(π i ) でない
ω オートマトン 以上の条件を満たす無限列を特徴付けるため ϕ 0 型 Γ cl(ϕ 0 ) を状態とする ωオートマトンを構成する 遷移は Γ Γ によって定義
初期状態 特に π = ϕ 0 を満たす π を求めたいので ϕ 0 Γ 0 を要請する このためには ϕ 0 を含むϕ 0 型を初期状態とすればよい ( 複数あり得ることに注意 )
ア : (a b) (a b) (a b) a b a b b b b b イ : (a b) (a b) (a b) (a b) ウ : b b b b b
ア : (a b) (a b) (a b) a b a b b b b b イ : (a b) (a b) (a b) (a b) ウ : b b b b b
ア イ ウ
ラベル 以下の条件を調べるために 命題記号とその否定を状態 (ϕ 0 型 ) のラベルとして明示 P Γ i ならば P L(π i ) である P Γ i ならば P L(π i ) でない
ア : (a b) (a b) (a b) a b a b b b b b イ : (a b) (a b) (a b) (a b) ウ : b b b b b
ア : (a b) (a b) (a b) a b a b b b b b イ : (a b) (a b) (a b) (a b) ウ : b b b b b
ア a b イ ウ b
経路の条件 ωオートマトン上の無限経路 Π=Γ 0,Γ 1,Γ 2, で 以下の条件を満たすものを特徴付けたい ϕ Γ i ならば ある j i が存在して ϕ Γ j
経路の条件 以上の無限経路の条件は 次のように言い換えることができる Π=Γ 0,Γ 1,Γ 2, は 各 ϕ cl(ϕ 0 ) に対して F( ϕ) の要素を無限回含む ここで F( ϕ) = {Γ ϕ Γ または ϕ Γ}
F( (a b)) は? 1. ない 2. ア 3. アとイ 4. アとウ 5. アとイとウ 6. イ 7. イとウ 8. ウ イ : ア : (a b) (a b) (a b) a b a b b b b b (a b) (a b) (a b) (a b) ウ : b b b b b F( ϕ) = {Γ ϕ Γ または ϕ Γ} ない 0% 0% 0% 0% 0% 0% 0% 0% ア アとイ アとウ アとイとウ イ イとウ ウ
ア : (a b) (a b) (a b) a b a b b b b b イ : (a b) (a b) (a b) (a b) ウ : b b b b b
ア : (a b) (a b) (a b) a b a b b b b b イ : (a b) (a b) (a b) (a b) ウ : b b b b b
ア a b イ ウ F( (a b)) = { ア, ウ } b
モデル検査 Kripke 構造 K= S, R, L 初期状態 s 0 S 論理式 ϕ 0 に対して π 0 =s 0 を満たす ϕ 0 のモデル π=π 0,π 1,π 2, が存在するか?
これは以下と等価 ωオートマトン上の無限経路 Π=Γ 0,Γ 1,Γ 2, で以下の条件を満たすものが存在するか? 各 ϕ cl(ϕ 0 ) に対して F( ϕ) の要素を無限回含む P Γ i ならば P L(π i ) である P Γ i ならば P L(π i ) でない
同期積 π の存在と Π の存在を一度に調べるために ωオートマトンと K との 同期積 を作る 状態 : s, Γ where {P P Γ} L(s) {P P Γ} L(s) = 初期状態 : s 0, Γ 0 それぞれの初期状態の組 遷移 : s, Γ s, Γ iff R(s, s ) and Γ Γ
同期積 a b a b a b
同期積 a b a b a b
存在しないのは? 20% 20% 20% a20% b 20% a b a b 1 4 5 2 3
同期積 a b a b a b
存在する遷移は? a b a a b 17% 17% 17% 17% 17% 17% b 2 1 3 5 6 4
同期積 a b a b a b
同期積 a b a b b
モデルが存在するための条件 ϕ 0 のモデル π=π 0,π 1,π 2, が存在するための必要十分条件 : 同期積における無限経路 π 0, Γ 0 π 1, Γ 1... で 各 ϕ cl(ϕ 0 ) に対して F( ϕ) の要素を無限回含むものが存在する ある種のループの存在
同期積 a b a b a b
同期積 a b a b b
ループの条件 ループは 初期状態から到達可能 ループは 各 ϕ cl(ϕ 0 ) に対して F( ϕ) の要素を含む 同期積の強連結成分を求めれば 上のようなループが存在するか 判定可能
レポート課題 ( e r) (a b) が常に成り立つことを検証するための ωオートマトンを構成せよ 以下のKripke 構造において 上記論理式が常に成り立つことを示せ a e r b
until π = ϕ until ψ iff π i = ψ for some i 0 and π j = ϕ for any j<i
release π = ϕ release ψ iff π i = ϕ for some i 0 and π j = ψ for any j i or π j = ψ for any j
until と release と π = (ϕ until ψ) iff π = ϕ release ψ π = (ϕ release ψ) iff π = ϕ until ψ
until と release と π = ϕ until ψ iff π = ψ (ϕ until ψ) π = release ψ iff π = ψ (ϕ release ψ)