双模倣性

双模倣性（Bisimulation）

双模倣性とは、理論計算機科学における概念で、異なる状態遷移系が互いに同じ動作をリプレイできる関係を指します。この特性を持つシステムは、相互に他方の動作を忠実に模倣できるため、観察者にとっては区別がつきません。

この概念は、状態遷移系の間での同値関係を示すものであり、実際には、クリプキモデルという特殊な状態遷移系に関連しています。このモデルでは、ラベル付きの状態遷移がなされ、双模倣性は様相論理学にも重要な役割を果たします。

双模倣性の形式的定義

双模倣性を定義する際には、状態遷移系のペアを考えます。二つの状態遷移系が双模倣的であるとは、これらが組み合わさった状態遷移系において互いに模倣し合う関係が存在することを意味します。具体的には、ラベル付き状態遷移系 $(S, Λ, →)$ において、双模倣性関係 $R$ は $S$ 上の二項関係となります。この関係は $R$ とその逆 $R^{-1}$ の両方がSimulation Preorderの性質を持つ必要があります。

形式的には、もし要素 $p$ と $q$ が双模倣性関係 $R$ に含まれるとき、以下の条件が必須です：

• - 任意のラベル $orall α ext{ と状態 } p'$ に対して、$p$ から直接遷移する場合、$q$ からも対応する遷移が存在し、かつ $(p', q')$ も $R$ に含まれること。

このように、二つの状態 $p$ と $q$ が双模倣的であるときは、$p ext{ と } q$ の関係は $p ilde{∼} q$ と表されます。この双模倣的関係は同値関係であり、最大の双模倣性関係となります。ただし、注意すべきは、$p$ が $q$ を模倣している場合でも、 $q$ から $p$ への模倣は成り立たない場合があることです。この双模倣性が成立するためには、双方の状態間での模倣が二項関係の逆である必要があります。

双模倣性の派生

双模倣性は場合によって修正が可能です。例えば、システムが外部の観測者から見えない動作を含む場合、双模倣性をゆるめ、外部からの視点を考慮しない「弱い双模倣性」を定義することが可能です。このように、状態遷移系はプログラミング言語の操作的意味論を整理する際に重要な役割を果たします。従って、プログラミング言語ごとに特有な条件に基づく厳密な双模倣性の定義が必要です。

まとめ

双模倣性は、システム間の動作の類似性を示す重要な理論です。その応用は、プログラミング言語の理論やモデル検証など、多岐にわたります。今後の研究においても、この概念はシステム間の関係を理解する上での強力なツールであり続けるでしょう。関連する用語には、操作的意味論や合同関係などがあります。

もう一度検索