基于时序逻辑规范自动合成搜救机器人控制器

本论文探讨了为协助搜救 (SAR) 的机器人合成构造正确控制器的方法。近年来，积极鼓励开发用于城市环境灾害缓解的辅助机器人，因为机器人可部署在人类搜救行动无法进入的危险和有害区域。为满足搜救中的可靠性要求，机器人的规范以线性时序逻辑表述，并合成为可作为控制器执行的有限状态机。生成的控制器是纯离散的，通过根据从传感器或其他机器人接收的输入改变其内部状态，与环境保持持续交互。由于搜救机器人必须协作以完成所需任务，本文考虑了共同实现共同目标的控制器合成问题。该分布式合成问题被证明是不可判定的，因此无法在完全通用情况下求解，但引入了一套设计原则以开发专用的可合成规范。特别是，通过引入经过验证的标准化通信协议并抢占机器人间的协商来解决通信与协作问题。机器人在图上行进，我们在其上考虑对静止和移动目标的搜索。搜索移动目标被表述为警察与强盗博弈，并开发了实现获胜策略的规范，以使所需机器人数量最小化。通过合成为执行静止目标搜救和移动目标搜索的机器人控制器，证明了该方法的可行性。结果表明，这些控制器能保证实现寻找并营救目标的共同目标。