Computer Engineering and Applications ›› 2016, Vol. 52 ›› Issue (10): 31-38.

Previous Articles     Next Articles

Verification of mobile robot obstacle avoidance strategies in uncertain environment based on formal modeling and probabilistic analysis

WANG Ming1, WANG Rui1, LI Xiaojuan1, GUAN Yong1, ZHANG Jie2, WEI Hongxing3   

  1. 1.Beijing Key Laboratory of Electronic System Reliability Technology, Capital Normal University, Beijing 100048, China
    2.College of Information Science & Technology, Beijing University of Chemical Technology, Beijing 100029, China
    3.School of Mechanical Engineering and Automation, Beijing University of Aeronautics & Astronautics, Beijing 100191, China
  • Online:2016-05-15 Published:2016-05-16

非确定性环境中移动机器人避障策略的验证
——基于形式化建模和概率分析

王  铭1,王  瑞1,李晓娟1,关  永1,张  杰2,魏洪兴3   

  1. 1.高可靠嵌入式系统技术北京市工程研究中心 电子系统可靠性技术北京市重点实验室,首都师范大学 信息工程学院,北京 100048
    2.北京化工大学 信息科学与技术学院,北京 100029
    3.北京航空航天大学 机械工程及自动化学院,北京100191

Abstract: In terms of mobile robot with actuator errors,sensor noise and other factors,the method of probabilistic model checking is proposed to verify and quantitatively analyze its obstacle avoidance strategies in uncertain environment.The obstacle avoidance motion of the mobile robot and uncertain movement of a dynamic obstacle are modeled as Markov Decision Processes.Furthermore,the important motion properties of mobile robot are translated to probabilistic computation tree logic formulae and verified in a probabilistic model checking tool.Finally,the results are obtained including the available time to succeed in avoiding the obstacle,the total time and energy consumption to reach the target location for mobile robot and the influences of the collision avoidance time on the obstacle avoidance methods when the operation errors occur; and the MATLAB is also used to verify the correctness of the successful avoidance time.

null

Key words: uncertain environment, mobile robot, obstacle avoidance, probabilistic model checking, Markov Decision Process

摘要: 针对存在制动机误差和传感器噪声等因素的移动机器人,提出采用概率模型检测的方法对非确定性环境中移动机器人的避障策略进行验证和定量分析。首先将移动机器人的避障运动和动态障碍物的不确定性运动建模为马尔可夫决策过程。然后运用概率计算树逻辑语言描述移动机器人运动的关键属性并使用概率模型检测工具对其进行验证。最后分析得到移动机器人成功避障所花费的避碰时间,移动机器人到达目标位置所需要的时间和能量以及操作误差发生时的避碰时间对避障策略的影响,并使用MATLAB仿真验证成功避碰时间的正确性。

关键词: 非确定性环境, 移动机器人, 避障, 概率模型检测, 马尔可夫决策过程