Petri Net

automata-theory distributed-systems

Definition

Petri Net

A petri net is a description of distributed systems and consists of of places and transitions.

Given a set of markings , a petri net is defined by a 5-tuple:

where:

• is the finite set of places
• is the finite set of transitions
• are the preconditions
• are the postconditions
• is the initial marking

A precondition defines the number of marks that a transition is consuming from a place .

A postcondition defines the number of marks that a transition is producing to a place .

Petri nets are named after Carl Adam Petri.

Place

A place is a (circle) node that can hold a certain number of marks.

Transition

A transition is a (square) node that can change the marking of outgoing places.

Firing Transition

Let be a transition and be a marking. If fires, the new marking of the petri net is given by:

Preconditions

Note that a transition can only fire at a marking if , meaning that:

In other words, every place used in must have at least marks at that place in the current marking .

Marking

A marking is a set of pairs that associates a place with the number of marks at that place.

Order of Markings

Let be two markings:

Addition of Markings

Let be three markings:

Subtraction of Markings

Let be three markings:

Example

Given a petri net , where:

If fires at , we get: