Coverability Graph

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


Motivation

Consider the following YAWL flow:

  • yawl-cr-unboundness.png.
  • 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:

  • petri-net-coverability-ex.png
  • how we can represent $\infty$ many nodes in this reachability graph?
  • petri-net-coverability-ex-reach.png
  • 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

  • petri-net-coverability-ex-reach2.png
  • 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


Sources