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

1、09 Apr 2002CS 367-Theory of Hybrid Automata1Theory of Hybrid AutomataSachin J Mujumdar09 Apr 2002CS 367-Theory of Hybrid Automata2Hybrid AutomataA formal model for a dynamical system with discrete and continuous componentsExample Temperature Control09 Apr 2002CS 367-Theory of Hybrid Automata3Formal

2、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)123,.,nXx xxx123,

3、.,nXx xxx123,.,nXx xxx09 Apr 2002CS 367-Theory of Hybrid Automata4Formal 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,“ju

4、mp”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()vV XR R09 Apr 2002CS 367-Theory of Hybrid Automata5Safe Semantics Execution of Hybrid Automaton continuous cha

5、nge(flows)and discrete change(jumps)Abstraction to fully discrete transition system Using Labeled Transition Systems09 Apr 2002CS 367-Theory of Hybrid Automata6Labeled Transition SystemsLabeled Transition System,SState Space,Q (Q0 initial states)Transition Relations Set of labels,A possibly infinite

6、 Binary Relations on Q,Region,R QTransition triplet ofa aqq 09 Apr 2002CS 367-Theory of Hybrid Automata7Labeled Transition SystemsTwo Labeled Transition SystemsTimed Transition System Abstracts continuous flows by transitions Retains info on source,target&duration of flowTime-Abstract Transition Sys

7、tem Also abstracts the duration of flows Called timed-abstraction of Timed Transition SystemstHSaHS09 Apr 2002CS 367-Theory of Hybrid Automata8Usually consider the infinite behavior of hybrid automaton.Thus,only infinite sequences of transitions consideredTransitions do not converge in timeDivergenc

8、e of time livenessNonzeno Cant prevent time from divergingLive Semantics09 Apr 2002CS 367-Theory of Hybrid Automata9Live 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

9、 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 System1iaiiqq 09 Apr 2002CS 367-Theory of Hybrid Automata10Composition of Hybrid AutomataTwo Hybrid Automata,H1&H2In

10、teract 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 2002CS 367-Theory of Hybrid Automata11Composition of Hybrid AutomataProduct of Transition SystemsLa

11、beled Transition Systems,S1&S2Consistency Check Associative partial function Denoted by Defined on pairs consisting of a transition from S1&a transition from S2S1 x S2 w.r.t State Space Q1 x Q2 Initial States Q01 x Q02 Label Set range()Transition Condition and 111aqq 222aqq 1212(,)(,)aq qq q 09 Apr

12、2002CS 367-Theory of Hybrid Automata12Composition of Hybrid AutomataParallel CompositionH1 and H2 of and of are consistent if one of the 3 is true a1=a2 consistency check yields a1 a1 belongs to Event space of H1 and a2=0 consistency check yields a1 a2 belongs to Event space of H2 and a1=0 consisten

13、cy check yields a1The Parallel Composition is defined to be the cross product w.r.t the consistency check111aqq 222aqq 1tHS2tHS09 Apr 2002CS 367-Theory of Hybrid Automata13Railroad Gate Control-ExampleCircular track,with a gate 2000 5000 m circumferencex distance of train from gatespeed b/w 40 m/s&5

14、0 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 2002CS 367-Theory of Hybrid Automata14Railroad Gate Control-Example09 Apr 2002CS 367-Theory of Hybrid Automata15Railroad Gate Control-Example09 Ap

15、r 2002CS 367-Theory of Hybrid Automata16Railroad 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 2002CS 367-Theory of Hybrid Automata17Verification4 paradigmatic Qs about the traces of the

16、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,

17、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 2002CS 367-Theory of Hybrid Automata18Rectangular AutomataFlow Conditions are independent of Control ModesFirst derivative,x dot,of each variable has

18、 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 w

19、ith control switchesTriangular Automata allows for comparison of variables09 Apr 2002CS 367-Theory of Hybrid Automata19State Space of Hybrid AutomataState Space is infinite cannot be ennumeratedStudied using finite symbolic representationx real numbered variable1=x=5 Finite symbolic representation o

20、f an infinite set of real numbers09 Apr 2002CS 367-Theory of Hybrid Automata20Observational 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 al

21、l 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 2002CS 367-Theory of Hybrid Automata21SummaryInt

22、roduction 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.Henzinger