Formally Constrained Reinforcement Learning for Traffic Signal Control at Intersections

Ensuring the safety of autonomous systems is paramount for their successful integration into real-world transportation networks. Autonomous Vehicles and Machine Learning-driven traffic management systems have the potential to enhance efficiency and mobility. However, their deployment presents significant safety challenges, particularly in managing interactions between autonomous systems, human-driven vehicles, and pedestrians. This paper addresses these challenges by focusing on Reinforcement Learning (RL)-based traffic signal control. It analyzes traffic safety using Time-To-Collision to identify potential traffic conflicts between vehicle interactions that could jeopardize safety. We propose a novel approach to mitigate these conflicts by guiding the learning process under a formally checked safety constraint. This approach leverages Satisfiability Modulo Theories as a formal method for rigorous verification to ensure that the RL agent's decisions remain within safe operational boundaries, even in dynamic and unpredictable traffic conditions. Additionally, our approach incorporates dynamic speed adjustment mechanisms to address scenarios in which safety constraints are violated. Through traffic simulations, we evaluate the effectiveness of our approach in achieving a balance between traffic signal optimization and traffic safety by ensuring the safe operation of RL under a safety constraint and demonstrate that this adaptive speed control strategy reduces both the frequency and severity of traffic conflicts.