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.
Method:
Lecturing; distribution of scientific handouts inviting to
self-study; challenging homework assignments that invite
students to mix the mastered techniques with their own
creativity; and seminar presentations in which students learn
how to digest and present relevant material.
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.
Topics covered:
Models of concurrent and distributed systems
(e.g. labelled transition systems, process algebra, event
structures, Petri nets, Buchi automata),
operational and denotational semantics,
semantic equivalences and implementation relations (linear versus branching time,
interleaving versus partial order semantics),
modal and temporal logic for concurrent systems (proof
theory and applications).
Related courses:
COMP3151/9191, taught last spring, also addresses the
modelling of concurrent systems, but with more emphasis on
communication via shared variables, and the solutions of
classical problems like mutual exclusion.
COMP3153/9153,
last taught last year, focuses more on the
applications of theories of concurrency than on their design.
This course describes several automatic verification
techniques, the algorithms they are based on, and the tools
that support them. It discusses examples to which the
techniques have been applied, and provide experience with the
use of several tools.
Prerequisites:
The ability to understand and deliver formal mathematical proofs.
Course material:
Scientific papers to be handed out or found in the library.
Seminar presentations:
Some lectures will consist of seminar presentations by
students taking the class. Every student is anticipated to present
(at least) one seminar, roughly 30 minutes to an hour long.
Upon request, the possibility exists to split presentations
over multiple weeks.
In preparation for your presentation you select a topic, read one
or more papers or (parts of) books on that topic, and make a summary
to be presented to the class. The mode of presentation can be
anything you like. You are encouraged to include a handout for
the class, containing a few vital points you want to get across.
Assignments will be posted here each
week, due back the following Monday at noon.
Here is my late policy.
I plan to return corrected homework to class on Tuesdays or
Thursdays, and, on request, discuss the solutions during the
Thursday tutorial session.
Sometimes homework may be labelled "test", meaning that it can be
regarded as a small take-home exam. Such tests must be done
without any collaboration whatsoever. For the normal homework,
collaboration is allowed as long as (1) you acknowledge in
writing all the people you discussed the problem with, and (2)
each student writes up his/her own solution without looking at
any writeup/notes from another student.