COMP6752: Topics in Concurrency

Topics, with suggested reading

Claimed topics:

Modal and temporal logic by Vivian Dang.
Hennessy–Milner Logics: Weak and Branching Bisimulation by Vincent Jackson.
Petri nets by Tiankuang Zhang.
Reasoning about knowledge in distributed systems by Courtney Darville.
Algorithmic verification by Aidan Farrell

Process algebra

Possible subjects for seminar talks are system description languages like CCS, CSP, ACP, LOTOS, mCRL2, the π-calculus or others. One idea is to take one of the main textbooks on process algebra (mentioned in the link above) and talk about any bit of it that we haven't covered yet in class. See also the links in the first handout.

Denotational semantics.
Structural operational semantics
Either could be one or more talks; for instance based on the handbook article mentioned in the link above.
Tools for the Specification and Verification of Concurrent Systems

Semantic models of concurrent and distributed systems

Event structures: do a web search especially on papers by Winskel. Here is a good one. Or this handout by me, from a previous version of this class that included event structures.
Petri nets
Chu spaces

A very nice talk could be based on the introductory paper on event structures by Nielsen, Plotkin and Winskel (1981): "Petri nets, event structures and domains, part I", TCS 13(1), pp. 85-108. Or tell us about Chu spaces, following the introduction on the website above. For Petri nets, the book by Reisig or the introductory paper by Peterson would make for a good first talk.

Semantic equivalences

linear versus branching time
In class I will treat only a few process semantics, but there are many others. My own overview paper linked above is a good starting point. Interesting talks could be about ready simulation semantics, following the paper by Bloom, Istrail and Meyer, or about failures (= testing) semantics, following the papers by Brookes, Hoare & Roscoe, Olderog & Hoare, or by Hennessy & De Nicola (references in the paper linked above). Or possibly my own paper on reward testing which elaborates on the work of Hennessy & De Nicola.
interleaving versus partial order semantics, true concurrency

Algorithms and decidability

Modal and temporal logic for concurrent systems

The linear time logic LTL or the branching time logic CTL* would be great subjects for seminar presentations. In my own paper CTL with deadlock detection there are a few good references to other papers on CTL and CTL*. More references on request.

Algorithmic verification

This topic will not be treated in class, as there is a separate course on it: COMP3153/9153. Nevertheless, you may select this topic for a seminar presentation.

model checking
automata on infinite structures
synthesis

Books:

E.M. Clarke, O. Grumberg & D.A. Peled: Model Checking, MIT Press.
R.P. Kurshan: Computer Aided Verification of Coordinating Processes, Princeton Series in Computer Science.

A talk could be based on one of those books.

Reasoning about knowledge in distributed systems

R. Fagin, J. Halpern, Y. Moses & M.Vardi: Reasoning about Knowledge, MIT Press.

Rob van Glabbeek

rvg@cse.unsw.edu.au