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.
