Formal Methods for Control of Traffic Flow: Automated Control Synthesis from Finite-State Transition Models

Today's increasingly populous cities require intelligent transportation systems that make efficient use of existing transportation infrastructure. However, inefficient traffic management is pervasive [1], [2], costing US$160 billion in the United States in 2015, including 6.9 billion h of additional travel time and 3.1 billion gal of wasted fuel [3]. To mitigate these costs, the next generation of transportation systems will include connected vehicles, connected infrastructure, and increased automation. In addition, these advances must coexist with legacy technology into the foreseeable future. This complexity makes the goal of improved mobility and safety even more daunting.