CEGAR-Driven Training and Verification Method for Safe Autonomous Driving Decision Models
-
摘要: 深度强化学习(DRL)融合深度学习的高维感知能力和强化学习的决策制定优势，在自动驾驶决策模型的开发中展现出显著潜力，然而作为安全攸关系统，自动驾驶决策模型在实际部署前需通过形式化验证以确保其安全性。为此，本文提出了一种基于反例引导抽象精化(CEGAR)的安全自动驾驶决策模型训练与验证方法，通过迭代优化和验证过程提升模型可靠性。首先，利用双深度Q网络(DDQN)算法训练决策模型，以学习高效的驾驶策略；随后，将基于深度强化学习的黑盒决策模型通过轨迹生成抽象为Kripke结构，并以预定义的安全属性为规约进行形式化验证。若验证失败，则通过反例引导抽象精化方法精化抽象域以消除虚假反例并重新验证；若检测到真实反例，则返回重新训练模型，迭代此过程直至所有属性通过验证，从而确保决策模型满足严格的安全性要求。为支持该方法的实施，本文基于CARLA仿真平台构建了符合OpenAI Gym接口的强化学习环境CarlaEnv，为模型的训练、验证和测试提供了多样化场景支持。相较于传统深度强化学习训练方法，该方法在保持决策性能的同时，通过形式化验证显著提升了模型可靠性，为安全攸关自动驾驶系统的开发提供了有效解决方案。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. -
表 1 本文工作与Trainify框架的不同
Trainify框架[25] 本文工作 研究对象 白盒系统 白盒系统、黑盒系统 验证机制 不区分真实和虚假反例 区分真实和虚假反例 应用场景 山地车、钟摆等六类
简单仿真模型真实自动驾驶需求 
下载: 导出CSV
1 DDQN筆法
1. for epirode=1 to M do 2. s0=Env.react() // 重算环境并樾彻始化状素s0 3. for t=0 to T do 4. 根据$\epsilon $贪婪策略在状态st出选择动作at，得到rt和st+1；//以$\epsilon $的概率随机选动作，否则选Q值最大的动作 5. 将transition=(s, a, r, s')存入经验回放区D；//将当前经验(st, at, rt, st+1)存入经验池D 6. 从D中随机均匀采样m个样本(s, a, r, s')，计算TD target；//从经验池中采样小批量样本，用于训练 7. ${y_{t}} = \left\{ \begin{aligned}& r_t, 当s_{t+1}为终止状态\\& r_t+ \gamma Q(s_{t+1}, {\mathrm{argmax}}_a Q(s_{t+1,a;},\theta);\theta') ,当s_{t+1}为非终止状态\end{aligned} \right. $//计算TD目标值：终止状态时目标值为rt，非终止状态时使用
DDQN双网络计算8. $\delta = |Q({s_t},{a_{t}};\theta ) - ({r_t} + \gamma Q(s{}_{t + 1},{{\mathrm{argmax}}_a}Q({s_{t + 1}},a;\theta );\theta ')) $//计算TD误差(预测值与目教值求的绝对值) 9. $Loss= \left\{ \begin{array}{ll}\frac{1}{2}{\delta ^2}\qquad for\\|\delta | - \frac{1}{2}\end{array} \right\}$//使用Huber损失(平滑L1损失)计算损失函数 10. 执行样度下降法，反向传摆里新怙计因结数$\theta=\theta+\alpha \cdot \Delta_\theta $//使用梯度下降更新估计网络参数$\theta $，$\alpha $为学习率 11. 每隔C步更新目标网络$\theta '=\theta $；//每隔C步将估计网络参数复制到目标网络 12. $s_{1}\leftarrow s_{t+1} $ //更所当前状态为下一状态，继续下一步 13. end 14. end 15. return $\theta $ // 返回训练好的估计网络参数$\theta $
下载: 导出CSV
表 2 行驶决策模型状态空间
状态空间
变量参数说明 参数范围 $ v $ 车辆当前的速度标量，单位 $ m/s $(米/秒) [0,20) $ d $ 车辆到车道中心线的横向距离，单位 $ m $(米) (–2,2) $ \theta $ 行驶方向与车道切线方向夹角，单位 °(度) (–60,60) $ {c}_{\text{rate}} $ 车辆到目的地的轨迹完成率，单位 $ \% $(百分号) (0,100)
下载: 导出CSV
表 4 行驶决策模型动作空间
动作 油门 转向 刹车 动作说明 a0 0.0 0.0 0.6 刹车 a1 0.5 0.0 0.0 直行 a2 0.5 -0.05 0.0 直行左微调 a3 0.5 0.05 0.0 直行右微调 a4 0.3 -0.3 0.0 小角度左转 a5 0.3 -0.5 0.0 大角度左转 a6 0.3 0.3 0.0 小角度右转 a7 0.2 0.7 0.0 大角度右转
下载: 导出CSV
表 3 制动决策模型状态空间
状态空间变量 参数说明 参数范围 $ v $ 车辆当前的速度标量，单位$ m/s $(米/秒) [0,20) $d_{obs}$ 自车到前方障碍的距离，单位$ m $(米) (0,50)
下载: 导出CSV
2 构建抽象Kripke结构算法
输入：强化学习环境Env，决策模型${\mathbb{N}} $，具体状态空间S，抽象粒度$\delta $，标签函数Label()，ACTL公式$\Phi $，消除环路函数eliminate_cycles() 输出：抽象Kripke结构$\hat K $ 1. 初始化：转换关系存储列表edges、抽象状态存储集合abs_states、标签存储字典label_dict 2. $\hat S\leftarrow discretize(S, \delta) $//通过抽象粒度$\delta $来离散具体状态空间S，得到抽象域$\hat S $ 3. ${\mathbb{A}} \leftarrow {\mathrm{g}}(\hat S)$//基于抽象域$\hat S $获得抽象转换器${\mathbb{A}} $ 4. for episode =1 to M do 5. s0=Env.reset()//重置环境并获得初始化状态s0 6. $\hat s_0 \leftarrow {\mathbb{A}}(s_0)$//抽象域映射，获得抽象状态$\hat s_0 $ 7. abs_states.add($\hat s_0 $)//记录抽象状态 8. label_dict[$\hat s_0 $]$\leftarrow $Label($\hat s_0,\Phi $)//根据属性规约$\Phi $使用标签函数标记抽象状态$\hat s_0 $ 9. fot t=0 to T do 10. at$\leftarrow {\mathbb{N}}$(st)//基于模型${\mathbb{N}} $和状态st悬着动作at 11. st+1, rt$\leftarrow $ Env.step(at)//执行动作at，获得奖励rt与下一状态st+1 12. $\hat{s_{t+1}}\leftarrow {\mathbb{A}}(s_{t+1}) $//抽象域映射，获得新的抽象状态$\hat{s_{t+1}} $ 13. abs_states.add($\hat {s_{t+1}} $)//记录抽象状态 14. label_dict[$\hat {s_{t+1}} \leftarrow Label(\hat {s_{t+1}}, \Phi)$]//使用标签函数标记抽象状态$\hat {s_{t+1}} $ 15. edges.append ($\hat s_t, \hat{s_{t+1}} $)//记录迁移关系($\hat s_t,\hat{s_{t+1}} $) 16. $s_t \leftarrow s_{t+1} $//更新具体状态 17. $\hat s \leftarrow \hat {s_{t+1}} $//更新抽象状态 18. end 19. end 20. eliminate_cycles(abs_states, edges)//消除状态转移关系edges中的环路 21. $\hat K \leftarrow $Kripke (S=abs_states, R=edges, L=label_dict)//使用迁移关系edges和标签字典label_dict构建Kripke结构 22. return $\hat K $//返回最终的抽象Kripke结构
下载: 导出CSV
表 5 ACTL公式定义决策模型安全性与活性
模型 属性 类型 解释 行驶决策模型 $\varPhi=AG(|d|<0.5 \wedge|\theta|<30) $ 安全性 车辆行驶过程中始终保持在安全区域 $\varPhi_2=AF(c_{rate}>99.9{\text{%}}) $ 活性 车辆到达目的地 制动决策模型 $\varPhi_3=AG(d_{obs}>2) $ 安全性 智能体车辆始终与前车保持2 m以上的距离 $\varPhi_4=AF(2<d_{obs}<10\wedge v=0) $ 活性 智能体车辆最终能在距离前车安全范围内制动
下载: 导出CSV
表 6 反例引导抽象精化方法验证决策模型结果
模型 属性 基于属性抽象的状态空间 初始抽象粒度 初始状态数 精化后状态数 验证结果 行驶决策模型 $ {\Phi}_{1} $ $ [[-2,-45{,}0]， $$ [2{,}45{,}100]] $ $ [1,22.5{,}25] $ 64 701 满足 $ {\Phi}_{2} $ 225 满足 制动决策模型 $ {\Phi}_{3} $ $ [[0{,}0],[20{,}50]] $ $ [5,12.5] $ 16 56 满足 $ {\Phi}_{4} $ 22 满足
下载: 导出CSV
-
[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. -
下载:
图(16) / 表(8)
计量
- 文章访问数: 18
- HTML全文浏览量: 1
- PDF下载量: 1
- 被引次数: 0
