Antichains Alternative Algorithms for LTL Satisfia

CentreFØdØrØenVØriationTehnialReportnumber2008.84Antihains:AlternativeAlgorithmsforLTLSatisabilityandModel-ChekingMartinDeWulf,LaurentDoyen,NiolasMaquet,Jean-FranoisRaskinhttp://www.ulb.a.be/di/ssd/fvThisworkwaspartiallysupportedbyaFRFCgrant:2.4530.02Antichains:AlternativeAlgorithmsforLTLSatisfiabilityandModel-Checking⋆M.DeWulf1,L.Doyen2,N.Maquet1⋆⋆andJ.-F.Raskin11CS,Universit´eLibredeBruxelles(ULB),Belgium2I&C,EcolePolytechniqueF´ed´eraledeLausanne(EPFL),SwitzerlandAbstract.Thelineartemporallogic(LTL)wasintroducedbyPnueliasalogictoexpresspropertiesoverthecomputationsofreactivesystems.Sincethissem-inalwork,therehavebeenalargenumberofpapersthathavestudieddeductivesystemsandalgorithmicmethodstoreasonaboutthecorrectnessofreactivepro-gramswithregardtoLTLproperties.Inthispaper,weproposenewefficientalgo-rithmsforLTLsatisfiabilityandmodel-checking.OuralgorithmsdonotconstructnondeterministicautomatafromLTLformulasbutworkdirectlywithalternatingautomatausingefficientexplorationtechniquesbasedonantichains.1IntroductionAmodelforanLTLformulaoverasetPofpropositionsisaninfinitewordwoverthealphabetΣ=2P.AnLTLformulaφdefinesasetofwords[[φ]]={w∈Σω|w|=φ}.ThesatisfiabilityproblemforLTLasks,givenanLTLformulaφ,if[[φ]]isempty.Themodel-checkingproblemforLTLasks,givenanomega-regularlanguageL(e.g.,thesetofallcomputationsofareactivesystem)andaLTLformulaφ,ifL⊆[[φ]].ThelinkbetweenLTLandomega-regularlanguagesisattheheartoftheautomata-theoreticapproachtoLTL[23].GivenaLTLformulaφ,wecanconstructanonde-terministicB¨uchiautomaton(NBW)Aφwhoselanguage,notedLb(Aφ),correspondsexactlytothemodelsofφ,i.e.,Lb(Aφ)=[[φ]].Thisreducesthesatisfiabilityandmodel-checkingproblemstoautomata-theoreticquestions.Thiselegantframeworkhastriggeredalargebodyofworksthathavebeenimple-mentedinexplicitstatemodel-checkingtoolssuchasSPIN[18]andinsymbolicstatemodel-checkingtoolssuchasSMV[14]andNUSMV[2].ThetranslationfromLTLtoNBWiscentraltotheautomata-theoreticapproachtomodel-checking.Whendoneexplicitly,thistranslationisworst-caseexponential.Ex-plicittranslationisrequiredforexplicitstatemodel-checking,whileinthesymbolicapproachtoLTLmodel-checking[3]theNBWissymbolicallyencodedusingbooleanconstraints.In[17],RozierandVardihaveextensivelycomparedsymbolicandexplicitapproachestosatisfiabilitycheckingusingalargenumberoftools.Fromtheirexperi-ments,thesymbolicapproachscalesbetter.⋆ThisresearchwassupportedbytheBelgianFNRSgrant2.4530.02oftheFRFCproject“Cen-treF´ed´er´eenV´erification”andbytheproject“MoVES”,anInteruniversityAttractionPolesProjectoftheBelgianFederalGovernment.⋆⋆ThisauthorissupportedbyaFNRS-FRIAgrant.EfficientalgorithmstoreasononlargeLTLformulasarehighlydesirable.First,aswritingformalrequirementsisadifficulttask,verifyingconsistencyisanissueforwhichefficientsatisfiabilitycheckingwouldbehighlyvaluable.Second,whenmodel-checkingasystemandespeciallyinthe“debugging”phase,wemaywanttocheckpropertiesthataretrueonlyunderasetofassumptions,inwhichcasespecificationsareoftheformρ1∧ρ2∧···∧ρn→φ,andareusuallyverylarge.Thereaderwillfindsuchlargeformulasforexamplein[1]andintheexperimentsreportedhere.Inthispaper,wepresentanewapproachtoLTLsatisfiabilityandmodel-checking.OurapproachavoidstheexplicittranslationtoNBWanddoesnotresorttopurebooleanreasoningasinthesymbolicapproach.Instead,weassociatetoeveryLTLformulaanalternatingB¨uchiautomatonoverasymbolicalphabet(sABW)thatrecognizesthemodelsoftheformula.Theuseofalternationinsteadofnondeterminism,andofsym-bolicalphabetsallowsfortheconstructionofcompactautomata(thenumberofstatesandsymbolictransitionsarelinearinthesizeoftheLTLformula).Whilethisconstruc-tioniswell-knownandisanintermediatestepinseveraltranslatorsfromLTLtoexplicitNBW[22],weprovideanewefficientwaytoanalyzesABW.Thisnewalgorithmisanextensionof[7],wherewehaveshownhowtoefficientlydecidetheemptinessproblemfor(non-symbolic)ABW.TheefficiencyofournewalgorithmreliesonavoidingtheexplicitconstructionofaNBWandontheexistenceofpre-ordersthatcanbeexploitedtoefficientlycomputefixpointexpressionsdirectlyoverthetransitionrelationofABW.ContributionsThethreemaincontributionsofthepaperareasfollows.First,weadaptthealgorithmof[7]forcheckingemptinessofsymbolicABW.Thealgorithmin[7]enumeratesthealphabetΣ,whichisimpracticalforLTLwherethealphabetΣ=2Pisofexponentialsize.Tocopewiththis,weintroduceawaytocombineBDD-basedtechniqueswithantichainalgorithms,takingadvantageofthestrengthsofBDDsforbooleanreasoning.Second,weextendthecombinationofBDDsandantichainstomodel-checkingofLTLspecificationsoversymbolicKripkestructures.In[7],onlyexplicit-statemodelsandspecificationsgivenasNBWswerehandled.Third,wehaveimplementedandextensivelytestedournewalgorithms.Whilethepreviousevalua-tionsofantichainalgorithms[6,7]wereperformedonrandomlygeneratedmodels,weexperimenthereournewalgorithmsonconcrete(i.e.,withameaningfulsemanticsasopposedtorandomlygeneratedinstances)satisfiabilityandmodel-checkingexamples.Mostofourexamplesaretakenin[17]and[19]wheretheyarepresentedasbenchmarkstocomparemodel-checkingalgorithms.Ournewalgorithmsoutperformstandardclas-sicalsymbolica