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

  1. Home
  2. >>
  3. Courses
  4. >>
  5. LFCPS Fa19
  6. >>
  7. Schedule
Textbook chapters for the individual lectures are linked below, including supporting slides marked with (⊞) and supporting videos marked with (▶). Neither slides nor videos always cover the full lecture. Flipped classroom material is marked with (N) but never covers the full lecture.

Schedule

DateLecture NotesChExtraDue
Tue08/27Cyber-physical systems: introduction1(▶) (⊞) 
Thu08/29Differential equations & domains2(▶) (⊞) (N) 
Fri08/30Rec: Syntax, Semantics, FOL, ODEsAsst 0 
Tue09/03Choice & control3(▶) (⊞) 
Thu09/05Safety & contracts4(▶) (⊞) Lab 0 
Fri09/06Rec: Logic, programs, transition relations
Tue09/10Dynamical systems & dynamic axioms5(▶) (⊞) code 
Thu09/12Truth & proof6(▶) (⊞) (N) Asst 1 
Fri09/13Rec: Common modeling errors and soundnesscode Beta 1 
Tue09/17Control loops & invariants7(▶) (⊞) code 
Thu09/19Events & responses8(▶) (⊞) code Lab 1 
Fri09/20Rec: Eventful tactical KeYmaera X proofscode 
Tue09/24Reactions & delays9(▶) (⊞) code 
Thu09/26Differential equations & differential invariants10(▶) (⊞) code Asst 2 
Fri09/27Rec: Time-triggered control, differentials, differential invariantscode Beta 2 
Tue10/01Differential equations & proofs11(▶) (⊞) code 
Thu10/03Reviewing logical foundations & CPSLab 2 
Fri10/04Rec: Differential invariants, differential cutscode 
Tue10/08Midterm
Thu10/10Ghosts & differential ghosts12(▶) (⊞) code Asst 3 
Fri10/11Rec: More on ghostsCheck 3 
Tue10/15Hybrid systems & games14(▶) (⊞) Beta 3 
Thu10/17Winning strategies & regions15(▶) (⊞) White paper 
Fri10/18Free: Mid-semester break
Tue10/22Winning & proving hybrid games16(▶) (⊞) code Lab 3 
Thu10/24Rec: Game semantics, Geri's game, and Bus games
Fri10/25Free: Tartan Community DayAsst 4 
Tue10/29Game proofs & separations17(▶) (⊞) 
Thu10/31Final exam
Fri11/01Rec: KeYmaera X Tips and Trickscode Beta 4 
Tue11/05Hybrid games & differential games(▶) (⊞) TOCL'17
Thu11/07Axioms & uniform substitutions18(▶) (⊞)  JAR'17Lab 4 
Fri11/08Rec: Convergence and uniform substcode 
Tue11/12Differential axioms & uniform substitutions18(▶) (⊞)  JAR'17
Thu11/14Verified models & verified runtime validation19(▶) (⊞)  FMSD'16Asst 5 
Fri11/15Differential invariants & proof theory13(▶) (⊞) Proposal 
Tue11/19Virtual substitution & real equations20(▶) (⊞) 
Thu11/21Virtual substitution & real arithmetic21(▶) (⊞) (N) , extra
Fri11/22Rec: Research trends in hybrid systems
Tue11/26Free: Project day
Thu11/28Free: Thanksgiving
Fri11/29Free: Thanksgiving
Tue12/03Distributed systems & hybrid systems(⊞)  LMCS'12
Thu12/05Differential equations & completenessLICS'18Project 
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 | slides | video | book | web | errata | abstract]

Textbook: Logical Foundations of Cyber-Physical Systems

Lab Schedule

PointsAssignmentDue
Asst 010Preparation AssignmentFri08/30
Lab 010Scavenger HuntcodeThu09/05
Asst 150Introduction to Hybrid ProgramsThu09/12
Beta 120Charging Station (Betabot)codeFri09/13
Lab 170Charging Station (Veribot)codeThu09/19
Asst 260Loops and ProofsThu09/26
Beta 220Follow the Leader (Betabot)codeFri09/27
Lab 280Follow the Leader (Veribot)codeThu10/03
Asst 360Proofs, Differential InvariantsThu10/10
Check 310Robots on Racetracks (Checkbot)codeFri10/11
Beta 320Robots on Racetracks (Betabot)codeTue10/15
Lab 370Robots on Racetracks (Veribot)codeTue10/22
Asst 460ODEs, Ghosts, and GamesFri10/25
Beta 420Static and Dynamic Obstacles (Betabot)codeFri11/01
Lab 480Static and Dynamic Obstacles (Veribot)codeThu11/07
Asst 560Uniform Substitution and Other Fun TopicsThu11/14
White paper20Star-lab White PaperThu10/17
Proposal80Star-lab ProposalFri11/15
Project100Star-lab Final ProjectThu12/05
Paper100Term PaperFri12/06
Slides0Slides and PresentationTue12/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.