Traffic Network Control from Temporal Logic Specifications

TL;DR

This paper introduces a formal methods-based framework for designing traffic signal control policies that satisfy complex temporal logic specifications, ensuring correctness and efficiency in large traffic networks.

Contribution

It develops a novel approach leveraging model checking and structural properties of traffic networks to generate correct-by-construction controllers efficiently.

Findings

The framework guarantees satisfaction of complex control objectives.

Exploits componentwise monotonicity for scalable reachability analysis.

Achieves linear scaling in computation with respect to network size.

Abstract

We propose a framework for generating a signal control policy for a traffic network of signalized intersections to accomplish control objectives expressible using linear temporal logic. By applying techniques from model checking and formal methods, we obtain a correct-by-construction controller that is guaranteed to satisfy complex specifications. To apply these tools, we identify and exploit structural properties particular to traffic networks that allow for efficient computation of a finite state abstraction. In particular, traffic networks exhibit a componentwise monotonicity property which allows reach set computations that scale linearly with the dimension of the continuous state space.