Efficient Traffic Management - A Formal Methods Approach

Abstract:

This project is developing a formal methods approach to meet temporal logic specifications in traffic control. Formal methods is an area of computer science that develops efficient techniques for proving the correct operation of systems, such as computer programs and digital circuits, and for designing systems that are correct by construction.  We have uncovered two key structural properties of traffic networks that make them amenable to this approach. The first property is “mixed monotonicity” which relaxes the classical notion of an order-preserving (“monotone”) system.  This property allows a computationally efficient finite abstraction applicable to a macroscopic model of traffic flow in a road network.  The second structural property is decomposability into sparsely connected sub-networks. Using this property, we have exhibited a compositional synthesis technique that introduces supply and demand contracts between the subsystems and ensures the soundness of the composite controller. The ongoing research tasks include: 
1) designing more flexible contracts than guaranteed demand and supply at all times,
2) developing probabilistic transition models from statistical data and a synthesis framework that guarantees satisfaction of specifications with high probability,
3) adding optimality criteria to specifications,
4) control synthesis for freeway onramp and arterial signaling coordination,
5) validation with a hybrid freeway/arterial simulation tool that is being developed.