多自主机器人的协作及其群体行为分析

在本文中，我们扩展了先前关于协作自主机器人的研究，以纳入环境变化以及群体中机器人数量变化可能影响分配给机器人群体任务执行效率的情形。我们提出了一种基于机器人行为划分的新方法。描述子例程的子图使我们能够使用有限数量的状态组合对自主机器人之间的高级交互进行建模，从而避免可达性的组合爆炸。我们识别了能够确保机器人交互正确性的系统。提出了用于验证和分析组合机器人行为的新技术。划分图使我们能够对自主机器人之间的高级交互进行建模，并检测死锁、缺乏终止等异常。提出了使用模型检测方法验证和分析组合机器人行为的技术。所描述的系统Dedan验证器仍在开发中。在不久的将来，计划进行定时与概率验证。