Statistical Model Checking for Traffic Models

Thamilselvam, B. and Kalyanasundaram, Subrahmanyam and Parmar, Shubham and Panduranga Rao, M. V. (2021) Statistical Model Checking for Traffic Models. In: 24th Brazilian Symposium on Formal Methods, SBMF 2021, 6 December 2021through 10 December 2021, Virtual, Online.

Full text not available from this repository. (Request a copy)

Abstract

Statistical Model Checking (SMC) is a popular technique in formal methods for analyzing large stochastic systems. As opposed to the expensive but exact model checking algorithms, this technique allows for a trade-off between accuracy and running time. SMC is based on Monte Carlo sampling of the runs of the stochastic system, and lends itself to stochastic discrete event simulators as well. In this paper, we use SMC to analyze traffic models like car-following and lane-changing models. We achieve this through an integration of the SMC tool MultiVeStA with the discrete event simulation software for urban mobility, SUMO. As illustration of the approach and the tool chain, we compare the car-following and lane-changing models against various performance parameters like throughput, emissions and waiting times. Importantly, the use of formal methods allows for formulating and evaluating complex queries that can be asked of the model. The results show the utility of such a tool chain in performing complex quantitative what-if analyses of various traffic models and policies. © 2021, Springer Nature Switzerland AG.

[error in script]

IITH Creators:

IITH Creators	ORCiD
Panduranga Rao, M. V.	UNSPECIFIED
Kalyanasundaram, Subrahmanyam	UNSPECIFIED

Item Type:

Conference or Workshop Item (Paper)

Additional Information:

Acknowledgment. Thamilselvam is supported by the project M2Smart: Smart Cities for Emerging Countries based on Sensing, Network and Big Data Analysis of Multimodal Regional Transport System, JST/JICA SATREPS (Program ID JPMJSA1606), Japan and Shubham Parmar is supported by the DST National Mission for Interdisciplinary Cyber-Physical Systems (NM-ICPS), Technology Innovation Hub on Autonomous Navigation and Data Acquisition Systems: TiHAN Foundations at Indian Institute of Technology (IIT) Hyderabad.

Uncontrolled Keywords:

Car following and lane changing models; Statistical Model Checking; Traffic modeling and simulation

Subjects:

Computer science

Divisions:

Department of Computer Science & Engineering

Depositing User:

. LibTrainee 2021

Date Deposited:

30 Sep 2022 12:08

Last Modified:

30 Sep 2022 12:08