バイシミュレーション

理論計算機科学において、双模倣とは状態遷移システム間の二項関係であり、一方のシステムが他方のシステムをシミュレートし、その逆もまた同様であるように動作するシステムを関連付けます。

直感的に言えば、2つのシステムが双相似であるとは、あるルールに従ってゲームをプレイしていると仮定した場合、互いの動きが一致することを意味します。この意味では、観察者にとってそれぞれのシステムを区別することはできません。

正式な定義

ラベル付き状態遷移システム （S ,Λ,→）（Sは状態の集合、はラベルの集合、→はラベル付き遷移の集合（すなわち、のサブセット））が与えられた場合、双模倣は二項関係であり、 Rとその逆は両方ともシミュレーションである。このことから、双模倣の対称閉包は双模倣であり、すべての対称シミュレーションは双模倣であることが分かる。したがって、一部の著者は双模倣を対称シミュレーションとして定義している。^[1]${\displaystyle \Lambda }$ ${\displaystyle S\times \Lambda \times S}$ ${\displaystyle R\subseteq S\times S}$ ${\displaystyle R^{T}}$

同様に、Rが双模倣となるのは、 Rのすべての状態ペアと のすべてのラベルλに対して次の条件が満たされる場合のみです。 ${\displaystyle (p,q)}$ ${\displaystyle \Lambda }$

• ならば、 が存在する。${\displaystyle p\mathrel {\overset {\lambda }{\rightarrow }} p'}$ ${\displaystyle q\mathrel {\overset {\lambda }{\rightarrow }} q'}$ ${\displaystyle (p',q')\in R}$
• ならば、となるような が存在する。${\displaystyle q\mathrel {\overset {\lambda }{\rightarrow }} q'}$ ${\displaystyle p\mathrel {\overset {\lambda }{\rightarrow }} p'}$ ${\displaystyle (p',q')\in R}$

Sにおける2つの状態pとqが与えられたとき、p がqと双相似（と表記）であるための必要十分条件は、 となる双相似 R が存在することである。これは、双相似関係∼がすべての双相似の和集合であることを意味する。すなわち、ある双相似Rに対して となるとき、まさに となる。 ${\displaystyle p\,\sim \,q}$ ${\displaystyle (p,q)\in R}$ ${\displaystyle (p,q)\in \,\sim \,}$ ${\displaystyle (p,q)\in R}$

双似集合は和集合に関して閉じている。^{[注 1]}したがって、双似関係自体も双似である。これはすべての双似の和集合であるため、唯一の最大の双似である。双似は反射閉包、対称閉包、推移閉包に関しても閉じている。したがって、最大の双似は反射閉包、対称閉包、推移閉包でなければならない。このことから、最大の双似、すなわち双似は同値関係であることが分かる。^[2]

代替定義

リレーショナル定義

バイシミュレーションは、関係の合成の観点から次のように定義できます。

ラベル付き状態遷移システム が与えられたとき、双模倣関係は、S上の二項関係R（すなわち、R ⊆ S × S）であり、${\displaystyle (S,\Lambda ,\rightarrow )}$ ${\displaystyle \forall \lambda \in \Lambda }$

$${\displaystyle R\ ;\ {\overset {\lambda }{\rightarrow }}\quad {\subseteq }\quad {\overset {\lambda }{\rightarrow }}\ ;\ R}$$ そして $${\displaystyle R^{-1}\ ;\ {\overset {\lambda }{\rightarrow }}\quad {\subseteq }\quad {\overset {\lambda }{\rightarrow }}\ ;\ R^{-1}}$$

関係合成の単調性と連続性から、双似集合は和集合（関係の半集合における結合）に関して閉じていることが直ちに示され、簡単な代数計算により、双似性の関係（すべての双似性の結合）は同値関係であることが示される。この定義と、それに関連する双似性の扱いは、任意の合流的量子において解釈できる。

固定点の定義

双類似性は、不動点理論の観点から、順序理論的に定義することもでき、より正確には、以下に定義される特定の関数の最大不動点として定義されます。

ラベル付き状態遷移システム( , Λ, → )が与えられたとき、 上の二項関係から上の二項関係への関数を次のように定義します。 ${\displaystyle S}$ ${\displaystyle F:{\mathcal {P}}(S\times S)\to {\mathcal {P}}(S\times S)}$ ${\displaystyle S}$ ${\displaystyle S}$

を 上の任意の二項関係とします。は、次の条件を満たす×内のすべてのペアの集合として定義されます。 ${\displaystyle R}$ ${\displaystyle S}$ ${\displaystyle F(R)}$ ${\displaystyle (p,q)}$ ${\displaystyle S}$ ${\displaystyle S}$

$${\displaystyle \forall \lambda \in \Lambda .\,\forall p'\in S.\,p{\overset {\lambda }{\rightarrow }}p'\,\Rightarrow \,\exists q'\in S.\,q{\overset {\lambda }{\rightarrow }}q'\,{\textrm {and}}\,(p',q')\in R}$$ そして $${\displaystyle \forall \lambda \in \Lambda .\,\forall q'\in S.\,q{\overset {\lambda }{\rightarrow }}q'\,\Rightarrow \,\exists p'\in S.\,p{\overset {\lambda }{\rightarrow }}p'\,{\textrm {and}}\,(p',q')\in R}$$

双類似度はの最大の不動点として定義されます。 ${\displaystyle F}$

エーレンフォイシュト・フライセ ゲームの定義

バイシミュレーションは、攻撃者と防御者の2人のプレイヤー間のゲームとして考えることもできます。^[3]

「攻撃者」が最初に行動し、から任意の有効な遷移を選択することができます。つまり 、 ${\displaystyle \lambda }$ ${\displaystyle (p,q)}$ $${\displaystyle (p,q){\overset {\lambda }{\rightarrow }}(p',q)}$$ $${\displaystyle (p,q){\overset {\lambda }{\rightarrow }}(p,q')}$$

「防御側」は攻撃側の動きに応じて、またはのいずれかからその遷移にマッチさせようと試みなければなりません。つまり、以下の条件を満たすものを見つけなければなりません 。 または ${\displaystyle \lambda }$ ${\displaystyle (p',q)}$ ${\displaystyle (p,q')}$ ${\displaystyle \lambda }$ $${\displaystyle (p',q){\overset {\lambda }{\rightarrow }}(p',q')}$$ $${\displaystyle (p,q'){\overset {\lambda }{\rightarrow }}(p',q')}$$

攻撃側と防御側は、次の状況になるまで交互にターンを続けます。

• 防御側は攻撃側の動きにマッチする有効なトランジションを見つけることができません。この場合、攻撃側が勝利します。
• ゲームは両方とも「デッド」な状態（つまり、どちらの状態からも遷移がない）に到達します。この場合、防御側が勝利します。${\displaystyle (p,q)}$
• ゲームは永久に続き、その場合、防御側が勝利します。
• ゲームは既に訪れた状態 に到達します。これは無限プレイと同等であり、防御側の勝利となります。${\displaystyle (p,q)}$

上記の定義によれば、防御側に勝利戦略が存在する場合のみ、システムは双シミュレーションとなります。

余代数的定義

状態遷移システムの双模倣は、共変冪集合関数の型に対する余数的双模倣の特別な場合である。すべての状態遷移システムは、から の冪集合への関数に全単射的に写像でき、 と表され、次のように定義される。 ${\displaystyle (S,\Lambda ,\rightarrow )}$ ${\displaystyle \xi _{\rightarrow }}$ ${\displaystyle S}$ ${\displaystyle S}$ ${\displaystyle \Lambda }$ ${\displaystyle {\mathcal {P}}(\Lambda \times S)}$ $${\displaystyle p\mapsto \{(\lambda ,q)\in \Lambda \times S:p{\overset {\lambda }{\rightarrow }}q\}.}$$

を - 番目の投影とし、 についてそれぞれ および にマッピングします 。の順方向 像は、のサブセットである 3番目の要素を削除することによって定義されます 。 についても同様です。 ${\displaystyle \pi _{i}\colon S\times S\to S}$ ${\displaystyle i}$ ${\displaystyle (p,q)}$ ${\displaystyle p}$ ${\displaystyle q}$ ${\displaystyle i=1,2}$ ${\displaystyle {\mathcal {P}}(\Lambda \times \pi _{1})}$ ${\displaystyle \pi _{1}}$ $${\displaystyle P\mapsto \{(\lambda ,p)\in \Lambda \times S:\exists q.(\lambda ,p,q)\in P\}}$$ ${\displaystyle P}$ ${\displaystyle \Lambda \times S\times S}$ ${\displaystyle {\mathcal {P}}(\Lambda \times \pi _{2})}$

上記の表記法を用いると、関係が遷移システム上の双模倣となるのは、その関係上に遷移システムが存在し、その図が${\displaystyle R\subseteq S\times S}$ ${\displaystyle (S,\Lambda ,\rightarrow )}$ ${\displaystyle \gamma \colon R\to {\mathcal {P}}(\Lambda \times R)}$ ${\displaystyle R}$

は可換である。つまり、 の場合、方程式 は となり、は の関数表現である。 ${\displaystyle i=1,2}$ $${\displaystyle \xi _{\rightarrow }\circ \pi _{i}={\mathcal {P}}(\Lambda \times \pi _{i})\circ \gamma }$$ ${\displaystyle \xi _{\rightarrow }}$ ${\displaystyle (S,\Lambda ,\rightarrow )}$

バイシミュレーションの変種

特殊な文脈においては、双模倣の概念は、追加の要件や制約を加えることで洗練されることがある。例えば、スタッター双模倣（stutter bisimulation）は、あるシステムの1つの遷移が、他のシステムの複数の遷移と一致する可能性があるが、その際、中間状態が開始状態と等しい（「スタッター」）ことを条件とする。^[4]

状態遷移システムに、サイレント（または内部）アクション（外部​​の観察者からは見えないアクション）の概念が含まれる場合は、別のバリエーションが適用されます。その場合、双模倣は、弱い双模倣に緩和されます。つまり、2 つの状態と が双類似であり、 から何らかの状態に至る内部アクションがいくつかある場合、からに至る内部アクションがいくつか（ゼロの場合もある）ある状態が存在する必要があります。プロセス上の関係が弱い双模倣である場合、以下が成り立ちます（ 、、 はそれぞれ観測可能な遷移とミュート遷移です）。 ${\displaystyle \tau }$ ${\displaystyle p}$ ${\displaystyle q}$ ${\displaystyle p}$ ${\displaystyle p'}$ ${\displaystyle q'}$ ${\displaystyle q}$ ${\displaystyle q'}$ ${\displaystyle {\mathcal {R}}}$ ${\displaystyle {\mathcal {S}}\in \{{\mathcal {R}},{\mathcal {R}}^{-1}\}}$ ${\displaystyle a,\tau }$

$${\displaystyle \forall p,q.\quad (p,q)\in {\mathcal {S}}\Rightarrow p{\stackrel {\tau }{\rightarrow }}p'\Rightarrow \exists q'.\quad q{\stackrel {\tau ^{\ast }}{\rightarrow }}q'\wedge (p',q')\in {\mathcal {S}}}$$ $${\displaystyle \forall p,q.\quad (p,q)\in {\mathcal {S}}\Rightarrow p{\stackrel {a}{\rightarrow }}p'\Rightarrow \exists q'.\quad q{\stackrel {\tau ^{\ast }a\tau ^{\ast }}{\rightarrow }}q'\wedge (p',q')\in {\mathcal {S}}}$$

これは、関係「までの」双模倣の概念と密接に関係しています。 ^{[どのように？ ] [5]}

典型的には、状態遷移システムがプログラミング言語の操作的意味論を与える場合、双模倣の正確な定義はプログラミング言語の制約に固有のものとなる。したがって、一般に、文脈に応じて複数の種類の双模倣（または双類似性）関係が存在する可能性がある。

双模倣と様相論理

クリプキモデルは（ラベル付き）状態遷移システムの特殊なケースであるため、双模倣は様相論理においても話題となる。実際、様相論理は双模倣に関して不変な一階述語論理の一部である（ファン・ベンテムの定理）。

アルゴリズム

2つの有限遷移システムが双相似であるかどうかのチェックは多項式時間で実行できます。^[6]最も高速なアルゴリズムは、最も粗い分割問題への縮小による分割改良を使用した準線形時間です。

参照

• シミュレーションの予約
• 合同関係
• 確率的バイシミュレーション

注記

1. 2 つの双模倣の結合は双模倣であることを意味します。

参考文献

1. Jančar, Petr and Srba, Jiří (2008). 「Defender's Forcingによる双相似性の決定不可能性」 . J. ACM . 55 (1). ニューヨーク, NY, USA: Association for Computing Machinery: 26. doi :10.1145/1326554.1326559. ISSN  0004-5411. S2CID  14878621.
2. ミルナー、ロビン(1989).コミュニケーションと同時実行性. 米国: Prentice-Hall, Inc. ISBN 0131149849。
3. スターリング、コリン (1999). 「双模倣、様相論理、モデル検査ゲーム」. Logic Journal of the IGBL . 7 (1): 103–124 .
4. クリステル・バイアー;加藤園、ヨースト・ピーター(2008)。モデル検査の原則。 MITプレス。 p. 527.ISBN​ 978-0-262-02649-9。
5. Damien Pous (2005). 「弱双模倣のためのアップトゥテクニック」. Proc. 32nd ICALP . Lecture Notes in Computer Science . 3580. Springer Verlag: 730– 741.
6. Baier & Kataen (2008)、Corollary 7.45、p. 486.

さらに読む

• パーク、デイヴィッド (1981). 「無限列上の並行性とオートマトン」. ピーター・ドイッセン編.理論計算機科学. 第5回GIカンファレンス議事録, カールスルーエ.計算機科学講義ノート. 第104巻.シュプリンガー出版社. pp.  167– 183. doi :10.1007/BFb0017309. ISBN 978-3-540-10576-3。
• ミルナー、ロビン（1989年）『コミュニケーションと同時実行性』プレンティス・ホール、ISBN 0-13-114984-9。
• サンジョルジ、ダヴィデ(2011). 『双模倣と共帰納法入門』 ケンブリッジ大学出版局, イギリス. ISBN 9781107003637. OCLC  773040572。

外部リンク

ソフトウェアツール

• CADP : さまざまな双シミュレーションに従って有限状態システムを最小化および比較するためのツール
• mCRL2 : さまざまな双シミュレーションに従って有限状態システムを最小化および比較するためのツール
• バイシミュレーションゲーム