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

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

Date		Lecture Notes	Ch	Extra	Due
Tue	08/27	Cyber-physical systems: introduction	1	(▶) (⊞)
Thu	08/29	Differential equations & domains	2	(▶) (⊞) (N)
Fri	08/30	Rec: Syntax, Semantics, FOL, ODEs			Asst 0
Tue	09/03	Choice & control	3	(▶) (⊞)
Thu	09/05	Safety & contracts	4	(▶) (⊞)	Lab 0
Fri	09/06	Rec: Logic, programs, transition relations
Tue	09/10	Dynamical systems & dynamic axioms	5	(▶) (⊞) code
Thu	09/12	Truth & proof	6	(▶) (⊞) (N)	Asst 1
Fri	09/13	Rec: Common modeling errors and soundness		code	Beta 1
Tue	09/17	Control loops & invariants	7	(▶) (⊞) code
Thu	09/19	Events & responses	8	(▶) (⊞) code	Lab 1
Fri	09/20	Rec: Eventful tactical KeYmaera X proofs		code
Tue	09/24	Reactions & delays	9	(▶) (⊞) code
Thu	09/26	Differential equations & differential invariants	10	(▶) (⊞) code	Asst 2
Fri	09/27	Rec: Time-triggered control, differentials, differential invariants		code	Beta 2
Tue	10/01	Differential equations & proofs	11	(▶) (⊞) code
Thu	10/03	Reviewing logical foundations & CPS			Lab 2
Fri	10/04	Rec: Differential invariants, differential cuts		code
Tue	10/08	Midterm
Thu	10/10	Ghosts & differential ghosts	12	(▶) (⊞) code	Asst 3
Fri	10/11	Rec: More on ghosts			Check 3
Tue	10/15	Hybrid systems & games	14	(▶) (⊞)	Beta 3
Thu	10/17	Winning strategies & regions	15	(▶) (⊞)	White paper
Fri	10/18	Free: Mid-semester break
Tue	10/22	Winning & proving hybrid games	16	(▶) (⊞) code	Lab 3
Thu	10/24	Rec: Game semantics, Geri's game, and Bus games
Fri	10/25	Free: Tartan Community Day			Asst 4
Tue	10/29	Game proofs & separations	17	(▶) (⊞)
Thu	10/31	Final exam
Fri	11/01	Rec: KeYmaera X Tips and Tricks		code	Beta 4
Tue	11/05	Hybrid games & differential games		(▶) (⊞) TOCL'17
Thu	11/07	Axioms & uniform substitutions	18	(▶) (⊞)  JAR'17	Lab 4
Fri	11/08	Rec: Convergence and uniform subst		code
Tue	11/12	Differential axioms & uniform substitutions	18	(▶) (⊞)  JAR'17
Thu	11/14	Verified models & verified runtime validation	19	(▶) (⊞)  FMSD'16	Asst 5
Fri	11/15	Differential invariants & proof theory	13	(▶) (⊞)	Proposal
Tue	11/19	Virtual substitution & real equations	20	(▶) (⊞)
Thu	11/21	Virtual substitution & real arithmetic	21	(▶) (⊞) (N) , extra
Fri	11/22	Rec: Research trends in hybrid systems
Tue	11/26	Free: Project day
Thu	11/28	Free: Thanksgiving
Fri	11/29	Free: Thanksgiving
Tue	12/03	Distributed systems & hybrid systems		(⊞)  LMCS'12
Thu	12/05	Differential equations & completeness		LICS'18	Project
Fri	12/06	Rec: Prepare for Grand Prix			Paper
Tue	12/10	CPS V&V Grand Prix			Slides

The lecture schedule is tentative!

The chapter numbers indicated above refer to the following textbook:

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]

Lab Schedule

	Points	Assignment		Due
Asst 0	10	Preparation Assignment		Fri	08/30
Lab 0	10	Scavenger Hunt	code	Thu	09/05
Asst 1	50	Introduction to Hybrid Programs		Thu	09/12
Beta 1	20	Charging Station (Betabot)	code	Fri	09/13
Lab 1	70	Charging Station (Veribot)	code	Thu	09/19
Asst 2	60	Loops and Proofs		Thu	09/26
Beta 2	20	Follow the Leader (Betabot)	code	Fri	09/27
Lab 2	80	Follow the Leader (Veribot)	code	Thu	10/03
Asst 3	60	Proofs, Differential Invariants		Thu	10/10
Check 3	10	Robots on Racetracks (Checkbot)	code	Fri	10/11
Beta 3	20	Robots on Racetracks (Betabot)	code	Tue	10/15
Lab 3	70	Robots on Racetracks (Veribot)	code	Tue	10/22
Asst 4	60	ODEs, Ghosts, and Games		Fri	10/25
Beta 4	20	Static and Dynamic Obstacles (Betabot)	code	Fri	11/01
Lab 4	80	Static and Dynamic Obstacles (Veribot)	code	Thu	11/07
Asst 5	60	Uniform Substitution and Other Fun Topics		Thu	11/14
White paper	20	Star-lab White Paper		Thu	10/17
Proposal	80	Star-lab Proposal		Fri	11/15
Project	100	Star-lab Final Project		Thu	12/05
Paper	100	Term Paper		Fri	12/06
Slides	0	Slides and Presentation		Tue	12/10
Sum	1000	points 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.