Statistical Model Checking for Traffic Models

• B. Thamilselvam IIT Hyderabad
• Subrahmanyam Kalyanasundaram IIT Hyderabad
• Shubham Parmar IIT Hyderabad
• M.V. Panduranga Rao IIT Hyderabad

Resumo

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.

Palavras-chave: Statistical Model Checking, Traffic modeling and simulation, Car following and lane changing models