MAE 6740 CS 6 Hybrid Systems Prof Hadas Kress Gazit haDAS kress gaZEET hadaskg cornell edu 8 25 2011 When where who T R 10 10 11 25 Upson 111 Website http web mae cornell edu hadaskg courses mae6740 html Hadas Kress Gazit 210 Upson hadaskg cornell edu Office hours Tuesday 3 4PM or by appointment Hybrid systems What are they and why do we care Hybrid system Hybrid systems Systems with both continuous and discrete dynamics Continuous time Differential equations Infinite uncountable state space Discrete event Automata languages Usually finite state Can model Continuous systems with identifiable modes Bouncing ball K J Johansson M Egerstedt J Lygeros and S Sastry On the regularization of zeno hybrid automata Systems and Control Letters 38 141 150 1999 Can model Continuous systems with identifiable modes Walking robot Moore E Z Campbell D Grimminger F Buehler M Reliable stair climbing in the simple hexapod RHex Robotics and Automation IEEE International Conference on vol 3 no pp 2222 2227 2002 Can model Continuous systems with identifiable modes Biological systems Can model Continuous systems with identifiable modes Robot motion D Conner Integrating Planning and Control for Constrained Dynamical Systems doctoral dissertation tech report CMURI TR 08 01 Robotics Institute Carnegie Mellon University January 2008 H Kress Gazit D C Conner H Choset A Rizzi and G J Pappas Courteous cars Decentralized multiagent traffic coordination IEEE Robotics and Automation Magazine March 2008 Can model Embedded systems discrete logic controls continuous systems BMW 72 networked microprocessors Boeing 777 1280 networked microprocessors Can model Embedded systems discrete logic controls continuous systems Nuclear reactor Modes Without rods With rod 1 With rod 2 T 0 1 T 50 T 0 1 T 56 T 0 1 T 60 Rod 1 and 2 cannot be used simultaneously Once a rod is removed you cannot use it for 10 minutes Specification Keep temperature between 510 and 550 degrees If T 550 then either a rod is available or we shutdown the plant Discrete logic Rod1 NoRod Shutdown Rod2 Hybrid model T 510 y1 10 y2 10 Rod1 T 0 1 T 56 y1 1 y2 1 T 510 T 550 y1 10 T 510 y1 0 NoRod T 0 1 T 50 y1 1 y2 1 T 550 T 550 y2 10 T 510 y2 0 T 550 y1 10 y2 10 Analysis Is shutdown reachable Algorithmic verification NO Shutdown T 0 1 T 50 y1 1 y 2 1 true Rod2 T 0 1 T 60 y1 1 y2 1 T 510 Can model Continuous systems with hybrid specifications Can model Coordination of continuous systems Automated Highway System Pravin Varaiya Smart cars on smart roads problems of control IEEE Transactions on Automatic Control AC 38 2 195 207 1993 Can model Synchronization of continuous hybrid discrete systems Train gate example x raise approach lower exit Controller System Train Gate Controller Safety specification If train is within 10 meters of the crossing then gate should completely closed Liveness specification Keep gate open as much as possible Train model x 2000 near far 50 x 40 x 1000 x 1000 approach exit x 100 x 2000 past x 0 50 x 30 50 x 30 x 0 x 100 Gate model raise open raising 90 9 raise 0 90 lower raise 90 90 lower raise lowering 9 0 lower closed 0 0 0 lower Controller model y 0 exit true Going tolower y 1 y d y 0 approach lower idle y 0 exit true raise y 1 y 0 approach Going to raise y 1 y d Synchronized transitions x 2000 near far 50 x 40 x 1000 x 1000 approach exit past x 0 50 x 30 50 x 30 x 0 x 100 x 100 x 2000 y 0 exit true Going tolower y 1 y d y 0 approach lower y 0 Going to raise exit y 1 true raise idle y 1 y 0 approach y d Verifying the controller x raise approach lower exit Controller System Train Gate Controller Safety specification Can we avoid the set 0 10 x 10 Parametric verification YES if d 49 5 And many more examples Questions Issues Is the model good Is it tractable Can we abstract refine it Is the system stable Is it safe Does it do what we want it to do How can we make it stable safe Interest Community Cyber Physical Systems Identified as a technical priority in the 2007 PCAST report http www ostp gov pdf nitrd review pdf HSCC http hscc2011 cs sunysb edu part of CPS week http www cpsweek org Objective of this course Provide an overview of hybrid systems modeling control and verification techniques Common language for disjoint disciplines traditional control and computer science Will NOT cover every aspect of the field Tentative schedule Modeling 5 lectures General formulation Trajectories continuous and discrete behaviors Special classes of HS Analysis abstractions 4 lectures Stability Simulation Bisimulation Reachability Tentative schedule Verification 5 lectures Barrier certificates SOS Simulation based methods Temporal logics Model checking Deductive verification Tools Control 4 lectures Game theoretic Logic based optimal control Symbolic control Tentative schedule Stochastic HS 2 lectures Markov chains Probabilistic analysis Topics 2 lectures Systems biology Model reduction Project presentations 2 lectures Prerequisites Undergraduate level courses in linear algebra and differential equations Knowledge of Linear system theory and automata theory is helpful This course is intended for students from different disciplines and as such will provide the necessary background material This is an advanced graduate class with open ended assignments and cutting edge topics Text No required textbook List of references links on website Handouts Lecture notes Skeletons posted before the lecture Grading and philosophy Paper presentation s done in pairs 30 Two mini projects 30 Course project 40 Ideally tied to your research Proposal 1 2 pages due tentatively on Nov 8 Final report 6 pages max due on Dec 12 Presentation last 2 classes Possible projects Model analyze verify a hybrid system Survey a few related recent papers Audit Paper presentation s done in pairs 30 Two mini projects 30 Course project 40 Paper presentations Scheduling Doodle poll Max of 4 people per day 2 papers Email will be sent out Tuesday 8 30 after class Papers Will be provided posted on website Can choose to do a different paper need to run it by me at least 10 days in advance Rubrics