Verification of Data-Aware Processes

The need of combining static (i.e., data-related) and dynamic (i.e., process-related) aspects has been increasingly recognized as a key requirement towards the design, verification, and understanding of complex systems. An essential element for traditional verification is that states are propositional, resulting in a finite-state transition system. However, in the presence of data, states need to be modeled relationally, causing the transition system to become infinite-state in general. Furthermore, data call for verification languages based on first-order temporal logics. The resulting verification problem is much harder than in the finite-state setting, leading to undecidability even for severely restricted systems. In this course, we tackle the fundamental challenge of finding a tradeoff between the expressiveness of the verification language, and that of the data-aware process formalism, making verification decidable without compromising the ability to capture real-world scenarios. This requires to synergically combine different techniques deeply rooted in logic and computation.