Open Access
ARTICLE
Applying Probabilistic Model Checking to Path Planning in an Intelligent Transportation System Using Mobility Trajectories and Their Statistical Data
Honghao Gao1, 2, 5, Wanqiu Huang1, 4, Xiaoxian Yang3
1 School of Computer Engineering and Science, Shanghai University, Shanghai, China;
2 Computing Center, Shanghai University, Shanghai, 200444, P.R. China;
3 School of Computer and Information Engineering, Shanghai Polytechnic University, Shanghai, China;
4 Shanghai Key Laboratory of Computer Software Evaluating and Testing, Shanghai, China;
5 Shanghai Shang Da Hai Run Information System Co., Ltd, Shanghai, China
* Corresponding Author: Xiaoxian Yang,
Intelligent Automation & Soft Computing 2019, 25(3), 547-559. https://doi.org/10.31209/2019.100000110
Abstract
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.
Keywords
Cite This Article
H. Gao, W. Huang and X. Yang, "Applying probabilistic model checking to path planning in an intelligent transportation system using mobility trajectories and their statistical data,"
Intelligent Automation & Soft Computing, vol. 25, no.3, pp. 547–559, 2019. https://doi.org/10.31209/2019.100000110