A Counter Abstraction Technique for the Verification of Probabilistic Swarm Systems


We introduce a method for formally verifying properties of arbitrarily large swarms whose agents are modelled probabilistically. We define a parameterised probabilistic semantics for modelling swarms and observe that their verification problem against PLTL specifications is undecidable. We develop a partial procedure for verifying arbitrarily large swarms based on counter abstraction and show its correctness. We present an implementation and report the experimental results obtained when verifying a swarm foraging protocol.

Proceedings of the 18th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2019)