双模倣性

双模倣性（そうもほうせい、Bisimulation）とは、理論計算機科学における複数の状態遷移系の間の同値関係を意味する。そのようなシステムは、互いに他のシステムの動作をシミュレートできるという意味で同じ動作が可能である。

直感的に言えば、同じ動作をする2つのシステムは「双模倣的」である。その意味で観察者から見て両システムは区別できない。

クリプキモデルは（ラベル付き）状態遷移系の特殊ケースであるため、双模倣性は様相論理学の概念とも言える。

[編集] 形式的定義

ラベル付き状態遷移系 (S, Λ, →) について、「双模倣性」関係は S 上の二項関係 R （すなわち、R ⊆ S × S）であり、ここで R と R^-1 は Simulation Preorder である。

R が双模倣性であるとは、S 内のあらゆる要素のペア (p,q) が R に含まれるとき、Λ の全要素 α と S の全要素 p' について次が成り立つ。

$\begin{matrix} & \alpha & \\ p & \rightarrow & p' \\ \end{matrix}$

ここで以下の関係が成り立つ S の要素 q' が存在する。

$\begin{matrix} & \alpha & \\ q & \rightarrow & q' \\ \end{matrix}$

(p',q') も R の要素である。

S 内の2つの状態 p と q があり、p が q と「双模倣的」であることを p ∼ q と表記する。その場合、双模倣性 R には (p, q) が含まれる。

双模倣的関係 ∼ は一種の同値関係である。さらに、それは与えられた遷移系上の最大の双模倣性関係である。

p が q の模倣であり、q が p の模倣であっても、双模倣性があるとは限らないことに注意が必要である。p と q が双模倣的であるためには、p から q への模倣と q から p への模倣が二項関係における「逆; inverse」でなければならない。

場合によっては条件を加えて双模倣性を修正する場合がある。例えば、状態遷移系が見えない動作を伴う場合（外部の観測者からは見えない動作）、そのような外部から見えない動作を無視して双模倣性をゆるめ、「弱い双模倣性」とすることもできる。

一般に状態遷移系はプログラミング言語の操作的意味論を与える。その場合、双模倣性の厳密な定義はそのプログラミング言語の条件に固有のものとなる。したがって、一般に状況によって複数種類の双模倣性関係が存在しうる。