Verifying Emergence of Bounded Time Properties in Probabilistic Swarm Systems

Abstract

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.

Cite

Text

Lomuscio and Pirovano. "Verifying Emergence of Bounded Time Properties in Probabilistic Swarm Systems." International Joint Conference on Artificial Intelligence, 2018. doi:10.24963/IJCAI.2018/56

Markdown

[Lomuscio and Pirovano. "Verifying Emergence of Bounded Time Properties in Probabilistic Swarm Systems." International Joint Conference on Artificial Intelligence, 2018.](https://mlanthology.org/ijcai/2018/lomuscio2018ijcai-verifying/) doi:10.24963/IJCAI.2018/56

BibTeX

@inproceedings{lomuscio2018ijcai-verifying,
  title     = {{Verifying Emergence of Bounded Time Properties in Probabilistic Swarm Systems}},
  author    = {Lomuscio, Alessio and Pirovano, Edoardo},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2018},
  pages     = {403-409},
  doi       = {10.24963/IJCAI.2018/56},
  url       = {https://mlanthology.org/ijcai/2018/lomuscio2018ijcai-verifying/}
}