Theory of Hybrid Automata：混合自动机理论.pptVIP

09 Apr 2002 CS 367 - Theory of Hybrid Automata Theory of Hybrid Automata Sachin J Mujumdar Hybrid Automata A formal model for a dynamical system with discrete and continuous components Example – Temperature Control Formal Definition A Hybrid Automaton consists of 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) Formal Definition Initial, Invariant Flow conditions – vertex labeling functions init(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 X’ Events Finite set of events, Σ Edge labeling function, event: E ? Σ, for assigning an event to each control switch Continuous State – points in Safe Semantics Execution of Hybrid Automaton – continuous change (flows) and discrete change (jumps) Abstraction to fully discrete transition system Using Labeled Transition Systems Labeled Transition Systems Labeled 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 of Labeled Transition Systems Two 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 timed-abstraction of Timed Transition Systems Live Semantics Usually 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 diverging Live Transition Systems Trajectory of S (In)Finite Sequence of ai, qii≥1