Hybrid Systems Theory presented by Tom HenzingerSlide 2Slide 3Slide 4Slide 5Slide 6Slide 7Slide 8Slide 9Slide 10Slide 11Slide 12Hybrid Systems TheorySlide 21Slide 22Slide 23Slide 24Slide 25Compositional Hybrid Systems Modeling and Simulation I: HyVisual (based on Ptolemy II)Compositional Hybrid Systems Modeling and Simulation II: Generating SIMULINK models from Hybrid Bond GraphsSlide 28Continuous System Verification: ProblemContinuous System Verification: ApproachContinuous System Verification: ImplementationFrom Continuous to Hybrid System VerificationSlide 33Slide 34NSFFoundations of Hybrid and Embedded Software SystemsUC Berkeley: ChessVanderbilt University: ISISUniversity of Memphis: MSIProgram ReviewMay 10, 2004Berkeley, CAHybrid Systems Theory presented by Tom Henzinger1. Robust hybrid systems 2. Stochastic hybrid systems 3. Compositional hybrid systems 4. Computational hybrid systemsCHESS Program Review, May 10, 2004 2A Formal Foundation for Embedded Systemsneeds to combineComputationPhysicality+Theories of -composition & hierarchy -computability & complexityBTheories of -robustness & approximation -probabilities & discountingRCHESS Program Review, May 10, 2004 3Continuous Dynamical SystemsState space: Rn Dynamics: initial condition + differential equationsRoom temperature: x(0) = x0 x’(t) = -K·x(t)xtx0Analytic complexity.CHESS Program Review, May 10, 2004 4Discrete Transition SystemsState space: Bm Dynamics: initial condition + transition relationHeater:heattofonof onCombinatorial complexity.CHESS Program Review, May 10, 2004 5Hybrid AutomataState space: Bm  Rn Dynamics: initial condition + transition relation + differential equationsThermostat:tofonx0ofx’ = -K·xonx’ = K·(H-x)x  lx  ux  Ux  LCHESS Program Review, May 10, 2004 6slightly perturbed automatonThe Robustness IssueHybrid AutomatonPropertyCHESS Program Review, May 10, 2004 7SafeHybrid Automatonx = 3The Robustness IssueCHESS Program Review, May 10, 2004 8UnsafeHybrid Automatonx = 3+The Robustness IssueCHESS Program Review, May 10, 2004 9value(Model,Property): States  Bvalue(Model,Property): States  R Towards Robust Hybrid AutomataCHESS Program Review, May 10, 2004 10value(Model,Property): States  Bvalue(m,T) = (X) (T  pre(X))discountedValue(Model,Property): States  RdiscountedValue(m,T) = (X) max(T, pre(X))discount factor 0<<1 Towards Robust Hybrid AutomataCHESS Program Review, May 10, 2004 11a cbReachability (coSafety)  c … undiscounted propertyT(F Ç pre(T)) = T T 2  c … discounted property 1 max(0,  ¢  pre(1)) = CHESS Program Review, May 10, 2004 12Robustness Theorem [de Alfaro, Henzinger, Majumdar]:If discountedBisimilarity(m1,m2) > 1 - , then |discountedValue(m1,p) - discountedValue(m2,p)| < f().Further Advantages of Discounting:-approximability because of geometric convergence (avoids non-termination of verification algorithms)-applies also to probabilistic systems and to games(enables reasoning under uncertainty, and control)Main Result (so far, only for discrete systems)CHESS Program Review, May 10, 2004 20 Hybrid Systems Theory1 Robust hybrid systems2 Stochastic hybrid systemsTheory of discounting. Timed and stochastic games and optimal control.CHESS Program Review, May 10, 2004 21 Hybrid Systems Theory1 Robust hybrid systems2 Stochastic hybrid systemsTheory of discounting. Timed and stochastic games and optimal control.3 Compositional hybrid systems4 Computational hybrid systemsAgent algebras and interface theories. Hybrid systems simulation (Ptolemy II, GME). Hybrid systems verification (polyhedral & ellipsoidal methods). Code generation from hybrid systems (Ptolemy II, Giotto).CHESS Program Review, May 10, 2004 22ModelRequirementsResourcesVerificationImplementationEnvironmentautomatic (model checking)automatic (compilation)The Compositionality IssueCHESS Program Review, May 10, 2004 23ComponentRequirementsResourcesVerificationImplementationComponentThe Compositionality IssueCompositionno change necessaryno change necessaryCHESS Program Review, May 10, 2004 24ComponentRequirementsResourcesVerificationImplementationComponentThe Compositionality IssueCompositionno change necessaryno change necessary(time, fault tolerance, etc.)CHESS Program Review, May 10, 2004 25ComponentRequirementsResourcesVerificationImplementationComponentThe Compositionality IssueCompositionno change necessaryno change necessary(time, fault tolerance, etc.)Agent algebras. Interface theories.Virtual machines.CHESS Program Review, May 10, 2004 26HyVisual is being used to nail down an operational semantics for hybrid systems.Compositional Hybrid Systems Modeling and Simulation I: HyVisual (based on Ptolemy II)CHESS Program Review, May 10, 2004 27Compositional Hybrid Systems Modeling and Simulation II: Generating SIMULINK models from Hybrid Bond GraphsTHE SIMULINK ENVIROMENT• Using Simulink blocks and subsystems we can create a block diagram that corresponds to the Hybrid Bond Graph in GME. • Simulink provides variable step solvers for the simulation of ODEs, with error control and zero crossing detection.GMESIMULINKTwo Tank ExampleTank1 Pressure Tank2 PressureCHESS Program Review, May 10, 2004 28 Hybrid Systems Theory1 Robust hybrid systems2 Stochastic hybrid systemsTheory of discounting. Timed and stochastic games and optimal control.3 Compositional hybrid systems4 Computational hybrid systemsAgent algebras and interface theories. Hybrid systems simulation (Ptolemy II, GME). Hybrid systems verification (polyhedral & ellipsoidal methods). Code generation from hybrid systems (Ptolemy II, Giotto).CHESS Program Review, May 10, 2004 29Continuous System Verification: ProblemGiven •control system•control set•target set Consider decision problemsCHESS Program Review, May 10, 2004 30Continuous System Verification: Approach1. Express decision problems as optimization problems2. Derive Hamilton-Jacobi-Bellman (HJB) partial diferential equation of value functions3. Obtain support functions of using convex analysis4. Obtain tight outer and inner ellipsoidal approximations toCHESS Program Review, May 10, 2004 311. Matlab ‘toolbox’ to calculate ellipsoidal approximations and display