Petri Network

The Petri network is a graph type that contains two kind of nodes : Sequence and Transition. These nodes are linked through oriented vertices with the constraint the start and end nodes of a vertice must be of different kind. A vertice leaving a sequence must end by a transition. A vertice leaving a transition must end by a sequence.

The sequences of a petri network can contain a discrete amount of tokens. The set of tokens within a petri network at a given time is called marking. The petri network goes from one marking to another when a transition fires. A transition can fire when all the upstream sequences contain the amount of tokens required. This amount is indicated by the vertice linking the sequence to the transition. When fired, tokens are distributed to the downstream sequences. The amount distributed is indicated by the vertice linking the transition to the sequence.

A petri network contains a set of initial sequences. Those sequences contain a set of tokens. This set constitutes the initial marking. It also contains a set of final sequences. When all sequences in that subset harbors the amount of tokens required, the network reaches a final state.

In our case, we use a more restrictive kind of petri network : a safe petri network.