The Foundations of Alignments of Process Models

Process models are a cornerstone of information systems. They define how a system can achieve a goal by executing actions in a coordinated manner. Process models serve different purposes: communicating ideas, simulating systems, or defining precise execution instructions. Hence, there are often several "related" models, each appropriate for its purpose, that shall be consistent with each other. This calls for means to verify that two process models define equivalent behaviour once their actions have been aligned, i.e., mapped according to their semantics. Despite decades of research on behaviour equivalence, however, there is a lack of a formal grounding for verifying behaviour equivalence without imposing any assumption on the structure of the alignment relation. This project sets out to develop the foundations of behaviour equivalence for process models for which the alignment contains potentially overlapping groups of actions of arbitrary size. It will contribute equivalence notions, their complexity analysis, verification algorithms, and methods for root-cause analysis of non-equivalence for the full spectrum of process model semantics, including linear-time and branching-time semantics as well as interleaving and concurrency semantics. The theoretical results will be complemented by an open-source implementation of the devised verification algorithms and comprehensive case studies in business process automation.