Cyber-Physical Computation 2019/2020

Welcome to the webpage of the course "Cyber-Physical Computation 2019/2020".

Cyber-physical systems are networks of computational devices that closely interact with physical processes in order to reach a prescribed goal; for example a desired velocity, a desired temperature or, more generally, a desired energy level. They range from small medical devices, such as pacemakers and insulin pumps, to networks of autonomous vehicles and district-wide smart grids. Our course is devoted to such systems.

More specifically, the main goal of the course is two-fold: 1) to prepare the student to a disciplined way of developing and analysing cyber-physical systems, by presenting their basic principles, adequate models of computation and respective tools; 2) and to introduce the student to the main limitations of the state-of-the-art techniques in the area, via pedagogical illustrations extracted from real world-scenarios involving e.g. cruise controllers, sampling algorithms, and timed variants of concurrent algorithms. At the end of the course, the student will know:

• the basic principles of cyber-physical computation;
• representative models and tools for the development and analysis of cyber-physical systems. In particular, he or she will be familiar with the tools Uppaal, Lince, and KeYmaera, which cover model checking, testing, simulation, and theorem proving;
• in which ways the state-of-the-art is limited, and the potential outcomes of solving these limitations.

There are several models and tools for cyber-physical systems. We will focus just on the representative cases. At the same time, we will draw a parallel with the usual models of classic computation, so that the student understands in which ways cyber-physical computation extends the classical counterpart. Briefly, we will focus on timed/hybrid automata, the standard (operational) model for cyber-physical computation and related aspects of concurrency; a hybrid while-language in Hoare style, as a sequential, compositional model for cyber-physical programs; and differential dynamic logic, as a way to systematically analyse the behaviour of cyber-physical systems. In detail, we will go over the following topics:

• Automata theory: basic notions, regular expressions, bisimulation, non-determinism and other kinds of branching (Lecture 1).
• Timed automata: composition and synchronisation, bisimulation, Zeno behaviour, and model checking (Lecture 2).
• Hybrid automata: composition and synchronisation, bisimulation, verification of reachability properties (Lecture 3).
• Modal logic: basic notions of logic and modalities, calculi, and bisimulation (Lecture 4).
• While-languages: a toy programming language, operational semantics and iteration (Lecture 5).
• Timed and hybrid programming languages: a toy programming language, operational semantics, iteration, Zeno behaviour revisited (Lecture 5).
• Dynamic logic: program modalities, calculi, and differential dynamic logic (Lecture 6).