Towards Autonomous Robotic Systems - 16th Annual Conference, TAROS 2015, Liverpool, UK, September 8-10, 2015, Proceedings
Towards Autonomous Robotic Systems - 16th Annual Conference, TAROS 2015, Liverpool, UK, September 8-10, 2015, Proceedings
复制标题
迈向自主机器人系统 - 第 16 届年会，TAROS 2015，英国利物浦，2015 年 9 月 8-10 日，会议记录
DOI：
10.1007/978-3-319-22416-9_4
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Antuña L
中科院分区：
文献类型：
--
作者：
Antuña L
机器人群体的全局行为对于实现其导航任务目标非常重要。这些紧急行为可以通过模型检查等技术进行验证，以评估其正确性。模型检测基于系统的离散模型（如网格中的群），详尽地探索所有可能的行为。模型检测中的一个常见问题是当模型的状态很多时会出现状态空间爆炸。我们提出了一种新的实现对称性减少，在相对于一个参考的编码导航算法的形式，利用网格中的群的对称性。我们将相对编码应用于为NuSMV模型检查器建模的群导航算法Alpha。状态空间和验证结果与绝对（或全局）和相对编码的theAlphaalgorithm的比较突出了我们的方法的优势，允许模型检查更大的网格大小和更多的机器人，从而验证更复杂的紧急行为。例如，在全局编码中，验证了具有3个机器人和最大允许单元大小的网格的属性，而使用相对编码增加了该大小。此外，在agrid中，为3个机器人群验证属性的时间从近10小时减少到仅7分钟。我们的方法是转移到其他群体导航算法。
The emergent global behaviours of robotic swarms are important for them to achieve their navigation task goals. These emergent behaviours can be verified to assess their correctness, through techniques like model checking. Model checking exhaustively explores all possible behaviours, based on a discrete model of the system, such as a swarm in a grid. A common problem in model checking is the state-space explosion that arises when the states of the model are numerous. We propose a novel implementation of symmetry reduction, in the form of encoding navigation algorithms relatively with respect to a reference, exploiting the symmetrical properties of swarms in grids. We applied the relative encoding to a swarm navigation algorithm,Alpha, modelled for the NuSMV model checker. A comparison of the state-space and verification results with an absolute (or global) and a relative encoding of theAlphaalgorithm highlights the advantages of our approach, allowing model checking both larger grid sizes and higher numbers of robots, and consequently verifying more complex emergent behaviours. For example, a property was verified for a grid with 3 robots and a maximum allowed size ofcells in a global encoding, whereas this size was increased tousing a relative encoding. Also, the time to verify a property for a swarm of 3 robots in agrid was reduced from almost 10 hours to only 7 minutes. Our approach is transferable to other swarm navigation algorithms.