Representation of a vehicular traffic model using hybrid systems

TL;DR

This paper models vehicular traffic dynamics using hybrid systems and employs formal verification with KeYmaera to ensure the model's correctness, bridging continuous and discrete traffic behaviors.

Contribution

It introduces a hybrid systems representation of traffic models and applies formal verification techniques to validate their correctness.

Findings

Successful formal verification of the traffic model using KeYmaera

Demonstration of hybrid systems as effective tools for traffic flow analysis

Enhanced understanding of discrete and continuous traffic dynamics

Abstract

There is a great diversity of formal models to understand the dynamics of transport and vehicular flow on a road. Many of these models are inspired by the dynamics of flows governed by partial differential equations. However, it is possible to simplify these models to ordinary equations by considering constant variations in some of the input variables in this type of models. However, given that these types of systems present discrete changes when the vehicle density is altered in some sections of the lane, it seems reasonable to make use of hybrid systems to better understand the evolution of these dynamics. In this work we are interested in making use of dynamic differential logic to formally verify one of these models proposed in ordinary equations. This verification will be done through a proof assistant specially designed for hybrid systems called KeYmaera. Once we adapt the model to a hybrid system representation we proceed to use KeYmaera to verify that the proposed model is formally correct.