ペトリネットとは?
ペトリネットは以下の4つの要素で構成されます。
- プレースの集合P
- トランジッションの集合T
- それぞれのトランジッションが発火するために、各プレースで消費するトークンの数Pre∈NT×P
- それぞれのトランジッションが発火したあと、各プレースに追加されるトークンの数Post∈NT×P
各プレースからトークンの数への関数m∈NPを、マーキングと呼びます。
ペトリネットの状態はマーキングで表されます。
あるトランジッションt∈Tと全てのプレースp∈Pについて、m(p)≧Pre(t)ならば、
マーキングがmの時tは発火可能と呼び、m[t>と書きます。
発火後のマーキングは変化し、変化後の状態をm'としてm[t>m'と書きます。
この時、任意のプレースp∈Pについて、m'(p)=m(p)-Pre(t,p)+Post(t,p)が成り立ちます。
マーキングmのペトリネットのトランジッションがトランジッションの列u∈T*の順に従って全て発火でき、
最後にマーキングがm''になる時にも、m[u>m''と書きます。
この時、uをu1u2に分けると、
途中のマーキングをm'としてm[u1>m'[u2>m''が成り立ちます。