A swarm robotic system consists of a team of robots performing cooperative tasks without any centralized coordination. In principle, swarms enable flexible and scalable solutions; however, designing individual control algorithms that can guarantee a required global behavior is difficult. Formal methods have been suggested by several researchers as a mean to increase confidence in the behavior of the swarm. In this work, we propose to model swarms as hybrid systems and use reachability analysis to verify their properties. We discuss challenges and report on the experience gained from applying hybrid formalisms to the verification of a swarm robotic system.
翻译:群体机器人系统由一组机器人组成,在没有任何集中协调的情况下执行合作任务。原则上,群体能够带来灵活和可扩展的解决办法;然而,设计个人控制算法以保障必要的全球行为是困难的。一些研究人员建议采用正规方法,作为增强对群体行为信心的一种手段。在这项工作中,我们提议将群体模拟成混合系统,并利用可达性分析来核实其特性。我们讨论挑战,并报告在将混合形式主义用于核实群体机器人系统方面取得的经验。