EECI 2012: Algorithmic Verification of Hybrid Systems: Difference between revisions
No edit summary |
No edit summary |
||
| Line 11: | Line 11: | ||
== Additional Material and Further Reading == | == Additional Material and Further Reading == | ||
* <p> [http://robotics.eecs.berkeley.edu/~sastry/ee291e/lygeros.pdf Lecture Notes on Hybrid Systems] (by John Lygeros): A rough introduction to hybrid systems. Chapters 5 and 6 are on various analysis techniques relevant for this short course. </p> | * <p> [http://robotics.eecs.berkeley.edu/~sastry/ee291e/lygeros.pdf Lecture Notes on Hybrid Systems] (by John Lygeros): A rough introduction to hybrid systems. Chapters 5 and 6 are on various analysis techniques relevant for this short course. </p> | ||
Revision as of 10:09, 14 May 2012
| Prev: Deductive Verification of Hybrid Systems | Course home | Next: Synthesis of Reactive Control Protocols |
This lecture focuses on the verification of hybrid systems. We first discuss finite-state under- and over-approximations of hybrid dynamics and how these finite-state models coupled with the model checking tools can be used to verify temporal logic properties against hybrid dynamics. Then, we present a procedure for constructing finite-state, under-approximations which will later be used in the course in the synthesis of hierarchical control protocols. We finally introduce the notions of approximate bisimulations and bisimulation functions and how they can be used in verification of temporal properties.
Lecture Materials
Additional Material and Further Reading
Lecture Notes on Hybrid Systems (by John Lygeros): A rough introduction to hybrid systems. Chapters 5 and 6 are on various analysis techniques relevant for this short course.
