Comparative Concurrency Semantics

Time & Place:

Tuesdays 12–2pm and Thursdays 12–1pm in Mathews (F23) room 308.

February 28 – April 5 & April 17 – May 24 (i.e. 12 weeks).

Tutorial and discussion Thursdays 2–3pm in Goldstein (D16) room G01.

March 8 – April 5 & April 19 – May 31 (again 12 weeks).

Units of credit: 6 (= ⅛ standard annual study load)

Instructor:

Rob van Glabbeek, Office 522, NICTA (L5), tel. 83060492. Email: rvg@cse.unsw.edu.au

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.

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.

A list of suggested topics, with books and papers on each topic, is being compiled here. Deviations from these suggestions are encouraged. Please inform me of your choice as soon as possible, to make sure that your topic has not yet been claimed by another student. Also select a time slot as soon as you can.

Homework:

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.

Exams:

There will be an in-class exam on Friday June 15 from 9:00-12:00 in ASB 107. At the exam you are allowed to have 4 pages (2 sheets used at both sides) A4 of notes (written or typed), but no other sources of information.

Course credit plan:

Seminar presentation 35%, In-class exam 25%, Tests + Homework 40%.

WWW page:

http://www.cse.unsw.edu.au/~rvg/3152/

Course notes:

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