Verification of data-aware commitment-based multiagent system

In this paper we investigate multiagent systems whose agent inter- action is based on social commitments that evolve over time, in presence of (possibly incomplete) data. In particular, we are inter- ested 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.