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

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

项目编号： No.61303014

项目类型： 青年科学基金项目

立项/批准年度： 2014

项目学科： 自动化技术、计算机技术

项目作者： 王瑞

作者单位： 首都师范大学

项目金额： 23万元

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

中文关键词： 运动规划；概率模型检测；机器人验证；时间自动机；

英文摘要： 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 trajecto

英文关键词： Motion Planning；Problistic Model Checking；Robot verification；Timed Automata；