Verifying Petri Net-Based Process Models using Automated Planning

Published in Workshop on Strategic Modeling and Reasoning meets Process Mining (SMRPM’19), held in conjuction with the 23rd IEEE Int. Conference on Enterprise Computing (EDOC’19). Paris, France, 28-31 October, 2019

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. If verification problems are converted into planning problems, one can seamlessly leverage the best performing automated planners, with evident advantages in terms of versatility and customization.

Authors: Simone Agostinelli, Fabrizio Maria Maggi, Andrea Marrella, Massimo Mecella.