Research school 3 : Logic of Dynamical Systems

Lecturers : AndrĂ© Platzer and Sarah Loos (CMU).

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