LINEAR ENCODINGS OF BOUNDED LTL MODEL CHECKING

LogicalMethodsinComputerScienceVol.2(5:5)2006,pp.1–64fication,JohannesKeplerUniversity,Altenbergerstrasse69,A-4040Linz,Austriae-mailaddress:[e-mail],cLaboratoryforTheoreticalComputerScience,HelsinkiUniversityofTechnology,P.O.Box5400,FI-02015TKK,Finlande-mailaddress:{Keijo.Heljanko,Tommi.Junttila}@tkk.fidDepartmentofComputerScience,UniversityofIllinoisatUrbana-Champaign,201GoodwinAve.,Urbana,IL61801-2302,USAe-mailaddress:[e-mail]tute,ETHZentrum,CH-8092Z¨urich,Switzerlande-mailaddress:[e-mail]undedmodelchecking(BMC)forlineartempo-rallogic(LTL).Wepresentseveralefficientencodingsthathavesizelinearinthebound.Furthermore,weshowhowtheencodingscanbeextendedtoLTLwithpastoperators(PLTL).Thegeneralisedencodingisstilloflinearsize,butcannotdetectminimallengthcounterexamples.Byusingthevirtualunrollingtechniqueminimallengthcounterexam-plescanbecaptured,however,thesizeoftheencodingisquadraticinthespecification.WealsoextendvirtualunrollingtoB¨uchiautomata,enablingthemtoacceptminimallengthcounterexamples.OurBMCencodingscanbemadeincrementalinordertobenefitfromincrementalSATtechnology.Withfairlysmallmodificationstheincrementalencodingcanbefurtherenhancedwithaterminationcheck,allowingustoprovepropertieswithBMC.Ananalysisoftheliveness-to-safetytransformationrevealsmanysimilaritiestotheBMCencodingsinthispaper.Weconductexperimentstodeterminetheadvantageofem-ployingdedicatedBMCencodingsforPLTLovercombiningmoregeneralbutpotentiallylessefficientapproacheswithBMC:theliveness-to-safetytransformationwithinvariantcheckingandB¨uchiautomatawithfaircycledetection.ExperimentsclearlyshowthatournewencodingsimproveperformanceofBMCcon-siderably,particularlyinthecaseoftheincrementalencoding,andthattheyareverycompetitiveforfindingbugs.DedicatedencodingsseemtohaveanadvantageoverusingmoregeneralmethodswithBMC.Usingtheliveness-to-safetytranslationwithBDD-basedinvariantcheckingresultsinanefficientmethodtofindshortestcounterexamplesthatcom-plementstheBMC-basedapproach.ForprovingcomplexpropertiesBDD-basedmethodsstilltendtoperformbetter.2000ACMSubjectClassification:F.3.1,B.6.3,D.2.4,F.4.1.Keywordsandphrases:BoundedModelChecking–LTL–PLTL–LivenesstoSafety–NuSMV.LOGICALMETHODSlINCOMPUTERSCIENCEDOI:10.2168/LMCS-2(5:5)2006cA.Biere,K.Heljanko,T.Junttila,T.Latvala,andV.SchuppanCCCreativeCommons2A.BIERE,K.HELJANKO,T.JUNTTILA,T.LATVALA,ANDV.SCHUPPANIntroductionBoundedmodelchecking[BCCZ99]wasintroducedasanalternativetobinarydecisionsdiagrams(BDDs)toimplementsymbolicmodelchecking.Thispaperdescribessomeofthekeyresultsof[Lat05,Sch06]onboundedmodelchecking,andsomeextensions.Themainresultshavebeenpublishedin[LBHJ04,LBHJ05,HJL05,SB04,SB05].Thebasicideabehindboundedmodelchecking(BMC)istorestrictthegeneralmodelcheckingproblemtoaboundedproblem.InsteadofaskingwhetherthesystemMviolatesthepropertyψ,weaskwhetherthesystemMhasanycounterexampleoflengthktoψ.ThisboundedproblemisencodedintoSAT,thepropositionalsatisfiabilityproblem,inordertoobtainthebenefitsofsymbolicrepresentationsofstates.Inotherwords,aBooleanformula|[M,¬ψ,k]|isgeneratedwhichissatisfiableiffMhasacounterexampletoψoflengthk.ThesatisfiabilityofthisformulacanthenbecheckedwithaSATsolver.ThekeyinsightbehindBMCforlinear-timeformalismssuchaslineartemporallogic(LTL)isthatawitnessforLTLgivenasaninfiniteexecutionpathofthesystemcanbecapturedbyafinitepathintwoways:eitherthefinitepathrepresentsallitsinfiniteextensionsorthefinitepathloopsandinfactcapturesthebehaviourofaninfinitepath.Letπ=s0s1s2...beaninfinitepathofasystem.Wesaythatπisa(k,l)-loopifπ=(s0s1...sl−1)(sl...sk)ωsuchthat0l≤kandsl−1=sk.InBMCthetransitionrelationT(s,s′)ofasystemMisrepresentedsymbolicallyasaBooleanformula,wherethestatess,s′aremodelledasbitvectors.Tocapturethefinitepathsoflengthk,weunrollthetransitionrelationktimesandobtainthefollowingBooleanformula:|[M]|k⇔I(s0)∧k^i=1T(si−1,si).HereI(s)istheinitialstatepredicateandT(s,s′)atotaltransitionrelationpredicate.SinceonlycounterexamplestothegivenLTLformulaψshouldbeaccepted,additionalconstraintsmustbegeneratedtorestrictthemodelsoftheBooleanformula.Ifwedenotetheformulaconstraintsby|[¬ψ]|k,theBooleanformula|[M,¬ψ,k]|⇔|[M]|k∧|[¬ψ]|kissatisfiableiffMhasacounterexampleoflengthktoψ.ComparedwithusingBDDstoimplementsymbolicmodelchecking,BMChasafewadvantages.BMCcanleveragetheimpressivegainsthathavebeenachievedinSATsolvertechnologyinrecentyears[BS05].TheincreaseinefficiencyofthesolverscandirectlybetranslatedtomoreeffectiveBMC.TheuseofSATproceduresasapracticalimplementationtechniquetosearchforboundedlengthexecutionsofsystemshasalsobeenusedinthecontextofSAT-basedartificialintelligence(AI)planning[KS92,KS96]andinsequentialATPG[KL93].Inpractice,SATsolversseemtobeabletosolvecertainproblemsthatarenotfeasibleforBDDs.AnimportantadvantageofBMCisthatthecounterexamplesproducedbymostBMCencoding