Specification and Verification of Commitment-Regulated Data-Aware Multiagent Systems

Marco Montali, Diego Calvanese, and Giuseppe De Giacomo

Proc. of the 29th Italian Conf. on Computational Logic (CILC 2014). Volume 1195 of CEUR Workshop Proceedings, http://ceur-ws.org/. 2014.

In this paper we investigate multiagent systems whose agent interaction is based on social commitments that evolve over time, in presence of (possibly incomplete) data. In particular, we are interested in modeling and verifying how data maintained by the agents impact on the dynamics of such systems, and on the evolution of their commitments. This requires to lift the commitment-related conditions studied in the literature, which are typically based on propositional logics, to a first-order setting. To this purpose, we propose a rich framework for modeling data-aware commitment-based multiagent systems. In this framework, we study verification of rich temporal properties, establishing its decidability under the condition of "state-boundedness", i.e., data items come from an infinite domain but, at every time point, each agent can store only a bounded number of them.


@inproceedings{CILC-2014,
   title = "Specification and Verification of Commitment-Regulated
Data-Aware Multiagent Systems",
   year = "2014",
   author = "Marco Montali and Diego Calvanese and De Giacomo, Giuseppe",
   booktitle = "Proc. of the 29th Italian Conf. on Computational Logic
(CILC 2014)",
   pages = "84--98",
   volume = "1195",
   series = "CEUR Workshop Proceedings, http://ceur-ws.org/",
}
pdf url