COMP6752 — 2018 — Course outline

Topics Notes Homework

Modelling Concurrent Systems

Time & Place:
Mondays 10:00–12:00 in Business School (E12) room 130 and Tuesdays 10:00–11:00 in Business School (E12) room 232.
February 26 – March 27 & April 9 – May 22 (i.e. 12 weeks).
Tutorial and discussion Tuesdays 13:00–14:00 in Mathews (F23) room 309.
March 6–27 & April 10 – May 29 (i.e. 12 weeks).
Units of credit: 6 (= ⅛ standard annual study load)
Instructor:
Rob van Glabbeek, Data61, CSIRO, tel. 9490 5938. 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.
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.
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 10:00am. 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.
Exams:
There will be a 3-hour in-class exam during June 2018. 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 30%, In-class exam 30%, Tests + Homework 40%.
Course Evaluation and Development: response to CATEI evaluation
The only criticism on this course in the last CATEI evaluations 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.
WWW page:
http://www.cse.unsw.edu.au/~rvg/6752/
Course notes:
This file will keep track of the material covered so far, and list the handouts distributed to date.

Rob van Glabbeek rvg@cse.unsw.edu.au