June 17, 2013Francesco Belardinelli (Laboratoire IBISC, Université d'Evry) P1-05
Artifact systems have recently received considerable attention in the business process community. These can be described in terms of interacting modules, or artifacts, consisting of a data model and a lifecycle, which account respectively for the relational structure of data and their evolutions over time. However, by considering data and processes as equally relevant tenets, the typical questions concerning the verification of these services become inherently more difficult and can no longer be solved by current methodologies. Specifically, the presence of data means that the number of states in artifact systems is infinite in general.
In this talk I will present agent-based abstraction techniques that can be deployed to make the model checking problem amenable, thus obtaining decidability results for specific classes of artifact systems. These results enable the verification of basic temporal-epistemic properties in a first-order setting.
The research presented in this talk is joint work with Prof A. Lomuscio and Dr F. Patrizi and it has received funding within the EU STREP Project ACSI.