Reachability graph

A reachability graph (also called marker graph ) is a directed graph that can be obtained from a Petri net and an initial marker. It is generated in that, starting with the initial marking, the set of transitions activated in the marking is determined and the subsequent marking is calculated in each case. The markings are represented by nodes in the reachability graph and the transition from a mark to its next mark is noted as an edge in the graph. This process is repeated for each subsequent marking.

Formal definition

The reachability graph of a network is defined as, where is the set of nodes, the set of marks of nodes, and the set of directed edges of the graph. ${\displaystyle {\mathcal {N}}}$ ${\displaystyle RG({\mathcal {N}})=(M(V),E)}$ ${\displaystyle V}$ ${\displaystyle M(V)}$ ${\displaystyle E}$

E consists of triples , where m is a marking that can be reached from the initial marking and from which it is possible to get to m 'by switching the transition t. Each node of the reachability graph is a marker M _{i of} the node set V of the network. A path of the marking graph is created by changing the marking, that is, a reassignment of the marks at V. The complete graph shows the transitions from each M _i to M _{i + 1} through E (M _i , t, M _{i + 1} ). ${\displaystyle (m,t,m')}$

Algorithm for generating the reachability graph

The following algorithm in pseudocode generates the reachability graph of a network and the initial marking ${\displaystyle {\mathcal {N}}}$ ${\displaystyle m_{0}}$

 function create_reachability_graph(N, m0)
   V := {}
   E := {}
   pending = {m0}
   while pending is not empty
     choose m from pending
     pending := pending \ {m}
     if m not in V
       V := V  ${\displaystyle \cup }$ {m}
       foreach transition t activated in m do
         calculate m' such that  ${\displaystyle m{\xrightarrow {t}}m'}$
         E := E  ${\displaystyle \cup }$ {(m, t, m')}
         pending := pending  ${\displaystyle \cup }$ {m'}

Analysis of reachability graphs

Petri nets can be analyzed with the help of reachability graphs. For example, the reachability graph can be used to identify whether a network with a given initial marker is alive . The reversibility of the network can also be demonstrated or refuted.

example

Consider the following uncolored Petri net PN with the initial marking 2p1 + p2.

The transitions t1, t2 and t3 are activated in the initial marking.

Accessibility graph for Petri net PN

1st iteration

V = {2p1 + p2, p1 + 2p2, 2p1 + p3}

E = {(2p1 + p2, t1, p1 + 2p2), (2p1 + p2, t2, 2p1 + p3), (2p1 + p2, t3, 2p1 + p3)}

2nd iteration

V = {2p1 + p2, p1 + 2p2, 2p1 + p3, 3p2, p1 + p2 + p3}

E = {(2p1 + p2, t1, p1 + 2p2), (2p1 + p2, t2, 2p1 + p3), (2p1 + p2, t3, 2p1 + p3), (p1 + 2p2, t1, 3p2), ( p1 + 2p2, t2, p1 + p2 + p3), (p1 + 2p2, t3, p1 + p2 + p3), (2p1 + p3, t1, p1 + p2 + p3)}

3rd iteration

V = {2p1 + p2, p1 + 2p2, 2p1 + p3, 3p2, p1 + p2 + p3, 2p2 + p3, p1 + 2p3}

E = {(2p1 + p2, t1, p1 + 2p2), (2p1 + p2, t2, 2p1 + p3), (2p1 + p2, t3, 2p1 + p3), (p1 + 2p2, t1, 3p2), ( p1 + 2p2, t2, p1 + p2 + p3), (p1 + 2p2, t3, p1 + p2 + p3), (2p1 + p3, t1, p1 + p2 + p3), (3p2, t2, 2p2 + p3) , (3p2, t3, 2p2 + p3), (p1 + p2 + p3, t1, 2p2 + p3), (p1 + p2 + p3, t2, p1 + 2p3), (p1 + p2 + p3, t3, p1 + 2p3)}

4th iteration

V = {2p1 + p2, p1 + 2p2, 2p1 + p3, 3p2, p1 + p2 + p3, 2p2 + p3, p1 + 2p3, p2 + 2p3}

E = {(2p1 + p2, t1, p1 + 2p2), (2p1 + p2, t2, 2p1 + p3), (2p1 + p2, t3, 2p1 + p3), (p1 + 2p2, t1, 3p2), ( p1 + 2p2, t2, p1 + p2 + p3), (p1 + 2p2, t3, p1 + p2 + p3), (2p1 + p3, t1, p1 + p2 + p3), (3p2, t2, 2p2 + p3) , (3p2, t3, 2p2 + p3), (p1 + p2 + p3, t1, 2p2 + p3), (p1 + p2 + p3, t2, p1 + 2p3), (p1 + p2 + p3, t3, p1 + 2p3), (2p2 + p3, t2, p2 + 2p3), (2p2 + p3, t3, p2 + 2p3), (p1 + 2p3, t1, p2 + 2p3)}

5th iteration

V = {2p1 + p2, p1 + 2p2, 2p1 + p3, 3p2, p1 + p2 + p3, 2p2 + p3, p1 + 2p3, p2 + 2p3, 3p3}

E = {(2p1 + p2, t1, p1 + 2p2), (2p1 + p2, t2, 2p1 + p3), (2p1 + p2, t3, 2p1 + p3), (p1 + 2p2, t1, 3p2), ( p1 + 2p2, t2, p1 + p2 + p3), (p1 + 2p2, t3, p1 + p2 + p3), (2p1 + p3, t1, p1 + p2 + p3), (3p2, t2, 2p2 + p3) , (3p2, t3, 2p2 + p3), (p1 + p2 + p3, t1, 2p2 + p3), (p1 + p2 + p3, t2, p1 + 2p3), (p1 + p2 + p3, t3, p1 + 2p3), (2p2 + p3, t2, p2 + 2p3), (2p2 + p3, t3, p2 + 2p3), (p1 + 2p3, t1, p2 + 2p3), (p2 + 2p3, t2 3p3), (p2 + 2p3, t3, 3p3)}

No transition is activated in the last marker 3p3.

Limits in the creation of reachability graphs

Accessibility graphs can only be fully calculated for restricted networks. For unrestricted networks the reachability graph would be infinitely large. In such cases are often overlapping graphs constructed. In many cases, coverage graphs do not allow statements about the reversibility of the network, but they can be used to formally consider other aspects, such as the unlimited number of places.