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

Textbook chapters for the individual lectures are linked below, including supporting slides marked with (S) and supporting videos marked with (V). Neither slides nor videos always cover the full lecture. Flipped classroom material is marked with (N) but never covers the full lecture.


DateLecture NotesChExtraDue
Tue09/01Cyber-physical systems: introduction1(V) (S
Thu09/03Differential equations & domains2
Fri09/04Rec: Syntax, Semantics, FOL, ODEsAsst 0 
Tue09/08Choice & control3
Thu09/10Safety & contracts4Lab 0 
Fri09/11Rec: Logic, programs, transition relations
Tue09/15Dynamical systems & dynamic axioms5
Thu09/17Truth & proof6Asst 1 
Fri09/18Rec: Common modeling errors and soundnessBeta 1 
Tue09/22Control loops & invariants7
Thu09/24Events & responses8Lab 1 
Fri09/25Rec: Eventful tactical KeYmaera X proofs
Tue09/29Reactions & delays9
Thu10/01Differential equations & differential invariants10Asst 2 
Fri10/02Rec: Time-triggered control, differentials, differential invariantsBeta 2 
Tue10/06Differential equations & proofs11
Thu10/08Reviewing logical foundations & CPSLab 2 
Fri10/09Rec: Differential invariants, differential cuts
Tue10/13??Midterm I??
Thu10/15Ghosts & differential ghosts12Asst 3 
Fri10/16Free: Day for Community EngagementCheck 3 
Tue10/20Hybrid systems & games14Beta 3 
Thu10/22Winning strategies & regions15White paper 
Fri10/23Free: Mid-semester break
Tue10/27Winning & proving hybrid games16Lab 3 
Thu10/29Game proofs & separations17
Fri10/30Rec: Game semantics, Geri's game, and Bus gamesAsst 4 
Tue11/03Exam review
Thu11/05??Midterm II??
Fri11/06Rec: KeYmaera X Tips and TricksBeta 4 
Tue11/10Hybrid games & differential games TOCL'17
Thu11/12Axioms & uniform substitutions18 JAR'17 Lab 4 
Fri11/13Rec: Convergence and uniform subst
Tue11/17Differential axioms & uniform substitutions18 JAR'17
Thu11/19Verified models & verified runtime validation19 FMSD'16 Asst 5 
Fri11/20Differential invariants & proof theory13Proposal 
Tue11/24Free: Project day
Thu11/26Free: Thanksgiving
Fri11/27Free: Thanksgiving
Tue12/01Virtual substitution & real equations20
Thu12/03Virtual substitution & real arithmetic21,
Fri12/04Rec: Wrestling with real arithmetic
Tue12/08Distributed systems & hybrid systems LMCS'12
Thu12/10Differential equations & completeness JACM'20 Project 
Fri12/11Rec: Prepare for Grand PrixPaper 
TBACPS V&V Grand PrixSlides 

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, Cham, 2018. 659 pages. ISBN 978-3-319-63587-3.
    [bib | doi | slides | video | book | web | errata | abstract]

Logical Foundations of Cyber-Physical Systems

Lab Schedule

Asst 010Preparation AssignmentFri09/04
Lab 010Scavenger HuntThu09/10
Asst 150Introduction to Hybrid ProgramsThu09/17
Beta 120Charging Station (Betabot)Fri09/18
Lab 170Charging Station (Veribot)Thu09/24
Asst 260Loops and ProofsThu10/01
Beta 220Follow the Leader (Betabot)Fri10/02
Lab 280Follow the Leader (Veribot)Thu10/08
Asst 360Proofs, Differential InvariantsThu10/15
Check 310Robots on Racetracks (Checkbot)Fri10/16
Beta 320Robots on Racetracks (Betabot)Tue10/20
Lab 370Robots on Racetracks (Veribot)Tue10/27
Asst 460ODEs, Ghosts, and GamesFri10/30
Beta 420Static and Dynamic Obstacles (Betabot)Fri11/06
Lab 480Static and Dynamic Obstacles (Veribot)Thu11/12
Asst 560Uniform Substitution and Other Fun TopicsThu11/19
White paper20Star-lab White PaperThu10/22
Proposal80Star-lab ProposalFri11/20
Project100Star-lab Final ProjectThu12/10
Paper100Term PaperFri12/11
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.