Think Stitch
PRINCIPIA  最近の更新


Isabelle による双模倣性の最大不動点による定義との同値性とトレース同値含意の証明

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

双模倣(Bisimulation and Bisimilar)

双模倣性は2つの状態遷移系が同じであるかどうかを判定するための重要な基準の1つなんだそうです.ラベル付き遷移システム(Labelled-Transition System, LTS)が遷移関係 M で与えられているとします.

\[ M \subseteq S \times E \times S \]

ここで S は状態の集合,E はラベル(イベント)の集合です.

状態間の関係 R

\[ R \subseteq S \times S \]

が双模倣(bisimulation)であるとは次のように定義されているそうです.

\begin{align} & \forall p, q, e. (p, q) \in R \Rightarrow \\ &\qquad (\forall p'. (p, e, p') \in M \Rightarrow (\exists q'. (q, e, q') \in M \land (p', q') : R)) \land \\ &\qquad (\forall q'. (q, e, q') \in M \Rightarrow (\exists p'. (p, e, p') \in M \land (p', q') : R)) \end{align}

平たくいえば,(p, q) ∈ R であるような p と q があったとき,p から先で起こりうることは q から先でも起こるし,逆もいえるということです.異なる遷移システムを比較している場合は,一方ができることは他方もできて,逆もいえるというわけです.

2つの状態 p と q が双模倣(bisimilar)であるとは,ある双模倣(bisimulation)R が存在して (p, q) ∈ R となることだそうです.日本語だとちょっとややこしいですけど.記号では次のように書くそうです.

\[ p \sim q \]

この関係 〜 は同値関係で,さらに最大の双模倣(bisimulation)になるのだそうです.ますますややこしいです.

Wikipedia をながめていたら,双模倣関係には別の定義があると書いてありました.ある関数 F があって,その最大不動点が双模倣関係だというのです(なにそれかっこいいと思いました).関数 F の定義は次のように書いてありました.

\begin{align} & F(R) = \{(p, q)\,| \\ &\qquad (\forall e, p'. (p, e, p') \in M \Rightarrow (\exists q'. (q, e, q') \in M \land (p', q') : R)) \land \\ &\qquad (\forall e, q'. (q, e, q') \in M \Rightarrow (\exists p'. (p, e, p') \in M \land (p', q') : R)) \} \end{align}

双模倣(bisimulation)の定義と似ていますけど,こちらは後ろから前を求めるような感じになってます.

ちょっと調べてみたら,このあたりのことはよく知られていて,coinduct とかなんとか,なにやら奥の深い話があるそうです.ここではそっちに深入りすることはせず,上の2つの定義が同値であることを証明してみたいと思います.

前準備

まず状態とラベル(イベント)の集合(型)を用意しておきます.

typedecl state
typedecl label

遷移関係 M を宣言しておきます.以下に定義する各関数でいちいち引数に持たせるのが面倒だからです.特定の M を用意するわけではないので,一般性は失いません.

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

準備は以上です.

Bisimulation の定義

状態上の関係 R が bisimulation であることを表す述語 bisim を定義します.上の定義のとおり書くだけです.

definition bisim :: "(state * state)set => bool"
where
  "bisim R = (ALL p q a. (p, q) : R -->
               (ALL p'. (p, (a, p')) : M -->
                 (EX q'. (q, (a, q')): M & (p', q') : R)) &
               (ALL q'. (q, (a, q')) : M -->
                 (EX p'. (p, (a, p')): M & (p', q') : R)))"

Bisimular 関係の定義

続いて bisimilar 関係の定義です.これもそのままです.

definition Bs :: "(state * state)set"
where
  "Bs = {(p, q). EX R. bisim R & (p, q) : R}"

関数 F の定義

definition F :: "(state * state)set => (state * state)set"
where
  "F R = {(p, q). (ALL a p'. (p, (a, p')) : M -->
                    (EX q'. (q, (a, q')) : M & (p', q') : R)) &
                  (ALL a q'. (q, (a, q')) : M -->
                    (EX p'. (p, (a, p')) : M & (p', q') : R))}"

2つの定義が同値であることの証明

証明すべき命題は次のものです.

Bs = gfp F

ここで gfp F は関数 F の最大不動点(greatest fixed point)です.Isabelle で用意されている関数です.

詳細な説明は抜きにして証明だけ示します.関数 F が単調であることを示すこと(mono F)と,coinduct_set という推論規則を使うところがポイントです(と,Isabelle のチュートリアルに書いてあったので,わけもわからず使ってみただけなんですけどね :P)

lemma monoF [intro]: "mono F"
apply(unfold mono_def F_def)
apply(auto)
apply(rename_tac S R p q a p')
apply(blast)
apply(blast)
done

lemma gfp1: "[| x : gfp f; mono f |] ==> x : f (gfp f)"
by (metis gfp_unfold)

lemma b1: "[| bisim R; (a, b) : R |] ==> (a, b) : gfp F"
apply(rule coinduct_set)
apply(rule monoF)
apply(assumption)
apply(unfold bisim_def F_def)
apply(auto)
apply(blast)
apply(blast)
done

lemma b2: "bisim (gfp F)"
apply(unfold bisim_def)
apply(auto)
apply(drule gfp1)
apply(rule monoF)
apply(unfold F_def)
apply(auto)
apply(drule gfp1)
apply(rule monoF)
apply(unfold F_def)
apply(auto)
done

lemma b3: "(a, b) : gfp F ==> EX R. bisim R & (a, b) : R"
apply(rule_tac x="gfp F" in exI)
apply(auto)
apply(rule b2)
done

theorem "Bs = gfp F"
apply(unfold Bs_def)
apply(auto)
apply(erule b1)
apply(assumption)
apply(rule b3)
apply(assumption)
done

双模倣性はトレース同値を含意することの証明

あちこち覗いていた文書の1つに,双模倣性はトレース同値を含意すると書いてありました.トレースというのは遷移システム(あるいはプロセス)が初期状態から発生させるイベントの列のことです.平たくいえば実行ログってことですね.遷移システムが発生させうるトレースは遷移システムごとに決まるわけで,それをすべて集めた集合を考えれば,その遷移システムの振る舞いを表していると考えることができるます.上の表明の意味は,2つの状態 p と q が双模倣なら,そこから発生するトレースのすべての集合は一致するという意味です.これについてはすでに知っていました.自分のプログラムで実際に使っているので.そうなる理由もほぼ自明のような気もしますけど,ちゃんと証明してみることにします.

計算列の定義

指定された初期状態から可能な遷移の道筋を,状態も含めて並べたものを計算列と呼ぶことにします.これをすべて求めた集合を paths と呼ぶことにします.帰納的定義を使います.

inductive_set
paths :: "state => (state * event * state)list set"
for p :: state
where
  base0 [intro]: "[] : paths p" |
  base1: "(p, (e, q)) : M
            ==> [(p, (e, q))] : paths p" |
  step: "[| (q, (e, q')) : M; cs : paths p; cs ~= [];
            snd (snd (hd cs)) = q |]
            ==> (q, (e, q'))#cs : paths p"

計算列をトレースに変換する関数 path_to_trace

計算列をトレースに変換する関数 path_to_trace を定義します.ラベル(イベント)の部分を取り出すだけです.map を使ってもいいんですけど,わかりやすく再帰的定義を直接書きました.

fun path_to_trace :: "(state * event * state)list => event list"
where
  "path_to_trace [] = []" |
  "path_to_trace ((p, (e, q))#cs) = e#(path_to_trace cs)"

トレース集合 traces の定義

すべての計算列の集合 paths の関数 path_to_trace による像を求めればトレース集合になります.バッククオォートは像を意味します.

definition traces :: "state => event list set"
where
  "traces p = path_to_trace ` (paths p)"

双模倣がトレース同値を含意することの証明

双模倣が対称であることは自明なので,トレース集合の一方の包含関係を示せば十分でしょう.示すべき命題は次のものになります.

EX R. bisim R & (p, q) : R ==> traces p <= traces q

証明だけ示します.

lemma bisim_D: "bisim R ==>
(ALL p q a. (p, q) : R -->
               (ALL p'. (p, (a, p')) : M -->
                 (EX q'. (q, (a, q')): M & (p', q') : R)) &
               (ALL q'. (q, (a, q')) : M -->
                 (EX p'. (p, (a, p')): M & (p', q') : R)))"
apply(unfold bisim_def)
apply(auto)
done

lemma b0 [rule_format]:
  "ps : paths p
  ==> bisim R --> (p, q) : R -->
  (EX qs : paths q. length ps = length qs &
    (ALL k < length ps.
      fst (snd (ps!k)) = fst (snd (qs!k)) &
       (snd (snd (ps!k)), snd (snd (qs!k))) : R))"
apply(erule paths.induct)
apply(auto)
apply(drule bisim_D)
apply(drule_tac x="p" in spec)
apply(drule_tac x="q" in spec)
apply(drule_tac x="e" in spec)
apply(clarsimp)
apply(drule_tac x="qa" in spec)
apply(clarsimp)
apply(rule_tac x="[(q, e, q')]" in bexI)
apply(auto)
apply(erule paths.base1)
(**)
apply(case_tac cs)
apply(auto)
apply(frule_tac x="0" in spec)
apply(clarsimp)
apply(case_tac qs)
apply(clarsimp)
apply(clarsimp)
apply(drule bisim_D)
apply(drule_tac x="b" in spec)
apply(drule_tac x="ba" in spec)
apply(drule_tac x="e" in spec)
apply(clarsimp)
apply(drule_tac x="q'" in spec)
apply(clarsimp)
apply(rule_tac x="(ba, e, q'a)#(ab, ac, ba)#lista" in bexI)
apply(auto)
apply(case_tac k)
apply(auto)
apply(case_tac k)
apply(auto)
apply(erule paths.step)
apply(auto)
done

lemma p2t0 [rule_format]:
  "ALL qs. length xa = length qs &
  (ALL k path_to_trace xa = path_to_trace qs"
apply(induct_tac xa)
apply(auto)
apply(case_tac qs)
apply(auto)
apply(rotate_tac -1)
apply(drule_tac x="0" in spec)
apply(clarsimp)
apply(drule_tac x="lista" in spec)
apply(auto)
done

theorem
  "EX R. bisim R & (p, q) : R
     ==> traces p <= traces q"
apply(unfold traces_def)
apply(clarsimp)
apply(drule_tac R="R" and p="p" and q="q" in b0)
apply(auto)
apply(rule_tac x="qs" in rev_image_eqI)
apply(auto)
apply(rule p2t0)
apply(auto)
done
2013/12/17
© 2013,2014,2015 PRINCIPIA Limited