Verifying Emergence of Bounded Time Properties in Probabilistic Swarm Systems

Verifying Emergence of Bounded Time Properties in Probabilistic Swarm Systems

Alessio Lomuscio, Edoardo Pirovano

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence
Main track. Pages 403-409. https://doi.org/10.24963/ijcai.2018/56

We introduce a parameterised semantics for reasoning about swarms as unbounded collections of agents in a probabilistic setting. We develop a method for the formal identification of emergent properties, expressed in a fragment of the probabilistic logic PCTL. We introduce algorithms for solving the related decision problems and show their correctness. We present an implementation and evaluate its performance on an ant coverage algorithm.
Keywords:
Agent-based and Multi-agent Systems: Agent Theories and Models
Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis
Multidisciplinary Topics and Applications: Validation and Verification