Applying Probabilistic Model Checking to Path Planning in an Intelligent Transportation System Using Mobility Trajectories and Their Statistical Data

Path planning is an important topic of research in modern intelligent traffic systems (ITSs). Traditional path planning methods aim to identify the shortest path and recommend this path to the user. However, the shortest path is not always optimal, especially in emergency rescue scenarios. Thus, complex and changeable factors, such as traffic congestion, road construction and traffic accidents, should be considered when planning paths. To address this consideration, the maximum passing probability of a road is considered the optimal condition for path recommendation. In this paper, the traffic network is abstracted as a directed graph. Probabilistic data on traffic flow are obtained using a mobile trajectory-based statistical analysis method. Subsequently, a probabilistic model of the traffic network is proposed in the form of a discretetime Markov chain (DTMC) for further computations. According to the path requirement expected by the user, a point probability pass formula and a multiple-target probability pass formula are obtained. Probabilistic computation tree logic (PCTL) is used to describe the verification property, which can be evaluated using the probabilistic symbolic model checker (PRISM). Next, based on the quantitative verification results, the maximum probability path is selected and confirmed from the set of K-shortest paths. Finally, a case study of an emergency system under real-time traffic conditions is shown, and the results of a series of experiments show that our proposed method can effectively improve the efficiency and quality of emergency rescue services.