Systems and Software Verification 2. Temporal Logic システム情報科学府 情報工学専攻 荒木研究室 修士2年 住田 辰雄 目次 • • • • • • 2.0 時相論理 2.1 時相論理の言語 2.2 時相論理の構文 2.3 時相論理の意味論 2.4 PLTLとCTL 2.5 CTL*の記述力 2006/9/14 モデル検査勉強会 2 2.0 時相論理 • 時相論理 – 時間の経過の概念を含む記述や推論を扱うのに 適した論理である – 一階述語論理などと比較して，時相論理は明快 かつ単純である • 時間を表すtパラメータが存在しない – 形式意味論に基づき，不可欠なモデル検査ツー ルが存在する 2006/9/14 モデル検査勉強会 3 2.1 時相論理の言語 • CTL* – システムの実行に関する性質を形式的に記述することが できる – 1.原子命題 • 実行系列とは状態の列であり，時相論理は状態について原子命 題を用いて記述する • 原子命題は与えられた状態について真偽を取る • Ex. nice_weather, open, in_phase_1, x+2=y, etc. – 2. ブール結合子 • • • • 2006/9/14 真と偽 否定（￢），論理積（∧），論理和（∨），含意（⇒），同値（⇔） 今後述語命題とは原子命題とブール結合子の混合物を指す Ex. error ⇒ ￢warm モデル検査勉強会 4 2.1 時相論理の言語 • 3. 論理結合子 – 論理結合子は単なる状態それぞれについてではなく，ある実行系列 の状態の列に関して記述する – Pは現在の状態の性質とする – XP • 次の状態がPを満足する • Ex. P ∨ XP – FP • 以降いずれかの状態がPを満足する • Ex. alert ⇒ F halt – GP • 以降全ての状態がPを満足する • GはFの対偶である – Gφ≡￢F￢φ • Ex. G(alert ⇒ F halt) 2006/9/14 モデル検査勉強会 5 2.1 時相論理の言語 • 4. 入れ子構造 – 論理結合子を組み合わせることで新たな論理式を作るこ とができる – FとGは反復性質の表現に良く用いられる • GF – 常にφを満たすような状態がいつか存在する • FG – ある状態から常にφを満たす • 5. U and W – φ1 U φ2 • φ2が真になるまでφ1は真である – φ1 W φ2 • φ2が真でない間はφ1は真である 2006/9/14 モデル検査勉強会 6 2.1 時相論理の言語 EG P : (= E￢F￢P) EF P : P P P P AF P : (= ￢E￢FP) P P 2006/9/14 P AG P : (= ￢EF￢P) P P P モデル検査勉強会 P P P P 7 2.1 時相論理の言語 • 6. 経路限定子 – これまではある実行系列に対する性質についてのみ扱う ことができたが，経路限定子を用いることで複数の実行 系列を評価することができる – Aφ • 現在の状態から始まる全ての実行系列はφを満たす – Eφ • 現在の状態から始まるいくつかの実行系列の中にφを満たす状 態が存在する – AはEの対偶である • Aφ≡￢E￢φ 2006/9/14 モデル検査勉強会 8 2.2 時相論理の構文 • CTL*の形式文法 φ, ψ ::= P1 | P2 | … |￢φ|φ∧ψ|φ⇒ψ|… |Xφ|Fφ|Gφ|φUψ|… 原始命題 ブール結合子 論理結合子 |Eφ|Aφ 経路限定子 • 各モデル検査は，特有の原始命題や論理結 合子を含む • CTLやPLTLなどのモデル検査で扱うことの 出来る範囲はCTL*の断片に制限される 2006/9/14 モデル検査勉強会 9 2.3 時相論理の意味論 • 時相論理のモデルはKripke構造と呼ばれる • CTL*のような状態ベースの論理において状 態にラベル付けする命題は重要な役割を果 たすが，遷移にラベル付けするアクションは あまり意味を成さない 2006/9/14 モデル検査勉強会 10 2.3 時相論理の意味論 σ, i |= P P ∈ l(σ(i)) σ, i |= ￢φ σ, i |≠ φ σ, i |= φ∧ψ σ, i |= φかつσ, i |= ψ σ, i |= Xφ i ＜ |σ| かつ σ, i+1 |= φ σ, i |= Fφ i ≦ j ≦ |σ| かつ j |= φを満たすjが存在する σ, i |= Gφ i ≦ j ≦ |σ| を満たす全てのjに対してσ, ｊ |= φ σ, i |= φUψ i ≦ j ≦ |σ| かつσ, ｊ |= ψを満たす jが存在し， i ≦ k ＜ j を満たす全 てのkに対して，σ, k |= φ σ, i |= Eφ σ(0)…σ(i) = σ’(0)…σ’(i)かつσ’, i |= φを満たすσ’が存在する σ, i |= Aφ σ(0)…σ(i) = σ’(0)…σ’(i) を満たす全てのσ’に対してσ’, i |= φ 表2.3 CTL*の意味論 2006/9/14 モデル検査勉強会 11 2.3 時相論理の意味論 • 補足 – A, σ, i |= φ • 実行系列σのi番目の状態においてφが真である • 以降Aを省略し，単にσ, i |= φと表記する – σ, i |≠ φ • 実行系列σのi番目の状態においてφが真ではない – σ(i) • 実行系列σのi番目の状態 – |σ| • 実行系列σの長さ – A |= φ • Aの全ての実行系列σに対して，σ, 0 |= φが真である 2006/9/14 モデル検査勉強会 12 2.3 時相論理の意味論 • 時間の本質 – σ, i |= φにおいてパラメータiは実行系列σの時間 の経過を示しており，一階述語論理のパラメータt と類似しているが，2つの論理には重要な違いが 存在する • 瞬間は実行系列におけるある点である • CTL*において，時間は不連続に表現される 2006/9/14 モデル検査勉強会 13 2.4 PLTL と CTL • 命題線形時間時相論理PLTLと分岐時間時 相論理CTLはモデル検査器において最も一 般的に用いられる時相論理である． • これらの起源は異なるがどちらもCTL*の断 片である 2006/9/14 モデル検査勉強会 14 2.4 PLTL と CTL • PLTL – PLTLはCTL*からAとE経路限定子を除いた論理である – PLTLは非決定的な選択が可能な各実行ステップにおい て，与えられた実行系列から分岐するような他の実行系 列を検査することができない • Fig. 2.4のA1とA2を区別することが不可能 – 経路論理式という表現を用い，このような形式化に対して 線形時相論理と呼ぶ – AG EFPを記述することができない • Pは常に到達可能である 2006/9/14 モデル検査勉強会 15 2.4 PLTL と CTL P, Q P, Q A1 : A2: P P Q 2006/9/14 P Q モデル検査勉強会 16 2.4 PLTL と CTL • CTL – CTLはCTL*にAかE経路限定子の範囲の元で唯一つの 論理結合子（X, F, U, etc.）の使用を求める論理である – CTLはある実行系列を繰り返し検査するため，複数の論 理結合子を入れ子にすることができない • Fig.2.4のA1とA2を区別することができる – 状態論理式という表現を用い，真偽は現在の状態とそれ から到達可能な状態領域にのみ依存し，現在の実行系 列に依存しない – EGFPを記述することができない • Pを無限に満たすような実行系列の存在 2006/9/14 モデル検査勉強会 17 2.4 PLTL と CTL • PLTLとCTLの比較 – システムに期待される振る舞いを記述する際に，CTLの欠点はPLTL よりも厄介である – CTLのたいていの欠点はFCTL(Fair CTL)を用いることで解消される • E(GF P ∧ GF Q) – – – – CTLのモデル検査はPLTLのモデル検査よりも効率的である 単に性質を記述することが目的であるならば，PLTLが向いている 網羅的な検証が目的であるならば，CTLが向いている ありそうなエラーを検出したいが，網羅的な検証までは望まないなら ば，PLTLが向いている – 代表的なモデル検査ツール • PLTL…SPIN • CTL…SMV 2006/9/14 モデル検査勉強会 18 2.5 CTL*の記述力 • まず第一に，何をモデル化するかの決定がな ければ，どんな論理も何も表現することは出 来ない – 第一章に登場したオートマトンは確率やタイミン グといった性質は必要がないため，考慮する必 要がなかった – 求められる記述力はどのようなモデルを記述した いかによって変化する • 実用的な面からすれば，CTL*はほぼ実用的 である 2006/9/14 モデル検査勉強会 19
© Copyright 2024 ExpyDoc
