Model checking LTL using constraint programming

ModelCheckingLTLusingConstraintProgramming?JavierEsparzaandStephanMelzerInstitutfurInformatik,Arcisstrae21TechnischeUniversitatMunchen,D-80333Munchen,Germanye-mail:fesparza,[e-mail]-checkingproblemfor1-safePetrinetsandlinear-timetemporallogic(LTL)consistsofdeciding,givena1-safePetrinetandaformulaofLTL,whetherthePetrinetsatisesthepropertyen-codedbytheformula.Thispaperintroducesasemidecisiontestforthisproblem.Byasemidecisiontestweunderstandaprocedurewhichmayanswer‘yes’,inwhichcasethePetrinetsatisestheproperty,or‘don’tknow’.Thetestisbasedonavariantofthesocalledautomata-theoreticapproachtomodel-checkingandonthenotionofT-invariant.Weanal-ysethecomputationalcomplexityofthetest,implementitusing2lp{aconstraintprogrammingtool,andapplyittotwocasestudies.Thispaperisa(very)abbreviatedversionof[6].1IntroductionLinear-timetemporallogic(LTL)isawell-knownformalismforspecifyingprop-ertiesofconcurrentsystems.TheproblemofdecidingifaconcurrentsystemsatisesaLTLformulaiscalledthemodel-checkingproblem(ofLTL).In[16]VardiandWolperintroducedanautomata-theoreticapproachtothisproblem.Theapproachassumesthatthereexistsasemanticmappingwhichassociatestoaconcurrentsystemsysanite(labelled)transitionsystemAsys.Itaskstheveriertoperformthefollowingthreetasks[9,16]:{BuildaBuchiautomatonA:forthenegationoftheformulatobechecked.A:acceptsexactlyallinnitesequencesthatviolatetheformula.{ConstructaBuchiautomatonAp,calledtheproductofAsysandA:.ApacceptsalltheinnitecomputationsofAsysthatareacceptedbyA:,i.e.,allinnitecomputationsofAsysthatviolate.{CheckwhethertheproductautomatonApisempty,i.e.,whetheritacceptsnoinnitesequences.AsyssatisesiffApisempty.Themainproblemofthisapproachisthewell-knownstate-explosionphe-nomenon:thesizeofthetransitionsystemAsyscangrowexponentiallyinthesizeofsys.Severalsuggestionshavebeenmadetosolveoratleastpalliatethisproblem:thetransitionsystemAsyscanbereplacedbyatraceautomaton[9],?ThisworkissupportedbytheSonderforschungsbereichSFB-342A3.andthesizeofAsyscanbereducedbymeansofdierenttechniqueslikestubbornsets[14],sleepsets[9],orothers.Inthispaperweintroducestillanothertechniquetoavoidthestate-explosion,whichcanbeappliedwhenthesystemismodelledasa1-safePetrinet.Thetechniqueisasemidecisiontest,thatis,aprocedurewhichmayanswer‘yes’,inwhichcasethepropertytobecheckedholds,or‘don’tknow’.Asemidecisiontesthasinterestonlyifforrelevantcasestudiesitanswers‘yes’andperformsfasterthanexactmethods.Weprovideevidenceinthisdirectionintheformofacomplexityanalysisandtwocasestudies.ForsystemsmodelledasPetrinetsthetransitionsystemAsysisjustthewell-knownreachabilitygraph.Anstraightforwardapplicationoftheautomata-theoreticapproachwouldproceedby(1)buildingthereachabilitygraph,andby(2)constructingtheproductautomaton;itwouldobviouslysuerfromthestateexplosionproblem.Therst(minor)contributionofthispaperistoshowthatstep(2)canbeperformedbeforestep(1).Morespecically,wedescribeseveralwaysofconstructinga‘productBuchinet’NpfromaPetrinetNsysandaBuchiautomatonA:.Usingthisconstructionitisimmediatetoreducethemodel-checkingproblemtoacertain‘netemptiness’problem,verysimilartotheemptinessproblemofBuchiautomata.WeselecttheconstructionoftheproductBuchinetmostsuitableforoursemidecisiontest.ThetestisbasedonthenotionofT-invariant,andcanbeseenasageneralizationofthead-hocproofmethodintroducedandappliedin[7].Weshowthatthetestcanbeimplementedintheframeworkofconstraintprogramming[12]usingtheconstraintprogrammingtool2lp[13].Finally,weapplythetesttoaleaderelectionandtoasnapshotalgorithm.Thepaperisorganisedasfollows.Section2describesthemaincomponentsoftheautomata-theoreticapproachtomodel-checking,tailoredforthecaseinwhichthesystemismodelledbyaPetrinet.Section3showshowtoconstructtheproductBuchinets.Section4introducesthetestfornetemptiness.Section5containstheimplementationin2lp.Section6isdevotedtothecasestudies.Thepaperisanabbreviatedversionof[6].Thereadercanndtheretheproofsoftheresults,adetaileddescriptionofthecasestudies,andadditionalresults.2Theautomata-theoreticapproachtomodel-checking2.1TransitionsystemsAlabelledtransitionsystemisafourtuple(Act;Q;;q0),whereActisanalpha-betofactions,Qisasetofstates,QActQisasetoftransitions,andq02Qistheinitialstate.Afullrunofalabelledtransitionsystemisaninnitesequenceq0a0q1a1q2:::suchthat(qi;ai;qi+1)2foreveryi0.Wealsodenoteafullrunbyq0a0!q1a1!q2:::.Whenlabelledtransitionsystemsareusedassemanticsofsomeprocessalge-braonlythelabelsofthetransitionscarryusefulinformation;theintermediatestatesareusuallyirrelevant.Wespeakinthiscaseofanaction-basedseman-tics.Inaction-basedsemanticsthefollowingdenitionisuseful:Aninnitesequencea0a1a2:::ofactionsofTisanactionrunifthereexistsafullrunq0a0!q1a1!q2a2!:::.TheactionlanguageLa(T)ofTisthesetofallactionruns.Whenlabelledtransitionsystemsareusedassemanticsoflanguageswithvariables,theinformationabouttheactualvaluesofthevariablesisencodedintothestates;thelabelsofthetransitionsareusuallyirrelevant.Wespeakinthiscaseofastate-basedsemantics