Probabilistic Model Checking for Robot Path Planning
Xia Chun-ru · Jisuanji fangzhen · 2015
Aiming at the problem that mobile robot is always influenced by the environment in practical applications,a new method based on probabilistic model checking was proposed for path planning. The main factors of environment that may have an influence on the robot were analyzed. The motion behavior of robot was considered as an uncertain action,then Markov Decision Process(MDP) model was built. Meanwhile,the properties were described in Probabilistic Computation Tree Logic(PCTL) to express complex and diverse needs of behavior. The model was verified and analyzed on the PRISM platform for finding the global optimal path and quantitative data. The simulation experiment demonstrates that this optimal path can meet the mission requirements and collision-free and always avoid complex environment areas to ensure that the robots complete the task in maximum probability. The comparison experiments demonstrate the correctness and effectiveness of the method.