非确定性环境中移动机器人实时避障的概率模型检测

Probabilistic Model Checking for Real-time Obstacle Avoidance of Mobile Robot in a Non-deterministic Environment

移动机器人的避障问题是机器人学的重要问题,实时避障是移动机器人安全导航的关键.针对移动机器人存在的制动机误差和传感器噪声等不确定因素,采用概率模型检测的方法对实时避障控制策略进行验证和定量分析.首先,将目标机器人的避障运动及动态障碍物的非确定运动建模为马尔科夫决策过程,其中避障策略包括等待避障、减速避障和加速避障.然后,运用概率计算树逻辑语言描述目标机器人运动的关键属性并使用概率模型检测工具进行验证.最后,分析得到目标机器人与动态障碍物发生碰撞的最大概率值;目标机器人采取减速(加速)避障时,减速(加速)行驶的最佳时间;目标机器人的控制误差对避障运动的影响等.实验结果表明某些参数影响目标机器人的避障效果,并为参数值的选择提供参考依据.

Mobile robot obstacle avoidance is an important problem in robots and the real-time obstacle avoidance is the key for robots to navigate reliably. For the actuator errors, sensor noise and other uncertainties of the mobile robot, this paper adopts the method of probabilistic model checking to verify and quantify its real-time obstacle avoidance strategies. First, the target robot obstacle avoidance motion and some dynamic obstacles uncertain movements in the experimental environment are modeled as a Markov decision process, where the obstacle avoidance strategies include waiting avoidance, deceleration avoidance and acceleration avoidance. Then, use the language of probabilistic computation tree logic to describe motion properties and use the probabilistic model checking tool to verify them. Finally, analyze and obtain the maximum probability of occurring collision between the target robot and obstacles, the best time to decelerate （accelerate）when the target robot uses the deceleration （ acceleration ） method to avoid obstacles, some influences on obstacle avoidance by control errors and so on. Experimental results show that some parameters of the target robot affect the obstacle avoidance effects and provide reference value to choose the values of these parameters.