Theory-of-Hybrid-Automata：混合自动机理论课件

Theory of Hybrid AutomataSachin J Mujumdar09 Apr 20021CS 367-Theory of Hybrid AutomataHybrid AutomataA formal model for a dynamical system with discrete and continuous componentsExample Temperature Control09 Apr 20022CS 367-Theory of Hybrid AutomataFormal DefinitionA Hybrid Automaton consists of following:1.Variables Finite Set(real numbered)Continuous Change,Values at conclusion at of discrete change,2.Control GraphFinite Directed Multigraph(V,E)V control modes(represent discrete state)E control switches(represent discrete dynamics)09 Apr 20023CS 367-Theory of Hybrid AutomataFormal Definition3.Initial,Invariant&Flow conditions vertex labeling functionsinit(v)initial condition whose free variable are from Xinv(v)free variables from Xflow(v)free variables from X U 4.Jump ConditionsEdge Labeling function,“jump”for every control switch,e EFree Variables from X U X5.EventsFinite set of events,Edge labeling function,event:E ,for assigning an event to each control switchContinuous State points in 09 Apr 20024CS 367-Theory of Hybrid AutomataSafe SemanticsExecution of Hybrid Automaton continuous change(flows)and discrete change(jumps)Abstraction to fully discrete transition systemUsing Labeled Transition Systems09 Apr 20025CS 367-Theory of Hybrid AutomataLabeled Transition SystemsLabeled Transition System,SState Space,Q (Q0 initial states)Transition RelationsSet of labels,A possibly infiniteBinary Relations on Q,Region,R QTransition triplet of09 Apr 20026CS 367-Theory of Hybrid AutomataLabeled Transition SystemsTwo Labeled Transition SystemsTimed Transition System Abstracts continuous flows by transitionsRetains info on source,target&duration of flowTime-Abstract Transition SystemAlso abstracts the duration of flowsCalled timed-abstraction of Timed Transition Systems09 Apr 20027CS 367-Theory of Hybrid AutomataUsually consider the infinite behavior of hybrid automaton.Thus,only infinite sequences of transitions consideredTransitions do not converge in timeDivergence of time livenessNonzeno Cant prevent time from divergingLive Semantics09 Apr 20028CS 367-Theory of Hybrid AutomataLive Transition SystemsTrajectory of S(In)Finite Sequence of i1 Condition q0 rooted trajectoryIf q0 is initial state,then intialized trajectoryLive Transition System(S,L)pairL infinite number of initialized trajectories of STracei1 is finite initialized trajectory of S,or trajectory in L corresponding sequence i1 of labels is a Trace of(S,L),i.e.the Live Transition System09 Apr 20029CS 367-Theory of Hybrid AutomataComposition of Hybrid AutomataTwo Hybrid Automata,H1&H2Interact via joint eventsa is an event of both Both must synchronize on a-transitionsa is an event of only H1 each a-transition of H1 synchronizes with a 0-duration time transition of H2Vice-Versa09 Apr 200210CS 367-Theory of Hybrid AutomataComposition of Hybrid AutomataProduct of Transition SystemsLabeled Transition Systems,S1&S2Consistency CheckAssociative partial functionDenoted by Defined on pairs consisting of a transition from S1&a transition from S2S1 x S2w.r.t State Space Q1 x Q2Initial States Q01 x Q02Label Set range()Transition Condition and 09 Apr 200211CS 367-Theory of Hybrid AutomataComposition of Hybrid AutomataParallel CompositionH1 and H2 of and of are consistent if one of the 3 is truea1=a2 consistency check yields a1a1 belongs to Event space of H1 and a2=0 consistency check yields a1a2 belongs to Event space of H2 and a1=0 consistency check yields a1The Parallel Composition is defined to be the cross product w.r.t the consistency check09 Apr 200212CS 367-Theory of Hybrid AutomataRailroad Gate Control-ExampleCircular track,with a gate 2000 5000 m circumferencex distance of train from gatespeed b/w 40 m/s&50 m/sx=1000 m“approach”eventmay slow down to 30 m/sx=-100 m(100m past the gate)“exit event”ProblemTrain AutomatonGate AutomatonController Automaton09 Apr 200213CS 367-Theory of Hybrid AutomataRailroad Gate Control-ExampleTrain Automaton09 Apr 200214CS 367-Theory of Hybrid AutomataRailroad Gate Control-ExampleGate Automatony position of gate in degrees(max 90)9 degrees/sec09 Apr 200215CS 367-Theory of Hybrid AutomataRailroad Gate Control-ExampleController Automatonu reaction delay of controllerz clock for measuring elapsed timeQuestion:value of“u”so that,y=0,whenever-10=x=1009 Apr 200216CS 367-Theory of Hybrid AutomataVerification4 paradigmatic Qs about the traces of the HReachabilityFor any H,given a control mode,v,if there exists some initialized trajectory for its Labeled Transition System(LTS),can it visit the state of the form (v,x)?EmptinessGiven H,if there exists a divergent initialized trajectory of the LTS?(Finitary)Timed Trace Inclusion ProblemGiven H1&H2,if every(finitary)timed trace of H1 is also that of H2(Finitary)Time-Abstract Trace Inclusion ProblemSame as above consider time-abstract traces09 Apr 200217CS 367-Theory of Hybrid AutomataRectangular AutomataFlow Conditions are independent of Control ModesFirst derivative,x dot,of each variable has fixed range of values,in every control modeThis is independent of the control switchesAfter a control switch value of variable is either unchanged or from a fixed set of possibilitiesEach variable becomes independent of other variablesMultirectangular Automata allows for flow conditions that vary with control switchesTriangular Automata allows for comparison of variables09 Apr 200218CS 367-Theory of Hybrid AutomataState Space of Hybrid AutomataState Space is infinite cannot be ennumeratedStudied using finite symbolic representationx real numbered variable1=x=5 Finite symbolic representation of an infinite set of real numbers09 Apr 200219CS 367-Theory of Hybrid AutomataObservational Transition SystemsDifficult to(dis)prove the assertion about behavior of H sampling of only piecewise continuous trajectory of LTS at discrete time intervalsReminder Transition abstracts the information of all the intermediate states visitedSolutionLabel each transition with a regiontransition,t,is labeled with region,R,iff all intermediate&target states of t lie in Ri.e.Observational Transition System from continuous observation of hybrid automaton09 Apr 200220CS 367-Theory of Hybrid AutomataSummaryIntroduction to Hybrid SystemsFormal Definition of Hybrid SystemsChange from hybrid to fully-discrete systems-Safe SemanticsLabeled transition SystemsComposition of Hybrid AutomataProperties of Hybrid AutomataObservational Transition SystemsTheorems&Theories presented in paper,for further reading “The Theory of Hybrid Automata”Thomas A.Henzinger09 Apr 200221CS 367-Theory of Hybrid Automata