Model Checking Knowledge and Linear Time PSPACE Ca

ModelCheckingKnowledgeandLinearTime:PSPACECasesKaiEngelhardt?,PeterGammie,andRonvanderMeyden?SchoolofComputerScienceandEngineering,TheUniversityofNewSouthWales,andNationalICTAustralia??,Sydney,NSW2052,Australia,{kaie|peteg|meyden}@cse.unsw.edu.auAbstract.Wepresentageneralalgorithmschemeformodelcheckinglogicsofknowledge,commonknowledgeandlineartime,basedonsimu-lationstoaclassofstructuresthatcapturethewaythatagentsupdatetheirknowledge.WeshowthattheschemeleadstoPSPACEimplemen-tationsofmodelcheckingthelogicofknowledgeandlineartimeinsev-eralspecialcases:perfectrecallsystemswithasingleagentorinwhichallcommunicationisbysynchronousbroadcast,andsystemsinwhichknowledgeisinterpretedusingeithertheagents’currentobservationonlyoritscurrentobservationandclockvalue.Inalltheseresults,commonknowledgeoperatorsmaybeincludedinthelanguage.Matchinglowerboundsareprovided,anditisshownthatalthoughthecomplexityboundmatchesthePSPACEcomplexityofthelineartimetemporallogicLTL,asafunctionofthemodelsizetheproblemsconsideredhaveahighercomplexitythanLTL.1IntroductionThelogicofknowledge[5]hasbeenproposedasaformalismtoexpressinforma-tiontheoreticpropertiesindistributedandmulti-agentsystems,andhasbeenshowntobeusefulfortheanalysisofdistributedsystemsprotocols[9],informa-tionflowsecurityproperties[10,21,24],aswellasforproblemssuchasdiagnosisandrecoverability[3,4].Thesemanticsforknowledgeoperatorscanbedefinedinavarietyofways,dependingonwhatinformationagentsusewhencomputingwhattheyknow.Atoneextreme(the“observationalsemantics”)agentsrelyonlyontheircurrentobservation,attheother(the“synchronousperfectrecallsemantics”)agentsrelyonthelogofalltheirpastobservations.Inbetweenliesa“clockseman-tics”inwhichagentsrelyontheircurrentobservationplusaclockvalue.These?WorkwaspartiallysupportedbyARCDiscoveryGrantRM02036.??NationalICTAustraliaisfundedthroughtheAustralianGovernment’sBackingAustralia’sAbilityinitiative,inpartthroughtheAustralianResearchCouncil.ThethirdauthorthankstheComputerScienceDepartment,CourantInstitute,NewYorkUniversityfortheirhospitalityinhostingasabbaticalvisitduringwhichthisworkwasconducted.2KaiEngelhardt,PeterGammie,andRonvanderMeydensemanticshavedifferentmotivations:theperfectrecallsemanticsismostappro-priateforsecurityanalysesandderivationofprotocolsthatmakeoptimaluseofinformation;theothersemanticsareclosertosystemimplementations.Anumberofmodelcheckersforthelogicofknowledgehavebeenrecentlybeendeveloped,whichembodydifferentchoicesofsemanticsfortheknowl-edgeoperatorsanddifferenttypesofexpressivenessforthetemporaldynamics.MCMAS[13]dealswiththeobservationalinterpretationofknowledgeandthebranchingtimelogicCTL.DEMO[27]dealswiththedynamiclogicbased“up-datelogic”[1],whichhandleswhatisineffecttheperfectrecallsemanticsforknowledge.ThesystemMCK[7]coversabroadspectrumofdefinitionsofknowl-edge(observational,clock,perfectrecall),aswellasdealingwithbothlineartimeandbranchingtimetemporallogic.Wheretheydealwiththeperfectrecallsemanticsforknowledge,thesesys-temsplacesevereconstraintsontheinteractionbetweenknowledgeandtemporaloperators,forreasonsofinherentcomplexity.ThecomplexityofmodelcheckingthecombinationofthelineartimetemporallogicLTLwithknowledgeopera-torsinterpretedaccordingtotheperfectrecallsemanticshasbeenstudiedbyvanderMeydenandShilov[23],whoshowthatthisproblemisdecidablebutwithanon-elementarylowerbound,andundecidablewhenoperatorsforcom-monknowledge(atypeoffixpointoverknowledgeoperators)areaddedtothelanguage.(Shilovetal[17,18,8]havealsostudiedbranchingtimeversionsoftheseresults.)However,asweshowinthispaper,thisgeneralresultdoesnotprecludetheexistenceofspecialcasesinwhichthismodelcheckingproblemhaslowercomplexity,evenwhencommonknowledgeoperatorsareincludedinthelan-guage.Weidentifyanumberofcaseswheretheproblem(includingcommonknowledge)issolvableinPSPACE.Theseincludesystemswithasingleagent(discussedinSection5.1)andsystemsinwhichallcommunicationisbysyn-chronousbroadcast(treatedinSection5.2)TheresultconcerningasingleagentimprovesthenonelementaryupperboundforthesingleagentcaseobtainedfromthealgorithmofvanderMeydenandShilov.Ourapproachtotheproofoftheseresultsisbymeansofageneralalgorithmscheme(presentedinSection4)thatreliesupontheexistenceofasimulationfromthe(ineffect,infinite)systemsbeingcheckedtoafinitestructurethatrep-resentsthewaythatagentsupdatetheirknowledgeinthesystem.Inadditiontotheresultsabouttheperfectrecallsemantics,weshowthatthisschemecanbeusedtoobtainPSPACEcomplexityresultsformodelcheckingthelogicofknowledgeandlineartimeforotherinterpretationsforknowledge:inparticu-lar,weshowthatthiscomplexityboundappliesinthecaseofboththeclocksemanticsandtheobservationalsemantics(seeSection6).AsthecomplexityofmodelcheckingthelineartimetemporallogicLTLaloneisalreadyPSPACE-complete,itmayseemfromtheseresultsthattheextraexpressivenessofthelogicofknowledgeinthesecasescomesatnoextracost.Infact,weshowthatthereisasenseinwhichthesemodelcheckingproblemsareharderthanmodelcheckingLTLalone,byfocussingonthecomplexityofModelCheckingKnowledgeandLinearTime:PSPACECases3modelcheckingafixedfo