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. Flipped classroom material is marked with (N) but never covers the full lecture.

Schedule

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

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.