Efficient Traffic Management- A Formal Methods Approach Poster.pdf

This project is developing a formal methods approach to meet temporal logic specifications in traffic control. Formal methods offer 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. This project is bringing these powerful techniques to bear on traffic networks.

This year we introduced a new class of specifications, called directed specifications, which encourage high or low valued signal trajectories. We have shown that this class encompasses an expressive fragment of temporal logic and that typical specifications in traffic management are indeed directed. Directed specifications offer major advantages when paired with monotone systems which
preserve a partial order of states. Monotonicity occurs naturally in a large class of traffic flow models, therefore the combination of directed specifications and monotone dynamics has great practical relevance.

First, we showed that directed specifications paired with monotone dynamics are amenable to a systematic form of assumption mining; that is, identifying the set of admissible disturbance signals that generate trajectories satisfying the specification. We developed a multidimensional bisection algorithm that exploits the ordering present in the monotone system model and converges to the
boundary of the assumption set from above and below.

Next, we demonstrated the benefits of directed specifications in formal control synthesis for monotone systems. In particular we developed sparse abstractions that prevent an exponential blowup in the number of transitions in a finite state
abstraction using the directed property of the specification. This was enabled by a new notion of “directed alternating simulation relation.” We further used directed specifications for compositional control synthesis where controllers are synthesized for subsystems and the interactions of the subsystems are accounted for with directed assume-guarantee contracts. When applied to the problem of synthesizing an intersection signal controller, the aforementioned methods dramatically reduce runtime and memory requirements.
In a separate line of work we developed a model predictive control (MPC) strategy that confines the evolution of an urban traffic network to a user-defined “safe” set. Unlike other MPC methods that rely on finite horizons and cannot guarantee safety indefinitely, the new strategy guarantees safety using a finite state abstraction of the system and minimizes a finite horizon cost, such as total
travel time.