Theory-of-Hybrid-Automata：混合自動(dòng)機(jī)理論課件

1、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

2、 following:Variables Finite Set (real numbered)Continuous Change, Values at conclusion at of discrete change,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 De

3、finitionInitial, 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 Jump ConditionsEdge Labeling function, “jump” for every control switch, e EFree Variables from X U XEventsFinite s

4、et 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 transi

5、tion 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

6、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 Time

7、d 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

8、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

9、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

10、 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 parti

11、al 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 H

12、2 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 consi

13、stency 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”ProblemTrai

14、n 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 3

15、67 - 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

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

17、Given 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

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

19、 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 Fin

20、ite 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 visitedS