15-424: Foundations of Cyber-Physical Systems (Fa'13)

Bundle of all lecture notes on Foundations of Cyber-Physical Systems


Mon 08/26Cyber-physical systems: introductionCh 1
Wed 08/28Differential equations & domainsCh 2.2,2.3,App.B
Fri 08/30Rec: ODE, FOL, quizsol
Mon 09/02Labor Day (no class)
Wed 09/04Choice & controlCh 2.2,2.3Lab 0 
Fri 09/06Rec: HP: Syntax, semantics, example
Mon 09/09Safety & contractsCh 2.2,2.3
Wed 09/11Dynamical systems & dynamic axiomsCh 2.5.2Asst 1 Beta 1 
Fri 09/13Rec: Did you prove what you meant to prove?
Mon 09/16Truth & proofCh 2.5.2,App.A
Wed 09/18Control loops & invariantscode Ch 2.5.2&4Lab 1 
Fri 09/20Rec: Invariants and proofs (Jan)code 
Mon 09/23Events & delayscode 
Wed 09/25Proofs & arithmeticcode App.D,Ch 5Asst 2 Beta 2 
Fri 09/27Rec: Events to delays (Stefan)code 
Mon 09/30Differential equations & differential invariantscode Ch 3.5
Wed 10/02Differential equations & proofscode Ch 3.5Lab 2 
Fri 10/04Rec: Differential invariants (Khalil)
Mon 10/07Recap (Jan)Asst 3 
Wed 10/09Midterm
Fri 10/11Rec: Stuff
Mon 10/14Dynamic logic & dynamical systemsBeta 3 
Wed 10/16Differential invariants & proof theoryLMCS'12
Fri 10/18Mid-semester break
Mon 10/21Ghosts & differential ghostsLMCS'12Lab 3 
Wed 10/23Trains & proofsCh 7,ICFEM
Fri 10/25Rec: LabsAsst 4 Beta 4 
Mon 10/28Differential & temporal logicCh 4
Wed 10/30Differential & temporal proofsCh 4
Fri 11/01Rec: Differential ghosts, differential invariantsLab 4 
Mon 11/04Virtual substitution & real equationsApp.D
Wed 11/06Virtual substitution & real arithmeticApp.D
Fri 11/08Rec: Safety in motion, real arithmeticAsst 5 Beta 5 
Mon 11/11Hybrid systems & gamespdf
Wed 11/13Winning strategies & regionspdf
Fri 11/15Rec: Game examplesLab 5 
Mon 11/18Winning & proving hybrid gamespdf
Wed 11/20Game proofs & separationscode ,pdf
Fri 11/22Rec: Game proofsBeta 6 
Mon 11/25Project Day (no class)
Wed 11/27Thanksgiving (no class)
Fri 11/29Thanksgiving (no class)
Mon 12/02Logical theory & completeness
Wed 12/04Logical foundations of CPS
Fri 12/06Rec: Wrap-up, recapLab 6 
Mon 12/09Finals week (no class)Paper 
Thu 12/12Final exam1pm-4pm
The lecture schedule is tentative!
Reading: The chapters Ch i.j for further reading refer to chapters in the textbook in addition to the lecture notes.

Lab Schedule

Lab 010Scavenger HuntcodeWed 09/04
Asst 160Introduction to Hybrid ProgramsWed 09/11
Beta 120Robot on Rails (Betabot)codeWed 09/11
Lab 180Robot on Rails (Veribot)codeWed 09/18
Asst 260Loops and ProofsWed 09/25
Beta 220Robots on Highways (Betabot)Wed 09/25
Lab 280Robots on Highways (Veribot)Wed 10/02
Asst 360Proofs, Diamonds, Differential InvariantsMon 10/07
Beta 320Robots on Racetracks (Betabot)Mon 10/14
Lab 380Robots on Racetracks (Veribot)Mon 10/21
Asst 460Differential Invariants and Nondeterministic AssignmentFri 10/25
Beta 420Robots in a Plane (Betabot)codeFri 10/25
Lab 480Robots in a Plane (Veribot)codeFri 11/01
Asst 560Differential Auxiliaries, dTL, Quantifier EliminationFri 11/08
Beta 520Robots vs. Roguebots (Betabot)codeFri 11/08
Lab 580Robots vs. Roguebots (Veribot)codeFri 11/15
Beta 620Star-lab (Betabot)Fri 11/22
Lab 680Star-lab (Veribot)Fri 12/06
Paper100Term PaperMon 12/09
Sum1010points listed

The Lab and Assignment Schedule is tentative!
Theory assignments are due at start of lecture on the due day.
Programming lab assignments are due at 23:59 on the due day.

For an overview of the labs, see Labs & Assignments.