A Personalized Lane-Change Safety Verification Framework Based on Driving Style and Formal Modeling

Ensuring the safety of lane-change maneuvers remains a critical challenge in autonomous driving, especially given the variability in individual driving behaviors. However, most existing decision-making models fail to account for driver heterogeneity, resulting in overly generalized and potentially unsafe strategies. In this paper, we propose a personalized lane-change risk verification framework that integrates unsupervised driving style classification with formal stochastic modeling. We first propose a volatility-based feature extraction method and employ k-means++ clustering to identify three representative driving styles - aggressive, normal, and conservative - from naturalistic trajectory data. We then construct a modular Network of Stochastic Timed Automata (NSTA) to represent individualized driving dynamics and enforce TTC-based safety constraints, enabling probabilistic safety verification. Finally, we propose a data-driven runtime verification pipeline, which evaluates the lane-change safety of individual maneuvers using real-world inputs. Experiments on 205 lane-change cases from the highD dataset demonstrate the framework's ability to quantify safety probabilities across different driving styles. Results show that aggressive behaviors significantly increase the risk of unsafe lane changes, underscoring the importance of behavior-aware modeling. This work provides a structured and interpretable alternative to black-box risk models for autonomous vehicle decision-making.