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 $M\subseteq P\times \mathbb{N}$, a petri net is defined by a 5-tuple:

$$⟨P,T,{}^{\bullet }(),({)}^{\bullet },m_0⟩$$

where:

• $P$ is the finite set of places
• $T$ is the finite set of transitions
• ${}^{\bullet }():T\to M$ are the preconditions
• $({)}^{\bullet }:T\to M$ are the postconditions
• $m_0\in M$ is the initial marking

A precondition ${}^{\bullet }t\in M$ defines the number of marks that a transition $t$ is consuming from a place $p$.

A postcondition $t^{\bullet }\in M$ defines the number of marks that a transition $t$ is producing to a place $p$.

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 $t\in T$ be a transition and $m_0\in M$ be a marking. If $t$ fires, the new marking of the petri net is given by:

$$m_1=m_0\ominus {}^{\bullet }t\oplus t^{\bullet }$$

Preconditions

Note that a transition $t\in T$ can only fire at a marking $m_0\in M$ if ${}^{\bullet }t\le m_0$, meaning that:

$$\forall p\in P:{}^{\bullet }t(p)\le m_0(p)$$

In other words, every place $p$ used in ${}^{\bullet }t$ must have at least ${}^{\bullet }t(p)$ marks at that place in the current marking $m_0$.

Marking

A marking $m\in M$ is a set of pairs that associates a place $p\in P$ with the number of marks $m(p)\in \mathbb{N}$ at that place.

Order of Markings

Let $m,m^{\prime }\in M\subseteq P\times \mathbb{N}$ be two markings:

$$m\le m^{\prime }⟺\forall p\in P:m(p)\le m^{\prime }(p)$$

Addition of Markings

Let $m,m^{\prime },m^{\prime \prime }\in M\subseteq P\times \mathbb{N}$ be three markings:

$$m\oplus m^{\prime }=m^{\prime \prime }⟺\forall p\in P:m^{\prime \prime }(p)=m(p)+m^{\prime }(p)$$

Subtraction of Markings

Let $m,m^{\prime },m^{\prime \prime }\in M\subseteq P\times \mathbb{N}$ be three markings:

$$m\ominus m^{\prime }=m^{\prime \prime }⟺\forall p\in P:m^{\prime \prime }(p)=m(p)-m^{\prime }(p)$$

Example

Given a petri net $⟨\{s_1,s_2\},\{t\},{}^{\bullet }(),({)}^{\bullet },m_0⟩$, where:

$$\begin{array}{rl}{}^{\bullet }t& =\{s_1\mapsto 1,s_2\mapsto 0\}\\ t^{\bullet }& =\{s_1\mapsto 2,s_2\mapsto 2\}\\ m_0& =\{s_1\mapsto 1,s_2\mapsto 0\}\end{array}$$

If $t$ fires at $m_0$, we get:

$$\begin{array}{rl}{m}_1& =m_0\ominus {}^{\bullet }t\oplus t^{\bullet }\\ m_1(s_1)& =m_0(s_1)-{}^{\bullet }t(s_1)+t^{\bullet }(s_1)\\ & =1-1+2\\ & =2\\ m_1(s_2)& =m_0(s_2)-{}^{\bullet }t(s_2)+t^{\bullet }(s_2)\\ & =0-0+2\\ & =2\end{array}$$