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

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

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