自时态逻辑规范中自动合成搜索与救援控制器
摘要：搜索和救援机器人的正确构建控制器的合成被考虑。近年来，在城市环境中进行灾害缓解的机器人的发展受到积极鼓励，因为机器人可以在危险和危险区域部署，而人类搜索和救援行动是不可能的。为了满足SAR中的可靠性要求，机器人的规范是以线性时间逻辑的形式说明的，并且合成为可以执行为控制器的有限状态机。所得到的控制器是纯离散的，并通过根据它们从传感器或其他机器人接收到的输入来改变其内部状态，与其环境进行持续的交互。由于SAR机器人必须合作完成所需的任务，因此考虑了共同实现一个共同目标的控制器的合成。这个分布式合成问题是不可判定的，因此它不能以完全的通用方式解决，但是引入了一套设计原则，以开发专门的可合成规范。特别是，通过引入经过验证的标准化通信协议和在机器人之间预先协商来解决通信和合作问题。机器人在一个图上移动，在这个图上考虑对静止和移动目标的搜索。搜索移动目标被转化为一个警察和强盗的游戏，并且开发了实现获胜策略的规范，以使所需的机器人数量最小化。通过合成执行搜索和救援静止目标以及搜索移动目标的机器人的控制器，证明了方法的可行性。显示了这些控制器确保实现了寻找和营救目标的共同目标。
作者：Clemens Wiltsche
论文ID：1304.6898
分类：Systems and Control
分类简称：cs.SY
提交时间：2013-04-26