On the Formal Verification of Diffusion Phenomena in Open Dynamic Agent Networks

Belardinelli, Francesco and Grossi, Davide ORCID: 0000-0002-9709-030X (2015) On the Formal Verification of Diffusion Phenomena in Open Dynamic Agent Networks. In: AAMAS 2015.

Text camera_ready_aamas15.pdf - Unspecified Download (333kB)

Abstract

The paper is a contribution at the interface of social network theory and multi-agent systems. As realistic models of multi-agent systems, we assume agent networks to be open, that is, agents may join or leave the network at run-time, and dynamic, that is, the network structure may change as a result of agents actions. We provide a formal model of open dynamic agent networks (ODAN) in terms of interpreted systems, and define the problem of model checking properties of diffusion phenomena, such as the spread of information or diseases, expressed in a first-order version of computation-tree logic. We establish the decidability of the model checking problem by showing that, under specific conditions, the verification of infinite-state ODAN can be reduced to model checking finite bisimulations.

Item Type:	Conference or Workshop Item (Unspecified)
Uncontrolled Keywords:	Agent Networks, Diffusion Phenomena, First-order Temporal Logic
Depositing User:	Symplectic Admin
Date Deposited:	05 May 2016 15:55
Last Modified:	15 Dec 2022 22:04
Related URLs:	Author
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3000637