Verification of Data-Aware Commitment-Based Multiagent Systems

Proc. of the 13th Int. Conf. on Autonomous Agents and Multiagent Systems (AAMAS 2014). 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. Our framework includes a domain and system ontology, described in a lightweight description logic, which is used by the agents as a common ground for their interaction, and actions, driven by events, that specify how data, events, commitments, and agents themselves, evolve over time. One particular agent, called the institutional agent, makes use of a first-order version of a commitment machine, to keep track of the status of contracts among agents. 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{AAMAS-2014,
   title = "Verification of Data-Aware Commitment-Based Multiagent
Systems",
   year = "2014",
   author = "Marco Montali and Diego Calvanese and De Giacomo, Giuseppe",
   booktitle = "Proc. of the 13th Int. Conf. on Autonomous Agents and
Multiagent Systems (AAMAS 2014)",
   pages = "157--164",
}