Verification of Artifact-Centric Multi-Agent Systems - Alessio Lomuscio
Artifact-Centric systems are a particular kind of web-services where data feature prominently in the system description. The emphasis on data makes automata-based formalisms commonly used to model services insufficient and calls for the explicit representation of the evolution of the underlying databases. In this talk I will explore the verification problem for artifact-centric multi-agent systems, i.e., systems of agents interacting through artifact systems. I will point to the undecidability of the model checking problem of these systems when analysed against specifications based on first-order temporal-epistemic logic. I will then analyse conditions that enable us to obtain a decidable problem through finite abstractions that are bisimilar to a given model. The talk is based on results published at IJCAI2011, ICSOC2011, and KR2012.