双模倣性

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

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

つまり、R が双模倣性関係であるとは、S の要素のペア (p, q) が R に含まれるときに、Λ の要素 α と S の要素 p' について次の性質が満たされ、かつ R^-1 に対しても同様の性質が満たされることをいう。

${\displaystyle p\mathrel {\overset {\alpha }{\rightarrow }} p'}$ならば、${\displaystyle q\mathrel {\overset {\alpha }{\rightarrow }} q'}$の関係が成り立つ S の要素 q' が存在し、(p', q') も R に含まれる。

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)」でなければならない。

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

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

• 操作的意味論
• 状態遷移系
• Simulation Preorder
• 合同関係