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

3.1 Teaching methods

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.

3.2 Individual report and oral presentation

The student will write an individual report (max. 7 pages) about a scientific article in the area of cyber-physical systems. The individual report should distill the article and present a critique analysis of the latter. The report will then be orally presented in the last lecture of the course (max. 20 min.).

Here are the articles that the student can choose from (max. 1 per student):

Both individual report and corresponding presentation will be graded: finalGrade = 0.7*IndividualReport + 0.3*Presentation.

The individual report should be sent to the email and no later than the 18th of November. As mentioned before, the presentations are scheduled for the 12th of November.

N.b. Further than evaluating the student's knowledge on cyber-physical computation, the goal of this assessment is to hone requisite skills for a successful research career: namely, to understand the main ideas of a scientific work, to form a rigorous, critical analysis of it, and to properly explain ideas/opinions to peers both orally and in written.

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

Coordinator: 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: 2021-02-12 Fri 00:13