Data-Aware Business Processes: balancing between expressiveness and verifiability

Traditionally, business processes are formalized and verified by solely considering the control-flow perspective, completely abstracting away from the data perspective. While this "divide et impera" approach has produced a flourishing literature and very interesting results, it falls short of providing an overall understanding and of how processes really operate in a concrete organizational setting. 
In this presentation, I will overview the research we carried out during the last five years on the challenging problem of marrying processes and data, consequently providing solid underlying principles for their verification. In the first part of the presentation, I will discuss recent proposals for formally describing data-aware business processes, and how such models relate to concrete process modeling notations and systems. We will then delve into verification, considering in particular the challenging problem of model checking data-aware business processes against variants of branching- and linear-time first-order temporal logics. We will show that, unsurprisingly, this problem is undecidable in the general case. We will then single out the main sources of undecidability, taking into account the features offered by the model as well as those offered by the corresponding verification logics. By operating on such features, we will finally show how a suitable trade-off between expressiveness and verifiability can indeed be achieved, not only obtaining robust decidability results, but also showing how conventional model checking techniques can be employed, in principle, to concretely solve this problem.

Contact person: Carlo Combi