Abstract
Recent advances in the field of Business Process Management (BPM) have brought about several suites able to model data objects along with the traditional control flow perspective. Nonetheless, when it comes to formal verification there is still a lack of effective verification tools on imperative data-aware process models and executions: the data perspective is often abstracted away and verification tools are often missing. Automated Planning is one of the core areas of Artificial Intelligence where theoretical investigations and concrete and robust tools have made possible the reasoning about dynamic systems and domains. Moreover planning techniques are gaining popularity in the context of BPM. Starting from these observations, we provide here a concrete framework for formal verification of reachability properties on an expressive, yet empirically tractable class of data-aware process models, an extension of Workflow Nets. Then we provide a rigorous mapping between the semantics of such models and that of three important Automated Planning paradigms: Action Languages, Classical Planning, and Model-Checking. Finally, we perform a comprehensive assessment of the performance of three popular tools supporting the above paradigms in solving reachability problems for imperative data-aware business processes, which paves the way for a theoretically well founded and practically viable exploitation of planning-based techniques on data-aware business processes.