ペトリネット

プロセス間の同期を有向グラフとトークンで表現する。各プロセスの現在の状態を、トークンがどの状態ノードに置かれているかで表す。状態ノードと遷移ノードが交互に矢印で結ばれていて、遷移ノードの発火条件が満たされると、矢印にしたがってトークンが移動する。（図2.5[queuing system M/D/3/2]はhttp://pdv.cs.tu-berlin.de/~azi/petri.htmlから引用）

ペトリネットの動く様子が見えるページがある。