Parameterised Verification of Data-Aware Multi-Agent Systems
Abstract
We introduce parameterised data-aware multi-agent systems, a formalism to reason about the temporal-epistemic properties of arbitrarily large collections of homogeneous agents, each operating on an infinite data domain. We show that their parameterised verification problem is semi-decidable for classes of interest. This is demonstrated by separately addressing the unboundedness of the number of agents and the the data domain. In doing so we reduce the parameterised model checking problem for these systems to that of parameterised verification for interleaved interpreted systems. We illustrate the expressivity of the formal model by modelling English auctions with an unbounded number of bidders on unbouded data and show how the technique here introduced can be used to give formal guarantees on the resulting system behaviour.
Cite
Text
Belardinelli et al. "Parameterised Verification of Data-Aware Multi-Agent Systems." International Joint Conference on Artificial Intelligence, 2017. doi:10.24963/IJCAI.2017/15Markdown
[Belardinelli et al. "Parameterised Verification of Data-Aware Multi-Agent Systems." International Joint Conference on Artificial Intelligence, 2017.](https://mlanthology.org/ijcai/2017/belardinelli2017ijcai-parameterised/) doi:10.24963/IJCAI.2017/15BibTeX
@inproceedings{belardinelli2017ijcai-parameterised,
title = {{Parameterised Verification of Data-Aware Multi-Agent Systems}},
author = {Belardinelli, Francesco and Kouvaros, Panagiotis and Lomuscio, Alessio},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2017},
pages = {98-104},
doi = {10.24963/IJCAI.2017/15},
url = {https://mlanthology.org/ijcai/2017/belardinelli2017ijcai-parameterised/}
}