Dates: January 20 to January 24, 2014
Local contact: Filippo Bonchi
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
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.
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.
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.
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.
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.
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.
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.
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.
Students will design a hybrid controller to follow a lead robot along a straight line without colliding. Students get to assume continuous sensing.
This lecture will discuss the basics of proofs and frequently used techniques for proving.
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.
Students will modify their hybrid controller for following a lead robot so that it no longer requires continuous sensing.
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.
This lecture will discuss how to find and use differential invariants in proofs.
Students will prove safety properties about systems with curved dynamics using KeYmaera and have the opportunity to catch up on unfinished practical assignments.
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.
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.
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.
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.