时间自动机课件

OutlineThetheoryofTimedautomataAcasestudyFirstintroducedbyRajeevAlurandDavidL.Dillin1990,RajeevAlurandDavidL.Dill.Automataformodelingreal-timesystems.InProceedings,

17thInternationalColloquiumonAutomata,LanguagesandProgramming,1990.R.AlurandD.L.Dill.:`Atheoryoftimedautomata‘InTheoret.Comput.Sci.,Vol.126,No.2,1994,pp.183-235Afinite-stateBuchiautomatonextendedwithasetofrealvaluevariablesTimedsafetyautomata

OffLightBrightPressPressPressPressWANT:ifpressisissuedtwice

quicklythenthelightwillgetbrighter;otherwisethelightisturnedoff.

SimpleLightControlSimpleLightControlOffLightBrightSolution:Addareal-valuedclockx

x:=0x<=3x>3PressPressPressPressAddingcontinuousvariablestostatemachinesTimedAutomatanmaClocks:

x,yx<=5&y>3x:=0GuardBooleancombinationofcomparisonswithInteger/rationalboundsResetActionperformedonclocks(

n,x=2.4,y=3.1415)

(

n,x=3.5,y=4.2415)wait(1.1)Transitions(

n,x=2.4,y=3.1415)

(

m,x=0,y=3.1415)aState

(

location,x=v,y=u)wherev,uareinRAction

forsynchronizationnmaClocks:

x,yx<=5&y>3x:=0Transitions:(

n,x=2.4,y=3.1415)

(

n,x=3.5,y=4.2415)

wait(1.1)(

n,x=2.4,y=3.1415)

wait(3.2)x<=5y<=10LocationInvariantsg1g2g3g4

Invariantsensureprogress!!AddingInvariantsTimedAutomata：SyntaxTimedAutomata:atuple(L,l0,A,V,I,E)L:afinitesetoflocationsl0:initiallocationsA:afinitesetoflabels(alphabet)V:afinitesetofclockvariablesI:alocationconstrainfunctionE:afinitesetofedges.Eachedgehasasourcelocationl,atargetlocationl‘Guardg(variableconstrain)LabelainA(elabelsalsoallowed)AsubsetuofclockvariablestoberesetTimedAutomata:Semantics

ForatimedautomatonA,defineaninfinite-statetransitionsystemS(A)

States

Q:astateqisapair(l,v),wherelisalocation,andvisaclockvector,mappingclocksinXtoR+,satisfyingI(l)

(l0,v)is

initialstate

iflisinV0andv(x)=0

Elapseoftimetransitions:foreachnonnegativerealnumberd,(l,v)-d->(l,v+d)ifbothvandv+d

satisfyI(l)Locationswitchtransitions:(l,v)-a->(l’,v’)ifthereisanedge(l,a,g,l,l’)suchthatvsatisfiesgandv’=v[l:=0]ParallelCompositionTheproductofautomataWeusetimedautomatanetworktomodelthemProductConstructionABx<4x:=0x>3aba|a,x:=0abcCDy<4y:=0y>3bb|b,y:=0bcACBCx<4x:=0x>3ab,y:=0a|a,x:=0ADy<4y>3cBDx<4y<4x>3,b|x>3,b,y:=0a|a,x:=0y>3ca,x:=0Verification

SystemmodeledastimedautomatanetworksPropertiesspecifiedasCTLformulars.VerificationproblemreducedtoreachabilityortotemporallogicmodelcheckingApplicationsReal-timecontrollersAsynchronoustimedcircuitsSchedulingDistributedtiming-basedalgorithmsspecificationofthegoal系统需求现实environmentPLCprogramPLCfulfilsVerificationgoalspecificationoftheenvironmentspecificationofthecontrol系统规范结构描述

plantdiagramPLCprogramModelcheckingspecificationofthegoal系统需求automatonfortheplantautomatonfortheprogramModelcheckingspecificationofthegoal系统需求automatonfortheplantautomatonfortheprogramT_plant||T_program|=Property模型检测：APLCControlSystemInTheaterSteevecontroller:Partofatheatermachinerycontrolsystem

Steeve

usedforpullinglightandscreen,canmoveupanddown,locatedatanypresetheight,poweredbymotor.Range15-195ControlmodeAutomatic:giventhetargetheight,thesteeveachieveautomaticlly.Manual:

usercanletthesteevemoveup,downandstop

StructureofSteeveControlSystemRequirementsInnaturallanguageThesteevestopsattherequiredheight.Thesteevemustmoveunderthesafetyrange,cannotexceedtheupperandlowerbounds.Makesurethewholeoperationcanbefinishedwithin60s.Modelingbytimedautomata9signalsaredefinedforsynchronization,theyarestop,start,up,down,impulse,inc,cw,acw

andsp.Onesignalissharedbytwocomponentsfortheirsynchronization

Therelationshipoftheheightandtheimpulsenumberis:impulse_number=height*21timeunitis0.01sUserAutomatonFiniteautomataa=1:automaticmode.

a=0:manualmode

Ifwewanttosimulateasequenceofoperations,canbemodeledasTAMotorAutomatonmotorwithfixedspeedsensorissuesanimpulseevery2timeunits.Constrainformulay<=2belongstoI(rt_acw)Cyclictransition,y

isresetto0,signalimpulseisissuedeverytwotimeunitesuntilstopordersp

isreceivedSensorAutomatonThereistimedelaybetweensensorreceivingimpulseandsendinginc

tocontroller.Thedelayisbelow1timeunite.Clockvariablex

isusedtorepresentthetimedelay.ControllerAutomatonFunctionCmp,convert,nhigh,nlow,chVariablesh_req:requiredheighth_curr:currentheightmtargetcountingnumberncurrentcountingnumberControllertraces8traces,halfforrisingup,halfforfallingdown.AutomaticmodeUsergivesarequiredheight,thesteevereachesthere.(0,3,5,7,0)Beforereachingthere,usersuddenlystopit.(0,3,5,8,0)ManuelmodePressup,laterpressstop.(0,1,5,8,0)Forgettopressstop,whenreachthebound,motorisforcedtostop.(0,1,5,10,0)PropertyverificationUsetoolUppaalAtimedautomataverificationtoolPropertiesdescriptionAsimpliedversionofCTL:temporaloperatorsareF(<>)andG([])PropertyverificationthesystemshouldbedeadlockfreeA[]notdeadlockIntheautomaticmode,whentheusersetstherequiredheight,thesteeveshouldeventuallyreac