双模倣性
双模倣性（そうもほうせい、Bisimulation）とは、理論計算機科学における複数の状態遷移系の間の同値関係を意味する。そのようなシステムは、互いに他のシステムの動作をシミュレートできるという意味で同じ動作が可能である。
直感的に言えば、同じ動作をする2つのシステムは「双模倣的」である。その意味で観察者から見て両システムは区別できない。
クリプキモデルは（ラベル付き）状態遷移系の特殊ケースであるため、双模倣性は様相論理学の概念とも言える。
形式的定義
ここでは、一つの状態遷移系の上で双模倣性を定義する。二つの状態遷移系の双模倣性は、それらの和として得られる状態遷移系の双模倣性から導かれる。 ラベル付き状態遷移系 (S, Λ, →) について、「双模倣性」関係は S 上の二項関係 R （すなわち、R ⊆ S × S）であり、R と R-1 が共に Simulation Preorder となるものである。
つまり、R が双模倣性関係であるとは、S の要素のペア (p,q) が R に含まれるときに、Λ の要素 α と S の要素 p' について以下の性質が満たされ、かつ R-1 に対しても同様の性質が満たされることをいう。
- [math] \begin{matrix} & \alpha & \\ p & \rightarrow & p' \\ \end{matrix} [/math]
- ならば以下の関係が成り立つ S の要素 q' が存在し、(p',q') も R に含まれる。
- [math] \begin{matrix} & \alpha & \\ q & \rightarrow & q' \\ \end{matrix} [/math]
S 内の2つの状態 p と q に対して (p,q) が R に含まれる双模倣性関係 R が存在するとき、p と q は「双模倣的」であるといい、 p ∼ q と表記する。
双模倣的関係 ∼ は同値関係である。さらに、それは与えられた遷移系上の双模倣性関係のうち最大のものを与える。
p が q の模倣であり、q が p の模倣であっても、双模倣性があるとは限らないことに注意が必要である。p と q が双模倣的であるためには、p から q への模倣と q から p への模倣が二項関係における「逆(en:Inverse relation)」でなければならない。
双模倣性からの派生
場合によっては条件を加えて双模倣性を修正する場合がある。例えば、状態遷移系が見えない動作を伴う場合（外部の観測者からは見えない動作）、そのような外部から見えない動作を無視して双模倣性をゆるめ、「弱い双模倣性」とすることもできる。
一般に状態遷移系はプログラミング言語の操作的意味論を与える。その場合、双模倣性の厳密な定義はそのプログラミング言語の条件に固有のものとなる。したがって、一般に状況によって複数種類の双模倣性関係が存在しうる。