15-819/18-879L: Logical Analysis of Hybrid Systems

15-819N: Logical Analysis of Hybrid Systems (Spring 2011) 18-879L: Logical Analysis of Hybrid Systems (Spring 2011) Instructor: André Platzer Units: 12 Semester: Spring 2011 Time: Tue, Thu 3:00-4:20 (note change) Place: NSH 3002 (note change) Blackboard: blackboard (only for grades) This course is cross-listed in Computer Science as 15-819N in the Advanced topics in Programming Language area. It is also cross-listed in Electrical & Computer Engineering as 18-879L in the Special Topics in Systems and Controls area at Carnegie Mellon University

Schedule

Date	Lecture	Assignment	Reading
Tue 01/11	Hybrid Systems Applications	none	none
Thu 01/13	Dynamical Systems	none	none
Tue 01/18	Hybrid Systems	none	App C
Thu 01/20	Hybrid System Examples	none	Ch 1, more
Tue 01/25	Differential Equations	none	App B
Thu 01/27	First-Order Logic	none	App A
Tue 02/01	Quantifier Elimination	none	App D.2.1-2
Thu 02/03	First-Order Real Arithmetic I	none	App D.2.1-2
Tue 02/08	First-Order Real Arithmetic II	Asst 1	App D.2.1-2
Thu 02/10	Real Algebraic Geometry	none	App D.2.2‑3
Tue 02/15	Hybrid Systems Model Checking	none	HSCC'07
Thu 02/17	Logic & Hybrid Programs	none	Ch 2.1-2.2
Tue 02/22	Hybrid Program Semantics	none	Ch 2.3
Thu 02/24	Differential Dynamic Logic	Asst 2	Ch 2.2‑2.5.2
Tue 03/01	Logical Proof Rules I	none	Ch 2.2‑2.5.2
Thu 03/03	Logical Proof Rules II	none	Ch 2.5
Tue 03/08	Spring Break	none
Thu 03/10	Spring Break	none
Tue 03/15	ETCS Verification	Asst 3	Ch 7
Thu 03/17	Image Computation Problem	none	HSCC'07
Tue 03/22	Differential-Algebraic Constraints	none	Ch 3.2
Thu 03/24	Differential-Algebraic Dynamic Logic	Whitepaper	Ch 3.3
Tue 03/29	Differential Invariants I	none	Ch 3.5
Thu 03/31	Differential Invariants II	Asst 4	Ch 3.5
Tue 04/05	Logic for Distributed Hybrid Systems	none	CSL'10
Thu 04/07	Compositional Verification of Distributed Hybrid Systems	none	CSL'10
Tue 04/12	Tutorial (David Renshaw)	none	ICFEM'11
Thu 04/14	Spring Carnival	none
Tue 04/19	Distributed Hybrid Systems Verification	none	CSL'10
Thu 04/21	Soundness	Proposal	Ch 2.6
Tue 04/26	Differential Temporal Dynamic Logic	none	Ch 4
Thu 04/28	Completeness	none	Ch 2.7
Fri 05/06	Final Projects Due	Project

The slides do not contain all material that has been covered in class. They reflect some part of the topic. The material is covered in detail in the book [1].

Textbook

The chapters indicated above refer to the textbook

André Platzer. Logical Analysis of Hybrid Systems:    Proving Theorems for Complex Dynamics. Springer, Heidelberg, 2010. 426 pages. ISBN 978-3-642-14508-7. [bib | ⧉ | doi | book | web | errata | abstract]