Traffic Intersections as Agents: A model checking approach for analysing communicating agents

The analysis of traffic policies, for instance, the duration of green and red phases at intersections, can be quite challenging. While the introduction of communication systems can potentially lead to better solutions, it is important to analyse and formulate policies in the presence of potential communication failures and delays. Given the stochastic nature of traffic, posing the problem as a model checking problem in probabilistic epistemic temporal logic seems promising. In this work, we propose an approach that uses epistemic modalities to model the effect of communication between multiple intersections and temporal modalities to model the progression of traffic volumes over time. We validate our approach in a non-stochastic setting, using the tool Model Checker for Multi-Agent Systems (MCMAS). We develop a Statistical Model Checking module and use it in conjunction with a tool chain that integrates a traffic simulator (SUMO) and a network simulator (OMNeT++/Veins) to study the impact of communications on traffic policies.