Formal synthesis for traffic control Murat Arcak University of California, Berkeley (UC Berkeley) We will present 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 will highlight key structural properties of traffic networks that make them amenable to this approach. The first structural property is “mixed monotonicity” which relaxes the classical notion of an order-preserving (“monotone”) system. We will see how this property allows a computationally efficient finite abstraction and we will illustrate the result on 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 will exhibit a compositional synthesis technique that introduces supply and demand contracts between the subsystems and ensures the soundness of the composite controller.