A Petri net (also known as a place/transition net or P/T net) is one of several mathematical modeling languages for the description of distributed systems. A Petri net is a directed graph consisting of two types of nodes: places (represented by circles) and transitions (represented by rectangles). They are joined by arcs (represented by arrows).
Arcs run from a place to a transition or vice versa, never between places or between transitions.
The places from which an arc runs to a transition are called the input places of the transition; the places to which arcs run from a transition are called the output places of the transition.
Graphically, places in a Petri net may contain a discrete number of marks called tokens. Any distribution of tokens over the places will represent a configuration of the net called a marking.
A transition of a Petri net may fire if it is enabled, i.e. there are sufficient tokens in all of its input places; when the transition fires, it consumes the required input tokens, and creates tokens in its output places. A firing is atomic, i.e., a single non-interruptible step.
Unless an execution policy is defined, the execution of Petri nets is nondeterministic when multiple transitions are enabled at the same time, any one of them may fire.
Since firing is nondeterministic, and multiple tokens may be present anywhere in the net (even in the same place), Petri nets are well suited for modeling the concurrent behavior of distributed systems.
There are many submodels of Petri Nets. I know of:
1. Elementary Net Systems.
3. Timed and Stochastic Petri Nets.
4. Coloured Petri Nets.
i think that when Modelling Concurrency, we can use Ideas of Active Components, or Transitions to describe Processess which rely on Input Data Preconditions called Tokens which are stored in Queues or other Buffers, also called Passive Components or Places.
there are people who develop Mathematical Apparatus that is used to analyze Properties of Concurrent Systems such as Reachability, Liveness, Boundedness. They are explained on Wikipedia.
i heard that there are automated tools that help to analyze, prove or disprove such qualities if given P/T Model.
See also: , Graphs, Elementary Net Systems Introduction, Introduction to Cooperating Processes & Synchronization, Petri Nets & Randezvous Concurrency, an Idiom.