Improved Bounded Model Checking for the Universal Fragment of CTL-中国期刊网

摘要 SAT-basedboundedmodelchecking(BMC)hasbeenintroducedasacomplementarytechniquetoBDD-basedsymbolicmodelcheckinginrecentyears,andalotofsuccessfulworkhasbeendoneinthisdirection.TheapproachwasfirstintroducedbyA.Biereetal.incheckinglineartemporallogic(LTL)formulaeandthenalsoadaptedtocheckformulaeoftheuniversalfragmentofcomputationtreelogic(ACTL)byW.Penczeketal.Astheefficiencyofmodelcheckingisstillanimportantissue,wepresentanimprovedBMCapproachforACTLbasedonPenczek'smethod.Weconsidertwoaspectsoftheapproach.Oneisreductionofthenumberofvariablesandtransitionsinthek-modelbydistinguishingthetemporaloperatorEXfromtheothers.Theotherissimplificationofthetransformationofformulaebyusinguniformpathencodinginsteadofadisjunctionofallpathsneededinthek-model.Withtheseimprovements,foranACTLformula,thelengthofthefinalencodingoftheformulaintheworstcaseisreduced.TheimprovedapproachisimplementedinthetoolBMVandiscomparedwiththeoriginalonebyapplyingbothtotwowellknownexamples,mutualexclusionanddiningphilosophers.Thecomparisonshowstheadvantagesoftheimprovedapproachwithrespecttotheefficiencyofmodelchecking.

1Samira El Bahi;Mohamed El Wartitil;Mohamed Yassin. Application of revised universal loss equation model.地球化学,2006-03.
2XIAO Jian-yu. Combination of Model Checking and Theorem Proving to Verify Embedded Software.通信与信息系统,2005-04.
3赵建华;李宣东;郑滔;郑国梁. Remove Irrelevant Atomic Formulas for Timed Automaton Model Checking.计算机科学与技术,2006-01.
4CHENJIXIU];WEIHANBAI. SOME GEOMETRIC PROPERTIES ON A MODEL OF UNIVERSAL TEICHMULLER SPACES.基础数学,1997-03.
5Jiang Jijiao. The Ecological Economic Model Based on Bounded Rational Agents.政治经济学,2005-04.
6Xianghua Wang;Xinyu Yang;Zheng Qin;Huijie Yang. Hierarchical interacting multiple model algorithm based on improved current model.物理电子学,2010-06.
7. An Improved Quality Function Deployment (QFD) Model.计算机应用技术,1999-01.
8LI Ke-Ping MAO Bo-Hua GAO Zi-You. An Improved Walk Model for Train Movement on Railway Network.物理,2009-06.
9FENGYucai YIBaolin. An Improved Direction Relation Detection Model for Spatial Objects.测绘科学与技术,2004-04.
10Maolin CHENG;Yun HAN. Parameter Estimation of a Mixed Production Function Model Based on Improved Firefly Algorithm and Model Application.系统科学,2018-04.

Improved Bounded Model Checking for the Universal Fragment of CTL

来源期刊

相关推荐

同分类资源更多

相关关键词

Improved Bounded Model Checking for the Universal Fragment of CTL

来源期刊

相关推荐

同分类资源 更多

相关关键词

同分类资源更多