Course notes for COMP4151: Comparative Concurrency Semantics
This file will keep track of the material covered so far, and list the
handouts distributed to date.
Tuesday 1-3-2005
Today I introduced the topics to be treated in this course:
representation, verification and design of concurrent systems.
Representation can be done by means of system description languages
such as CSP or CCS, or by means of models of concurrency such as
process graphs or labelled transition systems. Read the
first section of today's handout for the formal
definitions.
The basic operators common to the languages CCS and CSP are
choice (denoted _+_, an infix written binary operator),
action prefixing (a family of unary operators a._, one
for each action a) and inaction (a constant 0).
I gave a denotational semantics of the language BCCSP consisting of
those operators in terms of process graphs up to isomorphism.
Here are the definitions, in terms of process graphs without
predications and without a notion of final states, of the operators
mentioned above:
-
0 is the graph with one node (state) and no edges (transitions).
This one node is the initial state.
- a.G is obtained from G by adding a new state, which will be
the initial one, and a new a-labelled transition from this new
state to the initial state of G (which is no longer initial in a.G).
- G+H is obtained by taking the union of copies of G and H with
disjoint sets of states, and gluing together the initial states of G
and H. I warned that this definition contains an error, and as nobody
spotted it, this is now homework.
I explained what it means for an equivalence relation to be a
congruence for an operator, or, in other words, for the
operator to be compositional for the equivalence.
Isomorphism is a congruence for the operators above.
There will be homework, to be done by next Tuesday.
Thursday 3-3-2005
I defined two more operators on process graphs without predications
and without a notion of final states, namely the asynchronous parallel
composition || and the synchronous parallel composition or
intersection operator. I also indicated how a denotational
semantics maps the syntax, a system description languages such as CSP,
to a model, such as the class of process graphs.
I described the unfolding operator, turning every process graph
into a process tree. Giving a formal definition of this
operation is homework.
Tuesday 8-3-2005
I gave an overview of topics in the course, treating the overview of
models of concurrency from
the backpage of the
first handout.
Then I defined trace equivalence, completed trace equivalence,
infinitary trace equivalence and infinitary completed trace
equivalence on process graphs, and discussed their merits.
Thursday 10-3-2005
I used the example of a relay race to sketch process algebraic
verification methods, using CSP and CCS. This involved explaining the
parallel composition operators of CCS and CSP in greater detail.
I handed out "Notes on the methodology of CCS and CSP", and the first
chapters of "Process Algebra". You are encourage to browse through the
former, or both. The latter book starts with a bit of universal algebra.
Upon request, I described the meaning of the word
Process algebra.
Tuesday 15-3-2005
We discussed the first-week homework solutions in great detail.
Then we continued the example of the relay race, using it to describe
some differences between CCS, CSP and ACP. To express the interaction
between the two runners, we need to do three things:
- Synchronisation (a parallel composition square with diagonals)
- Restriction or Encapsulation (remove remnants of unsuccessful
communication)
- Abstraction (hide internal actions)
In CSP the parallel composition ||S takes case of 1 and 2,
and there is a separate abstraction operator.
In CCS the parallel composition | takes case of 1 and 3,
and there is a separate restriction operator.
ACP has separate operators for each of them.
Thursday 17-3-2005
In order to compare the behaviour of two systems, we need to take at
least traces and completed traces into account: the latter describe
deadlock behaviour. However, completed trace equivalence is not a
congruence for the synchronous parallel composition of CSP and for the
restriction operators of CCS and ACP. So we need a different semantic
equivalence with the properties that it (1) is a congruence and (2) is
finer than completed trace equivalence. There are several ways to find
such an equivalence. The people working with CCS chose the finest
reasonable equivalence thinkable, namely bisimulation equivalence.
Processes are identified only to avoid problems related to
distinguishing them. The people working with CSP on the other hand
chose the coarsest possible equivalence satisfying (1) and (2), which
is failures equivalence.
Theorem: Given an equivalence relation ~ on a domain D (a set of
mathematical objects such as process graphs), and given a number of
operators on D, there exists a coarsest congruence relation that is
finer than ~.
Such a congruence is called fully abstract with respect to ~
and the operators at hand.
The proof of this theorem is homework.
If ~ is CT-equivalence, then the congruence relation meant above is
called CT-congruence. It will turn out that CT-congruence is
the same as the failures equivalence of CSP.
Please read the definition of bisimulation equivalence in the first handout of this course, and have a look at
Section 4 in the handout on CCS and CSP (which you eventually are
expected to read in full). A more encyclopedic account of semantic
equivalences is found in the linear
time - branching time spectrum. Please read the first 7 pages of
this paper (skipping the first half of page 5) as well as the
paragraphs "definition", "testing scenario" and "infinite processes"
of the Sections 2 and 3.
Tuesday 22-3-2005
I explained recursion as a way of specifying processes, apart
from building them from constants and operators. We'll do that more
formal in April, by operational and denotation methods.
I extended the definitions of trace and completed trace equivalence to
processes with final states, and also defined language equivalence.
See Page 77 of the linear time -
branching time spectrum.
Then I defined simulation equivalence and bisimulation
equivalence. See Definition 8 on Page 28, Figure 5 on Page 29,
Definition 12 on Page 39, and Figure 9 on Page 42 of the linear time - branching time spectrum.
Counterexample 2 on Page 13 shows that simulation equivalence doesn't
respect deadlock behaviour, as represented by completed traces.
I also indicated that for every semantic equivalence =O
there typically is an collection O(p) of observations of
processes p, such that p =O q iff
O(p) = O(q). For trace equivalence =T for
instance, T(p) is the set of traces of p. There also is an
associated preorder, given by p 
O
q iff O(p) O(q).
In case of simulation equivalence we'll need a kind of branching
traces as observations, that will be defined in modal logic.
Thursday 24-3-2005
I presented modal characterisations of trace, simulation and
bisimulation equivalence. See the paragraphs Modal
Characterization in Sections 2, 3, 8 and 12 of the linear time - branching time spectrum
(pages 10, 12 (also reading the first line on page 7), 29 and 40).
No class on 29 and 31 march 2005
Tuesday 5-4-2005
I talked about weak equivalences, abstracting from internal
steps, and explained weak trace equivalence, weak completed
trace equivalence, weak bisimulation equivalence and
branching bisimulation equivalence, as well as the
rooted versions of the latter three.
You should now read all of the first handout,
except for the paragraph on non-well-founded sets. Also, read
Branching Time
and Abstraction in Bisimulation Semantics (Introduction and
Section 1 only; and you may skip the proof of the stuttering lemma).
These links do not cover the root-condition however, nor the
characterisation in terms of coloured traces. These you are supposed
to remember from class (or look up the full version of Branching
Time and Abstraction).
Thursday 7-4-2005
In fact, here is Branching Time and Abstraction.
You should read everything until "Another way" on page 572,
except the proofs of Lemma 2.5 and Theorems 3.5, 3.6, 3.7, 4.5 and 4.8.
Today we discussed complete axiomatisations on BCCS of strong and
branching bisimulation congruence, together with the corresponding
graph transformations. I also distributed a handout with an efficient
algorithm to decide bisimulation equivalence on finite-state systems.
The idea is that if you want to decide whether two finite state systems
are bisimilar, you make a big transition system by taking their
disjoint union, and you create the coarsest consisting colouring.
The system are bisimilar if and only if their initial states get the
same colour. How to make the colouring? Well, a colouring really is a
partition of all possible states. Start out by putting all
states in the same equivalence class, and keep splitting up
equivalence classes whenever their elements can be told apart in terms
of which successor classes can be reached by doing a-steps.
When the equivalence classes need no further splitting, you are done.
The details are in the distributed handout, copied from the handbook
of process algebra. Please read this before Tuesday, and prepare
questions on parts that are unclear.
Tuesday 12-4-2005
I gave some further explanation on rooted weak and branching
bisimulation. There are two equivalent definitions:
- Two process are rooted weak (or branching) equivalent if between
their root-unwindings there exists a weak (or branching) bisimulation
with the property that root nodes are not related to non-root nodes.
- Two processes P and Q are RWB equivalent if
- whenever P --a--> P' then Q ==a==> Q' and P' =WB Q'
- and when Q --a--> Q' then P ==a==> P' and P' =WB Q'.
Here P==a==> Q' denotes an a-step preceded and followed by
arbitrary many tau's. Also, in case a=tau. So the difference with
(unrooted) weak bisimulation is that a tau step is matched by at
least one tau-step.
Likewise, two processes P and Q are RBB equivalent if
- whenever P --a--> P' then Q --a--> Q' and P' =BB Q'
- and when Q --a--> Q' then P --a--> P' and P' =BB Q'.
So a rooted branching bisimulation acts like a strong
bisimulation in the first step.
Then I further explained the efficient decision algorithm for
bisimulation equivalence on finite state systems and indicated that it
applies with minor modifications also to branching bisimulation.
Finally I provided a handout on
c.p.o. theory and denotational semantics, and recommended you read
section 1.
Thursday 14-4-2005
I explained the basic partition-refinement algorithm for branching
bisimulation equivalence, illustrated with an example.
Moreover, I defined c.p.o.'s and continuous functions and stated the
fixed point theorem from the handout. As an example, I showed that the
trace sets of processes form a c.p.o. Here a trace set is
any set of finite sequences over Act that is nonempty and
prefix-closed. (Given prefix-closure, non-emptiness is the same as
requiring that the empty trace is always present.) They are ordered by
set-inclusion. It is a c.p.o. because there is a least element,
namely {epsilon}, the trace set that only contains the empty trace,
and any chain has a limit, namely its union. It is easy to check that
this limit is indeed a trace set (namely nonempty and prefix closed)
and is the smallest trace set that is larger or equal than any trace
set in the chain.
Tuesday 19-4-2005
I explained the basics of denotational semantics, following Section 3
of the handout, but so-far without fixed points and c.p.o.s.
Thursday 21-4-2005
Today we discussed deadlock, livelock and (possibly
fair) divergence, versus normal progress under a progress
assumption. In CSP, as well as in David Walkers version of
bisimulation semantics, livelock and divergence are identified, and
distinguished from normal progress, thereby implicitly assuming
choices to be unfair (a safe worst case scenario). In weak and
branching bisimulation semantics as used in ACP, choices are assumed
to be fair, and fair divergence is identified with normal progress,
and distinguished from livelock. Moreover, there is no distinction
between deadlock and livelock. This helps in the verification of
communication protocols, where you try to send a message as long as
needed until it succeeds and assume it will eventually arrive correctly.
I also explained how n-tuples can be seen as functions from an
n-element set, and the set of functions from A to B is denoted
AB. This helped explaining the type of a denotational
semantics.
Tuesday 26-4-2005
I worked my way through Section 3 of the c.p.o. handout (but skipping
the proof of Theorem 2).
Thursday 28-4-2005
I introduced structural operational semantics, following
this handout. All of this handout is required reading.
Tuesday 3-5-2005
Today I refreshed the our understanding of Hennessy-Milner logic, and
showed that the obvious definition of a "bisimulation preorder" yields
the same as "bisimulation equivalence".
Furthermore I gave some examples of the use of structural operational
semantics, namely the partial synchronous parallel composition of CSP
and, and as example of the use of negative premises, the priority operator.
Thursday 5-5-2005
This Thursday there will be no class; but we will more than make up
for that on Friday 6-5-2005.
Friday 6-5-2005
From 12:30 to 13:30 was the first seminar presentation in this course,
namely by Tim Bourke, on Event structures. Everyone got the
handout Petri Nets, Event Structures & Domains [Nielsen,
Plotkin & Winskel 1981]. Tim treated the translations between
causal nets and elementary event structures, described
in Section 2. These will later be augmented by translations between
elementary event structures and certain Scott domains.
Moreover, the translations will be upgraded to cover a larger class of
Petri nets, and accordingly larger classes of event structures and
domains.
From 14:00 to 14:50 Ansgar Fehnker gave an Introduction
to Explicit State Model Checking, as part of a
reading group on system software design and foundations of formal
methods that started this week. As a reference,
here is the syntax and semantics of CTL.
Tuesday 10-5-2005
I explained how fixed points where treated in Structural Operational
Semantics (SOS), and gave the full SOS of CCS and CSP, following
Sections 6.1 and 6.2 of the handout "Notes on the methodology of CCS
and CSP", also covering Section 5.1.
Now all material of this handout is covered, expect Sections
3.4, 4.5, 4.6, 5.3 (in part), 5.5. (in part) and 6.3--6.5. Read it.
Subsequently I defined 3 SOS formats: the "De Simone"-format, the GSOS
format (see the handout on SOS), and especially the ntyft/ntyxt-format
(in increasing order of generality).
A important theorem says that strong bisimulation equivalence is a
congruence for any operator in a language whose structural operational
semantics is in ntyft/ntyxt-format. All operators of CCS and CSP are in
the "De Simone" format, so surely in the ntyft/ntyxt-format. Hence
bisimulation is a congruence on these languages.
Thursday 12-5-2005
Today Chenyi and I gave the syntax and semantics of the modal
mu-calculus, in preparation of Chenyi's presentation next week.
Tuesday 17-5-2005
First we analysed the meaning of fixed points of modal formulas,
comparing it to the denotational semantics of fixed points of process
operations.
Next I recalled the SOS formats from last Tuesday, and illustrated how
the compositionality w.r.t. bisimulation semantics tends to fail when
we depart from the ntyft/ntyxt-format.
Finally I introduced two kinds of Petri nets, namely
condition/event-systems or B/E-nets and
place/transition-systems or S/T-nets. In the former,
there cannot me multiple tokens in the same place, and a transition
cannot fire if it would violate that requirement.
I sketched the interpretation of the operators 0, a._ and || in
terms of Petri nets.
P.S. Here is a file with the latex macro $\goto$
for making an arrow with a letter above it and here is the corresponding dvi-file.
Thursday 19-5-2005
Chenyi gave a presentation on Game based model checking, based on
Bisimulation, Model Checking and Other Games by Colin Stirling.
My proposal is to include the sessions of the
Goanna reading group of 29-04, 27-05 and 03-06 as part of this course.
The group meets at Applied Science, room 1010, on Fridays at 2:00 PM.
These 3 hours replace the last week of class, which is then cancelled.
Thus, the last day of class is Thursday, June 2.
Let me know at the next class if you object to this change.
Tuesday 24-5-2005
B/E-nets and S/T-nets can be combined into (form special cases of)
S/T-nets with capacities. These can be encoded in a behaviour
preserving way, in terms of ordinary S/T-nets.
The languages recognisable by finite Petri nets are a subclass of the
context sensitive languages, a superclass of the regular languages,
and incomparable with the context-free languages. Tim gave an example
from Peterson's book of a Petri net language that is not context-free.
Petri nets with inhibitor arcs can model counters and hence 2-counter
machines, and thus are as powerful as Turing machines.
Thursday 26-5-2005
Tim presented examples of what goes wrong when violating the
ntyft/ntyxt-format by testing for syntactic equality.
Interleaving versus true concurrency. Orthogonal to the linear time -
branching time spectrum we encountered 5 levels of precision in
modelling causality: interleaving semantics,
step semantics,
split semantics,
ST semantics or interval semantics, and
causal semantics.
Argument for using at least step semantics: modelling simultaneity.
Arguments for using at least ST-semantics: action refinement
and real-time consistency.
Friday 27-5-2005
Introduction to SPIN model-checker and paper review by Ralf Huuck:
Holzmann and Joshi. Model-driven software verification. SPIN, 2004.
Tuesday 31-5-2005
Today we explained the translation between Petri nets, event
structures, configuration structures, domains and process graphs, as
documented in the paper Petri Nets, Event Structures & Domains
by Nielsen, Plotkin & Winskel 1981, that was handed out by Tim on
Friday 6-5-2005. The connection between event structures and process
grahs is explained in this handout, that also
contains homework.
Thursday 2-6-2005
Seminar presentation by Thang.
Friday 3-6-2005
Goanna reading group. Applied Science 1010 at 2:00 PM.
I will be abroad from June 3 to June 18, 2005. I'll answer email
while away, but we can't meet (in Australia).
The final exam for this course will be Monday morning 20-6-2005.