A Counter Abstraction Technique for the Verification of Robot Swarms

Abstract

We study parameterised verification of robot swarms against temporal-epistemic specifications. We relax some of the significant restrictions assumed in the literature and present a counter abstraction approach that enable us to verify a potentially much smaller abstract model when checking a formula on a swarm of any size. We present an implementation and discuss experimental results obtained for the alpha algorithm for robot swarms.

Cite

Text

Kouvaros and Lomuscio. "A Counter Abstraction Technique for the Verification of Robot Swarms." AAAI Conference on Artificial Intelligence, 2015. doi:10.1609/AAAI.V29I1.9442

Markdown

[Kouvaros and Lomuscio. "A Counter Abstraction Technique for the Verification of Robot Swarms." AAAI Conference on Artificial Intelligence, 2015.](https://mlanthology.org/aaai/2015/kouvaros2015aaai-counter/) doi:10.1609/AAAI.V29I1.9442

BibTeX

@inproceedings{kouvaros2015aaai-counter,
  title     = {{A Counter Abstraction Technique for the Verification of Robot Swarms}},
  author    = {Kouvaros, Panagiotis and Lomuscio, Alessio},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {2015},
  pages     = {2081-2088},
  doi       = {10.1609/AAAI.V29I1.9442},
  url       = {https://mlanthology.org/aaai/2015/kouvaros2015aaai-counter/}
}