@Article{2019.100000110,
AUTHOR = {Honghao Gao, Wanqiu Huang, Xiaoxian Yang},
TITLE = {Applying Probabilistic Model Checking to Path Planning in an Intelligent Transportation System Using Mobility Trajectories and Their Statistical  Data},
JOURNAL = {Intelligent Automation \& Soft Computing},
VOLUME = {25},
YEAR = {2019},
NUMBER = {3},
PAGES = {547--559},
URL = {http://www.techscience.com/iasc/v25n3/39684},
ISSN = {2326-005X},
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.},
DOI = {10.31209/2019.100000110}
}