# 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):

- Optimizing Quantum Programs against Decoherence
- From Timed Reo Networks to Networks of Timed Automata
- Arrows, Robots, and Functional Reactive Programming
- An Extended Duration-Calculus for Hybrid Real-Time Systems

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 nevrenato@gmail.com
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.

### 3.3 Final grades

The table below contains the students' final grades.

Name | Final Grade |
---|---|

Ana | 17 |

Michael | 15 |

Vítor | 15 |

Xavier | 16 |

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