Evaluation, optimization, verification of traffic rules for automated vehicles in freeway lane-changing scenario

The safe deployment of Automated Driving Systems (ADS) requires traffic rules to be translated from qualitative natural-language clauses into measurable and executable decision criteria. However, formalized traffic rules may still contain vague propositions and missing quantitative parameters. This study proposes a framework for evaluating, optimizing, and verifying traffic rules for ADS in freeway lane-changing scenarios. In the evaluation stage, Metric Temporal Logic (MTL) is used to formalize relevant traffic rules, and a scenario-level method is developed to identify vague propositions and missing key parameters. In the optimization stage, Shanghai Naturalistic Driving Study (SH-NDS) data are used to develop an executable interpretation through a three-stage lane-changing model comprising judgment, execution, and stabilization. In the judgment stage, Shapley Additive Explanations (SHAP) and weighted quantile regression are used to identify key factors and derive lane-change initiation thresholds. In the execution stage, a Support Vector Machine (SVM) model classifies real-time interaction risk. In the stabilization stage, a dual-dimensional risk-assessment model determines longitudinal control responses. Verification results show that the proposed interpretation increases the minimum Generalized Time-to-Collision (GTTC) at lane-change initiation by 1.24 s, achieves an overall risk-classification accuracy of 94% during execution, and reduces Time-Exposed Time-to-Collision (TET) during stabilization by 1.934 s, corresponding to a reduction of 39.2%. The proposed framework provides a systematic method for converting qualitative traffic rules into measurable and executable requirements for ADS.