Traffic Network Control from Temporal Logic Specifications

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.

Cited by in corpus (5)

• Control Strategies for COVID-19 Epidemic with Vaccination, Shield Immunity and Quarantine: A Metric Temporal Logic Approach
• Formal Synthesis of Control Strategies for Positive Monotone Systems
• Control Barrier Functions for Abstraction-Free Control Synthesis under Temporal Logic Constraints
• Data-driven Variable Speed Limit Design for Highways via Distributionally Robust Optimization
• Control Synthesis for Cyber-Physical Systems to Satisfy Metric Interval Temporal Logic Objectives under Timing and Actuator Attacks