Stochastic Petri net

Stochastic Petri nets are a form of Petri net where the transitions fire after a probabilistic delay determined by a random variable. 
Definition.
A "stochastic Petri net" is a five-tuple "SPN" = ("P", "T", "F", "M"0, "Λ") where:
Correspondence to Markov process.
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 λ.