A model of a concurrent system that is expressed in a specific graphical notation and can be used to explore certain properties of the system. A Petri net consists of a set of places, a set of transition bars, and a set of directed edges. Each transition bar has an associated set of input places and an associated set of output places. A transition bar is linked to each of its input places by a directed edge from the place to the bar, and to each of its output places by a directed edge from the bar to the place.
States of the concurrent system are represented by the presence of tokens at places, with a specific state being represented by a specific allocation of tokens to places. Such an allocation is called a marking.
The example net shown in the diagram employs the conventional graphical notation. Places are represented by the circles labeled p … t, transition bars are represented by the lines labeled B1 … B4, and the initial marking is shown by the use of dots to represent tokens.Transition bars represent possible changes of state in the concurrent system. A transition bar can only fire (i.e. the change of state occur) when each of its input places holds at least one token. When a bar fires it removes one token from each of its input places and deposits one token at each of its output places. Thus the combination of the input and output places for a transition bar represents both the conditions under which the change of state can occur and the effects of that state change.
The firing of a transition bar is an indivisible event and simultaneous firing of two or more bars is therefore not possible. When the state is such that two or more bars are candidates to fire, each candidate must be considered individually.
By starting from an initial marking that represents an initial state of the system and applying a straightforward procedure that generates other markings that can be reached from this initial marking, it is possible to explore the possible states of the system and the ways in which these states can be reached. For example, both deadlock states and unproductive looping can be readily detected, and in general it is possible to check that the behavior of the system is as expected. However, while the procedure for generating reachable markings is straightforward, attempts at full analysis are often frustrated by the sheer number of such markings, and this can be infinite. Thus the general problem of determining whether a given marking is reachable from a given initial state is undecidable.
With the initial marking shown in the example net, both B1 and B3 are able to fire. Suppose that B1 fires. This removes the tokens from places p and t, and deposits a single token at place q. Now only B2 is able to fire. (B3 is no longer able to fire because there is no longer a token at place t.) When B2 fires, the token is removed from place q and new tokens are deposited at places p and t, thus restoring the initial marking. Should B3 now fire, a single token is deposited at place s, and B4 then fires, again restoring the initial marking. (This net may be viewed as modeling a system in which two processes compete for a shared resource. Availability of the resource is represented by the presence of a token at place t. Relevant states of one process, holding the resource or not holding the resource, are represented by tokens at places p and q respectively. Similarly tokens at places r and s represent relevant states of the other process.)