Applying Probabilistic Model Checking to Path Planning for a Smart Multimodal Transportation System Using IoT Sensor Data

With the development of artificial intelligence (AI) and the Internet of Things (IoT), public transportation systems in our daily lives are smarter than ever. A large number of wireless sensors are distributed in roadside units (RSUs), collecting traffic flow and public vehicle information to monitor and learn about road congestion, subway arrival, and traffic accidents in real-time. In this paper, we propose probabilistic model checking based path planning for a multimodal transportation system. First, a traffic network with different means of travel is formalized as a directional graph, and the traffic congestion probability is generated from IoT sensor data. Moreover, a discrete-time Markov chain (DTMC) is introduced as the formal model to support quantitative verification. Second, users may have different travel requirements except the shortest path, so user-oriented critical paths are proposed. Then, the minimum cost and the minimum congestion requirements are defined in the form of probabilistic computation tree logic (PCTL) to describe the verification property for evaluating the selected path. We focus on the temporal relations of key points that a user needs to visit to build the travel path. Third, the optimal path is identified and confirmed based on the quantitative results returned by the probabilistic model checker, PRISM, which is a supporting tool that verifies the property against the formal model. Finally, case studies are conducted to demonstrate the feasibility and availability of our proposed method for the smart transportation system.