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

计算机工程与应用 ›› 2016, Vol. 52 ›› Issue (10): 31-38.

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

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

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

出版日期:2016-05-15 发布日期:2016-05-16

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.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

摘要/Abstract

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

null

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

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.

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

王铭1，王瑞1，李晓娟1，关永1，张杰2，魏洪兴3. 非确定性环境中移动机器人避障策略的验证
——基于形式化建模和概率分析[J]. 计算机工程与应用, 2016, 52(10): 31-38.

WANG Ming1, WANG Rui1, LI Xiaojuan1, GUAN Yong1, ZHANG Jie2, WEI Hongxing3. Verification of mobile robot obstacle avoidance strategies in uncertain environment based on formal modeling and probabilistic analysis[J]. Computer Engineering and Applications, 2016, 52(10): 31-38.

[1]	廖列法，李浩瀚，李帅，朱合隆，李志军. 结合Winner-Take-All的足球机器人控制策略研究[J]. 计算机工程与应用, 2021, 57(7): 136-143.
[2]	王迪，李彩虹，郭娜，刘国名，高腾腾. 基于模糊势场法的移动机器人局部路径规划[J]. 计算机工程与应用, 2021, 57(6): 212-218.
[3]	蒋林，方东君，雷斌，李维刚. 单目视觉移动机器人导航算法研究现状及趋势[J]. 计算机工程与应用, 2021, 57(5): 1-9.
[4]	杨凌耀，张爱华，张洁，宋季强. 栅格地图环境下机器人速度势实时路径规划[J]. 计算机工程与应用, 2021, 57(24): 290-295.
[5]	张子然，黄卫华，陈阳，章政，李梓远. 基于双向搜索的改进蚁群路径规划算法[J]. 计算机工程与应用, 2021, 57(21): 270-277.
[6]	涂睿，王文格，卢成阳. 移动机器人实时采样路径重规划[J]. 计算机工程与应用, 2021, 57(20): 157-163.
[7]	林韩熙，向丹，欧阳剑，兰晓东. 移动机器人路径规划算法的研究综述[J]. 计算机工程与应用, 2021, 57(18): 38-48.
[8]	王科银，石振，杨正才，杨亚会，王思山. 改进强化学习算法应用于移动机器人路径规划[J]. 计算机工程与应用, 2021, 57(18): 270-274.
[9]	李二超，齐款款. 改进双向蚁群算法的移动机器人路径规划[J]. 计算机工程与应用, 2021, 57(18): 281-288.
[10]	贾文友，江磊，曹紫阳，梁利东. 能耗约束优化工业机器人作业轨迹[J]. 计算机工程与应用, 2021, 57(15): 245-250.
[11]	唐蕾，刘广钟. 改进TD3算法在四旋翼无人机避障中的应用[J]. 计算机工程与应用, 2021, 57(11): 254-259.
[12]	华洪，张志安，施振稳，陈冠星. 动态环境下多重A*算法的机器人路径规划方法[J]. 计算机工程与应用, 2021, 57(10): 173-180.
[13]	郭娜，李彩虹，王迪，张宁，刘国名. 结合预测和模糊控制的移动机器人路径规划[J]. 计算机工程与应用, 2020, 56(8): 104-109.
[14]	周睿慜，李辉. 改进动态规划算法的移动机器人路径规划[J]. 计算机工程与应用, 2020, 56(21): 20-24.
[15]	侯锐，卜旭辉. 任意初始位置机器人领航跟随型迭代学习编队[J]. 计算机工程与应用, 2020, 56(20): 226-231.