对称性约简实现对蜂群导航算法更复杂涌现行为的模型检测
机器人学
2015-10-12 v2
摘要
机器蜂群的涌现全局行为对实现其导航任务目标十分重要。这些涌现行为可通过模型检测等技术验证其正确性。模型检测基于系统的离散模型（如网格中的蜂群）穷举探索所有可能行为。模型检测中的一个常见问题是当模型状态众多时出现的状态空间爆炸。我们提出一种新颖的对称性约简实现，其形式是基于蜂群在网格中的对称特性，相对于参考点相对地编码导航算法。我们将相对编码应用于为NuSMV模型检测器建模的蜂群导航算法Alpha。将Alpha算法的绝对（或全局）与相对编码的状态空间和验证结果进行比较，凸显了我们方法的优势，允许对更大的网格尺寸和机器人数量进行模型检测，从而验证更复杂的涌现行为。例如，在全局编码中验证了网格含3个机器人且最大允许尺寸为8x8单元的某性质，而使用相对编码时该尺寸增至16x16。此外，在6x6网格中验证3机器人蜂群某性质的时间从近10小时减少到仅7分钟。我们的方法可迁移至其他蜂群导航算法。
引用
@article{arxiv.1505.05695,
title = {Symmetry Reduction Enables Model Checking of More Complex Emergent Behaviours of Swarm Navigation Algorithms},
author = {Laura Antuña and Dejanira Araiza-Illan and Sérgio Campos and Kerstin Eder},
journal= {arXiv preprint arXiv:1505.05695},
year = {2015}
}
备注
Accepted for presentation in Towards Autonomous Robotic Systems (TAROS) 2015, Liverpool, UK