The official time and place, which can be found in
the UNSW time table,
is moot, due the current mobility restrictions. Instead,
recordings of teaching are made available from this
webpage (see link above), and students can watch them whenever they like.
However, the tutorial is delivered synchronously, Thursdays 14:00 - 15:00, via zoom.
June 4 to July 2, and July 16 to August 6.
Moreover, some students may choose to deliver their seminar
presentation to the class synchronously, via zoom, or something equivalent.
This will happen during scheduled class hours, Mondays between
15:00 and 17:00, and/or Tuesdays between 14:00 and 16:00.
Units of credit: 6 (= ⅛ standard annual study load)
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.
Mode of teaching:
My mode of lecturing consist of talking while making drawings on the blackboard (or whiteboard).
I normally aim for an interactive style of teaching where
students understand the material at the time it is delivered.
Hereby I 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 I may ask a student to explain to the rest of the class something I just
talked about, thereby assuming that the mere fact they didn't
interrupt with a question indicates full understanding.
All of that is moot with the current restrictions on classroom teaching.
Instead of interactive lectures there will be recorded ones.
Students should stop the recording when something is unclear
and try to figure it out before continuing. This takes the
place of interrupting with questions. For this reason the
recordings of lectures are not as long as the allocated teaching hours.
The lectures go hand in hand with these notes.
The notes give precise definitions of the concepts I 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 I 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.
Tutorial:
Each Thursday from 2 to 3pm there will be an interactive 1-hour tutorial on
zoom.
You will gain access by means of the password 386800.
It will be used to discuss homework solutions or anything else that is unclear.
By default we only discuss items that are raised by one of the
students attending the tutorial, and often delegate answering
of questions to students as well.
On-line chat
The prime spot for asking questions is
the COMP 6752 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).
Related courses:
COMP3151/9191 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 T1, 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.
Moreover, there will be recordings of lectures.
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 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. You have a choice to present the
material synchronously via zoom or a similar platform, or to
prepare a recording, that others in the class can watch in
their own time. Slides or some other form of a concise message
for the class are welcome. By default, these presentations are
part of the material taught in this class, and exam questions
about them cannot be excluded.
I anticipate roughly 1 seminar presentation per Monday and
Tuesday lecture, starting from June 30. A schedule will be
compiled on the page Lectures and handouts.
Do select a slot by emailing me.
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.
The solutions should be uploaded
here as PDF by 10:00am the following Monday.
Here is my late policy.
Sometimes homework may be labelled "test", meaning that it can be
regarded as a small take-home exam. Such tests (like the final exam) 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.
Tuesday 18-08-2020 from 10:15-13:15am.
That day (if not changed) at 9am the exam will appear on
this webpage, linked from here, and at noon the
same day you are supposed to upload a scan of your answers as PDF in the
homework collection interface.
Do let me know asap if you foresee a problem with that.
You may use piazza if you find an exam question ambiguous,
but I will not answer general questions about the material
during the exam. The university guidelines say "No Exam
Materials permitted". However, this is an open book exam, and
you are free consult all your notes, as well as static
internet nets. (And if you find the answer there, please add a citation.)
But you may not consult other people in any way.
In addition, there will be a short oral exam via Skype or Zoom.
This will occur right after the final exams have been corrected.
I will ask you to select a time slot that is convenient for all concerned.
During the oral exam I may ask you some questions on the
overall material taught in this course, as well as specific
questions on your own answers to the final exam.
Course credit plan:
Tests + Homework 40%, written exam 30%, oral exam 10%, seminar 20%.
Your answers to the oral exam can also alter your written exam score (in both directions).
Course Evaluation and Development: response to class evaluation
The only criticism on this course in the last two 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 of textbooks while treating only a
chapter or two from each of them appears needlessly expensive.