## Objectives

The course provides a perspective on process algebra (architecture & calculi).

We start with well-established classical and probabilistic process algebras and illustrate their use in software engineering.

Given the rapid emergence of cyber-physical systems, we next give a special focus to timed and cyber-physical process algebras.

Finally, we lean on more uniform notions and techniques in process algebra, with the goal of giving theoretical foundations to the student and the tools necessary for (s)he to smoothly learn/adapt to modeling and reasoning about software composition in different computational paradigms.

This final part of the course will have a more theoretical, research-centred character, briefly presenting current research challenges.

## Syllabus

• Process Algebra: Nondeterministic and probabilistic systems.
• Labelled transition systems: Syntax, semantics, morphism and notions of equivalence (traces, bisimilarity and its variants).
• Algebra of nondeterministic processes: CCS (syntax, semantics and equational reasoning).
• Generalizing transition systems to the probabilistic case.
• Process algebra and modal logics: The Hennessy-Milner logic.
• Process Algebra: Cyber-physical systems.
• Timed Automata: Syntax, semantics, and notions of equivalence.
• Hybrid Automata: Syntax, semantics, and notions of equivalence.
• Introduction to UPPAAL.
• Process Algebra: An abstract view.
• Background: Monads and computational processes.
• Software components: Language and semantics.
• Interleaving and iteration.

## Summaries (2020-21)

Virtual classroom: ⚠ Links available in the summaries below ⚠

NOTE: Video record available from the course BlackBoard platform (in contents)

• Feb 18:

T - Introduction to the course: objectives, syllabus, pragmatics. Labelled transition systems. Determinism, non determinism and probabilism. Corresponding notions of morphism. [slides]

PL - Exercises on labelled transition systems. [exercises]

• Feb 24:

T - Probabilistic transition systems. Behavioural equivalences. Simulation and bisimulation for non-deterministic systems. Bisimilarity. [slides]

PL - Exercises on bisimilarity. [exercises]

• Mar 4:

T - Introduction to process algebra. Detailed study of CCS (Milner's Calculus of Communicating Systems): Operational semantics, expansion theorem; silent transitions. [slides]

PL - Exercises on bisimilarity (conclusion)

• Mar 11:

T - CCS: laws of calculus of reactive systems. The expansion theorem.

PL - Examples: specification of reactive systems in CCS.

• Mar 18:

T - Observational equivalences. The logic of Hennessy-Milner.

PL - Introduction to mCRL2: process modelling and verification. [slides] [tutorial] [file]

T - Real-time computing. Timed labelled transition systems: definition, examples, notions of composition, and observational equivalence.

PL - Exercises and examples. [slides]

• Apr 1: Easter holidays

• Apr 8: (lecture by Guillermina Cledou, Zoom link)

T - Advanced aspects of timed labelled transition systems: timelock and Zeno behaviour.

PL - UPPAAL (hands-on). [slides] [exercise]

T - Natural deduction: deductive reasoning and programming under the same umbrella. Simply typed lambda-calculus: equational system and semantics.

PL - Exercises. [slides]

T - Integration of algebraic operations in the simply typed lambda-calculus: read/send operations, latency, nondeterministic/probabilistic choice, cyber-physical interaction...

PL - Exercises. [slides] [code]

T - Sharing contexts: tensorial strength.

PL - Exercises. [slides]

T - The Hoover dam, a simple calculator, and the Knight's quest. A zoo of monads.

PL - Exercises. [slides] [Hoover dam and calculator] [Knight's quest]

T - Continuation of the previous lecture. Open challenges software architecture and calculi.

PL - Exercises.

## Pragmatics

### Assessment

• Two group assignments (groups of two students) to be presented and discussed with the class (80%).
• A number of short exercises (TPC-style) assigned regularly after classes to be solved individually (20%).
##### 1º Trabalho prático
O primeiro trabalho prático vai incidir na modelação e análise de um sistema ciber-físico com base na ferramenta UPPAAL. Datas relevantes:
• Publicação do trabalho no dia 14 de Abril 2021 (enunciado);
• Entrega até ao dia 18 de Maio de 2021;
• Apresentações no dia 20 de Maio de 2021.
##### 2º Trabalho prático
O segundo trabalho prático vai incidir na modelação e análise de um sistema ciber-físico com recurso a mónadas. Datas relevantes:
• Publicação do trabalho no dia 14 de Maio de 2021 (enunciado); (código);
• Entrega do trabalho até ao dia 15 de Junho de 2021;
• Apresentações no dia 17 de Junho de 2021.

##### Contact
• Appointments - Luis: Wed, 18:00-20:00 and Fri, 18:00-20:00 (please send an email the day before)
• Appointments - Renato: Wed, 17:00-18:00 (please send an email the day before)
• Last update: 2021.03.17