Dates: January 20 to January 24, 2014
Local contact: Filippo Bonchi
This
course studies the logic of dynamical systems, that is, logics and
proof principles for properties of dynamical systems. Dynamical
systems are mathematical models describing how the state of a system
evolves over time. They are important in modeling and
understanding many applications, including embedded systems and
cyber-physical systems combining cyber effects with physical effects.
In discrete dynamical systems, the state evolves in discrete
steps, one step at a time, as described by a difference equation or
discrete state transition relation. In continuous dynamical
systems, the state evolves continuously along a function, typically
described by a differential equation. Hybrid dynamical systems
or hybrid systems combine both discrete and continuous
dynamics.
This
course explores the theory, practice, and applications of the family
of differential dynamic logics, which includes logics for hybrid
systems and extensions to distributed hybrid systems and hybrid
games. It explains dynamical system models, logics of dynamical
systems, their semantics, and their axiomatization for proving
logical formulas about dynamical systems. We study differential
invariants, i.e., induction principles for differential equations.
We survey theoretical results, including soundness and
completeness and deductive power, and discuss algorithmic
implications. Differential dynamic logics have been implemented
in automatic and interactive theorem provers and have been used
successfully to verify safety-critical applications in automotive,
aviation, railway, and robotic domains. Throughout, we
highlight some of the connections that logics of dynamical systems
enjoy to other exciting fields, including proof theory, fixpoint
theory, (real) algebraic geometry, Lie algebra, computer algebra, and
numerical analysis.
The
results discussed in this course demonstrate that logic is a powerful
tool, not just for studying discrete phenomena, but also continuous,
distributed, and adversarial dynamics. Dynamic logics provide a
strong logical foundation for dynamical systems, including
cyber-physical systems. Such stable foundations for a
relatively young area make it a promising direction for future
research that is unique in its manifold connections to other pure and
applied sciences. Given the tremendous progress that logic for
classical software has made since its conception, we expect to see no
less from the area of logics for dynamical systems in which programs
reach out into the physical world.
Before the course begins, students should install Mathematica and KeYmaera. Instructions can be found here.
Monday:
9:00-10:45: Lecture 1: Basics of Hybrid Programs: Choice, Control & Domains
In the first lecture, we will cover the syntax and semantics of hybrid programs (HPs) and differential dynamic logic (dL). Most importantly, we will cover how to model the effects of discrete control choices on continuous physical dynamics.
TD (Theory): HP Syntax, Semantics, and Examples
Students will get practice learning the syntax of dL formulas, writing basic HPs, and developing an intuition for the behavior of hybrid systems.
11:00-12:30: Lecture 2: Safety & contracts
After covering the basics of how to model and design hybrid programs, we quickly move on to investigating the properties we want to verify. What does it mean to verify a hybrid system? How can we represent safety in dL? In this lecture we delve deeper into the subtleties and advantages of nondeterministic models which can cover the behavior of a class of controllers rather than a single system. Then we discuss how to represent the properties we want our HPs to satisfy.
13:30-14:30: Lecture 3: Dynamical systems & dynamic axioms
Lecture 2 demonstrated how useful and crucial contracts are for CPS. However, in this lecture we introduce the axioms of dL to go beyond understanding contracts in the light of dynamic testing.
14:30: TD (Practical): Did you prove what you meant to prove?
Students will practice writing contracts as formulas in dL. Then they will use the formal verification tool KeYmaera to prove safety and liveness properties about a robot reaching a charging station.
Tuesday:
9:00-10:45: Lecture 4: Truth & proof
In this lecture, we present the proof calculus for dL, which allows us to prove that the HPs we've created satisfy given safety contracts under all admissible behavior of the system.
TD (Theory): Proof Calculus
Students will begin working with the proof calculus for dL.
11:00-12:30: Lecture 5: Control loops & invariants
Lecture 1 on Choice & Control demonstrated how important control is in CPS and that control loops are a very important feature for making this control happen. Without loops, CPS controllers are limited to short finite sequences of control actions, which are rarely sufficient. In this lectures, we'll explore iterative repetition and how to prove properties about systems which can iteratively repeat arbitrarily often.
TD (Theory): Students will practice working with the proof rules related to loop invariants. They will also create a proof of safety by hand using the proof rules they have learned.
13:30-15:30: Lecture 6: Events & delays
This lecture will focus on how loops interface with differential equations in HPs. There are two important paradigms for handling this interaction between cyber and physical. The first paradigm is that of event-driven architecture, where reactions to events dominate the behavior of the system. The other paradigm is time-triggered control, which may only control the system at periodic intervals.
15:30: TD (Practical): Event-triggered car following
Students will design a hybrid controller to follow a lead robot along a straight line without colliding. Students get to assume continuous sensing.
Wednesday:
9:00-10:30: Lecture 7: Proofs & arithmetic ("Where do proofs stop")
This lecture will discuss the basics of proofs and frequently used techniques for proving.
11:00-12:00: Lecture 8: KeYmaera Proving Tutorial
In this lecture we introduce KeYmaera, a theorem prover for hybrid system to extend the theoretical proving techniques learned in Lecture 7 to practical applications.
13:00-14:30: TD (Practical): Time-triggered car following
Students will modify their hybrid controller for following a lead robot so that it no longer requires continuous sensing.
15:00-17:30: Lecture 9: Differential equations & differential invariants
In previous lectures and materials we have examined how to prove properties about hybrid programs with simple solutions. In this lecture we will introduce differential invariants for analyzing systems with differential equations which are not solvable or for which the solution may be computationally intractable.
TD (Theory): Curved motion
Students will model systems with curved dynamics. They will also practice finding differential invariants and taking syntactic derivatives.
Thursday:
9:00-10:30: Lecture 10: Differential equations & proofs
This lecture will discuss how to find and use differential invariants in proofs.
10:30-12:30: TD (Practical): Curved motion
Students will prove safety properties about systems with curved dynamics using KeYmaera and have the opportunity to catch up on unfinished practical assignments.
Friday:
9:00-10:00 Lecture 11: Ghosts & differential ghosts
Differential ghosts, also called differential auxiliaries, can also be used where differential invariants fall short for proving properties about differential equations without solutions in first-order arithmetic.
10:00-11:00 TD (Practical): Review and Future work
Students will have the chance to complete any unfinished work from previous practical assignments. They will also be given directions for optional advanced hybrid systems verification tasks.
11:15-12:00 Lecture 13: Hybrid systems & games
In this lecture we introduce adversarial dynamics into hybrid programs. The combination of discrete, continuous, and adversarial dynamics leads to hybrid games. Unlike Hybrid systems, hybrid games allow choices in the system dynamics to be resolved adversarially by different players who each have different objectives.
13:00-14:00 Lecture 14: Winning strategies & proofs
This lecture continues the study of hybrid games and the differential game logic introduced in the previous lecture, adding a discussion of how to prove properties about hybrid games.
14:00-14:45 Lecture 15: Logical foundations of CPS
15:30-17:00: Exam