Efficient Traffic Management- A Formal Methods Approach

This project is developing tools for traffic management and control using formal methods. By applying techniques such as model-checking and correct-by-construction synthesis, we ensure that traffic flow satisfies high-level objectives expressed using temporal logics that guarantee desirable behavior such as avoiding congestion, maintaining high throughput, ensuring fairness of ramp metering strategies, and reacting to incidents or unexpected conditions. Our techniques take advantage of inherent structure in traffic networks such as monotonicity properties, decomposability into sparsely connected subsystems, and hybrid dynamics. Exploiting such structure allows scalable and efficient design methodologies applicable to freeway ramp metering and traffic signal timing.