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; 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.
Teaching Rationale (item required by school):
The course is being taught this way because I think
this is the best way to achieve the learning outcomes.
Topics covered:
Models of concurrent and distributed systems
(e.g. labelled transition systems, process algebra, event
structures, Petri nets, Büchi 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, not taught this year, 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,
taught in parallel, 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 provides 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, and the webpage Notes.
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 11:30am.
Here is my late policy.
I plan to return corrected homework to class on Mondays (or
Wednesdays for homework that is hand-delivered in Monday's tutorial),
and, on request, discuss the solutions during the
Monday 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.
Course Evaluation and Development: response to CATEI evaluation
The only criticism on this course in the last CATEI evaluation
was the lack of a textbook, given that there is a steep learning curve.
Unfortunately there is no textbook that covers all aspects of
this course, and prescribing a handful textbooks while treating only a
chapter or two from each of them appears needlessly expensive.