Compositional controller synthesis for vehicular traffic networks

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.