Symmetry in temporal logic model checking

Miller,A.andDonaldson,A.F.andCalder,M.(2006)Symmetryintemporallogicmodelchecking.ACMComputingSurveys38(3).:22January2008GlasgowePrintsService:53SymmetryinTemporalLogicModelCheckingALICEMILLER,ALASTAIRDONALDSON,ANDMUFFYCALDERUniversityofGlasgowTemporallogicmodelcheckinginvolvescheckingthestate-spaceofamodelofasystemtodeterminewhethererrorscanoccurinthesystem.Oftenthisinvolvescheckingsymmetricallyequivalentareasofthestate-space.Theuseofsymmetryreductiontoincreasetheefficiencyofmodelcheckinghasinspiredawealthofactivityintheareaofmodelcheckingresearch.Weprovideasurveyoftheassociatedliterature.CategoriesandSubjectDescriptors:D.2.4[SoftwareEngineering]:SoftwareProgramVerification—Cor-rectnessproofs;validationGeneralTerms:Theory,VerificationAdditionalKeyWordsandPhrases:Modelchecking,symmetry,quotientgraph1.INTRODUCTIONAssoftware-controlledsystemsexpandandbecomemorecomplex,theimportanceoferrordetectionatdesign-timeincreases.Itisestimated[Schneider2003]that70%ofdesign-timeisspentonsimulationtominimizetheriskthaterrorsareexposedatalaterstageinproduction,involvingcostlyredesign.Temporallogicmodelchecking[Clarkeetal.1999;Merz2000;M¨uller-Olmetal.1999]isatechniquewherebythepropertiesofasystemcanbecheckedbybuildingamodelofthesystemandcheckingwhetherthemodelsatisfiestheseproperties.Themodelisconstructedusingaspecificationlanguage,andcheckedusinganautomaticmodelchecker.Failureofthemodeltosatisfyadesiredpropertyofthesystemindicateseitherthatthemodeldoesnotaccuratelyreflectthebehaviorofthesystem,orthatthereisanerror(bug)intheoriginalsystem.Examinationofcounterexamplesprovidedbythemodelcheckerenablestheusertoeitherrefinethemodel,ormoreimportantly,todebugtheoriginalsystem.Anysearchtechniqueusedinmodelcheckinginvolvestheexplorationofthestate-spaceassociatedwiththemodel.Inherentsymmetryoftheoriginalsystemwillbereflectedinthestate-space.Therefore,knowledgeofthesymmetryofthesystemcanbeusedtoavoidsearchingareasofthestate-spacewhicharesymmetricallyequivalenttoareasthathavebeensearchedpreviously.Severaldifferentapproachesandtechniqueshavebeenproposedforusingsym-metrytoreducethesizeofthestate-spacetobeexplored.SomeofthesehavebeenAuthors’addresses:A.Miller,A.Donaldson,M.Calder,DepartmentofComputingScience,UniversityofGlasgow,17LilybankGardens,Glasgow,UK,G128QQ;email:[e-mail];Permissiontomakedigitalorhardcopiesofpartorallofthisworkforpersonalorclassroomuseisgrantedwithoutfeeprovidedthatcopiesarenotmadeordistributedforprofitordirectcommercialadvantageandthatcopiesshowthisnoticeonthefirstpageorinitialscreenofadisplayalongwiththefullcitation.CopyrightsforcomponentsofthisworkownedbyothersthanACMmustbehonored.Abstractingwithcreditispermitted.Tocopyotherwise,torepublish,topostonservers,toredistributetolists,ortouseanycomponentofthisworkinotherworksrequirespriorspecificpermissionand/orafee.PermissionsmayberequestedfromPublicationsDept.,ACM,Inc.,2PennPlaza,Suite701,NewYork,NY10121-0701USA,fax[phone],[e-mail].c2006ACM0360-0300/2006/09-ART8$5.00.DOI10.1145/1132952/1132962:September2006.P1:QBMAcmj186-02ACM-CSURSeptember4,200621:532A.Milleretal.implementedwithinwidelyusedmodelcheckers[Bosnackietal.2002;Hendriksetal.2003;IpandDill1996;McMillan1993;WangandSchmidt2002].Indeed,thereisevenamodelcheckerdesignedprimarilyfortheverificationofhighlysymmetricsystems[Sistlaetal.2000].Inthisarticlewesurveyandclassifytheexistingresearchinthisarea.Notethatsomeofthemethodsdiscussedinthisarticlehaverecentlybeensurveyedinsomedetail[Sistla2004].Specifically,thatarticledescribesmethodsbasedonannotatedquotientstructures(AQSs)andrelatedguardedquotientstructures(GQSs).WediscusstheseapproachesinSections4.2,4.6,and4.7,anddescribehowtheyareimplementedusingtheSMCmodelcheckerinSection5.1.OursurveyhasamuchbroaderscopethanthatofSistla[2004].Weincludetheprecedingmethodswithinthewidercontextofsymmetryreductionmethodsformodelcheckingingeneral,andwedescribeagreaterrangeofsystemsthatemploysymmetryreductionmethods.2.MODELCHECKINGTemporallogicmodelchecking[Clarkeetal.1986,1999;Merz2000;M¨uller-Olmetal.1999]isanautomatictechniqueforverifyingfinitestateconcurrentsystems.Thetypeofsystemsthatweareconcernedwithmaintainacontinuinginteractionwiththeirenvironment,andarereferredtoasreactivesystems.Modelcheckinginvolvestheconstructionofamodelofasystem,usuallyintheformofaKripkestructure,andtheverificationoftemporallogicpropertiesofthismodel.LetVdenoteasetofvariables,andforeachv∈V,letD(v)bethedomainofv.ThesetofatomicpropositionsoverVisgivenbyAP={(v=val):v∈Vandval∈D(v)}.ForagivensetofvariablesV,aKripkestructureisdefinedintermsofAPthusly:Definition1.AKripkestructureMoverAPisatupleM=(S,R,L,S0)where:(1)Sisanonempty,finitesetofstates(2)R⊆S×Sisatotaltransitionrelationthatisforeachs∈S∃t∈Ssuchthat(s,t)∈R(3)L:S→2APisamappingthatlabelseachstateinSwiththesetofatomicpropositionstrueinthatstat