MCS: Modelling Concurrent Systems (Levels 10 and 11)
Welcome to MCS: Modelling Concurrent Systems (Levels 10 and 11)
Learning Outcomes
On successful completion of this course, you should be able to:
- construct accurate models of concurrent systems, including protocols and other distributed communicating systems
- analyse (models of) concurrent systems and show various notions of equivalence and refinement between them
- evaluate the comparative benefits and drawbacks of various concurrency models
- articulate safety and liveness properties of concurrent systems using temporal logic and other tools
- justify the correctness of concurrent systems under various assumptions about their executing context
Course Outline
Beginning with simple examples and protocols, we will develop a theory to describe models of concurrent systems of increasing complexity, based on process algebra. We will learn how to compare these models, and the key concepts that describe what it means for systems to be equivalent, such as bisimulation and trace equivalence. We will learn how to specify and prove properties of systems, and the assumptions we must make about the environment in which these systems operate, such as fairness. The course lectures will introduce concepts using standard examples, and students will apply what they have learned to new problems in homework questions delivered weekly. In tutorials, students can discuss solutions to their homework problems and get feedback on their work, developing their solutions into a summative homework portfolio that they submit for grading at two checkpoints throughout the semester.
Key Details:
Units of Time and place:
Tuesdays and Thursdays 16:00–17:00 in Appleton Tower room 2.11
September 17 – November 28 (i.e. 11 weeks).
Tutorial and discussion Mondays and/or Fridays 15:00–16:00 in Appleton Tower room 5.04.
September 23 – November 25 (i.e. 10 weeks).
Units of credit: 10 (= 1/12 standard annual study load)
Instructor:
Tutor: Rayhana Amjad, Email: rayhana.amjad@ed.ac.uk
Mode of teaching:
My mode of lecturing consist of talking while making drawings on the blackboard (or 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 we 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 we 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 we 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. The solutions will be discussed during the tutorial session.
Exams:
There will be a 2-hour in-class exam in April/May 2025. At the exam you are allowed to have 6 pages (3 sheets used at both sides) A4 of notes (written or typed), but no other sources of information.
Course credit plan:
Homework 60%, written exam 40%. Moreover, you should pass the exam in order to pass the course.
This file will keep track of the material covered so far, and list the handouts distributed to date.