Isabelle Tutorial その18

6.6 Case Study: Verified Model Checking

ケーススタディとしてComputation Tree Logic(CTL)を使ったモデル検査を取り上げます。モデル検査の基礎は集合論であり、これをHOLを使って見てみます。まずpropositional dynamic logic(PDL)と呼ばれる単純な様相論理を見てから、実際に多くのモデル検査器が使用するCTLに進みます。それぞれについて意味(|=)と再帰関数mcを定義し、それらが一致することを証明します。

ここで扱うモデルは、状態の集合と遷移からなる遷移システムです。それぞれの状態にはユニークな名前があり、またその状態が満たす原始命題が関連付けられています。状態の型は次のように定義します。

typedecl state

コマンドtypedeclは詳細を定義することなく新しい型を宣言します。同様に遷移を状態間の関係として宣言します。

consts M :: "(state * state) set"

コマンドconstsは詳細を定義することなく定数を宣言します。最後に、原始命題とラベリング関数を宣言します。

typedecl "atom"
consts L :: "state => atom set"

ラベリング関数は、それぞれの状態でどの原始命題が真となるかを表わします。

6.6.1 Propositional Dynamic Logic - PDL

PDLの式は原始命題、否定、論理積、そして二つの様相論理の演算子AXとEFから成ります。

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

式の意味を状態との正当性関係(|=)で定義します。

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)"

AX fは全ての次の状態(All neXt)においてfが真であることを意味し、EF fはfを満たす状態まで到達する可能性がある(there Exists some Future)ことを意味します。

次に、モデル検査器を考えます。モデル検査器は、与えられた式が真となる状態の集合を返すとします。これは次のような関数として定義できます。

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))"

M^-1 `` TはTに含まれる状態に遷移可能な状態を表わし、% T. mc f Un (M^-1 `` T)の最小不動点(lfp)はmc fに到達する可能性のある状態のみからなる集合を表わします。mc (EF f)が正しいことを簡単には理解できないかもしれませんが、問題ありません。すぐに証明します。

先に、確かに最小不動点を持つことを確認するため、lfpの中の関数が単調であることを証明します。

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

次に、EFの場合を個別の補題として証明します。

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)

残ったサブゴールの一つ目は次のようになっています。

 1. !!x. x : lfp (%T. A Un M^-1 `` T) ==> EX t. (x, t) : M^* & t : A

これは、lfpの帰納ルールで証明します。

apply(erule lfp_induct_set)
apply(rule mono_ef)
apply(simp)

 1. !!xa. xa : A |
          xa : M^-1 `` (lfp (%a. A Un M^-1 `` a) Int {x. EX t. (x, t) : M^* & t : A})
          ==> EX t. (xa, t) : M^* & t : A

M^*の推移律を使い、blastで証明が完了します。

apply(blast intro: rtrancl_trans)

二つ目のサブゴールに対して、まずは同じように進めます。

apply(rule subsetI)
apply(simp, clarify)

 1. !!x t. [| (x, t) : M^*; t : A |] ==> x : lfp (%T. A Un M^-1 `` T)

このサブゴールは(s, t) : M^*の帰納的推論から証明できそうです。しかし、モデル検査器は後ろ向き(tからsの向き)に探索していくため、前向きに働くrtrancl_inductは使えません。このような場合は、converse_rtrancl_inductを使用します。

[| (?a, ?b) : ?r^*; ?P ?b;
   !!y z. [| (y, z) : ?r; (z, ?b) : ?r^*; ?P z |] ==> ?P y |]
==> ?P ?a　　　　　　　　　　　　　　　　　　　　　　(converse_rtrancl_induct)

apply(erule converse_rtrancl_induct)

基底ケースはlfpを展開し証明できます。

apply(subst lfp_unfold [OF mono_ef])
apply(blast)

帰納ケースも同様です。

apply(subst lfp_unfold [OF mono_ef])
apply(blast)
done

この補題を使ってメインゴールを証明します。

theorem "mc f = {s. s |= f}"
apply(induct_tac f)
apply(auto simp add: EF_lemma)
done

Exercise 6.6.1

ENは次の意味を持つ、AXの双対となる演算子です。

s |= EN f = (EX t. (s, t) : M & t |= f)

EN fは既に定義したPDLの式で表わすことができます。更に、EFが次の定理を満たすことを証明します。

s |= EF f = (s |= f | s |= EN (EF f))

definition EN :: "formula => formula" where
"EN f == Neg (AX (Neg f))"

lemma "s |= EN f = (EX t. (s, t) : M & t |= f)"
apply(simp add: EN_def)
done

lemma "s |= EF f = (s |= f | s |= EN (EF f))"
apply(simp add: EN_def)
apply(rule iffI)
apply(blast dest: converse_rtranclE)
apply(blast intro: rtrancl_trans)
done

6.6.2 Computation Tree Logic - CTL

PDLの式に新しい演算子を追加します。

| AF formula

AF fはいずれfを満たす状態に到達する(Always in the Future)ことを意味します。これを形式化するために、遷移関係の列を定義します。

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

Paths sはsから遷移可能な全てのパスを返します。これを使ってAFの意味を定義します。

"s |= AF f    = (ALL p. p : Paths s --> (EX i. p i |= f))"

モデル検査器で使用する関数は少し複雑なので、別に定義します。

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

mc (AF f)はTの最小不動点で定義でき、ここでTはmc fと、Tに含まれる状態にのみ遷移可能な状態を含みます。

"mc (AF f)    = lfp(af (mc f))"

前と同じように、afが単調なことを証明します。

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

証明したいことはmc (AF f) = {s. s |= AF f}ですが、それぞれの向きについて別に証明します。まずは簡単な方からいきます。

lemma AF_lemma1: "lfp(af A) <= {s. ALL p : Paths s. EX i. p i : A}"

EFの時と同じように証明することもできますが、ここでは違うやり方をしてみます。David Parkにちなんで名付けられたPark帰納法を使用してみます。

?f ?A <= ?A ==> lfp ?f <= ?A　　　　(lfp_lowerbound)

apply(rule lfp_lowerbound)
apply(auto simp add: af_def Paths_def)

次のサブゴールが残ります。

 1. !!p. [| ALL t. (p 0, t) : M -->
                   (ALL p. t = p 0 & (ALL i. (p i, p (Suc i)) : M) -->
                           (EX i. p i : A));
            ALL i. (p i, p (Suc i)) : M |]
         ==> EX i. p i : A

このサブゴールは、tをp 1とすると証明できそうです。

apply(erule_tac x = "p 1" in allE)
apply(auto)
done

逆向きは、対偶を証明します。状態sがlfp (af A)に含まれないならば、sから始まり、Aに含まれない状態のみからなる無限の遷移列が作れるはずです。まず、無限の遷移列の中の一つの遷移のみを証明してみます。

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)"

この列のn + 1番目の状態は、Qを満たす任意の状態です。以下ではそのような状態が存在するという前提の元でのみ、この関数を使用します。

Qを満たす状態からまたQを満たす状態へ遷移可能ならば、Qを満たす状態のみからなる無限列を構成できることを証明します。

lemma infinite_lemma:
"[| Q s; ALL s. Q s --> (EX t. (s, t) : M & Q t) |] ==> EX p : Paths s. (ALL i. Q (p i))"

まず、無限列の性質と、Qを満たすという条件を同時に証明するため、結論を少し書き換えます。

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)

新しいサブゴールは、path s Qが存在することから証明します。

apply(rule_tac x = "path s Q" in exI)
apply(clarsimp)

 1. !!i. [| Q s; ALL s. Q s --> (EX t. (s, t) : M & Q t) |]
         ==> (path s Q i, SOME t. (path s Q i, t) : M & Q t) : M & Q (path s Q i)

残ったサブゴールはiに関する帰納法で証明します。

apply(induct_tac i)
apply(simp)

基底ケースは次のようになります。

 1. [| Q s; ALL s. Q s --> (EX t. (s, t) : M & Q t) |]
    ==> (s, SOME t. (s, t) : M & Q t) : M

結論のtが存在することは明らかです。これは、定理someI2_exで証明できます。

[| EX a. ?P a; !!x. ?P x ==> ?Q x |] ==> ?Q (SOME x. ?P x)　　　　(someI2_ex)

fastを使用して一気に進みます。

apply(fast intro: someI2_ex)

ここでblastではなくfastを使用したのは、結論部のスキーム変数がネストしており、someI2_exの結論部と単純には単一化できないためです。blastはこの単一化ができませんが、fastならばできます。

帰納ケースも同様ですが、SOMEがネストしているため少し複雑です。fastでは証明が完了しないため、一つずつsomeI2_exを適用していきます。

apply(rule someI2_ex)
apply(simp)
apply(rule someI2_ex)
apply(blast)
apply(blast)
done

ようやくAF_lemma1の逆を証明できます。

lemma AF_lemma2: "{s. ALL p : Paths s. EX i. p i : A} <= lfp(af A)"

まず、対偶の証明に変換します。

apply(rule subsetI)
apply(erule contrapos_pp)
apply(simp)

 1. !!x. x ~: lfp (af A) ==> EX p:Paths x. ALL i. p i ~: A

infinite_lemmaを破壊規則として適用すると、二つのサブゴールが得られます。

apply(drule infinite_lemma)

 1. !!x. ALL s. s ~: lfp (af A) --> (EX t. (s, t) : M & t ~: lfp (af A))
 2. !!x. EX p:Paths x. ALL i. p i ~: lfp (af A) ==> EX p:Paths x. ALL i. p i ~: A

どちらもnot_in_lfp_afDを使用して証明が完了します。

apply(auto dest: not_in_lfp_afD)

PDLと同様、メインの定理を証明します。

theorem "mc f = {s. s |= f}"
apply(induct_tac f)
apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2])
done

ここで定義したCTLは完全ではありません。CTLには演算子EUもあります。EU f gはgを満たす状態までずっとfを満たす状態のみの遷移列が存在する(there Exists ... Until ...)ことを意味します。補助関数を定義します。

primrec until :: "state set => state set => state => state list => bool" where
"until A B s []    = (s : B)" |
"until A B s (t#p) = (s : A & (s, t) : M & until A B t p)"

この補助関数を使用して、EUの意味を定義します。

"s |= EU f g  = (EX p. until {t. t |= f} {t. t |= g} s p)"

EUを、それ以外の演算子を使用して表わすことはできません。

EUに対するモデル検査器の定義は次のようにlfpを使用します。

"mc (EU f g)  = lfp(% T. mc g Un mc f Int M^-1 `` T)"

Exercise 6.6.2

上のCTLの定義に演算子EUを追加し、その意味とモデル検査器の振る舞いが一致することを証明します。

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

lemma EU_lemma1: "lfp(% T. A Un B Int (M^-1 `` T)) <= {s. EX p. until B A s p}"
apply(rule subsetI)
apply(erule lfp_induct_set)
apply(rule mono_eu)
apply(auto)
apply(rule_tac x = "[]" in exI)
apply(simp)
apply(rename_tac x xs)
apply(rule_tac x = "x#xs" in exI)
apply(simp)
done

lemma in_lfp_euI [rule_format]:
"ALL x. until B A x xs --> x : lfp(% T. A Un B Int M^-1 `` T)"
apply(induct_tac xs)
apply(subst lfp_unfold [OF mono_eu])
apply(simp)
apply(subst lfp_unfold [OF mono_eu])
apply(auto)
done

lemma EU_lemma2: "{s. EX p. until B A s p} <= lfp(% T. A Un B Int M^-1 `` T)"
apply(rule subsetI)
apply(clarsimp)
by(rule in_lfp_euI)

theorem "mc f = {s. s |= f}"
apply(induct_tac f)
apply(auto simp add:
  EF_lemma equalityI[OF AF_lemma1 AF_lemma2] equalityI[OF EU_lemma1 EU_lemma2])
done