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

Lecture notes are linked below, including lecture videos marked with (V) and supporting slides marked with (S). Slides do not always cover the full lecture. The lecture notes are significantly updated this semester, but the lecture videos are from Spring 2016.


DateLecture NotesChExtraDue
Tue08/28Cyber-physical systems: introduction1
Thu08/30Differential equations & domains2
Fri08/31Rec: ODE, FOL, prepAsst 0 
Tue09/04Choice & control3
Thu09/06Safety & contracts4 Lab 0 
Fri09/07Rec: Programs, properties, transitions, and examples
Tue09/11Dynamical systems & dynamic axioms5 LICS'12
Thu09/13Truth & proof6 Asst 1 
Fri09/14Rec: What is a proof and why?Beta 1 
Tue09/18Control loops & invariants7
Thu09/20Events & responses8Lab 1 
Fri09/21Rec: Eventful tactical proofs in KeYmaera X
Tue09/25Reactions & delays9
Thu09/27Differential equations & differential invariants10 Asst 2 
Fri09/28Rec: Events to delays and flying with differential invariantsBeta 2 
Tue10/02Differential equations & proofs11
Thu10/04Ghosts & differential ghosts12 LMCS'12, Lab 2 
Fri10/05Rec: Differential invariants, differential cuts, rolling down a hill
Tue10/09Differential invariants & proof theory13 LMCS'12 Asst 3 
Thu10/11Reviewing logical foundations & CPS LICS'12
Fri10/12Rec: Proving differential equations with cuts and differential ghosts
Tue10/16Verified models & verified runtime validation19 FMSD'16
Thu10/18MidtermBeta 3 
Fri10/19Free: Mid-semester break
Tue10/23Hybrid systems & games14 TOCL'15
Thu10/25Winning strategies & regions15 TOCL'15 Lab 3 
Fri10/26Rec: Game semantics, Geri's game, and Bus games
Tue10/30Winning & proving hybrid games16 TOCL'15
Thu11/01Game proofs & separations17 TOCL'15 TOCL'17 Asst 4 
Fri11/02Rec: Fun and games with proofsBeta 4 
Tue11/06Axioms & uniform substitutions18 JAR'17
Thu11/08Differential axioms & uniform substitutions18 JAR'17 Lab 4 
Fri11/09Rec: Uniform subst and reviewWhite paper 
Thu11/15Final examAsst 5 
Fri11/16Rec: Project modeling, baseball proving, decomposing models, logical model-predictive control
Tue11/20Free: Project day
Thu11/22Free: Thanksgiving
Fri11/23Free: Thanksgiving
Tue11/27Virtual substitution & real equations20Proposal 
Thu11/29Virtual substitution & real arithmetic21,
Fri11/30Rec: Real arithmetic for real
Tue12/04Distributed systems & hybrid systems LMCS'12
Thu12/06Model checking & reachability analysis
Fri12/07Rec: Prepare for Grand Prix
Tue12/11CPS V&V Grand Prix

The lecture schedule is tentative!

The chapter numbers indicated above refer to the following textbook:

  1. André Platzer.
    Logical Foundations of Cyber-Physical Systems.
    Springer, 2018. 659 pages. ISBN 978-3-319-63587-3.
    [bib | doi | book | web | abstract]

Lab Schedule

Asst 00Preparation AssignmentFri 08/31
Lab 010Scavenger HuntThu 09/06
Asst 160Introduction to Hybrid ProgramsThu 09/13
Beta 120Charging Station (Betabot)Fri 09/14
Lab 170Charging Station (Veribot)Thu 09/20
Asst 260Loops and ProofsThu 09/27
Beta 220Follow the Leader (Betabot)Fri 09/28
Lab 280Follow the Leader (Veribot)Thu 10/04
Asst 360Proofs, Diamonds, Differential InvariantsTue 10/09
Beta 320Robots on Racetracks (Betabot)Thu 10/18
Lab 380Robots on Racetracks (Veribot)Thu 10/25
Asst 460Differential Invariants, Cuts, and Being GhostlyThu 11/01
Beta 420Static and Dynamic Obstacles (Betabot)Fri 11/02
Lab 480Static and Dynamic Obstacles (Veribot)Thu 11/08
Asst 560Play Around with Hybrid GamesThu 11/15
White paper20Star-lab White PaperFri 11/09
Proposal80Star-lab ProposalTue 11/27
Project100Star-lab Final Project
Paper100Term Paper
Slides0Slides and Presentation
Sum1000points listed

The Lab and Assignment Schedule is tentative!
Labs have a due date and time for Betabots (due at start of lecture/recitation) and a different due date and time for Veribots (due at midnight). Theory assignments are due by midnight on the due day.

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