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:
Our mode of lecturing consist of talking while making drawings on the blackboard (or whiteboard).
We normally aim for an interactive style of teaching where
students understand the material at the time it is delivered.
Hereby we 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 we 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,
or at the latest by 10:00am the following Wednesday.
Here is our late policy.
On request, the solutions will be discussed during the Monday tutorial session.
Twice during the semester (midway, and at the end), you get the opportunity to submit a
portfolio of your best homeworks.