Petri Nets: Formal Definition
Formally, a PN can be defined as a 5-tuple (P, T, F, w, M0), where:
P = {P1, …, Pm} is a finite set of places.
T = {t1, …, tn} is a finite set of transitions.
F Í (P x T) È (T x P) is a set of arcs.
w : F ® {1, 2, …} is a weight function.
M0 : P ® {0, 1, 2, …} is the initial marking
with (P Ç T) = Æ and (P È T) ¹ Æ.