ラベル付き遷移系：3つのモノイド演算

ラベル付き遷移系αをラベル集合AからRel(X, Y)への写像として定義する。X = Y でないと、a, b∈Aに対するa;bは意味がない。しかし、a | b または a + b は意味がある。Aを指標とみると、ラベル付き遷移系とは、指標AのRelにおけるモデルである。

α:A→Rel(X, Y)、β:B→Rel(V, W)に対して、α+β:A+B→Rel(X+V, Y+W)とα×β:A×B→Rel(X×V, Y×W)は自然に定義でき、（分岐ではない）選択的実行と同時実行のモデルとなる。

A←K→B という単射スパンがあると、このスパンによりα*βという第三の積を定義できる。AへのKの埋め込み像をL、BへのKの埋め込み像をMとして、L→Mの同型をφとする。このとき、A×Bの部分集合 A*B = A*_L,MB を次のように定義する。

• (a, b)∈A*B ⇔ a∈Lならばb = φ(a)、b∈Mならばa=φ^-1(b)

要するに、L×Mの部分はKと同一視され潰れる。aとφ(a)は同時アトミックに働くとみなされる。この演算A*Bを使い、他はα×βと同じに作ったラベル付き遷移系をα*βと書く。

α*βは、H→A←K のようなラベルの余スパンを伴うラベル付き遷移の圏における結合を与える。もちろん、Relの結合に対応する結合も定義できる。