29th European Summer School in Logic, Language, and Information
University of Toulouse (France), 17-28 July, 2017

Verification of Data-Aware Processes

Diego Calvanese, Marco Montali

Logic and Computation (Advanced)

Second week, from 9:00 to 10:30, room E


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.



1. Introduction and Motivation (slides).

2. Data-Centric Dynamic Systems (slides).

3. Verification Logics (slides).

4. Counter Automata and Undecidability Results (slides).

5. Bisimulations and Decidability Results (slides).

6. Exploiting DCDSs: Models, Methods, Concrete Systems (slides).


Reference papers: see here.