Verifying Petri Net-Based Process Models using Automated Planning
The identification of control-flow errors in business processes (BPs) at design time is one of the most relevant tasks of the early phases of the Business Process Management (BPM) lifecycle, named BP verification. In this paper, starting from a Petri net-based representation of a BP model, we show how instances of the verification problem can be represented as planning problems in PDDL (Planning Domain Definition Language) for which planners can find a correct solution in a finite amount of time.