About this video
<p>Based on a transformation of BPMN to Petri nets, the reachability graph of a process (its state space) is built and analyzed for soundness properties. For instance, it is examined if the final state can always be reached and whether all transitions can contribute to a process instance.</p>