Analysing robot swarm behaviour via probabilistic model checking
详细信息 查看全文
- 作者：Savas Konur ; Konur@liverpool.ac.uk ; [Author Vitae] ; Clare Dixon CLDixon@liverpool.ac.uk ; [Author Vitae] ; Michael Fisher MFisher@liverpool.ac.uk ; [Author Vitae]
- 关键词：Robot swarms ; Swarm algorithms ; Formal verification ; Probabilistic model-checking
- 刊名：Robotics and Autonomous Systems
- 出版年：2012
- 出版时间：February 2012
- 年：2012
- 卷：60
- 期：2
- 页码：199-213
- 全文大小：1123 K
文摘
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.