基于UPPAAL的认知机器人控制行为建模与验证

摘要 随着机器人技术的高速发展，越来越多的人开始聚焦到认知机器人领域的研究，机器人系统中的两大研究领域主要是路径规划和任务规划，而传统的规划问题主要侧重于任务规划.本文的研究是在机器人基于行为的控制结构的基础上，提出机器人系统的任务规划层次框架.认知机器人的大部分的控制行为需要人的参与，这就要求这类机器人系统具有在线自适应的能力，而采用传统的验证方法验证其正确性和实时性上存在一定的局限性.采用形式化方法对认知机器人系统的简单实例建模并验证几个重要的属性，采用时间自动机对系统进行形式化的描述，并结合符号化模型检测工具Uppaal进行验证.针对系统的重要属性采用计算树逻辑的形式表述.