1 The Complexity of Temporal Logic Model Checking

1TheComplexityofTemporalLogicModelCheckingPh.Schnoebelen11IntroductionTemporallogic.Logicalformalismsforreasoningabouttimeandthetimingofeventsappearinseveralelds:physics,philosophy,linguistics,etc.Notsurprisingly,theyalsoappearincomputerscience,aeldwherelogicisubiquitous.Heretemporallogicsareusedinautomatedreasoning,inplanning,insemanticsofprogramminglanguages,inarticialintelligence,etc.Thereisoneareaofcomputersciencewheretemporallogichasbeenunusuallysuccessful:thespecicationandvericationofprogramsandsys-tems,anareaweshalljustcall\programmingforsimplicity.Intoday'scurricula,thousandsofprogrammersrstlearnabouttemporallogicinacourseonmodelchecking!Temporallogicandprogramming.Twentyveyearsago,Pnueliiden-tiedtemporallogicasaveryconvenientformallanguageinwhichtostate,andreasonabout,thebehavioralpropertiesofparallelprogramsandmoregenerallyreactivesystems[Pnu77,Pnu81].Indeed,correctnessforthesesys-temstypicallyinvolvesreasoninguponrelatedeventsatdierentmomentsofasystemexecution[OL82].Furthermore,whenitcomestolivenessprop-erties,theexpectedbehaviorofreactivesystemscannotbestatedasastaticproperty,orasaninvariantone.Finally,temporallogiciswellsuitedtoex-pressingthewholevarietyoffairnesspropertiesthatplaysuchaprominentroleindistributedsystems[Fra86].Fortheseapplications,oneusuallyrestrictsoneselftopropositionaltem-porallogic:ontheonehand,thisdoesnotappeartobeaseverelimi-tationinpractice,andontheotherhand,thisrestrictionallowsdecisionproceduresforvalidityandentailment,sothat,atleastinprinciple,theabove-mentionedreasoningcanbeautomated.Modelchecking.Generallyspeaking,modelcheckingisthealgorithmicvericationthatagivenlogicformulaholdsinagivenstructure(themodel1LaboratoireSpecication&Verication(LSV),ENSdeCachan&CNRS.Email:[e-mail],Volume4,1{44.c2002,byWorldScienticPublishingCo.Pte.Ltd.2Ph.Schnoebelenthatonechecks).Thisconceptismeaningfulformostlogicsandclassesofmodelsbut,historically,itwasdevelopedinthecontextoftemporallogicformulaeforniteKripkestructures,called\temporallogicmodelcheckinginthissurvey.Temporallogicmodelcheckinghasbeenaveryactiveeldofresearchforthelasttwodecadesbecauseofitsimportantapplicationsinverication(seee.g.[CW96]).Ahugeeorthasbeen,andisbeing,devotedtothedevelopmentofsmarterandbettermodelcheckingsoftwaretools,knownasmodelcheckers,thatcanverifyeverlargermodelsanddealwithawidevarietyofextendedframeworks(real-timesystems,stochasticsystems,opensystems,etc.).Wereferto[Hol91,Kur95,CGP99,BBF+01]formoredetailsonthepracticalaspectsofmodelchecking.Modelcheckingformodallogicians.Temporallogiccanbeseenassomebrandofmodallogic,butitseemsfairtosaythatmodelcheckingisnotapopularprobleminthemodallogiccommunity:forexampleitisnotmentionedinstandardtextbookssuchas[Ben85,HC96,BRV01].Thisisprobablybecausemodelcheckingistootrivialaproblemforthestan-dardmodallogicsbasedonimmediatesuccessors(itiseasyevenforPDL,see[CS93])andonlybecomesinterestingwhenrichertemporallogicsareconsidered.However,standardtextsontemporallogicaimedatlogicians(e.g.[Ben89,Sti92,GRF00])justbrieymentionthatmodelcheckingispossibleanddonotreallydealwiththecomputationalissuesinvolved.Arecentexceptionis[BS01]whereafewpagesaredevotedtomodelcheckingfor-calculisince,quoting[BS01,p.315]:Decidabilityandaxiomatizationarestandardquestionsforlogi-cians;butforthepractitioner,theimportantquestionismodel-checking.Thecomplexityofmodelchecking.Oncedecidabilityhasbeenproved,thenextbasicprobleminthetheoryofmodelcheckingismeasuringitscomplexity1.Thepointisthat,whentheprecisecomplexityofsomecomputationalproblemhasbeenestablished,itcanbesaidthattheoptimalalgorithmfortheproblemhasbeenidentiedandprovedoptimal.Here\optimalhasaprecisemeaning:oneonlyconsiderswhatcomputingresourcesareasymptoticallynecessaryandsucientforsolvingallinstances,includingthehardestones(i.e.,intheworstcase).Thesesimplicationsandabstrac-tionsaboutthecostofalgorithmsleadtoasurprisinglypowerfultheory1Weassumethereaderhassomebasicknowledgeofthetheoreticalframeworkofcomputationalcomplexity,andreferhimtostandardtextslike[Sto87,Joh90,Pap94]formoremotivationsanddetails.TheComplexityofTemporalLogicModelChecking3thathasbeenappliedsuccessfullyinahugenumberofelds.Intheeldoftemporallogicmodelchecking,thisresearchprogramledtoaclearerunderstandingofwhymodelcheckingworkssowell(ordoesnotwork).Italsoaddedanewdimensiononwhichtocomparedierentlogicalformalisms(alongsidethemoreclassicaldimensionsofexpressivepowerandcomplexityofvalidity).Thegoalsofthissurvey.Wepresentthemainresultsonthecomplex-ityofmodelcheckingandtheunderlyingalgorithmicideas.Thiscoversthemaintemporallogicsencounteredintheprogrammingliterature:LTL(from[GPSS80]),CTL(from[CE81]),CTL(from[EH86]),theirfragments,andtheirextensionswithpast-timemodalities2.Thepresentationismainlyfocusedoncomplexityresults,notontheusefulness,orelegance,orexpres-sivepower,ofthetemporallogicsweconsider3.However,whencomplexityofmodelcheckingisconcerned,we(tryto)explaintheideasbehindthealgorithmsandhardnessproofs,inthehopethattheset