Think Stitch
PRINCIPIA  最近の更新


Isabelle チュートリアルからモデル検査アルゴリズムの正当性検証の紹介

Theorem Prover Advent Calendar 2013の参加エントリです.

今回は自分で証明したものではなくて,Isabelle のチュートリアルにある例をご紹介したいと思います.定理証明支援系の威力を見せつけられた例なので,ぜひご紹介したかったのです.お題はモデル検査です.CTL (Computation Tree Logic) ベースのモデル検査アルゴリズムの正当性を証明した例です.まったくもってすごいことができるものです.しかも証明自体は状態が無限にある場合でも有効です.アルゴリズムは停止しませんけどね :P

準備

状態の集合(型)state と命題の集合 atom を用意しておきます.遷移関係を M で表します.各状態で成り立つ命題を表すラベル関数 L もあるとします.状態 s に対して L s はその状態で成り立つ命題の集合を表します.

typedecl state
typedecl "atom"
consts M :: "(state * state)set"
consts L :: "state => atom set"

CTL 式の定義

代数的データ型を使って CTL の式(構文)を定義します.選言,EG, AG は 連言,AF, EF の dual なので省略してます.

datatype formula = Atom "atom"
                 | Neg formula
                 | And formula formula
                 | AX formula
                 | EF formula
                 | AF formula

CTL 式の意味定義

次に CTL 式の意味を定義します.状態 s において CTL 式 f が真であることを s |= f と表します.|= はダブルターンスタイルのつもりです.Isabelle は関数に infix 表記の演算子を定義することができます.

primrec valid :: "state => formula => bool" ("(_ |= _)" [80,80] 80)
  where
  "s |= Atom a = (a : L s)" |
  "s |= Neg f = (~ (s |= f))" |
  "s |= And f g = (s |= f & s |= g)" |
  "s |= AX f = (ALL t. (s,t) : M --> t |= f)" |
  "s |= EF f = (EX t. (s,t) : M^* & t |= f)" |
  "s |= AF f = (ALL p : Paths s. EX i. p i |= f)"

順に見ていくことにします.(私がへたな説明をするよりちゃんとした本を見ていただく方がいいのですが.)

definition Paths :: "state => (nat => state)set" where
  "Paths s == {p. s = p 0 & (ALL i. (p i, p(i+1)) : M)}"

関数 Paths は指定された状態 s から可能なすべてのパスの集合を表します.無限の長さのパス,無限の要素を持つ集合があっさり表現できちゃうところが定理証明支援系のすごいところです.

モデル検査アルゴリズムの表現

次はモデル検査のアルゴリズムを表現します.モデル検査を行う関数を mc とします.関数 mc は CTL 式 f を受け取り,それが成り立つ状態の集合を返す関数です.

primrec mc :: "formula => state set" where
  "mc(Atom a) = {s. a : L s}" |
  "mc(Neg f) = -mc f" |
  "mc(And f g) = mc f Int mc g" |
  "mc(AX f) = {s. ALL t. (s,t) : M --> t : mc f}" |
  "mc(EF f) = lfp(%T. mc f Un (M^-1 `` T))" |
  "mc(AF f) = lfp(af(mc f))"

アルゴリズムは CTL 式の構造を再帰的にたどりながら実行します.

definition af :: "state set => state set => state set" where
  "af A T == A Un {s. ALL t. (s, t) : M --> t : T}"

EF も AF も,すでにマークされている状態の遷移元の状態を調べていくことになります.

アルゴリズムの正当性証明

証明したい命題は次のとおりです.

mc f = {s. s |= f}

証明だけ示します.

lemma mono_ef: "mono (%T. A Un (M^-1 `` T))"
apply(rule monoI)
apply(blast)
done

lemma EF_lemma: "lfp (%T. A Un (M^-1 `` T)) = {s. EX t. (s,t) : M^* & t : A}"
apply(rule equalityI)
apply(rule subsetI)
apply(simp)
apply(erule lfp_induct_set)
apply(rule mono_ef)
apply(simp)
apply(blast intro: rtrancl_trans)
apply(rule subsetI)
apply(simp, clarify)
apply(erule converse_rtrancl_induct)
apply(subst lfp_unfold[OF mono_ef])
apply(blast)
apply(subst lfp_unfold[OF mono_ef])
apply(blast)
done

lemma mono_af: "mono(af A)"
apply(simp add: mono_def af_def)
apply(blast)
done

theorem AF_lemma1: "lfp(af A) <= {s. ALL p : Paths s. EX i. p i : A}"
apply(rule lfp_lowerbound)
apply(auto simp add: af_def Paths_def)
apply(erule_tac x = "p 1" in allE)
apply(auto)
done

lemma not_in_lfp_afD:
  "s ~: lfp(af A) ==> s ~: A & (EX t. (s,t) : M & t ~: lfp(af A))"
apply(erule contrapos_np)
apply(subst lfp_unfold[OF mono_af])
apply(simp add: af_def)
done

primrec path :: "state => (state => bool) => (nat => state)" where
  "path s Q 0 = s" |
  "path s Q (Suc n) = (SOME t. (path s Q n,t) : M & Q t)"

lemma infinity_lemma:
  "[| Q s; ALL s. Q s --> (EX t. (s,t) : M & Q t) |] ==>
  EX p : Paths s. ALL i. Q(p i)"
apply(subgoal_tac
  "EX p. s = p 0 & (ALL i::nat. (p i, p(i+1)) : M & Q(p i))")
apply(simp add: Paths_def, blast)
apply(rule_tac x = "path s Q" in exI)
apply(clarsimp)
apply(induct_tac i)
apply(simp)
apply(fast intro: someI2_ex)
apply(simp)
apply(rule someI2_ex)
apply(blast)
apply(rule someI2_ex)
apply(blast)
apply(blast)
done

theorem AF_lemma2: "{s. ALL p : Paths s. EX i. p i : A} <= lfp(af A)"
apply(rule subsetI)
apply(erule contrapos_pp)
apply simp
apply(drule infinity_lemma)
apply(auto dest: not_in_lfp_afD)
done

theorem "mc f = {s. s |= f}"
apply(induct_tac f)
apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2])
done
2013/12/18
© 2013,2014,2015 PRINCIPIA Limited