Stochastic Petri nets are a form of Petri net where the transitions fire after a probabilistic delay determined by a random variable.
A stochastic Petri net is a five-tuple SPN = (P, T, F, M<sub>0</sub>, ÃÂ) where:
The reachability graph of stochastic Petri nets can be mapped directly to a Markov process. It satisfies the Markov property, since its states depend only on the current marking. Each state in the reachability graph is mapped to a state in the Markov process, and the firing of a transition with firing rate û corresponds to a Markov state transition with probability û.