CEGAR-Driven Training and Verification Method for Safe Autonomous Driving Decision Models

CHENG Zhuo; WANG Xiao; ZENG Xianghui; LU Jiaxing; ZUO Zhengkang; WANG Changjing

doi:10.11999/JEIT260109

Article Contents

Article Navigation > Journal of Electronics & Information Technology > 2026 >

CHENG Zhuo, WANG Xiao, ZENG Xianghui, LU Jiaxing, ZUO Zhengkang, WANG Changjing. CEGAR-Driven Training and Verification Method for Safe Autonomous Driving Decision Models[J]. Journal of Electronics & Information Technology. doi: 10.11999/JEIT260109

Citation:

CHENG Zhuo, WANG Xiao, ZENG Xianghui, LU Jiaxing, ZUO Zhengkang, WANG Changjing. CEGAR-Driven Training and Verification Method for Safe Autonomous Driving Decision Models[J]. Journal of Electronics & Information Technology. doi: 10.11999/JEIT260109

Citation:

CHENG Zhuo, WANG Xiao, ZENG Xianghui, LU Jiaxing, ZUO Zhengkang, WANG Changjing. CEGAR-Driven Training and Verification Method for Safe Autonomous Driving Decision Models[J]. Journal of Electronics & Information Technology. doi: 10.11999/JEIT260109

PDF( 8247 KB)

CEGAR-Driven Training and Verification Method for Safe Autonomous Driving Decision Models

doi: 10.11999/JEIT260109 cstr: 32379.14.JEIT260109

CHENG Zhuo^{1, 2
,},
WANG Xiao^{1, 2},
ZENG Xianghui²,
LU Jiaxing²,
ZUO Zhengkang^{1, 2, 3, 4},
WANG Changjing^{1, 2, 3, 4
,
,}

1.
Jiangxi Provincial Key Laboratory for High Performance Computing (Jiangxi Normal University), Nanchang 330022, China
2.
School of Artificial Intelligence, Jiangxi Normal University, Nanchang 330022, China
3.
National-level International S & T Cooperation Base of Networked Supporting Software (Jiangxi Normal University), Nanchang 330022, China
4.
Language Intelligence Research Center (Jiangxi Normal University), Nanchang 330022, China

Funds: The National Natural Science Foundation of China (62102171, 62462037, 62462036), Jiangxi Provincial Training Program for Academic and Technical Leaders of Major Disciplines (20232BCJ22013), The Key Project of Natural Science Foundation of Jiangxi Province (20242BAB26017)

Accepted Date: 2026-09-28
Rev Recd Date: 2026-09-28

Available Online: 2026-10-20

Abstract

Abstract

Objective Deep Reinforcement Learning (DRL) uniquely integrates the high-dimensional perception capabilities of deep learning with the autonomous decision-making optimization of reinforcement learning, demonstrating substantial promise for developing autonomous driving decision-making systems. Nevertheless, as a safety-critical system, autonomous driving mandates rigorous verifiability of its decision models prior to real-world deployment. Current DRL-based autonomous driving faces two principal challenges: first, the black-box nature of neural networks results in a lack of interpretability in the decision-making process; second, the continuous and infinite state space presents a state explosion problem for conventional formal verification methods. These challenges complicate ensuring the safety of DRL models in complex and dynamic traffic environments, thereby limiting their reliable application in practical scenarios. Prior approaches often decouple training from verification, or are tailored to white-box systems, inadequately addressing the verification demands of black-box continuous dynamical systems. To address these shortcomings, this paper aims to propose an innovative Counterexample-Guided Abstraction Refinement (CEGAR)-driven framework that achieves profound integration of training and formal verification for autonomous driving decision models. By establishing a mapping mechanism from black-box continuous systems to finite-state abstract models, coupled with an iterative refinement and retraining strategy, this framework aims to yield an autonomous driving system that possesses both intelligent decision-making capabilities and formal safety guarantees, thereby enhancing the trustworthiness of autonomous driving in complex urban settings. Methods This study adopts a systematic approach to develop and verify safe autonomous driving decision models. First, a reinforcement learning environment named CarlaEnv, compliant with the OpenAI Gym interface, was constructed based on the CARLA simulation platform, providing support for model training and testing with diverse urban scenarios. In terms of model architecture, a dual-module structure comprising driving decision and braking decision modules was designed using the Double Deep Q-Network (DDQN) algorithm. For the path-following task, a four-dimensional state space (velocity, lateral offset, relative yaw angle, trajectory completion rate) and an eight-dimensional discrete action space were meticulously designed, along with a multi-objective composite reward function. Guiding the agent to learn safe and efficient driving strategies.To address the challenge of formal verification for black-box systems, a trajectory generation-based abstraction modeling method is proposed: by collecting the interaction trajectories of the DRL agent in the simulation environment, the continuous state space is discretized using an interval abstraction domain. An efficient mapping from concrete states to abstract states is established via an R-tree data structure, ultimately constructing a formally verifiable Kripke structure. During the verification phase, ACTL temporal logic is employed to define safety and liveness properties, ensuring the eventual completion of tasks. The core innovation of the CEGAR mechanism lies in the authenticity assessment and classification of counterexamples: when a property violation is detected during model checking, an algorithm analyzes the realizability of the abstract counterexample in the concrete domain—if concrete states violating the atomic propositions exist, it is identified as a genuine counterexample, and its corresponding failure trajectories are added to the experience replay buffer to guide targeted model retraining. If the counterexample is spurious, a dimension-selective refinement strategy is adopted, subdividing only the state dimensions involved in the verified property through interval partitioning to avoid state space explosion. This closed-loop iteration of training-verification-refinement continues until all predefined properties are successfully verified. Results and Discussions Experiments conducted on the Town02 map of the CARLA simulation platform demonstrate that after 300 training episodes, the cumulative reward per episode of the driving decision model steadily increased from initially negative values to a positive range. Among the 300 episodes, 274 episodes achieved high cumulative rewards, with the average reward converging after approximately 150 episodes. The trajectory completion rate reached the 90-100% range in 269 out of 300 episodes (Fig. 8), confirming that the model has learned effective driving strategies. For the braking decision model, both episode rewards and average rewards in the reward curve gradually increased and stabilized after around 30 episodes (Fig. 9). In the successful braking curve, as training progressed, the model learned to effectively brake and maintain a safe distance within a range of 2 to 10 meters from the preceding vehicle. Formal verification results indicate that the driving decision model simultaneously satisfies both safety and liveness properties. Through the counterexample-guided refinement process, the number of abstract states required for verifying the safety property was refined from an initial 64 to 701, while the number required for the liveness property was refined to 225 (Table 6), effectively eliminating spurious counterexamples. During the CEGAR iteration process, the verification time overhead grows linearly with the state space size (Fig. 10), demonstrating the scalability of the proposed method. Horizontal performance comparison with two baseline methods, DQN and DDPG, shows that the proposed method outperforms the compared methods in terms of task completion rate (approximately 95%), mean lateral offset (approximately 0.4 m), and collision rate (remaining at 0% after 65 episodes) (Fig. 13). Reliability analysis indicates that under two complex scenarios (rainy weather and nighttime driving), the proposed method achieves mean cumulative episode rewards that are 4.6 to 10.8 points higher than those of DDQN, DQN, and DDPG, corresponding to improvements of 4.9% to 12.4% (Fig. 14). Ablation experiments compare three groups: Group A (no verification), Group B (single-shot verification), and Group C (full CEGAR method). The results show that Group C achieves the best performance across all three metrics: collision rate (3.1%), task completion rate (94.8%), and mean lateral offset (0.214 m) (Fig. 15). Complex scenario testing further validates the robustness of the proposed method under rainy weather and nighttime driving (Fig. 16), with a standard deviation of cumulative episode rewards of only 17.75 points. In summary, compared to traditional deep reinforcement learning methods, the proposed approach maintains decision-making performance while significantly enhancing model reliability and safety through the counterexample-guided refinement and retraining mechanism. Conclusions This paper proposes a comprehensive and integrated CEGAR-driven training and verification framework for autonomous driving decision models. The framework successfully bridges the gap between data-driven, learning-based autonomous systems and rigorous, mathematically grounded safety verification. By innovatively integrating trajectory-based abstraction methods for black-box systems, an efficient R-tree mapping structure, ACTL-based property specification, and an advanced CEGAR architecture equipped with counterexample authenticity assessment and dimension-selective refinement mechanisms, this approach constructs decision models that combine high performance with formal verification guarantees. Experimental results in a realistic simulation environment demonstrate that the framework effectively learns driving policies, achieves formal verification of key safety and liveness properties, and enhances the overall reliability of the model compared to traditional methods.

FullText(HTML)

References(35)

References

[1]	王晓娟. 城市环境下的深度强化学习车道保持决策方法研究[D]. [硕士论文], 西安理工大学, 2024. doi: 10.27398/d.cnki.gxalu.2024.000507. WANG Xiaojuan. Research on decision-making method of lane keeping with deep reinforcement learning in urban environments[D]. [Master dissertation], Xi'an University of Technology, 2024. doi: 10.27398/d.cnki.gxalu.2024.000507.
[2]	CHEN Shanzhi, HU Xinghua, ZHAO Jiahao, et al. A review of decision-making and planning for autonomous vehicles in intersection environments[J]. World Electric Vehicle Journal, 2024, 15(3): 99. doi: 10.3390/wevj15030099.
[3]	唐伦, 戴军, 成章超, 等. 基于数字孪生的多自动驾驶车辆分布式协同路径规划算法[J]. 电子与信息学报, 2024, 46(6): 2525–2532. doi: 10.11999/JEIT230678. TANG Lun, DAI Jun, CHENG Zhangchao, et al. Distributed collaborative path planning algorithm for multiple autonomous vehicles based on digital twin[J]. Journal of Electronics & Information Technology, 2024, 46(6): 2525–2532. doi: 10.11999/JEIT230678.
[4]	ZHAO Rui, LI Yun, FAN Yuze, et al. A survey on recent advancements in autonomous driving using deep reinforcement learning: Applications, challenges, and solutions[J]. IEEE Transactions on Intelligent Transportation Systems, 2024, 25(12): 19365–19398. doi: 10.1109/TITS.2024.3452480.
[5]	SHI Jiamin, ZHANG Tangyike, ZONG Ziqi, et al. Task-driven autonomous driving: Balanced strategies integrating curriculum reinforcement learning and residual policy[J]. IEEE Robotics and Automation Letters, 2024, 9(11): 9454–9461. doi: 10.1109/LRA.2024.3448237.
[6]	李国权, 程涛, 郭永存, 等. 基于深度强化学习的IRS辅助认知无线电系统波束成形算法[J]. 电子与信息学报, 2025, 47(3): 657–665. doi: 10.11999/JEIT240447. LI Guoquan, CHENG Tao, GUO Yongcun, et al. Deep reinforcement learning based beamforming algorithm for IRS assisted cognitive radio system[J]. Journal of Electronics & Information Technology, 2025, 47(3): 657–665. doi: 10.11999/JEIT240447.
[7]	TIAN Zhen, LIN Zhihao, ZHAO Dezong, et al. Evaluating scenario-based decision-making for interactive autonomous driving using rational criteria: A survey[J]. IEEE Transactions on Intelligent Transportation Systems, 2026, 27(2): 1709–1730. doi: 10.1109/TITS.2025.3636070.
[8]	刘伟权, 郑世均, 郭宇, 等. 三维点云目标识别对抗攻击研究综述[J]. 电子与信息学报, 2024, 46(5): 1645–1657. doi: 10.11999/JEIT231188. LIU Weiquan, ZHENG Shijun, GUO Yu, et al. A survey of adversarial attacks on 3D point cloud object recognition[J]. Journal of Electronics & Information Technology, 2024, 46(5): 1645–1657. doi: 10.11999/JEIT231188.
[9]	CHILAKAMARRI V K, FENG Zeyuan, and BANSAL S. Reachability analysis for black-box dynamical systems[C]. 2025 IEEE International Conference on Robotics and Automation (ICRA), Atlanta, USA, 2025: 3552–3558. doi: 10.1109/ICRA55743.2025.11127528.
[10]	KHAN N, ABDALLAH A, CELIK A, et al. Explainable AI-aided feature selection and model reduction for DRL-based V2X resource allocation[J]. IEEE Transactions on Communications, 2025, 73(9): 7633–7649. doi: 10.1109/TCOMM.2025.3554655.
[11]	MORGADO Â M R and POMBO N G C C. CARLA-GymDrive: Autonomous driving episode generation for the Carla simulator in a gym environment[J]. SoftwareX, 2024, 28: 101955. doi: 10.1016/j.softx.2024.101955.
[12]	ALIZADEH A, MOGHADAM M, BICER Y, et al. Automated lane change decision making using deep reinforcement learning in dynamic and uncertain highway environment[C]. 2019 IEEE Intelligent Transportation Systems Conference (ITSC), Auckland, New Zealand, 2019: 1399–1404. doi: 10.1109/ITSC.2019.8917192.
[13]	PALANISAMY P. Multi-agent connected autonomous driving using deep reinforcement learning[C]. 2020 International Joint Conference on Neural Networks (IJCNN), Glasgow, UK, 2020: 1–7. doi: 10.1109/IJCNN48605.2020.9207663.
[14]	KIRAN B R, SOBH I, TALPAERT V, et al. Deep reinforcement learning for autonomous driving: A survey[J]. IEEE Transactions on Intelligent Transportation Systems, 2022, 23(6): 4909–4926. doi: 10.1109/TITS.2021.3054625.
[15]	CHI Huicong, WANG Ping, WANG Chao, et al. Deep reinforcement learning with intervention module for autonomous driving[C]. 2022 IEEE 96th Vehicular Technology Conference (VTC2022-Fall), London, UK, 2022: 1–6. doi: 10.1109/VTC2022-Fall57202.2022.10012793.
[16]	ZHANG Mei, CHEN Kai, and ZHU Jinhui. An efficient planning method based on deep reinforcement learning with hybrid actions for autonomous driving on highway[J]. International Journal of Machine Learning and Cybernetics, 2023, 14(10): 3483–3499. doi: 10.1007/s13042-023-01845–2.
[17]	DU Danfeng, SHEN Mingyu, GUO Xiurong, et al. Hierarchical driving strategy for connected and autonomous vehicles making a protected left turn at signalized intersections[J]. Journal of Transportation Engineering, Part A: Systems, 2023, 149(3): 04022154. doi: 10.1061/JTEPBS.TEENG-7243.
[18]	BACCI E and PARKER D. Probabilistic guarantees for safe deep reinforcement learning[C]. The 18th International Conference on Formal Modeling and Analysis of Timed Systems, Vienna, Austria, 2020: 231–248. doi: 10.1007/978-3-030-57628-8_14.
[19]	KAZAK Y, BARRETT C, KATZ G, et al. Verifying deep-RL-driven systems[C]. Proceedings of the 2019 Workshop on Network Meets AI & ML, Beijing, China, 2019: 83–89. doi: 10.1145/3341216.3342218.
[20]	KWIATKOWSKA M, NORMAN G, and PARKER D. PROBABILISTIC Model Checking: Advances and Applications[M]. Cham: Springer, 2017: 73–121. doi: 10.1007/978-3-319-57685-5_3.
[21]	BOUDARDARA F, BOUSSIF A, MEYER P J, et al. A review of abstraction methods toward verifying neural networks[J]. ACM Transactions on Embedded Computing Systems, 2024, 23(4): 58. doi: 10.1145/3617508.
[22]	VAN WESEL P and GOODLOE A E. Challenges in the verification of reinforcement learning algorithms[R]. NASA/TM-2017-2196282017-219628, 2017.
[23]	FULTON N and PLATZER A. Safe reinforcement learning via formal methods: Toward safe control through proof and learning[C]. Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence and Thirtieth Innovative Applications of Artificial Intelligence Conference and Eighth AAAI Symposium on Educational Advances in Artificial Intelligence, New Orleans, USA, 2018: 6485–6492794.
[24]	WANG Yixuan, HUANG Chao, WANG Zhaoran, et al. Design-while-verify: Correct-by-construction control learning with verification in the loop[C]. Proceedings of the 59th ACM/IEEE Design Automation Conference, San Francisco, USA, 2022: 925–930. doi: 10.1145/3489517.3530556.
[25]	JIN Peng, TIAN Jiaxu, ZHI Dapeng, et al. TRAINIFY: A CEGAR-driven training and verification framework for safe deep reinforcement learning[C]. 34th International Conference Computer Aided Verification, Haifa, Israel, 2022: 193–218. doi: 10.1007/978-3-031-13185-1_10.
[26]	王戟, 詹乃军, 冯新宇, 等. 形式化方法概貌[J]. 软件学报, 2019, 30(1): 33–61. doi: 10.13328/j.cnki.jos.005652. WANG Ji, ZHAN Naijun, FENG Xinyu, et al. Overview of formal methods[J]. Journal of Software, 2019, 30(1): 33–61. doi: 10.13328/j.cnki.jos.005652.
[27]	魏普远, 何磊. 基于深度强化学习的自适应大邻域搜索算法在成像卫星调度问题中的应用[J]. 电子与信息学报, 2025, 47(12): 5005–5015. doi: 10.11999/JEIT251009. WEI Puyuan and HE Lei. A deep reinforcement learning enhanced adaptive large neighborhood search for imaging satellite scheduling[J]. Journal of Electronics & Information Technology, 2025, 47(12): 5005–5015. doi: 10.11999/JEIT251009.
[28]	CLARKE E M, HENZINGER T A, VEITH H, et al. Handbook of Model Checking[M]. Cham: Springer, 2018. doi: 10.1007/978-3-319-10575-8. (查阅网上资料,未找到本条文献页码信息,请确认).
[29]	ALUR R, HENZINGER T A, and KUPFERMAN O. Alternating-time temporal logic[J]. Journal of the ACM (JACM), 2002, 49(5): 672–713. doi: 10.1145/585265.585270.
[30]	KÖNIG B, RENSINK A, STOLTENOW L, et al. Counterexample-guided abstraction refinement for generalized graph transformation systems[C]. 18th International Conference Graph Transformation, Koblenz, Germany, 2025: 157–176. doi: 10.1007/978-3-031-94706-3_8.
[31]	CLARKE E M, GRUMBERG O, and LONG D E. Model checking and abstraction[J]. ACM Transactions on Programming Languages and Systems (TOPLAS), 1994, 16(5): 1512–1542. doi: 10.1145/186025.186051.
[32]	JACKSON D. Abstract model checking of infinite specifications[C]. Proceedings of the Second International Symposium of Formal Methods Europe on Industrial Benefit of Formal Methods, Barcelona, Spain, 1994: 519–531. doi: 10.1007/3-540-58555-9_113.
[33]	CLARKE E M, GRUMBERG O, JHA S, et al. Counterexample-guided abstraction refinement[C]. 12th International Conference Computer Aided Verification, Chicago, USA, 2000: 154–169. doi: 10.1007/10722167_15.
[34]	GUTTMAN A. R-trees: A dynamic index structure for spatial searching[C]. Proceedings of the 1984 ACM SIGMOD international conference on Management of data, Boston, USA, 1984: 47–57. doi: 10.1145/602259.602266.
[35]	LOISEAUX C, GRAF S, SIFAKIS J, et al. Property preserving abstractions for the verification of concurrent systems[J]. Formal Methods in System Design, 1995, 6(1): 11–44. doi: 10.1007/BF01384313.