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

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.

Schedule

DateLecture NotesChExtraDue
Tue08/27Cyber-physical systems: introduction1(V) (S
Thu08/29Differential equations & domains2(V) (S
Fri08/30Rec: Syntax, Semantics, FOL, ODEsAsst 0 
Tue09/03Choice & control3
Thu09/05Safety & contracts4Lab 0 
Fri09/06Rec: Logic, programs, transition relations
Tue09/10Dynamical systems & dynamic axioms5
Thu09/12Truth & proof6Asst 1 
Fri09/13Rec: Common modeling errors and soundnessBeta 1 
Tue09/17Control loops & invariants7
Thu09/19Events & responses8Lab 1 
Fri09/20Rec: Eventful tactical KeYmaera X proofs
Tue09/24Reactions & delays9
Thu09/26Differential equations & differential invariants10Asst 2 
Fri09/27Rec: Time-triggered control and flying with differential invariantsBeta 2 
Tue10/01Differential equations & proofs11
Thu10/03Reviewing logical foundations & CPS Lab 2 
Fri10/04Rec: Differential invariants, differential cuts
Tue10/08Midterm
Thu10/10Ghosts & differential ghosts12Asst 3 
Fri10/11Rec: ODE proofs and hybrid gamesCheck 3 
Tue10/15Differential invariants & proof theory13
Thu10/17Hybrid systems & games14Beta 3 
Fri10/18Free: Mid-semester break
Tue10/22Winning strategies & regions15
Thu10/24Winning & proving hybrid games16Lab 3 
Fri10/25Rec: TBDWhite paper 
Tue10/29Game proofs & separations17 TOCL'17
Thu10/31Final examAsst 4 
Fri11/01Rec: Fun and games with proofsBeta 4 
Tue11/05Hybrid games & differential games
Thu11/07Axioms & uniform substitutions18 JAR'17 Lab 4 
Fri11/08Rec: Convergence and uniform subst
Tue11/12Differential axioms & uniform substitutions18 JAR'17
Thu11/14Verified models & verified runtime validation19 FMSD'16 Asst 5 
Fri11/15Rec: KeYmaera X Tips and TricksProposal 
Tue11/19Virtual substitution & real equations20
Thu11/21Virtual substitution & real arithmetic21,
Fri11/22Rec: Real arithmetic for real
Tue11/26Free: Project day
Thu11/28Free: Thanksgiving
Fri11/29Free: Thanksgiving
Tue12/03CPS information-flow security and smartgrids LICS'18
Thu12/05Distributed systems & hybrid systems LMCS'12 Project 
Fri12/06Rec: Prepare for Grand PrixPaper 
Tue12/10CPS 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 | video | book | web | errata | abstract]

Logical Foundations of Cyber-Physical Systems

Lab Schedule

PointsAssignmentDue
Asst 010Preparation AssignmentFri 08/30
Lab 010Scavenger HuntThu 09/05
Asst 150Introduction to Hybrid ProgramsThu 09/12
Beta 120Charging Station (Betabot)Fri 09/13
Lab 170Charging Station (Veribot)Thu 09/19
Asst 260Loops and ProofsThu 09/26
Beta 220Follow the Leader (Betabot)Fri 09/27
Lab 280Follow the Leader (Veribot)Thu 10/03
Asst 360Proofs, Diamonds, Differential InvariantsThu 10/10
Check 310Robots on Racetracks (Checkbot)Fri 10/11
Beta 320Robots on Racetracks (Betabot)Thu 10/17
Lab 370Robots on Racetracks (Veribot)Thu 10/24
Asst 460Differential Invariants, Cuts, and Being GhostlyThu 10/31
Beta 420Static and Dynamic Obstacles (Betabot)Fri 11/01
Lab 480Static and Dynamic Obstacles (Veribot)Thu 11/07
Asst 560Play Around with Hybrid GamesThu 11/14
White paper20Star-lab White PaperFri 10/25
Proposal80Star-lab ProposalFri 11/15
Project100Star-lab Final ProjectThu 12/05
Paper100Term PaperFri 12/06
Slides0Slides and PresentationTue 12/10
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.