双模倣の定義

セリンガーの http://www.mathstat.dal.ca/~selinger/papers/catasynch.pdf などを参考に、ラベルなし（単純）のケースで述べておく。

s, s'∈S, t, t'∈T、双模倣を与える関係をR⊆S×T、遷移（1ステップ）を矢印で表す。また xRx' を x〜x' で示す。

1. s〜t, t→t' ならば、s'〜t', s→s' となるs'がS内にある。
2. s〜t, s→s' ならば、s'〜t', s→s' となるt'がT内にある。

以上が強双模倣の定義になる。普通の遷移以外に、無音遷移 x…→x' が定義されていれば、弱双模倣も定義できる。が、とりあえずラベルなしのケースでは強双模倣だけを考える。

SがTをRにより模倣できるとは、双模倣の半分の条件が成立すること：

• s〜t, t→t' ならば、s'〜t', s→s' となるs'がS内にある。

遷移グラフとしてT⊆S（Tは部分グラフ）のとき、Sは包含によりTを模倣できる。これが典型例。

模倣可能性は、遷移系全体の集まりにプレ順序を入れる。このプレ順序は、模倣を射とする圏を2値化して得られるやせた圏のことだ。プレ順序から導かれる同値関係が振る舞い同値を与え、同値類が振る舞い型となる。