UC Berkeley

We tackle the issue of scalability when synthesizing controllers for large signalized vehicular traffic networks with linear temporal logic specifications. Traffic networks lend themselves to a compositional synthesis approach because they are naturally decomposed into sub-networks. However, naïvely synthesizing controllers for individual sub-networks and interconnecting them can violate the specifications on the monolithic network. By exploiting notions of supply and demand in our system dynamics, we construct contracts between sub-networks that guarantee the soundness of the overall synthesized controller. The resulting decentralized control architecture consists of controllers that rely only on local state information.