Dynamic Linear Time Temporal Logic

DynamicLinearTimeTemporalLogicJesperG.Henriksen,BRICS1,DepartmentofComputerScience,UniversityofAarhus,NyMunkegade,DK-8000AarhusC,DenmarkP.S.Thiagarajan,2;3SPICMathematicalInstitute,92G.N.ChettyRoad,T.Nagar,Chennai600017,IndiaAbstractAsimpleextensionofthepropositionaltemporallogicoflineartimeisproposed.Theextensionconsistsofstrengtheningtheuntiloperatorbyindexingitwiththeregularprogramsofpropositionaldynamiclogic.ItisshownthatDLTL,theresultinglogic,isexpressivelyequivalenttothemonadicsecond-ordertheoryof!-sequences.Infact,asublogicofDLTLwhichcorrespondstopropositionaldynamiclogicwithalineartimesemanticsisalreadyexpressivelycomplete.WeshowthatDLTLhasanexponentialtimedecisionprocedureandadmitsanitaryaxiomatization.Wealsopointtoanaturalextensionoftheapproachpresentedheretoadistributedsetting.1IntroductionWepresenthereasimpleextensionofthepropositionaltemporallogicoflineartime.Thebasicideaistostrengthentheuntilmodalitybyindexingitwiththeregularprogramsofpropositionaldynamiclogic.Theresultinglogic,calleddynamiclineartimetemporallogic(DLTL),iseasytohandle.Ithasthefullexpressivepowerofthemonadicsecond-ordertheoryof!-sequences.IndeedasublogicofDLTLisalreadyexpressivelycomplete.Apleasantfeatureofthissublogicisthatitisjustpropositionaldynamiclogicoperatinginalineartimeframework.1BasicResearchinComputerScience,CentreoftheDanishNationalResearchFoundation.2PartofthisworkwasdonewhilevisitingBRICS.3PartofthisworkhasbeensupportedbytheIndo-FrenchCentreforthePromotionofAdvancedResearch(IFCPAR)project1502-1.PreprintsubmittedtoElsevierPreprint2April1998InadditiontoourexpressivenessresultsweshowthatDLTLhasanexponen-tialtimedecisionprocedure.Wealsoextendthewellknownaxiomatizationofpropositionaldynamiclogic[11]toobtainanaxiomatizationofDLTL.Ourworkmaybeviewedfromtwodierentperspectives.Therstoneisfromthestandpointofprocesslogics[6,16,18]whichattemptarapprochementbetweendynamicandtemporallogics.Howeverthestudyofprocesslogicsiscommittedtoviewingdynamiclogicasarestrictedkindofabranchingtimetemporallogic.Onethenattemptstobringinsomeadditionalmechanismsfortalkingaboutcomputationalpaths.Ourpointofdepartureconsistsofmerging,inaverysimpleway,dynamiclogicandtemporallogicinalineartimesetting.Thesecondperspectivehastodowithattemptstoaugmenttheexpressivepoweroflineartimetemporallogic.Onerouteconsistsofpermittingquan-ticationoveratomicpropositions.TheresultinglogiccalledQPTL[20]isasexpressiveasS1S,themonadicsecond-ordertheoryofsequencesbutitsdeci-sionprocedurehasnon-elementarytimecomplexity.Thesecondrouteconsistsofaugmentinglineartimetemporallogicwiththesocalledautomatoncon-nectives.TheresultinglogiccalledETL[26]isequalinexpressivepowertoS1Swhileadmittinganexponentialtimedecisionprocedure.Ourlogicis,inspirit,inspiredbyETLanditcanbeeasilytranslatedintoETL.ItmayappeartobeatrstsighttobeamerereformulationofETLwithsomecosmeticchanges.Thishoweverhastodowiththeinstinctiveidenticationonemakesbetweennitestateautomataandregularexpressions.InfactDLTLisquitedierentintermsofthemechanismsitoersforstructuringformulasandwefeelthatitismoretransparentandeasiertoworkwith.Theresultsandtheproofswepresentherearedesignedtosupportthisclaim.Ourapproachalsoleadstosmoothgeneralizationsinnon-sequentialsettingswheresimilarextensionsintermsofETLwillbehardtocopewith.Inthenextsectionwestartwithanaction-basedversionofoflineartimetemporallogicinordertoxterminology.InSection3wepresentDLTLanditssemantics.ThisisthenfollowedbyamoredetailedassessmentofthesimilaritiesandthedierencesbetweenETLandDLTL.InSection4weprovethedecidabilityofDLTLbyreducingittotheemptinessproblemforBuchiautomata.InSection5weshowthatDLTL,asublogicofDLTL,hasthesameexpressivepowerasS1S,themonadicsecond-ordertheoryofsequences.Wethenestablishsimilarresultsfortherst-orderfragmentofS1Swiththehelpofthe\star-freefragmentsofDLTLandDLTL.InSection6,weextendtheaxiomatizationofPDL(propositionaldynamiclogic)andthecompletenessproofin[11]toobtainnitaryaxiomatizationsofDLTLandDLTL.Inthenalsectionwepointtoanaturalgeneralizationin2thesettingofdistributedsystems.Thisgeneralizationiseminentlyaccessibleandoersadditionalsupporttoourbeliefthatthesynthesisofdynamicandtemporallogicsinalineartimeframeworkaspursuedhereisafruitfulone.2LinearTimeTemporalLogicOnekeyfeatureofthesyntaxandsemanticsofourtemporallogicisthetreatmentofactionsasrstclassobjects.TobringthisoutweformulateaversionofLTL(lineartimetemporallogic)inwhichthenext-statemodalityisindexedbyactionstakenfromaxedalphabetset.Throughtherestofthepaperwexanitenon-emptyalphabet.Weleta;brangeoverandrefertomembersofasactions.isthesetofnitewordsand!isthesetofinnitewordsgeneratedbywith!=f0;1;2;:::g.Weset1=[!anddenotethenullwordby.Welet;0rangeover!and;0;00rangeover.Finallyistheusualprexorderingdenedoverandforu21,weletprf(u)bethesetofniteprexesofu.NextwexacountablesetofatomicpropositionsP=fp1;p2;:::gandletp;qrangeoverP.ThesetofformulasofLTL()isthengivenbythesyntax:LTL()::=pjj_jhaijU:Throughtherestofthissection;willrangeoverLTL()