双模倣性のソースを表示

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

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

[[クリプキ意味論|クリプキモデル]]は（ラベル付き）状態遷移系の特殊ケースであるため、双模倣性は[[様相論理学]]の概念とも言える。<!-- 以下翻訳不能
In fact, modal logic is the fragment of [[first-order logic]] [[Closure (mathematics)|closed under]] bisimulation ([[Johan van Benthem (logician)|Van Benthem's theorem]]). -->

== 形式的定義 ==
ここでは、一つの状態遷移系の上で双模倣性を定義する。二つの状態遷移系の双模倣性は、それらの和として得られる状態遷移系の双模倣性から導かれる。

[[状態遷移系|ラベル付き状態遷移系]] (S, &Lambda;, &rarr;) について、「双模倣性」関係は S 上の[[二項関係]] R （すなわち、R &sube; S &times; S）であり、R と R<sup>-1</sup> が共に [[:en:Simulation preorder|Simulation Preorder]] となるものである。

つまり、R が双模倣性関係であるとは、S の要素のペア (p, q) が R に含まれるときに、&Lambda; の要素 &alpha; と S の要素 p' について次の性質が満たされ、かつ R<sup>-1</sup> に対しても同様の性質が満たされることをいう。
: <math>p \mathrel{\overset{\alpha}{\rightarrow}} p'</math>ならば、<math>q \mathrel{\overset{\alpha}{\rightarrow}} q'</math>の関係が成り立つ S の要素 q' が存在し、(p', q') も R に含まれる。

S 内の2つの状態 p と q に対して (p, q) が R に含まれる双模倣性関係 R が存在するとき、p と q は「双模倣的」であるといい、 p &sim; q と表記する。

双模倣的関係 &sim; は[[同値関係]]である。さらに、それは与えられた遷移系上の双模倣性関係のうち最大のものを与える。

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

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

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

== 関連項目 ==

* [[操作的意味論]]
* [[状態遷移系]]
* [[:en:Simulation preorder|Simulation Preorder]]
* [[合同|合同関係]]

{{Normdaten}}
{{DEFAULTSORT:そうもほうせい}}
[[Category:形式手法]]
[[Category:理論計算機科学]]
[[Category:数学に関する記事]]