A counter abstraction technique for verifying properties of probabilistic swarm systems

Abstract

We introduce a semantics for reasoning about probabilistic multi-agent systems in which the number of participants is not known at design-time. We define the parameterised model checking problem against PLTL specifications for this semantics, and observe that this is undecidable in general. Nonetheless, we develop a partial decision procedure for it based on counter abstraction. We prove the correctness of this procedure, and present an implementation of it. We then use our implementation to verify a number of example scenarios from swarm robotics and other settings.