形式验证中ROBDD变量排序算法的研究

Abstract

Abstract: The ill order of ROBDD variables may cause the crisis of state space explosion and, therefore, influence the use of the formal verification method.In this paper, we present an improved algoribhm by adding mutation and optimized evolution operations to the genetic ROBDD variables reordering algorithm in the CUDD package.The experimental results demonstrate that the proposed algorithm can reduce the number of ROBDD nodes within a tolerable time, and slow down the crisis of state space explosion in the formal verification.

Key words: font-family:Calibri, sans-serif, ">color:windowtext, ROBDD')">">ROBDD, variables reordering, genetic algorithm, ')">">

CLC Number:

V446

WANG Qing, YANG Mengfei.

Research on ROBDD Variables Reordering Algorithm in Formal Verification [J].Aerospace Contrd and Application, 2008, 34(2): 29-32.

0
/ / Recommend ROBDD; variables reordering; genetic algorithm;”. Please open it by linking:http://journal01.magtech.org.cn/Jwk3_kjkzjs/EN/abstract/abstract9393.shtml" name="neirong"> ROBDD; variables reordering; genetic algorithm;">

Add to citation manager EndNote|Reference Manager|ProCite|BibTeX|RefWorks

URL: http://journal01.magtech.org.cn/Jwk3_kjkzjs/EN/

http://journal01.magtech.org.cn/Jwk3_kjkzjs/EN/Y2008/V34/I2/29

[1]	DENG Ya, WANG Ze-Guo, ZHANG Jin-Jiang. A Method on Obstacle Avoidance Planning for Variable Geometry Truss [J]. , 2017, 43(5): 37-42.
[2]	ZHANG Jun-Jie, YAO Shi-Dong, PENG Bo, ZHANG Qing-Li. Path Optimization for the Deployment of NonCoplanar Configuration Solar Arrays [J]. , 2016, 42(1): 20-24.
[3]	YU Kai, XU Ming, JIA Ying-Hong, XU Shi-Jie. Design for OrbitTransfer Based on Ion Propulsion [J]. , 2013, 39(5): 39-42.
[4]	QIAN Hang, ZHENG Jian-Hua. Optimization Algorithm for Interplanetary Transfer Trajectories of SolarSail Spacecraft [J]. , 2012, 38(1): 18-22.
[5]	HU Qi, CHEN Jian, LI Yong. Numerical Simulation for Reorientation of Propellant in a Vane Tank under Microgravity [J]. Aerospace Contrd and Application, 2009, 35(6): 54-57.
[6]	ZHANG Jinfeng, SUN Chengqi, CAI Wei. Monocular Vision-Based Relative Position and Attitude Measurement Algorithm for Non-Cooperative Spacecrafts [J]. Aerospace Contrd and Application, 2009, 35(6): 50-53.
[7]	CHEN Changqing, XIE Yonghcun. Quadratic-Based Computation of Four-Impulse Optimal Rendezvous between Near Circular Orbits [J]. Aerospace Contrd and Application, 2009, 35(6): 45-49.
[8]	XU Jingyu, GAO Yijun. Sun Sensor-Based Orbit Position Estimating Method for GEO Satellites [J]. Aerospace Contrd and Application, 2009, 35(6): 41-44.
[9]	SHEN BenjianLIU HaiboJIA HuiYANG JIankun. CCD Chip’s Temperature Effect on Position Accuracy of Star Sensor [J]. Aerospace Contrd and Application, 2009, 35(6): 36-40.
[10]	LI Gming, YAO Yu. Design of Space Rendezvous and Docking Transverse Linear Movement Simulator Control System Based on H∞ Theory [J]. Aerospace Contrd and Application, 2009, 35(6): 30-35.
[11]	LIANG Dong, , WANG Pengji, , LIU Liangdong . A LIDAR-Based Autonomous Landing Site Selection Method for Pinpoint Lunar Soft Landing [J]. Aerospace Contrd and Application, 2009, 35(6): 24-29.
[12]	GONG Dezhu, WU Yanpeng, LU Xin. An Attempt at Improving Dynamic Performance of Star Tracker by Motion Compensation [J]. Aerospace Contrd and Application, 2009, 35(6): 19-23.
[13]	YUAN Li, CHENG Ming . Deep Space Exploration Mission-Oriented Flight Control Simulation and Support System#br# [J]. Aerospace Contrd and Application, 2009, 35(6): 13-18.
[14]	LI Guo. A Survey of GNC Critical Techniques for Development of China Spacecrafts in the Future [J]. Aerospace Contrd and Application, 2009, 35(6): 1-5.
[15]	YANG Mengfei JIA Yang CHEN Jianxin. Research on System Design of Lunar Rover [J]. Aerospace Contrd and Application, 2008, 34(3): 3-6.

Research on ROBDD Variables Reordering Algorithm in Formal Verification

PDF (PC)

Like

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Metrics

Comments

Recommended 0