资源描述：
《t. simple bounded ltl model checking》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、SimpleBoundedLTLModelCheckingTimoLatvala1,,ArminBiere2,KeijoHeljanko1,,andTommiJunttila3,1LaboratoryforTheoreticalComputerScienceHelsinkiUniversityofTechnologyP.O.Box5400,FI-02015HUT,Finland{Timo.Latvala,Keijo.Heljanko}@hut.fi2ETHZ¨urich,ComputerSystemsInstituteCH-8092Z¨urich,Switzerlandbie
2、re@inf.ethz.ch3ITC-IRSTViaSommarive18,38050Povo,Trento,Italyjunttila@irst.itc.itAbstract.Wepresentanewandverysimpletranslationoftheboundedmodelcheckingproblemwhichislinearbothinthesizeoftheformulaandthelengthofthebound.TheresultingCNF-formulahasalinearnumberofvariablesandclauses.Keywords:boundedm
3、odelchecking,LTL,lineartranslation,NuSMV.1IntroductionBoundedmodelchecking[1](BMC)isatechniqueforfindingbugsinfinitestatesys-temdesignsviolatingpropertiesspecifiedinlineartemporallogic(LTL).Themethodworksbymappingaboundedmodelcheckingproblemtothesatisfiabilityproblem(SAT).Givenapropositionalformulaen
4、codingaKripkestructureMrepresentingthesystem,anLTLformulaψandaboundk,apropositionalformula
5、[M,ψ,k]
6、iscreatedthatissatisfiableifandonlyiftheKripkestructureMcontainsacounterexampletoψoflengthk.BMChasestablisheditselfasacomplementarymethodtosymbolicmodelcheckingmethodsbasedon(ordered)binarydecisiondi
7、agrams(BDDs).ThebiggestadvantageofBMCcomparedtoBDDsisitsspaceefficiency;therearesomeBooleanfunctionswhichcannotbesuccinctlyencodedasaBDD.BMCalsoproducescounterexamplesofminimallength,whicheasestheirinterpretationandunderstandingfordebuggingpurposes.However,predictingthecaseswhereBMCismoreefficientc
8、omparedtoWorksupportedbytheHelsinkiGraduateSchoolinComputerScience,theAcademyofFinland(project53695),andtheNokiaFoundation.WorkpartiallysupportedbyFETprojectADVANCEcontractNoIST-1999-29082,EPSRCgrant93346/01(AnAutomataTheoreticApproachtoSoftwareModelChecking),andtheAcademyofFinland(project5369
9、5andgrantforresearchworkabroad).ThisworkhasbeensponsoredbytheCALCULEMUS!IHP-RTNECproject,contractcodeHPRN-CT-2000-00102,andhasthusbenefitedofthefinancialcontributionoftheCommis-sionthroughtheIHPprogramme.A.J.HuandA.K.
