Abstract: This paper proposes a new method of path planning based on probabilistic model checking in a complex dynamic environment. Aiming at robots are always influenced by external factors in practical applications, some environmental factors are put forward as influence parameters. Markov Decision Process（MDP）model is built and the mobile robot acts are considered uncertain actions. Meanwhile, the properties are described in Probabilistic Computation Tree Logic（PCTL） language to express complex and diverse needs of behavior. The model is verified and analyzed by the PRISM platform for finding the global optimal path that meets the properties. In addition, a strategy of collision avoidance with dynamic obstacles is presented based on the global planning path to realize the local plans for collision-free and at the same time it tries to ensure the maximum probability to complete tasks. The analytical and computer experiment results demonstrate the correctness and effectiveness of the method.

Key words: path planning, dynamic obstacles, probabilistic model checking, Markov decision process, probabilistic computation tree logic

摘要： 提出了一种动态复杂环境下采用概率模型检测技术进行路径规划的新方法。考虑到实际应用中机器人其移动行为总是受到外界因素的影响，将机器人移动行为看作一个不确定事件，提取环境中的影响因素，构建马尔可夫决策过程模型。采用时态逻辑语言描述机器人目标任务，表达复杂多样的需求行为。运用工具PRISM验证属性，得到满足任务需求的全局优化路径。另外，在全局路径的基础上提出了一种动态避障策略，实现避障局部规划的同时尽量保证机器人最大概率完成任务。通过理论和仿真实验结果证明该方法的正确性和有效性。

关键词: 路径规划, 动态障碍物, 概率模型检测, 马尔可夫决策过程, 概率计算树逻辑