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

  1. Home
  2. >>
  3. Courses
  4. >>
  5. LFCPS Fa21
  6. >>
  7. Schedule
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.
(V) = videos      (S) = slides


DateLecture NotesChExtraDue
Tue08/31Cyber-physical systems: introduction1(V) (S
Thu09/02Differential equations & domains2(V) (S
Fri09/03Rec: Syntax, Semantics, FOL, ODEsAsst 1 
Tue09/07Choice & control3(V) (S
Thu09/09Safety & contracts4(V) (S
Fri09/10Rec: Logic, programs, transition relationscode Lab 0 
Tue09/14Dynamical systems & dynamic axioms5(V) (Scode Beta 1 
Thu09/16Truth & proof6(V) (S
Fri09/17Rec: Common modeling errors and soundnesscode 
Tue09/21Control loops & invariants7(V) (Scode Lab 1 
Thu09/23Events & responses8(V) (Scode 
Fri09/24Rec: Eventful tactical KeYmaera X proofscode Asst 2 
Tue09/28Reactions & delays9(V) (Scode Beta 2 
Thu09/30Differential equations & differential invariants10(V) (Scode 
Fri10/01Rec: Time-triggered control, differentials, differential invariant termscode 
Tue10/05Differential equations & proofs11(V) (Scode Lab 2 
Thu10/07Reviewing logical foundations & CPS
Fri10/08Rec: Differential invariants, differential cutscode Asst 3 
Tue10/12Midterm I
Thu10/14Free: Mid-Semester Break
Fri10/15Free: Mid-Semester Break
Tue10/19Hybrid systems & games14(V) (SBeta 3 
Thu10/21Winning strategies & regions15(V) (SWhitepap. 
Fri10/22Rec: Game semantics, Geri's game, bus games
Tue10/26Winning & proving hybrid games16(V) (Scode Lab 3 
Thu10/28Ghosts & differential ghosts12(V) (Scode 
Fri10/29Rec: Game proofs and go with ghosts
Tue11/02Game proofs & separations17(V) (STOCL'17Beta 4 
Thu11/04Axioms & uniform substitutions18(V) (Smore
Fri11/05Free: Day for Community Engagement
Tue11/09Exam review(VLab 4 
Thu11/11Midterm II
Fri11/12Rec: Modeling and proving with diamondscode 
Tue11/16Verified models & verified runtime validation19(V) (SProposal 
Thu11/18Differential equations & completeness(V) (SJACM'20
Fri11/19Rec: Validation, Simulation and Synthesis
Tue11/23Free: Project day
Thu11/25Free: Thanksgiving
Fri11/26Free: Thanksgiving
Tue11/30Virtual substitution & real equations20(V) (SFM'21
Thu12/02Virtual substitution & real arithmetic21(V) (SCH, extraProject 
Fri12/03Rec: Wrestling with real arithmeticcode Paper 
Fri12/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 | slides | video | book | web | errata | abstract]

Textbook: Logical Foundations of Cyber-Physical Systems

Lab Schedule

Assignments, labs, and quizzes are released on Diderot.
Asst 10Preparation AssignmentFri09/03
Lab 010Scavenger HuntFri09/10
Beta 115Charging Station (Betabot)Tue09/14
Lab 175Charging Station (Veribot)Tue09/21
Asst 240Loops and ProofsFri09/24
Beta 220Follow the Leader (Betabot)Tue09/28
Lab 280Follow the Leader (Veribot)Tue10/05
Asst 340Proofs, Differential InvariantsFri10/08
Beta 330Robots on Racetracks (Betabot)Tue10/19
Lab 370Robots on Racetracks (Veribot)Tue10/26
Beta 420Static and Dynamic Obstacles (Betabot)Tue11/02
Lab 480Static and Dynamic Obstacles (Veribot)Tue11/09
Whitepap.20Star-lab White PaperThu10/21
Proposal80Star-lab ProposalTue11/16
Project100Star-lab Final ProjectThu12/02
Paper100Term PaperFri12/03
Slides0Slides and PresentationFri12/10
Sum780points listed

The Lab and Assignment Schedule is tentative!
Labs have a due date and time for Betabots and a different due date and time for Veribots. Theory assignments are due on the due day. More specific due times are listed on Diderot.

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