Cyber-Physical Computation 2019/2020

Table of Contents

1 Welcome

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.

2 Course Syllabus

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).

3 Grading

Our way of teaching will be based on the well-known tutorial system, but strongly oriented to a hands-on approach, supported by a carefully chosen palette of case-studies.

Grading will have both theoretical and practical components: 1) the student will write an individual report based on a research topic within the area of cyber-physical systems; 2) and also develop, in a principled way, a model of a cyber-physical system for handling a pedagogical, real-world problem (e.g. to descend a spacecraft safely into the ground).

Further details will be available soon.

4 Dates, materials, and contacts

Lecture Nr. - Date - Time Topic Lecturer Room
1 - 01/10/19 - 10h-12h and 14h-16h Course structure, Automata Theory RN 1.10 - Informatics Dep.
2 - 14/10/19 - 10h-12h and 14h-16h Timed Automata JP 0.05 - Informatics Dep.
3 - 15/10/19 - 11h-13h and 14h30m - 16h30m Hybrid Automata ER 1.10 - Informatics Dep.
4 - 22/10/19 - 11h-13h and 14h30m - 16h30m Modal Logic MA/AM 1.10 - Informatics Dep.
5 - 29/10/19 - 10h-12h and 14h-16h While-languages (Timed and Hybrid) RN 1.10 - Informatics Dep.
6 - 05/11/19 - 11h-13h and 14h30m - 16h30m Dynamic Logic MA/AM 1.10 - Informatics Dep.
7 - 12/11/19 - 10h-12h and 14h-16h Presentations RN 1.10 - Informatics Dep.

Responsible: Renato Neves.

5 Bibliography

Introduction to Automata Theory, Languages, and Computation (3rd Edition) Addison-Wesley Longman Publishing Co., Inc. Boston, MA, USA.

R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183 – 235, 1994.

T. A. Henzinger. The theory of hybrid automata. In LICS96': Logic in Computer Science, 11th Annual Symposium, 1996, pages 278–292. IEEE, 1996.

Blackburn, P., van Benthem, J. F., & Wolter, F. (Eds.). (2006). Handbook of modal logic (Vol. 3). Elsevier.

S. Goncharov, J. Jakob and R. Neves. A Semantics for Hybrid Iteration. In 29th International Conference on Concurrency Theory (CONCUR 2018), Springer, 2018.

S. Goncharov and R. Neves. An Adequate While-language for Hybrid Computation. In 21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019), ACM, 2019.

Platzer, A. (2018). Logical foundations of cyber-physical systems. Heidelberg: Springer.

G. Winskel. Formal Semantics of Programming Languages: an introduction. MIT Press Cambridge, 1993.

Author: Renato Neves

Created: 2019-10-09 Wed 17:09