Towards Temporal Verification of Emergent Behaviours in Swarm Robotic Systems
Towards Temporal Verification of Emergent Behaviours in Swarm Robotic Systems
复制标题
群体机器人系统中紧急行为的时间验证
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Michael Fisher
中科院分区：
文献类型：
--
作者：
C. Dixon;A. Winfield;Michael Fisher
机器人群是一组简单的机器人，它们被设计成一起工作来执行某些任务。这种蜂群依赖于：单个机器人的简单性;具有大量通常相同的机器人所固有的容错性;以及群体作为一个整体的自组织行为。虽然机器人群被部署在越来越复杂的领域，但设计能够保证所需全局行为的单独控制算法是困难的。在本文中，我们应用和评估使用的形式验证技术，特别是模型检测，分析机器人群体的紧急行为。这些技术，基于使用时序逻辑的系统的自动分析，使我们能够分析所有可能的行为，从而确定潜在的问题与机器人群符合一些所需的全球行为。为了展示这种方法，我们针对一个特定的群体控制算法，并显示如何自动时序分析可以帮助完善和分析这样的算法。
A robot swarm is a collection of simple robots designed to work together to carry out some task. Such swarms rely on: the simplicity of the individual robots; the fault tolerance inherent in having a large population of often identical robots; and the self-organised behaviour of the swarm as a whole. Although robot swarms are being deployed in increasingly sophisticated areas, designing individual control algorithms that can guarantee the required global behaviour is difficult. In this paper we apply and assess the use of formal verification techniques, in particular that of model checking, for analysing the emergent behaviours of robotic swarms. These techniques, based on the automated analysis of systems using temporal logics, allow us to analyse all possible behaviours and so identify potential problems with the robot swarm conforming to some required global behaviour. To show this approach we target a particular swarm control algorithm, and show how automated temporal analysis can help to refine and analyse such an algorithm.