Freeway traffic control from linear temporal logic specifications

We propose a methodology for synthesizing ramp metering control strategies for freeway networks from linear temporal logic specifications. Such specifications allow very rich control objectives constructed from temporal operators such as “always” and “eventually” combined with Boolean operators and encompass e.g. safety, reachability, and liveness conditions. We use the cell transmission model of traffic flow on freeway networks to obtain a piecewise affine model of the traffic network, and we apply recent results on control of such systems from temporal logic specifications to synthesize ramp metering strategies that are correct by construction. We demonstrate our approach on several examples.