ML Wiki

Coverability Graph

This is a way of representing states of workflows, similar to Reachability Graph

Motivation

Consider the following YAWL flow:

• .
• because of the Cancellation Regions the Reachability Graph of this workflow becomes infinitely large
• it is possible to know when we need to stop expanding it?
• if there was no Cancellation Region, it would be enough just to repeat it 2 times to see that there's no proper termination
• but in this case we don't know when to stop
• $\Rightarrow$ can no longer use it for checking for Workflow Soundness

However there is a concept of Coverability Graphs that are

• computationally less expensive
• can still be used to decide on some properties

Coverability

Let's consider the following Petri Net:

• • how we can represent $\infty$ many nodes in this reachability graph?
• • note that marking $[p_1, p_3] < [p_1]$ - strictly larger
• thus with marking $[p_1, p_3]$ the petri net can do all the same as $[p_1]$ plus a little bit more
• so if it's possible to get from one marking $M_1$ to another marking $M_2$ s.t. $M_2$ covers $M_1$ completely - then we have a loop

Coverability:

• marking $M$ is coverable by $M'$ $\iff$
• there $\exists$ a marking $M'$ s.t. $M \to^* M'$ and $M \leqslant M'$

Let's construct the coverability graph for this example

• • look at all the nodes that you can reach
• if you notice some marking that covers another marking, add a loop to the coverability graph
• • note that this graph is finite
• and we can see that in this graph we do have the option to complete