遷移構造と双模倣関係

「対象の幾何学的モデルが、対象の幾何学的モデルであるという、_そ˙ _の˙ _事˙_実˙ _自˙ _体˙ _に˙ _よ˙_っ˙ _て˙

（ipso facto）」というこの回答は、それ自体でみれば、「モデル（模型）」という語の直観

的理解に頼った、一見あまりに短絡的な回答であるだろう。しかし、カントの量・質・関 係・様相のカテゴリーのうち、最後の「様相」のカテゴリーの判断を扱う、現代の様相論 理と、そのモデルである遷移構造（クリプキ構造）の、理論計算機科学における現実的使 用をみれば、この回答が予想以上に洗練された内実を備えてくる——このことが、この論 文で最後に指摘したい主要なポイントである。

このことをみるために、序論で取り上げた、自動販売機の遷移構造を振り返る。

図4.1

この遷移構造は、100円を入れると、水ボタンを押されるかコーヒーボタンを押されるか に応じて、水かコーヒーを出す、そのような自販機の状態遷移図であった。これを再び眺 めればわかるとおり、基本的に遷移構造（状態遷移図）とは、点「・」とその間の有向な 辺「−→」からなる有向グラフであり、純粋な幾何学的モデルといえる。前に述べたとお り、この遷移構造のように、辺にラベル（名前）がつけられたものを、ラベル付き遷移構 造と呼ぶが、このラベルは、上の図で点に名前をつけているのと同様、ただ辺の種類を区 別するためのものであり、この純粋な幾何学性に本質的に影響するものではない。

さて、上のラベル付き遷移構造をP とすると、このラベル付き遷移構造 P ^を、コン ピューター科学者は、現実の自販機の模型、モデルとして用いる。そしてたとえば、P ^上 の点P₁ が表す状態で、次の様相式

[100](⟨coffee⟩[100](⟨coffee⟩tt∧ ⟨water⟩tt)∧ ⟨water⟩⟨[100](⟨coffee⟩⟨100⟩tt∧ ⟨water⟩tt)) が成り立つ、つまり、

P₁ |=

[100](⟨coffee⟩[100](⟨coffee⟩tt∧ ⟨water⟩tt)∧ ⟨water⟩⟨[100](⟨coffee⟩⟨100⟩tt∧ ⟨water⟩tt)) と判断する。これは、自販機の状態 P₁ で、100円を入れたら、コーヒーか水を出すこと ができて、どちらを出した場合も、また100円を入れたら、同様に、コーヒーか水を出 すことができる、という（この自販機の再帰的な機能についての）判断を表している。こ こで、いま実際に、上の遷移構造をモデルとして現実に組み立てられた、自販機があった としよう。さて、この場合、コンピューター科学者は、自分のこの判断はただ、上の遷移 構造についてのみ、真/偽の評価を受けるのであって、現実の自販機については、自分の この判断は真/偽の評価を受けない、などと考えるだろうか。言うまでもなく、彼はこの ときこの判断が、同時に、他ならぬ現実の自販機について、同じ真/偽の評価を受けるは ずであることを、改めて確認するまでもない前提としているだろう。それはもちろん、彼 のこの判断が、現実の自販機の遷移構造をモデルとしてなされたという、その事実自体に よって、彼はこの判断の真/偽を、現実の自販機についての客観的な評価とするだろうか らであり、また、逆にいえば、彼のこの判断の真/偽を、現実の自販機についての客観的な 評価とするためにこそ、自販機の遷移構造をモデルとして使用するのだろうからである。

ここで現代の様相論理を駆使するコンピューター科学者に特権的であることは、彼らは もはや、それがたんに自販機のモデルだから、という、「モデル（模型）」という語の直観 的理解によってのみ、自らの判断の真/偽の評価の客観性に、確信をもつ必要がない、と いうことである。彼らは現在事実上、そのような確信がもてる理論的・技術的根拠を有し ている。それが「双模倣bisimulation」と呼ばれる数学的に厳密に定義された関係概念で ある。

ただし、ここでのポイントを理解するために、「双模倣bisimulation」の厳密な定義（付 録 A.7）に立ち入る必要はない。ここでのポイントは、コンピューター科学者は、上の自 販機の遷移構造と、現実の自販機の間に、この「双模倣関係」を、_漸˙ _近˙ _的˙_{に形成できる、}˙ という原理的可能性に基づいて、遷移構造を使用することができる、ということである。

ここでは、このことを、いまの自販機の例に即して直観的に理解することで十分である。

そこでまず注意すべきことは、上の図は、現実の自販機の遷移構造の中でも最も単純化 されたものの一つであって、実際にはこの図が表す遷移構造よりも現実の自販機の挙動 を_よ˙ り忠実に再現する遷移構造が、無数に考えられる、ということである。たとえば、上˙ の図よりも現実の自販機の実際の挙動を_よ˙り忠実に再現していると考えられる、次のラベ˙ ル付き遷移構造Qを考えることができる。

図4.2

このように、自動販売機は現実には、時間に伴って少しずつ状態を変化させながら、100 円を入れたら、コーヒーか水を出し、その後また100円を入れたら、コーヒーか水を出し、

その後また100円を入れたら、· · ·、と以下同様に、この進展を繰り返していくだろう。

しかしここで、図4.1と図4.2の表す遷移構造P ^とQの間には、ある特別な対応関係 が成立している。まず P1 とQ1 をみてみよう。するとP1 からは100^{円遷移があって、}

その先にP₂という状態がある。これに対して、Q₁ からもまた、100円遷移があって、そ の先にQ2 という状態がある。このP1とQ1 の関係は逆もまた成り立つ。そこで今度は P2 とQ2をみてみよう。するとP2からはcoffee遷移があって、その先にP1 という状態 がある。これに対して、Q₂からもまた、coffee遷移があって、その先にQ₃という状態が ある。また、P2 からはwater 遷移もあって、その先にP1 という状態がある。これに対 して、Q2 からもまた、water遷移があって、その先にQ4 という状態がある。このP2 と Q₂ の関係は逆もまた成り立つ。そこで今度はP₁ とQ₃ をみてみよう。するとP₁ から は100円遷移があって、その先にP2 という状態がある。これに対して、Q3からもまた、

100円遷移があって、その先にQ5 という状態がある。このP1 とQ3 の関係は逆もまた 成り立つ。並行してP₁ とQ₄ もみてみよう。するとP₁ からは100円遷移があって、そ の先にP₂ という状態がある。これに対して、Q₄からもまた、100円遷移があって、その 先にQ8という状態がある。このP1とQ4 の関係は逆もまた成り立つ。そこで今度はP2

とQ₅ をみてみよう。するとP₂ からはcoffee遷移があって、· · ·、と、以下同様に続く。

おおよそこのような関係が、「双模倣bisimulation」関係である。以上によって感覚的 につかめるように、遷移構造上のある状態とある状態から始めて、そこから次から次へと どこまで次の状態に進んだとしても、一方がもつ状態遷移は他方ももち、逆もまた成り 立つとき、その意味で、どこまで進んでも、対応する状態の潜在能力を相互に（bi）模倣

（simulate）することができるとき、その出発点に位置するある状態とある状態が、（強）

双模倣関係にあると言われる。したがって今の場合、特に P₁ と Q₁ は双模倣であり、

P₁ ∼Q₁と表記される。

このとき、様相論理における最重要の基本定理である、ヘネシー・ミルナーの定理

（Hennessy-Milner theorem^{）が知られている。}

（HMT^）

双模倣関係にある、二つの遷移構造P, Q上の二つの状態は、ちょうど同じ様相式を満 たす。

つまり、二つの遷移構造P, Q^{が与えられたとき、}

それぞれに属するどの二つの状態P ∈ P, Q∈ Q^{と、どんな様相式}φについても、

if P∼Q, then P|=φ⇔Q|=φ となる。

したがって、いま、

φ:=

[100](⟨coffee⟩[100](⟨coffee⟩tt∧ ⟨water⟩tt)∧ ⟨water⟩⟨[100](⟨coffee⟩⟨100⟩tt∧ ⟨water⟩tt)) として、

P1 ∼Q1

かつ、

P1 |=φ より、

Q1 |=φ

がいえる。これは、コンピューター科学者が直接には図4.1の遷移構造P ^の状態P1 に適 用した真なる様相式が、そのまま、図4.2の遷移構造Q^の状態Q₁でも真なる様相式とな る、ということである。ここで、次の様相式も考えてみよう。

ψ:= [100](¬⟨coffee⟩tt∧ ⟨water⟩tt)

この式の意味は、この自販機のある状態について、100円を入れたら、コーヒーは買えず、

水だけが買える、ということである。この式はもちろん、図4.1の遷移構造P ^の状態P1

について偽である、つまり、

P1 ̸|=ψ

である。したがって、同様にヘネシー・ミルナーの定理より、

P1 ∼Q1

かつ、

P1 ̸|=ψ より、

Q1 ̸|=ψ

でもある。これは、様相式 ψが図4.1の遷移構造P ^の状態P1 で偽であると評価された 場合、それはそのまま、図4.2の遷移構造Q^の状態Q1 でも偽であると評価される、とい うことに他ならない。

ただし、図4.2の表す遷移構造Qもまた、現実の自販機そのものの挙動を、そのまま表 すものでは当然ありえない。そもそも、例えばコーヒーを出すcoffee遷移一つとってみて も、現実の自販機におけるこの動作にはその都度何らかの違いがあるだろう。さらにその 違いに応じて、この動作を完了した後の自販機の状態にも違いが生じるだろう。したがっ て当然のことながら、どんなに緻密な遷移構造も、現実の自販機それ自体を忠実に再現す ることはありえない。というより、一般に、現実の自販機それ自体を_必˙ _要˙_以˙ _上˙ _{に忠実に再}˙ 現することは、遷移構造の現実の使用にとって、深刻な障害になりさえする。その計算機 科学での極端な例が、あまりに詳細な状態遷移図を作った場合に、モデル検査において 検証すべき状態が爆発的な数にのぼり、検証が不可能になる、いわゆる「状態爆発 state explosion」である。

結局、遷移構造は、ある対象について、それが_わ˙_れ˙ _わ˙ _れ˙ _に˙ _関˙_心˙ _の˙ _あ˙ _る˙ _性˙ _{質をもつかど}˙ うかの判断を行うために形成される。そのためには、現実の対象から、適当な「抽象

abstraction」を行うことが必要となる。この「抽象」のプロセスの問題、その「適当さ

appropriateness」の問題は、それ自体、工学上の問題だけでなく、科学史・哲学史の上

でも集中的な探究が為されるべき重要な問題であるが、今われわれが確認したいことは、