Petri net

Summary

A Petri net is a model of concurrent systems made of places, which hold tokens, and transitions, which consume and produce tokens. Its underlying graph is a bipartite graph with places on one side and transitions on the other. The state of the net is a marking, the number of tokens in each place. A transition may fire when its input places hold enough tokens. Petri nets describe resources, synchronisation and concurrency, and questions such as reachability of a marking are central in verification.