University of Malta

Study-Unit Description
UOM Main Page
Apply - Admissions 2016
Campus Map button


TITLE Principles of Concurrency

LEVEL 05 - Postgraduate Modular Diploma or Degree Course


DEPARTMENT Computer Science

DESCRIPTION In order to be able to construct correct, efficient and dependable software for distributed systems, service-oriented systems and multi-core machines, engineers require a deep understanding of the fundamental concepts of concurrency. This course thus takes a formal approach to the modelling, specification and verification of concurrent systems. It explains how concurrent systems can be described in terms of state-transition models such as labelled transition systems and uses process calculi to model the behaviour of such concurrent systems. Correctness specification and verification is tackled both from the point of view of language equivalence, but also through the use of modal logics.

Study-unit Aims:

1. To familiarise the student with the main issues and characteristics of concurrent systems, such as non-determinism and reactive, non-terminating computation;
2. To show how these aspects affect correctness specification and verification;
3. To teach powerful mathematical tools such as induction and coinduction, and to show how these can be applied to formally reason about these systems;
4. To expose the student to algorthmic solutions to the verification of these systems.

Learning Outcomes:

1. Knowledge & Understanding:
By the end of the study-unit the student will be able to:

- describe a concurrent reactive system's behaviour formally using a Labelled Transition System;
- apply conductive reasoning so as to construct a bisimulation exhibiting the equivalence of two systems. If, conversely, the two systems are not equivalent, the student could also justify their inequality by exhibiting a game strategy that proves the inexistent of a satisfying bisimulation relation;
- formulate properties using modal logics and prove the satisfaction or otherwise of the property of a formally specified system.

2. Skills:
By the end of the study-unit the student will be able to:

- model (concurrent) systems and computation at different levels of abstraction;
- apply compositional design and analysis to programs.

Main Text/s and any supplementary readings:


- Reactive Systems: Modelling, Specification and Verification. Luca Aceto, Anna Ingolfsdottir, Kim Guldstand Larsen, Jiri Srba Cambridge University Press 2007 ISBN: 978-0-521-87546-2


- Communicating and mobile systems: the Pi-calculus Robin Milner Cambridge University Press 1999 ISBN 0-521-65869-1
- Introduction to Bisimulation and Coinduction Davide Sangiorgi Cambridge University Press 2012 ISBN 978-1-107-00363-7
- Modal and Temporal Properties of Processes Colin Sterling Springer 2001 ISBN 0-387-98717-7


STUDY-UNIT TYPE Lecture and Tutorial

Assessment Component/s Resit Availability Weighting
Examination (2 Hours and 30 Minutes) Yes 100%

LECTURER/S Adrian Francalanza

The University makes every effort to ensure that the published Courses Plans, Programmes of Study and Study-Unit information are complete and up-to-date at the time of publication. The University reserves the right to make changes in case errors are detected after publication.
The availability of optional units may be subject to timetabling constraints.
Units not attracting a sufficient number of registrations may be withdrawn without notice.
It should be noted that all the information in the study-unit description above applies to the academic year 2017/8, if study-unit is available during this academic year, and may be subject to change in subsequent years.
Study-unit Registration Forms 2017/8


For Undergraduate (Day) and Postgraduate students.


Academic Advisors 2017/8


Academic Advisors for ICT 1st year students (Intake 2017/8), NOW available

Faculty of ICT Timetables


ICT Timetables are available from Here.

Health and Safety Regulations for Labs Form

The Faculty of ICT Health and Safety Regulations for Laboratories form can be found here



Log In back to UoM Homepage