Title: Efficient Traffic Management: A Formal Methods Approach The objective of this project is to develop a formal methods approach to traffic management. 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. This project extends this formalism to traffic networks where correctness specifications include eliminating congestion, ensuring that the freeway throughput remains over a minimum threshold, that queues are always eventually emptied, etc. The task is then to design signal timing and ramp metering strategies to meet such specifications. To accomplish this task, the project takes advantage of the inherent structure of existing, validated mathematical models of traffic flow and develops computationally efficient design techniques. The results are tested with real traffic data from the Interstate 210 travel corridor in Southern California. The educational component of the project includes course development on modeling and control of traffic networks, featuring in particular the formal methods approach of this project, and organizing workshops to train traffic engineers and operation practitioners on the use of software tools and methodologies of the project. To meet rich control objectives expressed using temporal logic, the project exploits the piecewise affine nature of existing, validated traffic models, and derives efficient finite state abstractions that form the basis of correct-by-construction control synthesis. To ensure scalability, the project further takes advantage of inherent monotonicity properties and decomposibility into sparsely connected subsystems. The first research task is to develop a design framework for signal timing and ramp metering strategies for signalized intersections and freeway traffic control. The second task is the coordinated control of freeway onramps and nearby signalized intersections to address situations such as a freeway demand surge after a sporting event, or an accident on the freeway when signal settings must be adjusted to favor a detour route. The third task is to pursue designs that exploit the statistics of demand for probabilistic correctness guarantees, as well as designs that incorporate optimality requirements, such as minimizing travel time. Validation of the results is pursued with high-fidelity simulation models calibrated using traffic data from the Interstate 210 travel corridor.