Day1:

いやとにかく難しい、すぐにautomataの数学的な定義から、universe, model, satisfiable, decidable,続くのは難解な宇宙語,,,そして華麗なるMONAの世界へ(OSじゃないよ）。これはいきなり高速道路だ。

• 雑談
  • 検証技術も役に立つようになった
  • Intelなんかは30人ぐらいやとって、theorem proverとmodel checkingを融合してチェックしている
    • flという関数言語に落として、その変換の等価性検証はTPで、モデルチェックはmodelchekkerで

リンク集

• Formal Method
• 先生のHP
  • シラバス
• よくわかる定理証明:
• csc2108
• SMV
  • Ken McMillan's Home Page at UCB
• MONA
  • MONAを使おう
  • MONA: Monadic Second-Order Logic in Practice
• Isabelle/HOL
  • Isabelle/HOL
  • Getting Started With Isabelle
  • ProofGeneral Wiki
    • Tutorialいいかも

理論

• Theory: syntax

　　　　 |-P, Pが導出できるということ

• Model: semantics

　　　　　|=P, Pを満たすMがありますか？

• Complete

　　　　　 |-P <=> |=P

• FOL(MSOL)はComplete
• HOLはincomplete by Godel
• Model checking
  • CTL/LTLの違いはたいしたことはない

automata

• 形式記述

Automaton A=(S,Σ,δ,q0,F)

• どこまでがんばれるか？
  • (ab)^nは　アクセプタブル
  • a^nb^nは　そうでない
  • a^nb^nc^n はstackが２つあることになりチューリングマシンと同じになる
• emptinessが decidable(長さをみれば）
  • Pumping Lemma?

State数の程度の長さの言語ならばということ

L(A) \= φ　iff XXXXXでdesidableをきめる

　　 Aにアクセプトされる入力が無いということ？？

• boolean closureがやっぱりdecidable
  • Intersection of Automata

直積をとればいいじゃん
For automata A =(S,Σ,δ,q0,F), B =(S’,Σ,δ’,q’0,F’)
(S×S’, Σ, δ×δ’, (q0, q’0), F×F’)

• Union of Automata

(S∪S’∪{q},Σ,δ∪δ’∪{(q,ε,q0),(q,ε,q’0)},q, F∪F’)

• Complement of automata
  • automaton A= (S,Σ,δ,q0,F)
  • もしAがdetermisticならば Ac= (S,Σ,δ,q0,SｰF)

determisticでないものがれば、そうしてから、反転(Final似たいｓて）をするらしい

• ポイント！

M |=P ということは

　L(M) ⊆　L(P) <=> L(M) ∧L(P)c = φ

• だから、emptiness(φ)やintersection(∧),complementがdecidableならばＯＫよということになる

Buchi automata

• ω-languageなるものを受け付ける
• どうも言語に　ωのついたものは無限大の繰り返し
• finalが無限？
• complimentに関して deterministicのAのcomplimentは必ずしもdeterministicではない(b*a)ω

Monadic Second Order Logic(MSOL)

• 定義
  • Logical quantifiers, connectives: ∀, ∃, →, ¬, ∨, ∧, ＝
  • 1st order variable x,y / 2nd order (set) variable X,Y
  • Set operation: ∈
  • Unique function symbol: s
  • Unique constant: 0
• めも
  • SnSに対応づけられる
  • second orderといいっているのは 2nd order variable=set of positionを受け入れられるから？
  • ∈があれば、set X,Yに関する様々な論理は定義できる
  • x<yのようなポジションの大小関係を定義できる
    • どうもこの関係を、要素ベースで表すとrecursionになってMSOLでは禁じ手
    • 集合(X,Y)で定義することができるのが味噌らしい
  • S1Sのsatisfiablityは決定可能である
    • 例えば　formula Φが vaild, satisfiable, unsatisfiableというのは決定可能
  • 0,s(0),s(s(0))というふうになるのが S1S
  • S2Sは

0-s1(0)-s1(s1(0)) +s2(s1(0)) +s2(0)-S1(s2(0)) +s2(s2(0))

というふうにbinary treeになる

• MSOLのアプリケーション
  • TRSにおける最適なreduction戦略はありや？
  • Regular type inference in XML

宿題

• (1)Construction of complement of (non-deterministic) Buchi automata
• (2)Finish full Presburger arithmetic by MONA

Day2&3

• SMV記述要素
  • Logical connectives: &, |, !, ->, ….
  • Finite Set Expression: { …. }
  • Comments: --….
  • Variable declaration: VAR
  • Assignment: ASSIGN

init(var) := …. ; next(var) := …. ;

• Case sentense: case … : …; esac
• CTL formula: SPEC ….
• LTL formula: LTLSPEC …
• Sample(SMV)

MODULE main
VAR
request: boolean;
state: {ready, busy};
ASSIGN
init(state) := ready;
next(state) :=
case
state=ready & request : busy;
1 : {ready, busy};
esac;
SPEC AG(request -> AF (state = busy))

• モデルチェックの応用例
• 実習(NuSMV)
• CTLの書き方
  • CTL: Computation Tree Logic(Branching-time propositional temporal logic)
  • Model - a tree of computation paths
    • ifφ and ψ are CTL formulae, then so are:  ,    ,  
    • EX φ --- φ holds in some next states;
    • EF φ --- along some path, φ is true in a future state;
    • E[φ U ψ ] --- along some path, φ holds until ψ holds;
    • EG φ --- along some path, φ holds in every state
    • Universal quantification: AX φ , AF φ , A[φ U ψ ], AG ψ
• mutual exclusionをCTL/LTLで書くと、、
  • CTL

!EF((state1=c1) & (state2=c2))
AG((state1=t1) -> AF (state1=c1))

• LTL

G((state1=t1) -> F (state1=c1))
G(F(state1=t1 -> state2=c1))

Day4

今日は、モデルチェッキングをプログラム解析に応用する話だ
端的に言えば

抽象化(CFGとラベル）して、モデルチェッカをleast point engine(シミュレーションエンジン？）とし てつかって、様々なSPECをチェックする。SPECにはdead codeの定義とか様々つかえる

しかし、今日も難しい話をしている割には、ＰＰＴの数式が間違っていて、混乱させられる

• Analysys = Abstraction + Model checking
  • 領域をfiniteなものに抽象化することで、モデルチェック対象にできます
    • 例 (自然数→ (ZERO|PLUS))
• やり方
  • 1) abs:D→ Abs　のマッピングをつくる
  • 2) Absの上で、primitiveな関数の解釈を定義する
  • 3) loop文等の実行を同じように実現する工夫をする 1,2ができれば自動的にできる？
    • これをやるには"semantics"が重要で、よくわからんがモデルチェッカがつかえる。？？？
• Semanticsはどう定義する
  • loopなんかは"least fixed point"が解決してくれるので "Tarsky"に聞けよ！
  • 例:

関数型言語	complete lattice
ロジックプログラミング	ヘルブラン空間

• プログラム解析をどうすんの？
  • 基本はCFGをつくって、これを状態遷移システムに写像
  • ただし環境の持ち回りに注意する→ラベルにする
• "Dead Code Detection/Elimination"
  • CFGにして def_x, use_yといったラベルをつけていきます。
  • 直感的には dead codeの定義は↓
    • AG !(def_x & AX( AG !use_x | A[!use_x U def_x]))
    • def_xがってそこからのnext全部で、 use_xがないあるいは　def_xがあるまでuse_xがない
  • しかしだめなので本当は↓
    • AG !(def(x) & AX (A[!use(x) W def(x)]))
    • weak untileを使うのが味噌
    • loopで達することができない場合があるかららしい。。
• "Constant P
  • 同じくCDGで、conLit(e):eはコンスタントcですというを導入
    • AG!(use(x) & A'[!def(x) W ( stmt(x:=e) & conLit(e))])

Day5

定理証明の Isabelle/HOLを導入するため、禁断の cygwinをインストールした。
しかし、　Isabelle/HOLのインストールもできないし、やはり gnuproと衝突して
しまって、仕事も出来ない状態になってしまった。来週の会議に間に合わない。

いわゆる、今週最大のピンチ。

• Isabelle/Cygwin

DayX

インストールできない原因がわかった

• perlが /cygdrive/c..とcygwinとは別のものしかはいってなかった、setupよりインストールするとIsabelle2005が無事buildできた。
• xemacsには様々なモジュールが必要でこれも cygwinのsetupよりインストールすれば、証明将軍のご尊顔がすぐにでてきた。

というわけで、遅れを取り戻すぞーー、取り戻せるのかな？

Report(12/5までだがのびるかな）

• (1)Construction of complement of (non-deterministic) Buchi automata
• (2)Finish full Presburger arithmetic by MONA
• (3)31ゲーム、プレイヤーA,B（2名）
  • ０からプレイヤーAの先手で始まる。
  • どちらのプレイヤーも現在の数に１か２か３を足した数を答えられる。
  • ３１を言ったプレイヤーの負け。

◆たとえば、プレイヤーAが１（＋１）、プレイヤーBが２、３（＋２）、プレイヤーAが４，５、６（＋３）などと言っていく。
◆モデル検査（SMVでもSPINでも良い）で先手が必勝であることを示せ。

• (4)Needam-Schroeder PK protocol のモデル検査を行い、Man-in-the-middle のアタックを検出せよ。
• (5)Finish proof for qsort.
• (6)Prove “msort (msort.hs, topdown / bottomup merge_sort) returns an ascending chain” by Isabelle/HOL
• (7) Prove that the input and the output of qsort, msort are the same as multisets, by Isabelle/HOL.