基于概率时间自动机的移动机器人运动规划方法研究

A robot is a comprehensive system collecting environment sensing, localization, controlling and decision-making, etc. It is wildly used in all walks of life, which makes it a hot issue in both academic and industrial area. The safety and reliability of robots system should be highly ensured, in case of huge personal injuries or property damages caused by system failure. Formal methods are efficient means to make sure of the correctness and reliability of the system. The time constraints for robotic missions can be well expressed in temporal logic. In this project, we will focus on the motion planning problem of modern mobile robots in complicated environment. Model checking, one of formal methods, is adopted here. Design and implementation of the robot control software will be achieved for motion planning based on probabilitic timed automata. To check the effect of our approach, an experiment environment will be established as well. The difficulty of the project lies in the formalization of dynamic environment, motion space and kinematic models. We will do the research from the following three aspects: (1) formal modeling of environment, robots behavior and requirement specifications, (2) the generation of motion trajectories in dynamic environment, (3) continuous control input generation under discrete trajectories. This project is aiming at achieving a theoretical method and technical innovation, and then applying it to the design and verification of motion planning of mobile robots for medical service.

机器人是集环境感知、定位、控制决策等于一体的综合性系统,在众多行业中应用广泛,是国内外学术界和工业界的研究热点。机器人对系统的安全性和可靠性有着极高要求。其故障和失效将会导致人身和财产的重大损失。形式化方法是确保系统可靠性和正确性的重要手段。本课题基于现代移动机器人系统的特征，针对复杂环境下移动机器人的运动规划问题，将模型检测方法应用于运动规划中，研究机器人控制软件中基于概率时间自动机的运动规划方法，设计和实现相应算法，建立机器人试验环境，验证方法的有效性。该课题的研究难点在于机器人的动态环境、运动空间和运动学模型的形式化，课题将从以下三个方面展开研究：1、环境、机器人行为、属性规范的形式化建模方法；2、动态环境下运动轨迹生成；3、离散轨迹的连续控制输入生成。项目研究成果力求取得理论方法和技术创新，并应用于医疗服务领域移动机器人软件运动规划的设计和验证。

运动规划是机器人领域研究的热点和难点。本项目针对动态环境下移动机器人执行复杂任务的规划问题，首次提出了将概率模型检测方法结合传统的RRP算法来做规划。该方法提高了规划的准确性，并能够解决复杂任务。项目完成了环境、机器人行为、属性规范的形式化建模。结合RRP算法生成运动轨迹。并在运动学方程的约束下求出控制输入。首次使用SMT方法建模和求解运动规划问题。实验结果表明和最快的规划算法PDST相比速度提高了约80%，并且保证规划100%正确性。提出使用时间自动机建模和求解多机器人运动规划问题。该方法能规划出最优化、无碰撞且能够组成目标形状的路径，弥补了原方法的不足。上述运动规划方法已在实验室的移动机器人上得到应用。对机器人实时操作系统RGMP-ROS系统节点间的通信进行验证，在理论上证明了RGMP实时节点间的通讯时间小于0.1ms，以及实时节点中断响应时间和非实时节点间运行的任务无关。运用定理证明，对机器人操作系统ROS的核心功能--节点间通信设计的功能正确性和终止性进行验证。提取了与其相关的有序性、活跃性、正确性等6个重要属性进行形式化验证和分析。结果表明ROS节点间通信的设计符合终止性。此外，进行了机器人系统模块化建模方法和代码生成的研究。采用时间自动机模型，建立常用的机器人原子任务模型库和组合模板。开发了从时间自动机模型生成能够运行在ROS上的C++代码工具。该工具能够保证编码过程中不会引入人为错误，缩短机器人的开发周期。