《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 components Example Temperature Control09 Apr 20022CS 367 - Theory of Hybrid AutomataFormal DefinitionA Hybrid Automaton consists o
2、f following: Variables Finite Set (real numbered)Continuous Change, Values at conclusion at of discrete change,Control Graph Finite Directed Multigraph (V, E) V control modes (represent discrete state) E control switches (represent discrete dynamics)09 Apr 20023CS 367 - Theory of Hybrid AutomataForm
3、al DefinitionInitial, Invariant & Flow conditions vertex labeling functionsinit(v) initial condition whose free variable are from X inv(v) free variables from X flow(v) free variables from X U Jump Conditions Edge Labeling function, “jump” for every control switch, e E Free Variables from X U XEvent
4、s Finite 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 Semantics Execution of Hybrid Automaton continuous change (flows) and discrete change (jumps) Abstraction to fully dis
5、crete transition system Using Labeled Transition Systems09 Apr 20025CS 367 - Theory of Hybrid AutomataLabeled Transition SystemsLabeled Transition System, S State Space, Q (Q0 initial states) Transition Relations Set of labels, A possibly infinite Binary Relations on Q,Region, R Q Transition triplet
6、 of09 Apr 20026CS 367 - Theory of Hybrid AutomataLabeled Transition SystemsTwo Labeled Transition Systems Timed Transition System Abstracts continuous flows by transitions Retains info on source, target & duration of flow Time-Abstract Transition System Also abstracts the duration of flows Called ti
7、med-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 considered Transitions do not converge in time Divergence of time liveness Nonzeno Cant prevent time from
8、divergingLive Semantics09 Apr 20028CS 367 - Theory of Hybrid AutomataLive Transition SystemsTrajectory of S (In)Finite Sequence of i1 Condition q0 rooted trajectory If q0 is initial state, then intialized trajectory Live Transition System (S, L) pair L infinite number of initialized trajectories of
9、S Trace i1 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 & H2 Interact via joint events a is an eve
10、nt of both Both must synchronize on a-transitions a is an event of only H1 each a-transition of H1 synchronizes with a 0 -duration time transition of H2 Vice-Versa09 Apr 200210CS 367 - Theory of Hybrid AutomataComposition of Hybrid AutomataProduct of Transition Systems Labeled Transition Systems, S1
11、 & S2 Consistency Check Associative partial function Denoted by Defined on pairs consisting of a transition from S1 & a transition from S2 S1 x S2 w.r.t State Space Q1 x Q2 Initial States Q01 x Q02 Label Set range( ) Transition Condition and 09 Apr 200211CS 367 - Theory of Hybrid AutomataComposition
12、 of Hybrid AutomataParallel Composition H1 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 consistency check yields a1The Parallel Composition
13、 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 circumference x distance of train from gate speed b/w 40 m/s & 50 m/s x = 1000 m “approach” event may slow down to 30 m
14、/s x = -100 m (100m past the gate) “exit event”Problem Train Automaton Gate Automaton Controller Automaton09 Apr 200213CS 367 - Theory of Hybrid AutomataRailroad Gate Control - ExampleTrain Automaton09 Apr 200214CS 367 - Theory of Hybrid AutomataRailroad Gate Control - ExampleGate Automatony positio
15、n of gate in degrees (max 90) 9 degrees / sec09 Apr 200215CS 367 - Theory of Hybrid AutomataRailroad Gate Control - ExampleController Automatonu reaction delay of controller z 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 H Reachability For any H, given a control mode, v, if there exists some initialized trajectory for i
