您好,欢迎访问三七文档
当前位置:首页 > 商业/管理/HR > 质量控制/管理 > 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.WeshowthatDLTLhasanexponentialtimedecisionprocedureandadmitsa nitaryaxiomatization.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.Ourworkmaybeviewedfromtwodi erentperspectives.The rstoneisfromthestandpointofprocesslogics[6,16,18]whichattemptarapprochementbetweendynamicandtemporallogics.Howeverthestudyofprocesslogicsiscommittedtoviewingdynamiclogicasarestrictedkindofabranchingtimetemporallogic.Onethenattemptstobringinsomeadditionalmechanismsfortalkingaboutcomputationalpaths.Ourpointofdepartureconsistsofmerging,inaverysimpleway,dynamiclogicandtemporallogicinalineartimesetting.Thesecondperspectivehastodowithattemptstoaugmenttheexpressivepoweroflineartimetemporallogic.Onerouteconsistsofpermittingquan-ti cationoveratomicpropositions.TheresultinglogiccalledQPTL[20]isasexpressiveasS1S,themonadicsecond-ordertheoryofsequencesbutitsdeci-sionprocedurehasnon-elementarytimecomplexity.Thesecondrouteconsistsofaugmentinglineartimetemporallogicwiththesocalledautomatoncon-nectives.TheresultinglogiccalledETL[26]isequalinexpressivepowertoS1Swhileadmittinganexponentialtimedecisionprocedure.Ourlogicis,inspirit,inspiredbyETLanditcanbeeasilytranslatedintoETL.Itmayappeartobeat rstsighttobeamerereformulationofETLwithsomecosmeticchanges.Thishoweverhastodowiththeinstinctiveidenti cationonemakesbetween nitestateautomataandregularexpressions.InfactDLTLisquitedi erentintermsofthemechanismsito ersforstructuringformulasandwefeelthatitismoretransparentandeasiertoworkwith.Theresultsandtheproofswepresentherearedesignedtosupportthisclaim.Ourapproachalsoleadstosmoothgeneralizationsinnon-sequentialsettingswheresimilarextensionsintermsofETLwillbehardtocopewith.Inthenextsectionwestartwithanaction-basedversionofoflineartimetemporallogicinorderto xterminology.InSection3wepresentDLTLanditssemantics.Thisisthenfollowedbyamoredetailedassessmentofthesimilaritiesandthedi erencesbetweenETLandDLTL.InSection4weprovethedecidabilityofDLTLbyreducingittotheemptinessproblemforB uchiautomata.InSection5weshowthatDLTL ,asublogicofDLTL,hasthesameexpressivepowerasS1S,themonadicsecond-ordertheoryofsequences.Wethenestablishsimilarresultsforthe rst-orderfragmentofS1Swiththehelpofthe\star-freefragmentsofDLTLandDLTL .InSection6,weextendtheaxiomatizationofPDL(propositionaldynamiclogic)andthecompletenessproofin[11]toobtain nitaryaxiomatizationsofDLTLandDLTL .Inthe nalsectionwepointtoanaturalgeneralizationin2thesettingofdistributedsystems.Thisgeneralizationiseminentlyaccessibleando ersadditionalsupporttoourbeliefthatthesynthesisofdynamicandtemporallogicsinalineartimeframeworkaspursuedhereisafruitfulone.2LinearTimeTemporalLogicOnekeyfeatureofthesyntaxandsemanticsofourtemporallogicisthetreatmentofactionsas rstclassobjects.TobringthisoutweformulateaversionofLTL(lineartimetemporallogic)inwhichthenext-statemodalityisindexedbyactionstakenfroma xedalphabetset.Throughtherestofthepaperwe xa nitenon-emptyalphabet .Weleta;brangeover andrefertomembersof asactions. isthesetof nitewordsand !isthesetofin nitewordsgeneratedby with!=f0;1;2;:::g.Weset 1= [ !anddenotethenullwordby.Welet ; 0rangeover !and ; 0; 00rangeover .Finally istheusualpre xorderingde nedover andforu2 1,weletprf(u)bethesetof nitepre xesofu.Nextwe xacountablesetofatomicpropositionsP=fp1;p2;:::gandletp;qrangeoverP.ThesetofformulasofLTL( )isthengivenbythesyntax:LTL( )::=pj j _ jhai j U :Throughtherestofthissection ; willrangeoverLTL( )
本文标题:Dynamic Linear Time Temporal Logic
链接地址:https://www.777doc.com/doc-5930072 .html