Petri net

A Petri net is a directed bipartite graph that has two types of elements: places and transitions.

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.

Unless an execution policy (e.g. a strict ordering of transitions, describing precedence) is defined, the execution of Petri nets is nondeterministic: when multiple transitions are enabled at the same time, they will fire in any order.

The configuration of tokens distributed over an entire Petri net diagram is called a marking.

In this example, the firing of transition t generates a map that has the marking configured M1 in the image of M0 and results in Petri net PN1, seen in the bottom figure.

In the diagram, the firing rule for a transition can be characterised by subtracting a number of tokens from its input places equal to the multiplicity of the respective input arcs and accumulating a new number of tokens at the output places equal to the multiplicity of the respective output arcs.

with node partitions S and T. The preset of a transition t is the set of its input places:

, where In words We are generally interested in what may happen when transitions may continually fire in arbitrary order.

Another common variation, e.g. in Desel and Juhás (2001),[4] is to allow capacities to be defined on places.

matrices: Then their difference can be used to describe the reachable markings in terms of matrix multiplication, as follows.

Several subclasses of Petri nets have been studied that can still model interesting classes of concurrent systems, while these determinations become easier.

An overview of such decision problems, with decidability and complexity results for Petri nets and some subclasses, can be found in Esparza and Nielsen (1995).

It is a matter of walking the reachability-graph defined above, until either the requested-marking is reached or it can no longer be found.

This is harder than it may seem at first: the reachability graph is generally infinite, and it isn't easy to determine when it is safe to stop.

[8] In 2018, Czerwiński et al. improved the lower bound and showed that the problem is not ELEMENTARY.

[9] In 2021, this problem was shown to be non-primitive recursive, independently by Jerome Leroux[10] and by Wojciech Czerwiński and Łukasz Orlikowski.

To alleviate this problem, linear temporal logic is usually used in conjunction with the tableau method to prove that such states cannot be reached.

Linear temporal logic uses the semi-decision technique to find if indeed a state can be reached, by finding a set of necessary conditions for the state to be reached then proving that those conditions cannot be satisfied.

Some definitions of Petri nets explicitly allow this as a syntactic feature.

To be exact, a place can be made k-bounded by adding a "counter-place" with flow opposite to that of the place, and adding tokens to make the total in both places k. As well as for discrete events, there are Petri nets for continuous and hybrid discrete-continuous processes[14] that are useful in discrete, continuous and hybrid control theory,[15] and related to discrete, continuous and hybrid automata.

The term is also used specifically for the type of coloured nets supported by CPN Tools.

For this reason, it is a good idea to use the most simple net type possible for a given modelling task.

Accordingly, start and termination markings can be defined that represent the process status.

WF-nets have the soundness property,[24] indicating that a process with a start marking of k tokens in its source place, can reach the termination state marking with k tokens in its sink place (defined as k-sound WF-net).

The DSM-nets are realization of DSM-based plans into workflow processes by Petri nets, and are equivalent to WRI-WF-nets.

The DSM-net construction process ensures the soundness property of the resulting net.

Other ways of modelling concurrent computation have been proposed, including vector addition systems, communicating finite-state machines, Kahn process networks, process algebra, the actor model, and trace theory.

[27] Different models provide tradeoffs of concepts such as compositionality, modularity, and locality.

An approach to relating some of these models of concurrency is proposed in the chapter by Winskel and Nielsen.