プログラムの実行であるラン T→S が、ラベル付き境界付きグラフのあいだの準同型だとする。 Tは時刻を頂点として、アトミックな時間進展（evolution, progression）を辺とするグラフ Sは状態点を頂点として、アトミックな状態遷移（遷移ステップ）を辺とする…