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

《Theory-of-Hybrid-Automata：混合自动机理论课件》由会员分享，可在线阅读，更多相关《Theory-of-Hybrid-Automata：混合自动机理论课件（21页珍藏版）》请在装配图网上搜索。

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 fol

2、lowing: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 Definition

3、3.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 event

4、s,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 Lab

5、eled 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 Autom

6、ataLabeled 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 2002

7、7CS 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 Au

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

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

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

11、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 cons

12、istency 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

13、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 Hybr

14、id 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 de

15、lay 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 Labe

16、led 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 ProblemS

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

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

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

20、 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 wi

21、th 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