Formal Analysis of Lane-Changing Algorithms for Autonomous Vehicles using Probabilistic Model Checking

Abstract

Lane-changing algorithms play a critical role in ensuring passenger safety and traffic efficiency in the dynamic and stochastic environment of Autonomous Vehicles (AVs). Despite their safety-critical nature, these algorithms are predominantly analyzed using computer simulation. While simulations provide valuable insights, their samplingbased nature inherently limits their ability to capture all potential corner cases, which can lead to overlooked safety-critical scenarios. To address these limitations, we advocate for the use of probabilistic model checking as a more rigorous approach for the formal analysis of lane-changing algorithms. Probabilistic model checking is a formal verification technique that systematically explores all possible behaviors of a system within its modeled environment. Unlike simulations, it provides mathematical guarantees about the system’s behavior by exhaustively analyzing the model. This makes it particularly effective for identifying and addressing rare but critical scenarios that simulations might miss. Our proposed approach leverages Markov Decision Processes (MDPs) to model the stochastic dynamics of AV lane-changing maneuvers. MDPs represent the probabilistic nature of real traffic and the AV behavior and provide detailed dynamics of the system. Then properties of interest are formally specified using Probabilistic Computation Tree Logic (PCTL), a powerful logic for expressing complex temporal and probabilistic IX properties. Using the probabilistic model checker PRISM, we formally verified critical properties of the MOBIL (Minimizing Overall Braking Induced by Lane Changes) model, a widely adopted framework for AV lane change. We specifically investigated the safety and lane change efficiency, temporal performance, and system robustness under dynamic traffic conditions. We demonstrate with this work that probabilistic model checking not only surpasses the simulation limitations but also gives a complete and rigorous safety and reliability assurance framework for AV lane-changing algorithms. By formalizing and verifying these critical properties, this work establishes a foundation for developing more dependable and efficient AV systems that can robustly navigate the complexities and uncertainties of real-world traffic conditions.