Autosoft Journal

Online Manuscript Access

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 discrete-time 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.



Total Pages: 13


Manuscript ViewPdf Subscription required to access this document

Obtain access this manuscript in one of the following ways

Already subscribed?

Need information on obtaining a subscription? Personal and institutional subscriptions are available.

Already an author? Have access via email address?


Online Article


ISSN PRINT: 1079-8587
ISSN ONLINE: 2326-005X
DOI PREFIX: 10.31209
10.1080/10798587 with T&F
IMPACT FACTOR: 0.652 (2017/2018)
Journal: 1995-Present


TSI Press
18015 Bullis Hill
San Antonio, TX 78258 USA
PH: 210 479 1022
FAX: 210 479 1048