| 2/27/2010 | Sample midterm (handwritten scans) PDF and solutions PDF . |
| Note: All assignments will be due on 3/10/2010. | |
| 2/25/2010 | Assignment 6 ( comprehensive assignment on hybrid automaton). PDF . Due date is 3/10/2010. |
| 2/22/2010 | Midterm on march 3rd will cover lectures 1-12. Sample midterm and special office hrs. will be announced tomorrow. |
| 2/19/2010 | Assignment 5 (comprehensive assignment on timed automaton). PDF . Due date is 3/1/2010 or late on 3/3/2010 (wed). |
| 2/11/2010 | Assignment 4 (people without Simulink access only). PDF . Due date is 2/17/2010 (wed) or late on 2/22/2010 (monday) |
| 2/11/2010 | Assignment 4 (Simulink). PDF and tar ball with Simulink models . Due date is 2/17/2010 (wed) late on 2/22/2010 (mon). |
| 2/10/2010 | Simulink demo movie download (160 MB) |
| 2/4/2010 | Assignment 3 is to run/play around with Spin Tutorial/Demo is due Feb 10, 2010 (wednesday) or late on Feb. 17th (Wednesday). |
| Tarball for spin with hello world is here . | |
| To compile: "cd Src5.2.4" and run "make". | |
| helloWorld promela files are in the directory csci7000. | |
| More spin information at Spin webpage . | |
| 1/31/2010 | Assignment 2 is here is due Feb 8, 2010 (monday) or late on Feb. 10th (Wednesday). |
| 1/21/2010 | Assignment 1 is here is due Jan 27th, 2010 (Wed) or late on Feb. 1st (monday). |
| 1/20/2010 | Office hours will be on TW 11 a.m. to 12 noon @ECOT 624. |
| When | Mondays, Wednesdays (5 - 6:15 p.m) |
| Where | ECCR 139 |
| Instructor | Sriram Sankaranarayanan |
| Office Hours | Tuesdays, Wednesdays 11a.m - 12noon (ECOT 624), or by appointment. |
We will study a combination of basic ideas from automata theory and control theory to model and analyze these systems. These models are commonly used in design environments for control systems such as Simulink/Stateflow (tm), Scade(tm) and Labview(tm).
Systems with combined discrete and continuous behaviors are also
common the natural world. Many physical, chemical and biological
systems exhibit (almost) instantaneous discrete switches
that can affect the long term behavior of the system. Examples
include biochemical reaction mechanisms, cell signaling pathways,
quorum sensing in bacteria and cell interactions during embryonic
development.
Note: This course is NOT a substitute for a course on
embedded systems or real-time systems. Our two foci will be modeling
and verification.
| 1. | Review of Finite Automata and Discrete Event Systems. |
| 2. | Supervisory Control Theory. |
| 3. | Continuous Systems: Basics of Ordinary Differential Equations. |
| 4. | Modeling Formalisms: Statecharts, Simulink, Stateflow and Esterel. |
| 5. | Modeling Time: Discrete vs. Real Time, Timed Automata. |
| 6. | Formal Verification: Introduction. |
| 7. | Verification and Control of Timed Automata. |
| 8. | Modeling with Continuous Variables: Hybrid Automata. |
| 9. | Verification of Hybrid Automata (*) |
| 10. | Applications: Air Traffic, Robotics and so on (*) |
| 11. | Modeling biological systems using hybrid automata (*) |
Note: The symbol (*) denotes topics that will be covered partly through student presentations.
| Lec 1 | Introductory lecture: overview of the course |
| Slides: PDF | |
| Reading: Chapter 1 of Astrom and Murray's book (here) | |
| Watch this TED talk by Steven Strogatz. | |
| Lec 2 | Review of finite automata. Automata as system models. |
| Slides: PDF | |
| Lec 3 | Communicating Finite State Machines. |
| Slides: PDF | |
| Lecture Notes: PDF (updated 9pm 1/21/2010). | |
| Lec 4 | Finite Automata on Infinite Objects |
| Slides: PDF | |
| Lecture Notes: Finite-state Automata on Infinite Inputs by Madhavan Mukund . | |
| Note: We will cover the last 10 slides or so next lecture. | |
| Note-2: You may skip chapters 2 and 4 of the notes | |
| Lec 5 | Wrap up of Automata on Infinite Objects. |
| Slides: PDF | |
| Note: We will start on physical system models next week. | |
| Buchi Store: Buchi automata repository. | |
| Lec 6 | Models of Physical Systems |
| Slides: PDF | |
| Reading: Astrom and Murray, Chapter 2. | |
| Lec 7 | Models of Physical Systems (Simulation) |
| Slides: PDF | |
| Reading: Astrom and Murray, Chapter 2. | |
| Lec 8 | Timed Automata (Introduction) |
| Slides: PDF | |
| Reading: PDF . | |
| Lec 9 | Timed Automata (Closure + Region Construction) |
| Slides: PDF | |
| Reading (same as lec 8): PDF . | |
| Lec 10 | Timed Automata (Region Construction + Uppaal Demo) |
| Slides: PDF | |
| Lec 11 | Hybrid Automata (Introduction + Basic Properties) |
| Slides: PDF | |
| Reading-1: Chapter 3 of Lecture Notes on Hybrid Systems . | |
| Reading-2: Prof. Branicky's survey paper is a good overview. | |
| Lec 12 | Hybrid Automata (Semantics + Special Cases: multirate, rectangular, linear (affine) and non-linear) |
| Slides: PDF | |
| Reading-1: Chapter 3 of Lecture Notes on Hybrid Systems . | |
| Reading-2: Prof. Branicky's survey paper is a good overview. | |
| Lec 13 | Rectangular Hybrid Automata (Polyhedral Analysis) |
| Slides: PDF | |
| Lec 14 | Overview of reachability analysis techniques. |
| Reference: paper (esp. see related work) | |
| Lec 15 | Controller Synthesis (Supervisory Control) |
| Reference: book chapter | |
| Reference: Ramadge Wonham paper | |
| Lec 16 | Greg Emerson: Infinite games on finite graphs |
| Lecture Notes PDF | |
| Reference-1: Survey by Zielonka | |
| Reference-2: Survey by Gurevich | |
| Lecture 17 | Aditya Zutshi: Parameterized Systems and Counting Abstractions |
| Notes (evolving): PDF | |
| Reference-1 (Cache coherence protocol verification by Delzanno): PDF . | |
| Reference-2 (Modeling multi-robot systems by Correll and Martinoli): PDF . | |
| Lecture 18 | Zou Yun: Modeling Self-Assembling Systems. |
| Article-1 Klavins et al. IEEE Trans. Aut. Control PDF . | |
| Article-2 Whitesides survey PDF . | |
| Lecture 19 | Chris Cooper: Stochastic modeling of (bio) chemical reaction systems. |
| Notes (evolving): PDF | |
| Article-1 Gillespie's article on simulation PDF . | |
| Article-2 Arkin & McAdams PDF | |
| Lecture 20 | Daniel Fay: Markov Decision Processes and reinforcement learning. |
| Survey (on Markov Chains) PDF | |
| Survey PDF | |
| Inverted Helicopter Flight PDF youtube | |
| Lecture 21 | James Williamson: Timing Analysis for Cyber-Physical Systems. |
| Survey on challenges in CPS design PDF | |
| Paper on PRET architecture PDF | |
| Lecture 22 | Hadjar Homaie: Operator Errors in CPS and UI design |
| Paper on Automation Surprises here. | |
| Paper on Mistake Modeling PDF . | |
| Lecture 22 | Erwin Dunbar: SMT solvers k-induction and BMC for hybrid systems. |
| Paper on k-induction PDF | |
| Paper on BMC PDF | |
| Lecture 23 | Zyad Hassan: Probabilistics model checking (PRISM) |
| Paper on PRISM PDF | |
| Lecture 24 | Chenyu Zheng: Qualitative Reasoning. |
| Survey paper (long) PDF | |
| List of QR references here | |
| Lecture 24 | Concluding Lecture: Languages for Expressing CPS. |
| Video Link to CPSWeek Plenary here |
Graduate Students (CSCI 7000): First half of the course will involve short weekly assignments and an in class midterm. Second half will involve presenting a paper and a mini-project on modeling and verification. No homework assignments during this half.
Undergraduate Students (CSCI4830): First half of the course will involve short weekly assignments and an in class midterm. Second half will involve a project. Presenting a paper in class is not strictly required. However, participating in discussions centered around paper presentations with questions and comments is an important portion of this activity.
Paper presentations: Graduate students will be required to read and present a paper. This may include doing work on digging up related work, references, making slides and presenting to the class. Expect to present for 30-35 minutes. A list of paper topics will be made available. The presentations may have to be made individually (or in teams, if enrollment is high). The rest of the class will be expected to come prepared with questions.
Projects: Projects can be more open ended. Most projects will
involve solving an interesting control design problem, modeling your
solution as a cyber-physical system and proving some properties using
existing tools. This can also be an exercise in modeling a given
physical or biological phenomenon as a hybrid system and finding some
interesting properties of your model. A project report will be due in lieu
of the final.
Grading: Grades will be based on an absolute scale.
The overall score will be based on a combination of factors as below
(distance learning students see this note):
| Component | CSCI 7000 (grad) | CSCI 4830 (undergrad) |
| Assignments | 15% | 25% |
| Midterm | 25 % | 25% |
| Paper Presentations | 10% + 5% (participation) | 5% (participation) |
| Project | 35% | 35 % |
| Overall Participation | 10% | 10% |
| Total Score Range | Expected Grade |
| >= 75 % | A- and above |
| 60-75% | B- and above |
| 45-60% | C- and above |
Note (distance learning students): The course will be recorded
through CAETE. Distance learning students will have to make special
arrangements with the instructor regarding their course projects. Paper
presentations may not be feasible unless you are located near campus.
We will make special arrangements in lieu of such presentations.
[T09] Paulo Tabuada, Verification and Control of Hybrid Systems: A Symbolic Approach, Springer-Verlag, 2009, ISBN: 978-1-4419-0223-8. Online version through CU .
[L04] John Lygeros, Lecture Notes on Hybrid Systems .
Software: