バイシミュレーション

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

直感的に、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 人のプレイヤー間のゲームとして考えることもできます。

「攻撃者」が最初に行動し、から任意の有効な遷移 を選択できます。つまり、 または ${\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 )}$

特殊な状況では、バイシミュレーションの概念は、追加の要件や制約を加えることによって洗練されることがあります。一例として、スタッターバイシミュレーションがあります。これは、中間状態が開始状態（「スタッター」）と同等である場合に、1つのシステムの1つの遷移が他のシステムの複数の遷移と一致する可能性があるものです。^[3]

状態遷移システムに、と表記されることが多いサイレント（または内部）アクション、つまり外部の観察者からは見えないアクションの概念が含まれる場合は、異なるバリエーションが適用されます。その場合、双模倣は、弱い双模倣に緩和されます。つまり、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}}}$$

^これは、関係「までの」^双模倣^の概念と密接に関係しています。 ^[4]

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

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

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

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

• パーク、デイビッド (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 : さまざまな双シミュレーションに従って有限状態システムを最小化および比較するためのツール
• バイシミュレーションゲーム