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.
(V) = videos      (S) = slides      (N) = flipped

Schedule

DateLecture NotesChExtraDue
Tue09/01Cyber-physical systems: introduction1(V) (S) (N
Thu09/03Differential equations & domains2(V) (S
Fri09/04Rec: Syntax, Semantics, FOL, ODEsAsst 0 
Tue09/08Choice & control3(V) (S
Thu09/10Safety & contracts4(V) (SLab 0 
Fri09/11Rec: Logic, programs, transition relations(S
Tue09/15Dynamical systems & dynamic axioms5(V) (Scode 
Thu09/17Truth & proof6(V) (SAsst 1 
Fri09/18Rec: Common modeling errors and soundness(Scode Beta 1 
Tue09/22Control loops & invariants7(V) (Scode 
Thu09/24Events & responses8(V) (Scode Lab 1 
Fri09/25Rec: Eventful tactical KeYmaera X proofs(Scode 
Tue09/29Reactions & delays9(V) (Scode 
Thu10/01Differential equations & differential invariants10(V) (Scode Asst 2 
Fri10/02Rec: Time-triggered control, differentials, differential invariant terms(Scode Beta 2 
Tue10/06Differential equations & proofs11(V) (Scode 
Thu10/08Ghosts & differential ghosts12(V) (Scode Lab 2 
Fri10/09Rec: Differential invariants, differential cuts, differential ghostscode more
Tue10/13Reviewing logical foundations & CPSAsst 3 
Thu10/15Midterm I
Fri10/16Free: Day for Community Engagement
Tue10/20Hybrid systems & games14(V) (SBeta 3 
Thu10/22Winning strategies & regions15(V) (SWhite paper 
Fri10/23Free: Mid-semester break
Tue10/27Winning & proving hybrid games16(V) (Scode Lab 3 
Thu10/29Rec: Game semantics, Geri's game, bus games, proved games(S
Fri10/30Axioms & uniform substitutions18(V) (S
Tue11/03Game proofs & separations17(V) (STOCL'17Asst 4 
Thu11/05Differential axioms & uniform substitutions18(V) (SJAR'17Beta 4 
Fri11/06Rec: Convergence and uniform subst(Scode 
Tue11/10Exam review(VLab 4 
Thu11/12Midterm II
Fri11/13Rec: Modeling and proving with diamonds(Scode 
Tue11/17Verified models & verified runtime validation19(V) (S
Thu11/19Differential equations & completeness(SJACM'20
Fri11/20Rec: Synthesis, Simulation, and Validation(SProposal 
Tue11/24Free: Project day
Thu11/26Free: Thanksgiving
Fri11/27Free: Thanksgiving
Tue12/01Virtual substitution & real equations20(V) (S
Thu12/03Virtual substitution & real arithmetic21(V) (S) , extra
Fri12/04Rec: Wrestling with real arithmetic
Tue12/08Distributed systems & hybrid systems LMCS'12
Thu12/10TBAProject 
Fri12/11Rec: Practice for Grand PrixPaper 
Fri12/18CPS 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

Assignments, labs, and quizzes are released on Diderot.
PointsAssignmentDue
Asst 00Preparation AssignmentFri09/04
Lab 010Scavenger HuntThu09/10
Asst 140Introduction to Hybrid ProgramsThu09/17
Beta 115Charging Station (Betabot)Fri09/18
Lab 175Charging Station (Veribot)Thu09/24
Asst 240Loops and ProofsThu10/01
Beta 220Follow the Leader (Betabot)Fri10/02
Lab 280Follow the Leader (Veribot)Thu10/08
Asst 340Proofs, Differential InvariantsTue10/13
Beta 330Robots on Racetracks (Betabot)Tue10/20
Lab 370Robots on Racetracks (Veribot)Tue10/27
Asst 440ODEs, Ghosts, and GamesTue11/03
Beta 420Static and Dynamic Obstacles (Betabot)Thu11/05
Lab 480Static and Dynamic Obstacles (Veribot)Tue11/10
White paper20Star-lab White PaperThu10/22
Proposal80Star-lab ProposalFri11/20
Project100Star-lab Final ProjectThu12/10
Paper100Term PaperFri12/11
Slides0Slides and PresentationFri12/18
Sum860points 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 before midnight). Theory assignments are due before midnight on the due day.

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