Formal Verification of Opinion Formation in Swarms

We investigate the formal verification of consensus protocols in swarm systems composed of arbitrary many agents. We use templates to define the behaviour of the agents in an opinion dynamics setting and formulate their verification in terms of the associated parameterised model checking problem. We define a finite abstract model that we show to simulate swarms of any size, thereby precisely encoding any concrete instantiation of the swarm. We give an automatic procedure for verifying temporal-epistemic properties of consensus protocols by model checking the associated finite abstract model. We present a toolkit that can be used to generate the abstract model automatically and verify a given protocol by symbolic model checking. We use the toolkit to verify the correctness of majority rule protocols in arbitrary large swarms.