Model checking for a probabilistic branching time

ModelCheckingforaProbabilisticBranchingTimeLogicwithFairnessChristelBaierFakultatfurMathematik&InformatikUniversitatMannheim68131Mannheim,[e-mail]ofComputerScienceUniversityofBirmingham,EdgbastonBirminghamB152TT,[e-mail]19,1996AbstractWeconsiderprobabilistictransitionsystems,basedonprobabilisticautomataofSegala&Lynch[43],whichdistinguishbetweennon-deterministicandprobabilisticchoice.Thesesystemscanbedecomposedintoacollectionof\computationswhicharisebyresolvingnon-deterministic,butnotprobabilistic,choices.Thepresenceofnon-deterministismmeansthatcertainlivenesspropertiescannotbeestablishedunlessfairnessisassumed.WeintroduceaprobabilisticbranchingtimelogicPBTL,basedonthelogicTPCTLofHansson[22]andthelogicPCTLof[43],resp.pCTLof[9].Theformulasofthelogicexpresspropertiessuchas\everyrequestiseventuallygrantedwithprobabilityatleastp.WegivethreeinterpretationsforPBTLonconcurrentprobabilisticprocesses:therstisstandard,whileintheremainingtwointerpretationsthebranchingtimequantiersaretakentorangeovercertainfaircomputations.Finally,wepresentamodelcheckingalgorithmforverifyingwhetheraconcurrentprobabilisticprocesssatisesaPBTLformulaassumingfairnessconstraints.Contents1Introduction22Probabilistictransitionsystems63Concurrentprobabilisticsystems73.1Pathsinconcurrentprobabilisticsystems...................73.2Adversariesofconcurrentprobabilisticsystems................83.3Fairnessandstrictfairnessofadversaries...................9SupportedinpartbyEPSRCgrantGR/K42028.14Probabilisticbranchingtimetemporallogic105ModelcheckingforPBTL136Timecomplexityofmodelchecking217Example248ProofsofMainResults278.1Fairnessw.r.t.theprobabilisticchoices....................288.2Theprexrelationonpaths..........................298.3Extensionofnitebehaviourto(strictly)fairadversaries..........318.4ProofofTheorem2and3...........................328.5ProofofTheorem5and6...........................328.6ProofofTheorem4...............................398.7ProofofTheorem7...............................429FairnessalaVardi4510ModelcheckingforPBTL5011Concludingremarksandfurtherdirections531IntroductionProbabilistictechniques,andinparticularprobabilisticlogics,haveprovedsuccessfulinthespecicationandvericationofsystemsthatexhibituncertainty,forexample,fault-tolerantsystems,distributedsystems,andcommunicationprotocols.Givensuchasystem,oftenpresentedasaprobabilisticautomaton(nitetransitionsystemextendedwithprob-abilities,seee.g.[30,43,46]),thegoalofthevericationprocessistodeterminewhetherthestatesofthissystemsatisfyaformulaofsomeprobabilisticlogic.Typically,theveri-cationaimstoestablishqualitativeproperties,i.e.propertiesthatarefullledbyalmostallexecutions,whichamountstoshowingthatthepropertyissatisedwithprobability1,seee.g.[2,3,13,22,23,24,25,33,38,39,40,47].Althoughtheaboverequirementofprobability1isimportantinthecaseofe.g.safety-criticalsystems,forpracticalpurposesitisoftensucienttoshowthatthepropertyissatisedwithprobability1forsomesmall(anerror).Thesequantitativepropertiesalsoplayanimportantroleintheanal-ysisoftheaverage-casebehaviourofprobabilisticsystems.Morespecically,algorithmsareneededwhichshowthatagivenpropertyissatisedwithprobabilitye.g.12.Severalprobabilisticlogicshavebeenproposedwhichallowtospecifypropertiesoftheform\thesystemsatisesproperty’withprobabilityatleastpwherepisarealnumber2intheinterval[0,1].Forinstance,[28]and[19]introduceaprobabilisticdynamiclogic,[30,31]aprobabilisticextensionofamodallogic,[10]probabilisticrecursivelogics,[4,5,9,22,23,43]probabilisticextensionsofCTL.OurstartingpointisamodelforconcurrentprobabilisticsystemsbasedonprobabilisticautomataofSegala&Lynch[43],which,asisthecasein[4,9,13,14,27,39,40,47,49],exhibitbothprobabilisticandnon-deterministicchoice.Thismeansthatitispossibleinagivenstatetonon-deterministicallychoosebetweentwoormoreprobabilisticdistri-butionsonthesuccessorstates;thesedistributionsdeterminetheprobabilitywithwhichasuccessorstateistaken.Whendealingwithconcurrentprobabilisticsystems,thedis-tinctionbetweennon-deterministicandprobabilisticchoicesisnecessarysinceconcurrentsystemscontainstatesthatareinherentlynon-deterministic.Thenon-determinismmayarisee.g.fromtheasynchronicityofcertainsubprocesses,orexternalinterventionsuchasactiontakenbyenvironment.Itisconventionedthataschedulerdecideswhichofthesubprocessesperformsitsnextstep,andthatno(probabilistic)assumptionsaboutthesedecisions,whichanyschedulerhastoobey,areorcanbemade.Anyschedulerofaconcurentprobabilisticsystemresolvesthenon-deterministicchoices(butnottheproba-bilisticchoices;theseareresolvedbythesystemitself)andyieldsasequentialcomponentofthesystem.Thesequentialcomponentsarerepresentedbyprobabilistictransitionsys-temswhichareidentiedbyrequiringthatineverystatethereisatmostonedistribution(thisissimilartothe\generativemodelof[46]and\sequentialMarkovchainsconsid-erede.g.in[13,23,24,33,47]).Rangingoverallschedulers,aconcurrentprobabilisticsystemcanbedecompose