チュートリアル 形式的検証技術 Logical Framework と Modal Logic

Presentation on theme: "チュートリアル 形式的検証技術 Logical Framework と Modal Logic"— Presentation transcript:

1 チュートリアル 形式的検証技術 Logical Framework と Modal Logic
萩谷 昌己 なぞかけ研究者 協力：西澤弘毅（東大）

2 形式的検証技術 より信頼できる計算システムを目指して ディペンダビィティ 記号論理を用いた方法論とツール ハードウェア ソフトウェア
プロトコル アルゴリズム ディペンダビィティ 電気やガスのような社会のインフラとしての 情報技術 記号論理を用いた方法論とツール 最大限の信頼性、しかし、高い人的コスト ⇒safety criticalなシステム

3 形式的検証技術：方法論とツール 証明支援系 Logical Framework 状態探索系・モデル検査系 Modal Logic
高階述語論理・高階型理論＋帰納的定義 汎用（例えば、数学・論理体系自身） 半自動証明＋対話的証明 半自動の自動証明機能 --- tactic 状態探索系・モデル検査系 Modal Logic 時相論理（離散・連続・確率） 状態遷移系に特化（例えば、分散アルゴリズム） 全自動証明 静的解析（型検査・型推論・データフロー解析）を包含 様々な形での融合

4 高階述語論理と高階型理論 高階述語論理 高階型理論 関数や述語に関する量化（"$）が可能な論理 " f. ～ … 任意の関数 f について～
型付きλ計算 Curry-Howardの対応 依存型により高階述語論理を包含 Martin-Lofの型理論 Calculus of Constructions Logical Framework ..

5 Curry-Howardの対応 命題 ≡ 型 AÉB ≡ A®B A ならば B A から B への関数の型
命題 A の証明 ≡ A を型として持つ項 AÉB の証明 ≡ A の証明をもらって B の証明を返す関数 構成的な証明の考えに基づいている。 直観主義論理

6 依存型 P real(n) real(n)：大きさ n の実数の配列の型 例えば、自然数 n をもらって、
nat®real(n) n が浮いている。 Pn:nat. real(n) 関数をタプルと考えると自然。依存関数型（依存直積） 依存直和もある。 Curry-Howardの対応では "n:nat. real(n) という命題 "n:nat. P(n) の証明 ≡ 任意の n に対して、 P(n) の証明を返す関数 例えば要素がすべて0.0 P real(n) nÎnat

7 帰納的定義 多くの証明支援系には、 帰納的定義によって論理を拡張する機能が 備わっている。 型の帰納的定義 … 再帰的データ型
述語の帰納的定義 Curry-Howardの対応のもとでは同じ原理 最小の集合や関係の定義 cf. 余帰納（co-induction） 最大の集合や関係の定義

8 再帰的データ型 自然数 自然数を葉に持つ二分木 0 は自然数である。 x が（既に作られた）自然数ならば、 s(x) も自然数である。
以上のようにして作られるもののみが 自然数である。 0 : nat s : nat ® nat 自然数を葉に持つ二分木 leaf : nat ® bintree cons : bintree ® bintree ® nbintree

9 述語の帰納的定義 even(x) の定義 even(0) が成り立つ。 even(x) が成り立てば、
even(s(s(x))) も成り立つ。 以上のようにして even が導かれるときのみ、 even が成り立つ。

10 帰納的述語の証明 even(x) の証明 even0 は even(0) の証明である。 X が even(x) の証明ならば、
even1(x)(X) は、even(s(s(x))) の証明である。 以上のようにして作られるもののみが、 even(x) の証明である。 even0 : even(0) even1 : Px:nat. even(x) ® even(s(s(x)))

11 再帰的データの構成に関する帰納法 P(x) を自然数に関する述語とする。 任意の自然数 x に対して P(x) が成り立つ。
P(x) ならば P(s(x)) が成り立てば、 任意の自然数 x に対して P(x) が成り立つ。 P(x) を二分木 x に関する述語とする。 任意の自然数 i に対して P(leaf(i)) が成り立ち、 二分木 x と y に対して P(x) かつ P(y) ならば P(cons(x,y)) も成り立てば、 任意の二分木 x に対して P(x) が成り立つ。

12 帰納的述語の導出に関する帰納法 自然数の述語 P に関して、 の二つの条件が満たされているならば、 任意の自然数 x に対して、
P(x) が成り立つならば、P(s(s(x))) が成り立つ。 の二つの条件が満たされているならば、 任意の自然数 x に対して、 even(x) É P(x) が成り立つ。 even(x) の証明の構成に関する帰納法

13 高階述語論理と高階型理論 高階述語論理 高階型理論 関数や述語に関する量化（"$）が可能な論理 " f. ～ … 任意の関数 f について～
型付きλ計算 Curry-Howardの対応 依存型により高階述語論理を包含 Martin-Lofの型理論 Calculus of Constructions Logical Framework ..

14 Logical Framework 高階型理論の一種 論理体系を定義するためのフレームワーク 言明 文脈 |- 証明 : 命題
論理体系の性質 論理体系の間の関係 言明 文脈 |- 証明 : 命題 Adequacy Logical Frameworkの正規項が、 論理体系の証明と１対１に対応していること。 文脈まで考慮した帰納法 いろいろな論理による拡張 「文脈の多様化」 の導出

15 例：自然演繹 Snd：シグニチャ（定数の文脈） o : type É : o ® (o ® o) nd : o ® type
impI : (nd G1 ® nd G2) ® nd (G1 É G2) impE : nd (G1 É G2) ® nd G1 ® nd G2 暗黙の引数 … 本来ならば、 impI : PG1:o. PG2:o. (nd G1 ® nd G2) ® nd (G1 É G2)

16 impI : (nd G1 ® nd G2) ® nd (G1 ⊃ G2)
： G2 ÉI G1 É G2 ： ： G1 É G G1 ÉE G2 impE : nd (G1 É G2) ® nd G1 ® nd G2

17 ------------------ ÉE G2 É G [G2] -------------------- ÉE G ------ ÉI
G1 É G2 É G [G1] ÉE G2 É G [G2] ÉE G ÉI G1 É G ÉI G2 É G1 É G D D = impI (lx2:nd G2. impI (lx1:nd G1. impE (impE y x1) x2)) G1:o, G2:o, G:o, y:nd (G1ÉG2ÉG) |- D:nd (G2ÉG1ÉG) 文脈 言明

18 抽象化と関数適用 x : A1, G |- M : A2 ----------------------
局所的な宣言によって拡張された文脈 x : A1, G |- M : A2 |- lx : A1. M : Px : A1. A2 |- N1 : Px:A1. A G |- N2 : A1 |- N1 N2 : A2[N2 / x] x をもらって M を返す関数 A2 の x に N2 を代入 関数適用

19 例：シーケント計算 Sseq：シグニチャ o : type É : o ® (o ® o) hyp : o ® type
conc : o ® type init : hyp G ® conc G impR : (hyp G1 ® conc G2) ® conc (G1 É G2) impL : conc G1 ® (hyp G2 ® conc G3) ® (hyp (G1 É G2) ® conc G3) cut : conc G1 ® (hyp G1 ® conc G2 ) ® conc G2

20 ------------------------
D ： G1 É G2 É G Þ G2 É G1 É G G1:o, G2:o, G:o, y:hyp (G1ÉG2ÉG) |- D:conc (G2ÉG1ÉG)

21 自然演繹とシーケント計算 自然演繹ならばシーケント計算： ならば、以下を満たす E が存在 文脈を考慮した D の構成に関する帰納法
G1:o, …, Gn:o, x1:nd A1, …, xm:nd Am |- D:nd B ならば、以下を満たす E が存在 G1:o, …, Gn:o, x1:hyp A1, …, xm:hyp Am |- E:conc B 文脈を考慮した D の構成に関する帰納法 帰納ステップで文脈が上の形になることが必要。 D の構造に従って、 E を構成する手続きを定義することができる。 自動化の試み Meta Logical Framework [Schürmann, 01] 証明に対する再帰と場合分け

22 いろいろな論理による拡張 「文脈の多様化」 論理 変数でのコード例 LF [87] 一階述語論理 仮定の命題 LLF [96] 線形論理
メモリ OLF [00] 非可換線形論理 継続 CLF [02] 乗法的線形論理 プロセス 「文脈の多様化」

23 LF [Harper他 87] 関数の返り値の型が引数の項に依存

24 Linear LF [Cervesato他 96]
一箇所でしか使えない変数とその文脈を導入

25 Ordered LF [Polakow他 00] 一箇所でしか使えず、 その順番も指定されている変数と文脈を導入

26 Concurrent LF [Watkins他 02]
変数に束縛される項のパターンを指定

27 形式的検証技術：方法論とツール 証明支援系 Logical Framework 状態探索系・モデル検査系 Modal Logic
高階述語論理・高階型理論＋帰納的定義 汎用（例えば、数学・論理体系自身） 半自動証明＋対話的証明 半自動の自動証明機能 --- tactic 状態探索系・モデル検査系 Modal Logic 時相論理（離散・連続・確率） 状態遷移系に特化（例えば、分散アルゴリズム） 全自動証明 静的解析（型検査・型推論・データフロー解析）を包含 様々な形での融合

28 時相論理（Temporal Logic） 状態の遷移や時間の経過の観点より システムの性質を記述するための論理体系 線形時間時相論理
LTL（Linear Time Temporal Logic) 分岐時間時相論理 CTL（Computation Tree Logic） μ計算（m-calculus） モデル検査 時相論理で表現された性質を システムが満たすかどうかを検査すること

29 例：Petersonのアルゴリズム me = 0 you = 1 for (;;) { flags[me] = true;
turn = you; while (flags[you] == true) { if (turn != you) break; } // the critical section flags[me] = false; // the idle part

30 例：Petersonのアルゴリズム me = 1 you = 0 for (;;) { flags[me] = true;
turn = you; while (flags[you] == true) { if (turn != you) break; } // the critical section flags[me] = false; // the idle part

31 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}

32 Petersonのアルゴリズムの正当性 安全性 活性（飢餓が起きないこと） 活性が成り立つためには公平性が必要 公平性（fairness）
二つのプロセスが同時にはcritical sectionに入らない。 pc0=pc1=4にはならない。 活性（飢餓が起きないこと） プロセスがヘッダ部に入ったら、 必ずいつかはcritical sectionに入ることができる。 活性が成り立つためには公平性が必要 どちらのプロセスも必ず進んでいなければならない。 ここでは，critical sectionで無限ループに陥らないと仮定。 公平性（fairness） どちらのプロセスも無限回実行される。 （unconditional fairness）

33 Petersonのアルゴリズムの正当性の 時相論理による表現
安全性 LTL（Linear Time Temporal Logic) □(Ø(pc0=4 Ù pc1=4)) CTL（Computation Tree Logic） AG(Ø(pc0=4 Ù pc1=4)) 活性（飢餓が起きないこと） LTL □(pc0=0 É ◇(pc0=4)) CTL AG(pc0=0 É AF(pc0=4)) 公平性（fairness） LTL □(pc0=0 É ◇(pc0=1)) Ù ... LTLならば書けるが、CTLでは書けない。

34 Kripke構造 K = áS, R, Lñ S: 状態の集合 R: 状態間の遷移関係 R Í S×S
L(s) は、状態 sÎS において成り立つ 原子論理式の集合を与える。

35 例 S = {s0, s1, s2} R = {ás0, s1ñ, ás0, s2ñ, ás1, s0ñ, ás2, s0ñ}
L(s0) = Æ L(s1) = {P} L(s2) = Æ P s1 s0 ØP s2 ØP

36 状態の（無限）列 --- 実行経路 p=s0,s1,s2,… si Î S ("i³0) si R si+1 ("i³0) suffix pi =si,si+1,si+2,…

37 例 p=s0,s2,s0,s2,s0, s1,s0,s2,s0,s2,s0, … P s1 s0 ØP s2 ØP

38 論理式（正形式） f ::= P | ØP | fÙf | fÚf | ○f | □f | ◇f PLTL（命題線形時間時相論理）
untilは、 ここでは、 考えない。

39 意味論 |= P iff P Î L(s0) |= ØP iff P Î L(s0)
|= f1Ùf2 iff p |= f1 and p |= f2 |= f1Úf2 iff p |= f1 or p |= f2 |= ○f iff p1 |= f |= □f iff pi |= f for any i³0 |= ◇f iff pi |= f for some i³0 |= f p は f を充足する。

40 例 P s1 s0 ØP s2 ØP s1,s0,… |= P s1,s0,… |= ◇P s0,s1,s0,… |= ◇P …
s0,s2,s0,s2,s0,s1,s0,…|= ◇P s0,s1,s0,s1,s0,s2,s0,…|= □◇P P s1 s0 ØP s2 ØP

41 重要な性質 |= □f iff p |= fÙ○□f |= ◇f iff p |= fÚ○◇f

42 論理式の「証明」 意味論の別の定式化 Gi = L(si) È {ØP | PÎ L(si)}
P=G0,G1,G2,…のもとで f0 を証明 P |- f0 PÎG0 G0,G1,G2,… |- P ØPÎG0 G0,G1,G2,… |- ØP P |- f1 P |- f2 P |- f1Ùf2 P |- f1 P |- f1Úf2

43 G1,G2,… |- f -------------- G0,G1,G2,… |- ○f G0,G1,G2,… |- fÙ○□f
G0,G1,G2,… |- □f G0,G1,G2,… |- fÚ○◇f G0,G1,G2,… |- ◇f ただし、 ◇の方は、有限ステップの後に、 Úの左のブランチに進まなければならない。

44 G1,G2,… |- f ---------------- G1,G2,… |- fÚ○◇f ------------------
ただし、 ◇の方は、有限ステップの後に、 Úの左のブランチに進まなければならない。 G1,G2,… |- f G1,G2,… |- fÚ○◇f G1,G2,… |- ◇f G0,G1,G2,… |- ○◇f G0,G1,G2,… |- fÚ○◇f G0,G1,G2,… |- ◇f

45 G2 = L(s0) G1 = L(s1) G0 = L(s0) p=s0,s1,s0,…
G1,G2,… |- P　　　　　　　　　　 　G1,G2,… |- P　　　　　　　　　　　　　　　　　　　　 　　 　　　　　 　　　 　　　 　　　　　 　G1,G2,… |- PÚ○◇P　　　　　　 G1,G2,… |- PÚ○◇P　　　 　　　　G2,… |- □◇P 　　　　 　　 　　　　　 　　　　　 　　　 G1,G2,… |- ◇P 　　　　　　　　　　G1,G2,… |- ◇P　　　　　　　G1,G2,… |- ○□◇P 　　　　　　　 　 G0,G1,G2,… |- ○◇P　　　　　　　 　　　　G1,G2,… |- ◇PÙ○□◇P 　　　　　　　　　　 　 　　　　　　　　 　　　　　　　　　　 G0,G1,G2,… |- PÚ○◇P　　　　　　　　　　　G1,G2,… |- □◇P　　　　　　　　　　　 　　　　　　　　　 　　　　　　　　　 G0,G1,G2,… |- ◇P 　　　　　　　　　 G0,G1,G2,… |- ○□◇P　　　　　　　 　　　　　　　 G0,G1,G2,… |- ◇PÙ○□◇P G0,G1,G2,… |- □◇P G0 = L(s0) p=s0,s1,s0,…

46 充足可能性判定 G：リテラルの集合 文字 P=G0,G1,G2,… Gの無限列 P |- f0 を満たす P をちょうど受理する
P か ØP のどちらか一方が含まれる。 P=G0,G1,G2,… Gの無限列 P |- f0 を満たす P をちょうど受理する 無限オートマトンを構成することができる。 LTLの場合はBüchiオートマトン 一般に（例えばμ計算）、論理式を状態とし、 証明を遡るようなオートマトンを定義し、 決定化と否定によって所望のオートマトンを 得ることができる。 分岐時間の場合は無限木オートマトン

47 モデル検査 Kripke構造 K に対して、 以下のような実行経路 p が存在するか。 p = s0,s1,s2,…
Gi = L(si) È {ØP | PÎ L(si)} P=G0,G1,G2,…は先のオートマトンによって 受理される。 以上の判定のために、 K と先のオートマトンの同期積を構成。 同期積のオートマトンが空かどうか。

48 Logical Frameworkへ（余談）
融合の一つ？ |- の左は G の無限列 cf. [Bellin他, 01] 個々の G は文脈のようなもの |- の左がそのようなLogical Frameworkを 考えることができないか？ □f = Ø◇Øf なので、 □の証明は、◇の証明の構成に関する帰納法 すなわち、証明に対する再帰 … 余帰納に相当

49 ---------------------
G1,G2,… |- M : f G0,G1,G2,… |- next(M) : ○f P |- M : fÚ○◇f P |- dia(M) : ◇f [ P |- x : □f ] : P |- M[x] : fÙ○□f P |- mx. M[x] : □f 証明に対する再帰： （無限の）証明を 生成する手続き mは最小不動点 ではなくて 単純な再帰

50 ----------------------
(x:P,G),G1,G2,… |- x : P (x:ØP,G),G1,G2,… |- x : ØP P |- M1 : f P |- M2 : f2 P |- áM1, M2ñ : f1Ùf2 P |- M : f1 P |- inj1(M) : f1Úf2

51 課題 無限の文脈を定義する方法 「文脈の多様化」 再帰的な証明を表現する方法 そのような証明を探索する方法 再帰のネスト
無限の文脈を定義する方法 「文脈の多様化」 無限列 の一種 無限木（分岐時間） 再帰的な証明を表現する方法 そのような証明を探索する方法 再帰のネスト μ計算 少なくとも、従来のオートマトン理論的な 方法と同等の能力にしたい。 さらに、拡張？

52 まとめ Logical Framework Modal Logic（Temporal Logic ） 融合の可能性？
論理体系を表現するための型理論 文脈の多様化 証明に対する再帰的手続き Modal Logic（Temporal Logic ） 充足可能性とモデル検査の手続き 文脈の無限列に対するオートマトン 融合の可能性？