搜索
}w !#$%&’()+,-./012345yA|FIMUFacultyofInformaticsMasarykUniversityRelatingHierarchyofLinearTemporalPropertiestoModelCheckingbyIvana CernÆRadekPelÆnekFIMUReportSeriesFIMU-RS-2003-03Copyrightc 2003,FIMUApril2003RelatingHierarchyofLinearTemporalPropertiestoModelCheckingIvana Cern·aandRadekPel·anek?DepartmentofComputerScience,FacultyofInformaticsMasarykUniversityBrno,CzechRepublicfcerna,xpelanekg@fi.muni.czAbstract.ThehierarchyofpropertiesasoverviewedbyMannaandPnueli[23]relateslanguage,topology,!-automata,andlineartemporallogicclassi cationsofproperties.Weprovidenewcharacterisationsofthishi-erarchyintermsofautomatawithB¤uchi,co-B¤uchi,andStreettaccep-tanceconditionandintermsof LTLiand LTLihierarchies.Afterwards,weanalysethecomplexityofthemodelcheckingproblemforparticularclassesofthehierarchyandthankstothenewcharacterisationsweiden-tifythoselineartimetemporalpropertiesforwhichthemodelcheckingproblemcanbesolvedmoreef cientlythaninthegeneralcase.1IntroductionModelcheckinghasbecomeapopulartechniqueforformalveri cationofreac-tivesystems.Themodelcheckingprocesshasseveralphases themajoronesbeingmodellingofthesystem,speci cationofdesiredpropertiesofthesys-temandtheactualprocessofautomaticveri cation.Eachofthesephaseshasitsspeci cdif culties.Inthispaperwestudylineartemporalpropertiesandalgorithmsfortheautomaticveri cationoftheseproperties.Reactivesystemsmaintainanongoinginteractionwiththeirenvironmentandthusproducecomputations in nitesequencesofstates.Whenanalysingthebehaviourofsuchasystemweareinterestedinsome nitesetAPofob-servablepropositionsaboutstates.Hence,wecanviewacomputationofthesystemasanin nitewordover2AP.Ingeneral,wede neatemporalpropertyasalanguageofin nitewords.AreactivesystemSissaidtohaveapropertyPifallpossiblecomputationsofSbelongtoP.Theproblemofproperandcorrectspeci cationofpropertiesthesystemoughttosatisfyledtoacarefulstudyoftheoreticalaspectsofproperties.MannaandPnueli[23]haveproposedaclassi cationoftemporalpropertiesintoahierarchy.Theycharacterisetheclassesofthehierarchythroughfourviews:alanguage-theoreticview,atopologicalview,atemporallogicview,andanautomataview.Thefactthatthehierarchycanbede nedinmanydifferentwaysshowstherobustnessofthishierarchy.?SupportedbyGA CRgrantno.201/03/0509Modelcheckingtheoryisdevotedtothedevelopmentofef cientalgorithmsfortheautomaticveri cationofpropertiesofreactivesystems.Averysuccess-fulapproachtoverifyingpropertiesexpressedaslineartemporallogic(LTL)formulasmakesuseofautomataoverin nitewords.Heretheproblemofveri-fyingapropertyreducestotheproblemwhetheragivenautomatonrecognisesanon-emptylanguage(socallednon-emptinesscheck).Thecomplexityofthenon-emptinesscheckdependsonthetypeoftheautomaton.Bloem,Ravi,andSomenzi[1]havestudiedtwospecialisedtypesofautomata,calledweakandterminal,forwhichthenon-emptinesscheckcanbeperformedmoreef cientlythaninthegeneralcase.OurcontributionOuraimistoclassifytemporalpropertiesspeci ablebylin-eartemporallogicformulaswithrespecttothecomplexityoftheirveri ca-tion.Tothisendweprovideaclassi cationoftemporalpropertiesthroughtwonewviews.First,wecharacterisepropertiesintermsofautomataoverin nitewords(!-automata)withB¤uchi,co-B¤uchiandStreettacceptanceconditionandintermsofweakandterminalautomata.Weakandterminalautomataareusedintheveri cationprocessandarecheckedfornon-emptiness.Forthesecondcharacterisationweintroduceanewhierarchy(calledUntil-Releasehierarchy)ofLTLformulasbasedonalternationdepthoftemporalop-eratorsUntilandRelease.WeprovidearelationshipbetweentheUntil-ReleasehierarchyandthehierarchybyMannaandPnueli[23].Ournewclassi cationprovidesuswithanexactrelationshipbetweenthetypeofaformulaandthetypeofanautomaton,whichischeckedfornon-emptinessinthemodelcheckingprocessoftheformula.Inthesecondpartofthepaperweenquireintoparticularautomataandanalysethecomplexityoftheirnon-emptinesscheckinconnectionwithbothexplicitandimplicitrepresentationofautomata.Thisgivesusanexactrela-tionshipbetweentypesofpropertiesandthecomplexityoftheirveri cation.Finally,wediscussthepossibilityofexactdeterminationofthetypeofafor-mula.RelatedworkThepreviousworkonveri cation,whichtakesintoaccountaclassi cationofproperties,ispartlydevotedtotheproof-basedapproachtoveri cation[5].Papersonspecialisedmodelcheckingalgorithmseithercoveronlypartofthehierarchyorhaveaheuristicnature.VardiandKupferman[20]studythemodelcheckingofsafetyproperties.Schneider[26]isconcernedwithatranslationofpersistencepropertiesintoweakautomata.BloemandSomenzistudyheuristicsforthetranslationofaformulaintoweak(terminal)automa-ton[28]andsuggestspecialisedalgorithmsforthenon-emptinessproblem[1].Ourworkcoversalltypesofpropertiesandbringsoutthecorrespondencebe-tweenthetypeandthecomplexityofnon-emptinesscheck.PlanoftheworkSection2introducesthehierarchyofpropertiesaspresentedin[23]andestablishesnewcharacterisationsofthehierarchy.Firstwesup-2plementtheautomataviewandthanwerevisethecharacterisationthroughformulasoflineartemporallogic.Herewe ndausefortheUntil/Releasealternationdepthofformulas.Section3de ne