Analysing robot swarm behaviour via probabilistic model checking
Analysing robot swarm behaviour via probabilistic model checking
复制标题
DOI：
10.1016/j.robot.2011.10.005
复制
发表时间：
2012-02
期刊：
影响因子：
--
通讯作者：
Savas Konur;C. Dixon;Michael Fisher
中科院分区：
文献类型：
--
作者：
Savas Konur;C. Dixon;Michael Fisher
部署高复杂性的单个机器人的替代方案可以是利用包括大量相同且简单得多的机器人的机器人群。事实证明，这种群具有适应性、容错性和广泛适用性。然而，设计单个机器人算法以确保有效和正确的整体群体行为实际上是非常困难的。虽然在部署之前评估任何群算法的有效性的机制是必不可少的，但这种机制传统上涉及群行为的计算模拟，或机器人群本身的实验。然而，这种模拟或实验，就其性质而言，不能分析所有可能的群体行为。在本文中，我们将开发和应用自动概率形式验证技术的使用机器人群，涉及详尽的数学分析，以评估群是否真的会按要求行事。特别是，我们考虑一个觅食机器人的情况下，我们应用概率模型检测。
An alternative to deploying a single robot of high complexity can be to utilise robot swarms comprising large numbers of identical, and much simpler, robots. Such swarms have been shown to be adaptable, fault-tolerant and widely applicable. However, designing individual robot algorithms to ensure effective and correct overall swarm behaviour is actually very difficult. While mechanisms for assessing the effectiveness of any swarm algorithm before deployment are essential, such mechanisms have traditionally involved either computational simulations of swarm behaviour, or experiments with robot swarms themselves. However, such simulations or experiments cannot, by their nature, analyse all possible swarm behaviours. In this paper, we will develop and apply the use of automated probabilistic formal verification techniques to robot swarms, involving an exhaustive mathematical analysis, in order to assess whether swarms will indeed behave as required. In particular we consider a foraging robot scenario to which we apply probabilistic model checking.