Modelling Concurrent Systems

Time & Place:

Tuesdays 16:00–17:00 and Thursdays 16:00–17:00 in Appleton Tower room 2.11.

September 17 – November 28 (i.e. 11 weeks).

Tutorial and discussion Mondays 15:00–16:00 and/or Fridays 15:00–16:00 in Appleton Tower room 5.04.

September 23 – November 29 (i.e. 10 weeks).

Units of credit: 10 (= 1/12 standard annual study load)

Instructor:

Rob van Glabbeek, Email: Rob.van.Glabbeek@ed.ac.uk

Tutor:

Rayhana Amjad.

Aim:

This course tries to make students familiar with state-of-the-art techniques in modelling concurrent systems. This is done by comparing some of the more successful semantic models of concurrency found in the literature. The focus will be on the rationale behind the design decisions underlying those models, viewed from philosophical, mathematical and computational perspectives. The course contains important background knowledge for students aiming at a scientific career in which the design of mathematical models of system behaviour is a component.

Learning Outcomes:

By the end of the course students should be able to accurately model simple concurrent systems, in particular by being able to make an informed choice, out of the many types of models available, as to which one is (most) suitable for the task at hand. Additionally, they should be able to prove elementary properties of systems modelled thusly.

Method:

Lecturing; distribution of scientific handouts inviting to self-study; and challenging homework assignments that invite students to mix the mastered techniques with their own creativity.

Mode of teaching:

My mode of lecturing consist of talking while making drawings on the whiteboard. I normally aim for an interactive style of teaching where students understand the material at the time it is delivered. Hereby I try to discourage taking notes with the mere aim of deciphering them later. Students should ask questions at the time that something is less than 100% clear. Occasionally I may ask a student to explain to the rest of the class something I just talked about, thereby assuming that the mere fact they didn't interrupt with a question indicates full understanding.

The lectures go hand in hand with these notes. The notes give precise definitions of the concepts I teach, whereas the lectures are more hand-waving and try to illustrate their use. It is not possible to master the material while skipping reading the notes, and it is (almost) impossible to master the material without listening to the lectures. To reduce duplicate efforts, in the lectures I normally skip any formal definitions that can be found in the notes, and the notes normally skip examples and illustrations that are done in the lectures.

Video recordings of the lectures of a previous incarnation of this course, given at UNSW Sydney, are linked from the syllabus. Although the material has changed a little bit, these form another way to ingest much of this course offering.

On-line chat

The prime spot for asking questions is the MCS piazza exchange forum. All students are encouraged to answer the questions of other students in this forum.

Topics covered:

Models of concurrent and distributed systems (e.g. labelled transition systems, process algebra, event structures, Petri nets), operational and denotational semantics, semantic equivalences and refinement relations (linear versus branching time, interleaving versus partial order semantics), modal and temporal logic for concurrent systems (proof theory and applications).

Prerequisites:

The ability to understand and deliver formal mathematical proofs.

Course material:

Scientific papers to be handed out, and the webpage Notes. Moreover, there are video recordings of the lectures of a previous incarnation of this course.

Homework:

Assignments will be posted here each week. Each weekly homework comes in two batches; one following each of the two lectures given that week. Your solutions should be uploaded here as PDF by 10:00am the following Tuesday, or at the latest by 10:00am the following Wednesday. Here is my late policy. On request, the solutions will be discussed during the Friday and Monday tutorial sessions.
Twice during the semester (midway, and at the end), you get the opportunity to submit a portfolio of your best homeworks.

Exams:

There will be a 2-hour in-class exam. Strangely, the school has scheduled this exam to be in the 2nd semester exam diet (29 April - 24 May 2025). At the exam you are allowed to have 6 pages (3 sheets used at both sides) A4 of notes, but no other sources of information.

Course credit plan:

Homework 60% (namely 30% for each of your two portfolios), written exam 40%. Moreover, you should pass the exam in order to pass the course.

WWW page:

https://homepages.inf.ed.ac.uk/rvangla/MCS/

Course notes:

This file will keep track of the material covered so far, and list the handouts distributed to date.