Course notes for COMP6752: Comparative Concurrency Semantics
This file will keep track of the material covered so far, and list the
handouts distributed to date.
Wednesday 232016
Today I introduced the topics to be treated in this course:
formalising specifications as well as implementations of concurrent
systems, studying the criteria for deciding whether an implementation
meets a specification, and techniques for proving this.
Look here for the broader context.
Both specifications and implementations can be represented by means
of models of concurrency such as
labelled transition systems (LTSs) or process graphs.
I present the definition below.
Another way to represent concurrent systems is by means of process
algebraic expressions.
These concepts were illustrated by means of an example
(see below). It shows
how an implementation could be given as parallel composition of
components, enforcing synchronisation on certain actions.
When both specifications and implementations are given as LTSs, we
need a criterion or as to determine if they match. I indicated a
criterion based on bisimulation, that matched the states of the
related LTSs. I showed why it is useful here to abstract from
internal actions of the implementation.
When the specification and implementation are given as process
expressions, to decide whether they match one considers the meaning,
or semantics of these expressions. Often, this meaning is
given by mapping them to LTSs.
A process graph is a triple (S,I,→), with S a set
(of states), I∈S an initial state,
and → a set of triples (s,a,t) with s,t
∈S and a an action, drawn from a set Act.
An LTS is just a process graph without initial state.
(But sometimes LTS is used as synonym for process graph, i.e. with
initial state.)
We'll also use process graphs with a fourth component ✔⊆S
indicating the final states of the process: those in which the
system can terminate successfully.
Specifications and implementations can not only be represented by LTSs
or other models of concurrency, but also by process algebraic
expressions, where complex processes are build up from constants for
atomic actions using operators for sequential, alternative and
parallel composition. The most popular process algebraic languages
from the literature are CCS (the Calculus of Communicating Systems),
CSP (Communicating Sequential Processes) and ACP (the Algebra of
Communicating Processes). I present the syntax of
ACP, focusing on the partially synchronous parallel
composition operator.
The corresponding textbook is
J.C.M. Baeten & W.P. Weijland (1990): Process Algebra, Cambridge
University Press
or
W.J. Fokkink (2000):
Introduction to Process Algebra, Texts in
Theoretical Computer Science, An EATCS Series, Springer.
The syntax of ACP, the Algebra of Communicating Processes,
features the operations
 ε (successful termination)
(only present in the optional
extension ACP_{ε})
 δ (deadlock)
 a (action constant) for each action a.
 P.Q (sequential composition)
 P+Q (summation, choice
or alternative composition)
 PQ (parallel composition)
 ∂_{H}(P) (restriction, or
encapsulation) for each set of visible actions H.
 τ_{I}(P) (abstraction) for each set of
visible actions I
(only present in the optional
extension ACP_{τ}).
The atomic actions of ACP consists of
all a, b, c, etc. from a given set A
of visible actions, and one special action τ, that is meant to be
internal and invisible to the outside world. For each application, a
partial communication function γ: AxA > A is
chosen that tells for each two visible actions a and b whether
they synchronise (namely if γ is defined), and if so, what is
result of their synchronisation: γ(a,b).
The communication function is required to be commutative and associative.
The invisible action cannot take part in synchronisations.
Here are the definitions of these operators, in terms of process
graphs extended with a predicate ✔ that signals successful termination.

ε is the graph with one state and no transitions.
This one state is the initial state. It is marked with ✔.

δ is the graph with one state and no transitions.
This one state is the initial state. It is not marked as terminating.

a is a graph with two states (and initial and a final one) and
one transition between them, labelled a. The final state is
marked with ✔.
 G.H is the process that first performs G, and upon
successful termination of G proceed with H.
It is homework to write down a formal definition.
 G+H is obtained by taking the union of copies of G
and H with disjoint sets of states, and adding a fresh
state root, which will be the initial state of G+H.
For each transition I_{G} a> s in G, where
I_{G} denotes the initial state of G,
there will be an extra transition root a> s, and likewise,
for each transition I_{H} a> s in H, where
I_{H} denotes the initial state of H,
there will be an extra transition root a> s.
root is labelled with ✔ if
either I_{G} or I_{H} is.
 GH is obtained by taking the Cartesian product of the states of
G and H; that is, the states of GH are pairs (s,t) with
s a state from G and t a state from H. The initial state
of GH is the pair of initial states of G and H.
A state (s,t) is labelled ✔ if and only if both s
and t are labelled ✔. The transitions are
 (s,t) a> (s',t) whenever s a> s' is a transition in G,
 (s,t) a> (s,t') whenever t a> t' is a transition in H, and
 (s,t) c> (s',t') whenever s a> s' is a transition in G
and t b> t' is a transition in H, and γ(a,b)=c.
Intuitively, GH allows all possible interleavings of actions
from G and actions from H. In addition, it enables
actions to synchronise with their communication partners.
 ∂_{H}(G) is just G, but with all
actions in H omitted.
It is used to remove the remnants of unsuccessful communication, so
that the synchronisation that is enabled by parallel composition, is enforced.
 τ_{I}(G) is just G, but with all
actions in I renamed into τ.
Here is the example of the relay race presented in class.
There are two runners R_{1} and R_{1}
participating in the relay race, and while running they carry a baton.
Runner 1 starts running, and at the halfwaypoint passes the baton to
runner 2, who is waiting there. Then runner 2 runs the rest of the
race and delivers the baton at the finish.
We can describe the behaviour of the two runners by the ACP expressions:
R_{1} = start.give
R_{2} = receive.finish
Here start is the action of runner 1 starting the race,
give is the finish of runner 1 at the halfwaypoint,
where R_{1} gives the baton to R_{2},
receive is the action of runner 2 to accept the baton from runner 1 and start running,
and finish is the action of runner 2 of arriving at the finish.
An ACP expression describing the whole interaction is
τ_{I}(∂_{H}(R_{1}  R_{2}))
with H={give,receive} and I={handover}.
Here the communication function γ is given
by γ(give,receive) = γ(receive,give) = handover.
We drew the corresponding process graph in class, and after deleting
unreachable parts it looked just like the process graph of the expression
start.τ.finish
However, from a very high level of abstraction, where we abstract from
the relay in the relay race, and rather focus on the baton, which we
see departing by the action start, and subsequently arriving at
the finish by the action finish, we may want to specify the
overall behaviour of this race as
start.finish
To formally prove that the implementation matches this specification,
we need a relation between these processes that abstracts from the
internal action τ.
Thursday 332016
Today I presented the syntax semantics of the process algebra ACP.
See above for details.
The semantics presented was of the denotational kind,
and in terms if process graphs equipped with a state label ✔,
indicating successful termination. Here "denotational" entails that
each constant denotes a process graph (up to isomorphism)
and each ACP operator denotes an operational on process graphs
(creating a new graph out of one or two argument graphs).
I also treated the optional extension ACP_{ε},
whose semantics is given by process graphs (or LTSs) in which not only
end states but also intermediate states may be marked ✔.
Furthermore, I indicated why one would want to distinguish the processes
b + c and τ.b+τ.c. The reason is that in a context
of an environment that admits synchronisation on b,
but not on c, the first process always performs the (weak)
trace b,
whereas the second has the possibility to reach a state
of deadlock after doing the internal step τ.
Deadlock is a (bad) state of a system, in which no further actions are
possible, and the system does not terminate successfully.
Subsequently I introduced the concept of an equivalence relation, and recalled
that any equivalence relation on a set D gives rise to a partitioning
of D into equivalence classes (see Homework 1). Now one equivalence
relation ≡ is called finer (or more discriminating)
than another equivalence relation ~ if each ≡equivalence class
is included in a ~equivalence class, i.e. when p≡q
implies p~q for all p,q in D. Conversely, ~ is
called coarser than ≡.
Two processes p and q are partial trace
equivalent, notation P =_{PT} Q, if they have the
same partial traces. Here a partial trace of a process p
is the sequence of transition labels encountered on a path in the
process graph of p, starting from the initial state. Here a path can
be defined as an alternating sequence of states and transitions, where
each transition goes from the state before it to the state after it.
Processes p and q are completed trace equivalent,
notation P =_{CT} Q, if moreover they have the same
complete traces. Here a completed trace is a state that stems from a
maximal path; one that cannot be prolonged at the end.
One of the things we learned from the example of the relay race
is that we need an equivalence relation on processes that abstracts
from the internal action τ.
To formally prove that the implementation matches this specification,
we need a semantic equivalence that makes start.τ.finish equivalent with
start.finish. Such equivalences are called weak
or abstract. In contrast, an equivalence that treats τ
like any other action is strong or concrete.
The definitions of partial and completed trace
equivalence we encountered above
can all be regarded as definitions of strong partial trace
equivalence and strong partial completed trace equivalence, as long as we
treat τ like any other action. To arrive at a definition of weak
partial trace equivalence (=_{WPT}), we define a weak partial trace of a
process p as a strong partial trace of p from which all the
occurrences of τ have been omitted. Now two processes are
called weak partial trace equivalent if they have the same weak
partial traces. Weak completed trace equivalence can be defined
in the same vein.
Wednesday 932016
Today we looked at equivalence relations on process graphs or labelled
transition systems that are finer than partial or completed trace
equivalence, in the sense that they make more distinctions.
As a motivating example I indicated why one would want to distinguish
the processes
a.(b+c) and a.b + a.c. The reason is that in a context
of an environment that admits synchronisation on a and b,
but not on c, the first process always performs the trace ab,
whereas the second has the possibility to reach a state
of deadlock after doing a.
The definition of bisimulation equivalence, also called bisimilarity,
can be found in this handout,
which you should read until the header "Modal logic".
In that handout, LTSs and process graphs have an extra component ⊨
that is used to tell whether certain predicates, taken from a set P,
hold in certain states of our processes. In this course, we typically
consider only one predicate, namely ✔, telling that successful
termination is possible in a state. For this reason, a quadruple
(S,I,→,⊨) is presented as (S,I,→,✔).
On the set of all process graph we can study multiple equivalence
relations and order them w.r.t. their discriminating power.
I drew a spectrum of equivalence relations, with finer ones
located above coarser ones.
In this spectrum I located partial trace equivalence,
completed trace equivalence and
bisimulation equivalence, and treated examples showing their differences.
Bisimulation equivalence is at the top of the spectrum and
partial trace equivalence near the bottom. Completed trace equivalence
is somewhere in between.
Bisimulation equivalence is called a branching time equivalence,
because it takes into account at which point two different traces
branch off. Partial and completed trace equivalence at the other hand
are linear time equivalences, as they only focus on the linear
executions of a process, without taking branching into account.
The spectrum of weak trace equivalences is the same as in the strong case:
weak completed trace equivalence is finer (more
discriminating) than weak partial trace equivalence.
A weak version of bisimilarity is even finer.
Defining a weak form of bisimilarity is relatively tricky. As
we will see tomorrow by example, just contracting all τmoves in a labelled
transition system doesn't yield what we want to get. There are
several, subtly different, approaches in the literature. The most
prominent ones are weak bisimilarity and branching bisimilarity,
both defined in the abovelinked handout.
Thursday 1032016
In order to describe infinite processes in a language like ACP, we add
a bunch of constants X,Y,Z to the languages, known as process names.
Each process name X comes with a defining equation X = P_{X}
where P_{X} is any expression in the language, possibly
including X, or any other process names. The set of all such
defining equations (that are created separately for each application
of the language) is called a recursive specification. If any occurrence of a
process name in P_{X} lays within the scope of a
subexpression a.P'_{X} of P_{X}, the
recursive specification is guarded. Process names from a
guarded recursive specification are a good way to define (possibly
infinite) processes. An example is an a loop, defined by the
recursive specification X = a.X.
The syntax of CCS, the Calculus of Communicating Systems,
features the operations
 0 (inaction)
 a.P (action prefix) for each action a.
 P+Q (summation, choice
or alternative composition)
 PQ (parallel composition)
 P\a (restriction) for each action a.
The atomic actions of CCS consists of
all a, b, c, etc. from a given set A,
together with the complementary actions
a for each a
in A, and one special action τ, that is meant to be
internal and invisible to the outside world. By convention, if we put
an overbar over a complementary action
a, we get a again.
Here are the definitions, in terms of process graphs without
predicates and without a notion of final states, of the operators
mentioned above:

0 is the graph with one state and no transitions.
This one state is the initial state.
 a.G is obtained from G by adding a new state, which will be
the initial one, and a new alabelled 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 adding a fresh
state root, which will be the initial state of G+H.
For each transition I_{G} a> s in G, where
I_{G} denotes the initial state of G,
there will be an extra transition root a> s, and likewise,
for each transition I_{H} a> s in H, where
I_{H} denotes the initial state of H,
there will be an extra transition root a> s.
We can think of this operator, as unwinding the initial states
(roots) of G and H, and then gluing together
these roots to form the new initial state of G+H.
 GH is obtained by taking the Cartesian product of the states of
G and H; that is, the states of GH are pairs (s,t) with
s a state from G and t a state from H. The initial state
of GH is the pair of initial states of G
and H. The transitions are
 (s,t) a> (s',t) whenever s a> s' is a transition in G,
 (s,t) a> (s,t') whenever t a> t' is a transition in H, and
 (s,t) τ> (s',t') whenever s a> s' is a transition in G
and t a> t' is a transition in H.
Intuitively, GH allows all possible interleavings of actions
from G and actions from H. In addition, it enables
actions a to synchronise with their complementary actions
a; the result of such an
synchronisation is the internal action τ.
 G\a is just G, but with all actions a and
a omitted.
It is used to remove the remnants of unsuccessful communication, so
that the synchronisation that is enabled by parallel composition, is enforced.
Processes with loops are specified by means of recursive specifications,
just as for ACP (see above).
The main differences between ACP and CCS are:
 ACP makes a distinction between deadlock and
successful termination. As a consequence, action prefixing can be
replaced by action constants and a general sequential composition.
This would not work for CCS, as the behaviour of the sequential
composition depends on the successful termination of the first
component, which is not modelled in CCS.
 ACP adds two auxiliary operators, the left merge and the
communication merge, to enable a
finite equational axiomatisation of the parallel composition.
We have not treated this yet, and skipped those two operators for now.
 Whereas CCS combines communication and abstraction from internal
actions in one operator, in ACP these activities are separated. In CCS
the result of any communication is the unobservable action τ. In
ACP it is an observable action, from which (in the extended language
ACP_{τ}) one can abstract by applying an abstraction
operator τ_{I}, renaming designated actions into τ.
 CCS adheres to a specific communication format, admitting
only handshaking communication, whereas ACP allows a variety of
communication paradigms, including ternary communication, through the
choice of the communication function γ.
Weak and branching bisimulation equivalence, from the
handout;
read the section "Abstraction".
We also defined when one process simulates another. This is
like bisimulation, but in the transfer property the initiative is
always taken by the simulated
process, and the matching move should be taken by the simulating
process. Two processes are simulation equivalent if one
simulates the other and vice versa. This is not the same as
bisimulation equivalence, for there we insists on a single
relation that is at the same time a simulation in both directions.
The processes ab+a(b+c) and a(b+c) simulate each other,
but are not bisimulation equivalent.
When adding simulation equivalence to the spectrum of equivalence
relations that had already partial trace equivalence, completed trace
equivalence and bisimulation equivalence in it, it turns out that
simulation equivalence is finer that =_{PT}, coarser
than =_{B}, and incomparable with =_{CT}.
Wednesday 1632016 (by P. Höfner)
Today we looked at the HennessyMilner logic (HML).
It is modal logic. A brief summary of model logic can be found
in the handout.
Note, that my treatment is slightly different.
In particular I allowed modal operators specifying a set of actions, rather than
a single action.
The syntax of HML is given by
Φ = true
 false
 Φ∧Φ
 Φ∨Φ
 ¬Φ
 [K]Φ
 <K>Φ
If a process E has a property Φ, we write E ⊨ Φ.
The formal semantics is defined as follows
E ⊨ true   
E ⊭ false   
E ⊨ Φ∧Ψ  iff  E ⊨ Φ and E ⊨ Ψ 
E ⊨ Φ∨Ψ  iff  E ⊨ Φ or E ⊨ Ψ 
E ⊨ [K]Φ  iff  ∀F∈{E':Ea>E' and a∈K} . F ⊨ Φ 
E ⊨ <K>Φ  iff  ∃F∈{E':Ea>E' and a∈K} . F ⊨ Φ 
Note that some of the operators can be expressed in terms of others.
In the lecture I explained HML using a couple of different examples.
I also showed how to model the concept of deadlock or termination in HML.
We then looked into properties of HML formulas and processes.
In particular, we defined when two processes are indistinguishable.
Thursday 1732016 (by P. Höfner)
In today's lecture we continued to discuss HennessyMilner logic (HML). In particular we discuss some limitations of HML;
some of the limitations are not present when using another logic, namely Computation Tree Logic (CTL).
Therefore, we had a look at the syntax and the semantics of CTL. A couple of examples illustrated the power
and expressiveness of CTL. (A good overview over CTL can be found on
Wikipedia).
The last logic we discussed today was
Lineartime Temporal Logic (LTL).
Wednesday 2332016 to Thursday 742016 (by K. Engelhardt)
See this page,
also for homework.
Wednesday 1342016
I recalled 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.
This is what makes formal verification of big systems given as parallel compositions feasible.
An equivalence ~ is a congruence for a language L if
P ~ Q implies that C[P] ~ C[Q]
for every context C[ ]. Here a context C[ ] is an
Lexpression with a hole in it, and C[P] is the result of
plugging in P for the hole.
It is not hard to show that (strong) partial trace equivalence is a
congruence for encapsulation. This follows because the partial traces of
∂_{H}(P) are completely determined by the partial
traces of the process P itself (namely by removing all partial
traces with actions from H).
The same argument can be used to see that partial
trace equivalence is a congruence for all operators of CCS and ACP.
Partial trace equivalence is inadequate to deal with deadlock.
Adding deadlock information to partial trace semantics
yields completed trace semantics. However, completed trace equivalence
is not a congruence for all operators. It fails for the restriction
operator of CCS, which is the same as the encapsulation operator of ACP.
A counterexample was presented in class.
Strong bisimulation equivalence on the other hand is a congruence for all
operators of ACP, CCS and CSP. This is a reason to use bisimulation rather
then partial or completed trace equivalence.
(Treated through homework only:)
The congruence closure ~_{L} of ~ is defined by
P ~_{L} Q if and only if C[P] ~ C[Q]
for any Lcontext C[ ].
It can be shown that ~_{L} is the coarsest congruence finer than ~.
(Note that there are three statements in that last sentence.)
Thursday 1442016
I will give an introduction to equational logic, and present a complete
equational axiomatisation of bisimulation equivalence on the language
of (very) basic CCS (only using 0, action prefixing and +).
The axioms for BCCS are
$$\begin{array}{cc}
(P + Q) + R = P + (Q + R) & \mbox{(associativity of the +)} \\
P + Q = Q + P & \mbox{(commutativity of the +)} \\
P + P = P & \mbox{(idempotence of the +)} \\
P + 0 = P & \mbox{(0 is a neutral element of the +)} \\
\end{array}$$
If we want to axiomatise partial trace equivalence instead of
bisimilarity, there is an extra axiom
$$\alpha.(P+Q) = \alpha.P + \alpha.Q$$
Such equational axiomatisations all use the following rules
of equational logic:
$$P=P \qquad \frac{P=Q}{Q=P} \qquad \frac{P=Q \quad Q=R}{P=R} \qquad
\frac{P=Q}{C[P] = C[Q]}
\mbox{for any context} C[\ ].$$
Here, the equality signs = can be read as bisimilarity or any other
appropriate equivalence.
Expansion Theorem for CCS: Let $P := \sum_{i\in I}\alpha_i.P_i$
and $Q := \sum_{j\in J}\beta_j.Q_j$. Then
$$P  Q = \sum_{i\in I} \alpha_i (P_i  Q) + \sum_{j\in J} \beta_j (P  Q_j) +
\sum_{\begin{array}[t]{c}i\in I, j \in J \\ \alpha_i =
\bar\beta_j\end{array}}\tau.(P_i  Q_j).$$
By means of this theorem, and a similar treatment of the restriction
and renaming operators of CCS,
any CCS expression (with only guarded recursion) can be rewritten into
a bisimulation equivalent CCS
expression of the form $\sum_{i\in I}\alpha_i.P_i$. Such and
expression is called a head normal form.
If there is no recursion at all, this process can be iterated, and any
recursionfree CCS expression
can be rewritten in to a Basic CCS expression: one built solely
from 0, $+$ and action prefixing.
The above complete equational axiomatisation of (strong)
bisimulation equivalence for
basic CCS now extends to a complete equational axiomatisation of
all of recursionfree CCS.
When trying to apply this approach to weak bisimulation equivalence $=_{WB}$, we get stuck, because
$=_{WB}$ fails to be a congruence for the +operator, and hence fails
the last law of equational logic. A counterexample was presented yesterday.
This problem can be solved by
 giving up on full equational logic,
 giving up on $=_{WB}$
 or giving up on the +.
The language CSP follows the last approach. Its operational semantics is given here.
The syntax of CSP, the theory of Communicating Sequential Processes,
features the operations
 0 (inaction, originally written STOP)
 a.P (action prefix, originally written a→P) for each visible action a.
 P☐Q (external choice)
 P⊓Q (internal choice)
 P_{S}Q (parallel composition, enforcing
synchronisation over the set S of visible actions)
 P/a (concealment, originally written P\a) for each action a.
The atomic actions of CSP consists of
all a, b, c, etc. from a given set A of
visible actions. The syntax of CSP does not provide for invisible
actions, although τ does occur in the process graph semantics of
CSP; it is introduced by internal choice and by concealment.
Here are the definitions, in terms of process graphs without
predicates and without a notion of final states, of the operators
mentioned above:

0 is the graph with one state and no transitions.
This one state is the initial state.
 a.G is obtained from G by adding a new state, which will be
the initial one, and a new alabelled transition from this new
state to the initial state of G (which is no longer initial in a.G).
 G☐H is an operator that acts like a parallel composition
without synchronisation until a visible action from one of the two components
occurs, and from that moment onwards (internal or external) actions from
that component only are possible.
 G⊓H is defined to be τG + τH.
 G_{S}H is obtained by taking the Cartesian product of the states of
G and H; that is, the states of GH are pairs (s,t) with
s a state from G and t a state from H. The initial state
of GH is the pair of initial states of G and H. The transitions are
 (s,t) a> (s',t) whenever a is not in S
and s a> s' is a transition in G,
 (s,t) a> (s,t') whenever a is not in S
and t a> t' is a transition in H,
 and (s,t) a> (s',t') whenever a is in S
and s a> s' is a transition in G
and t a> t' is a transition in H.
Unlike the parallel compositions of CCS and ACP, the parallel
composition of CSP not only allows, but also enforces synchronisation.
For this reason CSP does not need a separate restriction or
encapsulation operator.
 G/a is just G, but with all actions a renamed into τ.
Wednesday 2042016
Today I turned to the alternative solution of the congruence problem raised
on Monday. In CCS, weak bisimulation equivalence =_{WB} is
replaced by weak bisimulation congruence =_{WBC}.
It is defined as the coarsest congruence contained in =_{WB},
obtained as the congruence closure of =_{WB} (see Wednesday
1342016 above). It turns out that P =_{WBC} Q iff for
all processes R we have P+R =_{WB} Q+R.
In fact, the same can be done for all other equivalences we
encountered (such as weak and strong completed trace equivalence)
and we indicated the resulting congruence closures on the linear time 
branching time spectrum, our map of equivalences, sorted by the "finer than"relation.
=_{WBC} can also be characterised as rooted weak
bisimilarity:
two processes are weak bisimulation congruent, iff after applying
an operation (rootunwinding) that preserves strong bisimilarity and
removes any loops going through the initial states they are
related by a rooted weak bisimulation, one that relates initial
states with initial states only.
Thursday 2142016
I presented another characterisation of =_{WBC}, and
illustrate it with examples:
Two processes P and Q are RWB equivalent iff
 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'.
Crucial here is that the mimicked astep is not optional.
RWB equivalence equals weak bisimulation congruence; it is finer,
i.e. more discriminating, than BB equivalence,
and it is a congruence for all operators of ACP, CCS and CSP.
The congruence closure of branching bisimilarity can be obtained in a
similar way: two processes are branching bisimulation congruent,
iff after applying
an operation (rootunwinding) that preserves strong bisimilarity and
removes any loops going through the initial states they are
related by a rooted branching bisimulation, one that relates initial
states with initial states only.
It turned out that two processes P and Q are RBB equivalent iff
 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'.
Next, I explained the partition refinement algorithm for deciding
(strong) bisimulation equivalence on finitestate processes. As
supporting material I handed out an actual handout, made of authentic
paper, copying Section 2.1, 2.2 and 3.1 of Chapter 6 of the Handbook
of Process Algebra.
Wednesday 2742016
Modulo strong, branching or weak bisimulation, every process graph can
be converted into one in which no two states are bisimilar.
The states of the canonical representation will be the bisimulation
equivalence classes (colours) of the states of the original graph.
The transitions between such states are defined in the obvious way,
and the initial state is the equivalence class containing the initial
state of the original system.
We also discussed deadlock, livelock and (possibly
fair) divergence, versus normal progress under a progress
assumption. Some formal definitions are in this handout.
A deadlock occurs in a state where no further actions are possible.
A livelock occurs in a state where no further visible (nonτ) actions are possible,
but always an internal action (τ) is possible.
A divergence is an infinite sequence of internal actions.
A livelock is a special kind of divergence. A divergence that is not a
livelock could be regarded "possibly fair" if one makes an appropriate
fairness assumption, because one might escape from it.
A progress assumption states that if we are in a state with an
outgoing transition, we will not stay in that state forever.
A fairness assumption says, of a choice between a certain
action g and an alternative, that if we encounter this choice
infinitely often, sooner or later g will be chosen.
A global fairness assumption assumes this for each and every
choice in the system.
In weak partial trace semantics, deadlock, livelock,
divergence and normal progress are all identified.
In CSP, as well as in David Walker's version of
weak bisimulation semantics, livelock and divergence are identified, and
distinguished from deadlock and normal progress, thereby implicitly assuming
choices to be unfair (a safe worst case scenario). In weak and
branching bisimulation semantics as used in CCS and 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.
Branching bisimulation with explicit divergence is
the finest useful weak equivalence found in the literature. It
distinguishes all four modes of progress: deadlock, livelock,
possibly fair divergence and normal progress.
A complete axiomatisation of =_{RWB} is obtained by adding
three τlaws to the axiomatisation of strong bisimulation equivalence.
$$\begin{array}{cc}
a.\tau.P = a.P \\
\tau.P + P = \tau.P \\
a.(\tau.P + Q) = a.(\tau.P + Q) + a.P
\end{array}$$
The latter two describe a kind of transitive closure on the LTS: if we
have two transitions
p τ> q a> r or p a> q τ> r,
then we obtain weakly bisimulation congruent systems by adding a
transition p a> r.
Thursday 2842016
Today, Andrew Semler gave a seminar on Ready Simulation Semantics,
following the paper
Bisimulation Can't Be Traced.
A GSOS language is any language with an operational semantics in the
GSOS format. It turns out that partial trace equivalence is not a
congruence for all such languages. The congruence closure of partial
trace equivalence for all GSOS contexts (i.e. the coarsest congruence
for all GSOS languages that is finer than =_{PT})
can be characterised as ready simulation equivalence.
Here two processes are ready simulation equivalent iff there are ready
simulation between them in both directions. A ready simulation is
just a simulation (half of a bisimulation) with the extra requirement
that related states have the same sets of initial actions (labels of
outgoing transitions). Two processes are ready simulation equivalent
iff they satisfy the same denial formulas. These are formulas
from the HennessyMilner Logic (HML), but restricted to the syntax
$$\phi ::= \langle a \rangle \phi ~~\mid~~ \phi \wedge \phi ~~\mid~~ \neg a ~(a\mathbin\in A).$$
For infinitestate systems we also need infinite conjunctions, just as
for HML. Thus, whenever two processes are not ready simulation
equivalent, there should be a denial formula that holds for the one,
but not for the other.
After the break, we modelled an abstract specification and an
implementation of the alternating bit protocol in the process algebra
ACP. I handed out 8 pages of the book "Process Algebra" by Baeten &
Weijland (1990).
Wednesday 452016
We further discussed the process algebraic modelling of the
specification and implementation of the alternating bit protocol.
The handout uses equational reasoning (applying axioms and such)
to show that the implementation is rooted branching bisimilar to the
specification. This mode of proving things is called equivalence checking.
Another form of equivalence checking is to directly show the rooted branching
bisimilarity of the transition systems of Spec and Impl, for instance
using the partition refinement algorithm. An alternative to
equivalence checking is model checking. This also involves
modelling the (implementation of) the protocol in a process algebra or
similar formalism, but instead of developing an abstract
specification, one formalises intended properties in terms of temporal
logics, like CTL or LTL. Then one applies techniques to directly show
that the (transition system generated by the) implementation of the
protocol satisfies its temporal formula. Out of the 8 major toolsets
for system verification surveyed here,
7 employ model checking and 4 employ equivalence checking.
Two of the latter use rooted branching bisimulation as their primary equivalence.
A more complete overview of tools is found on pages 9295 of
this book.
Of course equivalence checking and model checking can be combined:
there are theorems that tell is that if Spec ~ Impl for a
suitable equivalence ~, and Spec satisfies a temporal formula of a
particular form, then also Impl satisfies this formula.
The correctness of the alternating bit protocol (ABP) hinges on
a fairness assumption, saying that if you try to send a message
infinitely often, sooner or later it will come through correctly.
Without relying on such an assumption, the protocol is obviously
incorrect, on grounds that there can be no way to ensure correct message delivery.
Fairness assumptions are important in verification. If we refuse to
make them we declare any protocol like the ABP a priori incorrect, and
miss an opportunity to check the protocol logic for flaws that have
nothing to do with the unreliable nature of the communication channel.
A strong fairness assumption is already incorporated in the notions of
(rooted) branching (or weak) equivalence seen before. We will soon
encounter alternative forms of these equivalences that do not
incorporate a fairness assumption. Those equivalences would not be
suitable for the verification of the ABP.
I also treated the expansion theorem for ACP, as
one of the tools of equational reasoning employed in the verification
of the ABP.
Thursday 552016
Andreas Haratzis introduced Petri nets (with a paper handout),
and we discussed the interpretation of CCS in terms of Petri nets.
I made the definition of completed trace equivalence more precise.
For process graphs without a termination predicate, a path of a
process p is an alternating sequence of states and transitions,
starting from the state p and either infinite or ending in a
state, such that each transition goes from the state before it to the
state after it. It is complete if it is either infinite or ends
in a state from which no further transitions are possible.
A completed trace of p is the sequence of labels of the
transitions in a complete path. We write CT^{fin}(p) for the set of
finite completed traces of process p, and CT^{∞}(p)
for the set of all finite completed traces of p together with
its infinite traces. When writing just CT(p) it depends on
context which of the two is meant (i.e. this differs from one paper to the next).
Partial traces are defined likewise, but can end anywhere.
We write PT^{fin}(p) for the set of
finite partial traces of process p,
and PT^{∞}(p)
for the set of all finite partial traces of p together with
its infinite traces. Normally, PT(p) means PT^{fin}(p).
Now processes p and q are infinitary completed trace equivalent,
notation P =_{CT}^{∞} Q,
if CT^{∞}(p) = CT^{∞}(q).
It is a theorem that this implies that also PT^{∞}(p) = PT^{∞}(q).
Processes p and q are finitary completed trace equivalent,
notation P =_{CT}^{fin} Q,
if CT^{fin}(p) = CT^{fin}(q) and PT^{fin}(p) = PT^{fin}(q).
Here the last requirement cannot be skipped.
Likewise, processes p and q are infinitary partial trace equivalent,
notation P =_{PT}^{∞} Q,
if PT^{∞}(p) = PT^{∞}(q).
They are finitary partial trace equivalent,
notation P =_{CT}^{fin} Q,
if PT^{fin}(p) = PT^{fin}(q).
On processes that are equipped with a termination predicate ✔ on states
(like the accepting states from automata theory), partial traces and
completed traces are defined in such a way that we could just as well
have thought about the termination predicate that holds in a
state s as a special transition marked ✔ that goes
from s to a fresh state that is not connected in any other way.
Thus, for example, CT^{∞}(a.(ε+b.δ))
= {a✔, ab}.
Monday 952016
To arrive at a definition of weak
partial trace equivalence, we define a weak partial trace of a
process p as a strong partial trace of p from which all the
occurrences of τ have been omitted. Now two processes are
called weak partial trace equivalent if they have the same weak
partial traces. Obviously, we have infinitary weak partial trace equivalence
and finitary weak partial trace equivalence, depending on
whether or not infinite traces count as partial traces.
Infinitary weak completed trace equivalence (WCT^{∞}) can be
defined in the same way: two processes are infinitary weak completed trace equivalent
if, after leaving out all occurrences of τ from their (possibly
infinite) strong completed traces, their resulting sets of weak completed traced are the same.
Here one should realise that we can obtain a finite weak complete trace by
leaving out all occurrences of τ from an infinite strong complete trace.
The most straightforward form of finitary weak completed trace equivalence
(WCT^{fin})
is obtained by requiring that two process have the same set of weak
traces obtained from leaving out τ's from finite strong complete
traces—thereby skipping the finite traces obtained by leaving
out all occurrences of τ from infinite strong complete traces—and
moreover requiring that they have the same finite weak partial traces.
Surprisingly, WCT^{∞} is not finer than WCT^{fin}.
This is shown in the following table: WCT^{fin}
distinguishes deadlock from livelock, whereas WCT^{∞} does not.
  WCT^{fin}  WCT^{∞}  WCT^{Δ}  WCT^{λ} 
normal progress  a.b.0  $\{ab\}$  $\{ab\}$  $\{ab\}$  $\{ab\}$

fair divergence  a.Δb.0  $\{ab\}$  $\{ab,a\}$  $\{ab,a\Delta\}$  $\{ab\}$ 
livelock  a.(b.0+ τ.Δ.0)  $\{ab\}$  $\{ab,a\}$  $\{ab,a\Delta\}$  $\{ab,a\}$ 
deadlock  a.(b.0 + τ.0)  $\{ab,a\}$  $\{ab,a\}$  $\{ab,a\}$  $\{ab,a\}$ 
To arrive at a form of weak completed trace equivalence that is finer
than both, let WCT^{Δ}(p) be the set of sequences
obtained from CT^{∞}(p), by leaving out all
finite subsequences of τs, but replacing any infinite
subsequence of τs at the end by the special symbol Δ.
Two processes p and q are divergencepreserving (infinitary) completed trace equivalent,
notation P =_{WCT}^{Δ} Q,
if WCT^{Δ}(p) = WCT^{Δ}(q).
This equivalence distinguishes deadlock from livelock, and fair
divergence from normal process. However, it identifies fair
divergence and livelock.
None of the above equivalences would be suitable for a verification of
the alternating bit protocol. For there fair divergence is the
expected behaviour, and this should be distinguished from livelock,
which is bad behaviour.
To arrive at a form of weak completed trace equivalence that
distinguishes livelock from fair divergence, call a process q (or state) locked
if q has no partial trace containing a nonτ action.
A lock must be either a deadlock or a livelock.
Now a deadlock/livelocktrace of a process p, is the
sequence of visible actions on a path from q to a locked state q.
Let WCT^{λ}(p) be the set of
deadlock/livelocktrace of p.
Two processes p and q are deadlock/livelockpreserving (finitary) completed trace equivalent,
notation P =_{WCT}^{λ} Q,
if WCT^{λ}(p) = WCT^{λ}(q) and
also WPT^{fin}(p) = WPT^{fin}(q).
To distinguish all four phenomena, we can now define an equivalence
=_{WCT}^{Δλ} by
P =_{WCT}^{Δλ} Q iff
WCT^{Δ}(p) = WCT^{Δ}(q) and
WCT^{λ}(p) = WCT^{λ}(q).
Wednesday 1152016
Today Zilin Chen told about the algebraic theory of effects.
Assigned reading
The partition refinement algorithm for strong bisimilarity treated
earlier can be easily adapted to deal with branching bisimilarity.
Please read Sections 1, 2, 3 and 6 of
An O(m log n) Algorithm for Branching Bisimulation.
Thursday 1252016
Zilin finished his talk about algebraic effects, and distributed a handout.
Rob explained the partition refinement algorithm for branching bisimilarity.
The key idea is that τmoves between
states within the same block are skipped over, whereas τmoves
between different blocks are treated as if τ is any normal action.
For the rest it resembles the partition refinement algorithm for strong bisimilarity.
Ed explained how information from high royals that has not been securely
downgraded by dutiful bureaucrats stays hidden from lowly peasants.
Here is an handout.
Wednesday 1852016
A colouring of a labelled transition system is just a function that
associates a colour with every state. (Thus a colouring induces an
equivalence relation on states, and any equivalence relation induces a
colouring.) Now given a colouring, the potentials of a
state s of a certain colour, are all pairs (a,C)
with a an action and C a colour, such that s can
do some inert transitions followed by an noninert atransition
to a state with colour C.
Here a transition is inert if it is labelled τ and moreover goes
between two states of the same colour. Thus if (a,C) is
a potential of a state s, then either a≠τ or C is
not the colour of s. The colouring is consistent if all
states of the same colour also have the same potentials. Now one can
show that two states are branching bisimulation equivalent iff there
exists a consistent colouring that gives them the same colour.
Branching bisimilarity with explicit divergence ($BB^\Delta$) is
the finest useful weak equivalence found in the literature. It
distinguishes all four modes of progress: deadlock, livelock,
possibly fair divergence and normal progress.
Branching bisimulation equivalence with explicit divergence
can be defined in terms of consistent colourings:
State s is internally divergent w.r.t. a colouring is there is an
infinite path of τtransitions starting from s, only
passing through states with the same colour as s.
The colouring preserves internal divergence if for any colour either all
states of that colour are divergent w.r.t. the colouring, or none are.
Now two states are branching bisimulation equivalence with explicit
divergence if they receive the same colour by some consistent
colouring that preserves internal divergence.
Weak bisimilarity with explicit divergence ($WB^\Delta$) is
defined much simpler:
A weak bisimulation with explicit divergence is one that
relates divergent states to divergent states only.
Here a state is divergent if it is the start of an infinite
path, all of whose transitions are labelled τ.
I also showed that if $P \Rightarrow Q$ and $P =_{BB} Q$ then any process on
the $\tau$path from $P$ to $Q$ is branching bisimilar with $P$ and $Q$.
(A similar theorem holds for weak bisimilarity.)
Using this, the definition of a branching bisimulation could be
simplified. See the handouts linked above.
Thursday 1952016
LTL and CTL are defined on Kripke structures,
transition systems of which the states rather than the transitions are labelled.
Traditionally it is required that each state has at least one outgoing transition.
The statelabels are atomic propositions; a state could be labelled with zero, one or more of them.
Write $s \models \phi$ if the temporal logic formula $\phi$ (in CTL or LTL) holds for the state $s$.
To apply CTL or LTL to labelled transition systems we need a translation $\eta$ that maps
(states in) labelled transition systems to (states in) Kripke structures. We then define
validity of an LTL or CTL formula $\phi$ on a state $p$ in an LTL by $$p \models_\eta \phi \Leftrightarrow \eta(p) \models \phi$$
A suitable transition $\eta$ introduces a new state halfway each
nonτ transition, and transfers the transition label to that state.
Two processes (states in a deadlockfree LTS) satisfy the same LTL
formulas if they have the same infinite traces. For finitelybranching
processes, we even have "iff".
Two processes (states in a deadlockfree LTS) satisfy the same LTL_{X}
formulas if they have the same weak infinite traces (obtained by
leaving out τ's).
Two processes (states in a deadlockfree LTS) satisfy the same CTL
formulas if they are bisimilar. For finitelybranching processes, we even have "iff".
For general processes, we also have "iff", provided that we use CTL
with infinite conjunctions.
Two processes (states in a deadlockfree LTS) satisfy the same CTL_{X}
formulas if they are branching bisimilar with explicit divergence.
We even have "iff", provided that we use CTL_{X}
with infinite conjunctions.
We also extended the above results to LTSs that may
have deadlocks (states without outgoing transitions).
There are several approaches found in the literature:
 Translate any LTS (possibly with deadlock) into a Kripke
structure without deadlock by adding a selfloop to any state in the
Kripke structure that otherwise would be a deadlock.
Then use the standard interpretation (in terms of infinite paths)
of the LTL or CTL operators on deadlockfree Kripke structures.
 Stick to the translation defined earlier, thereby obtaining
Kripke structures that could have deadlocks.
Change the interpretation of LTL and CTL by using complete
paths instead of infinite paths for the interpretation of formulas.
The complete paths are the infinite paths, together with all finite
paths ending in a deadlock sate.
 Stick to the translation defined earlier, thereby obtaining
Kripke structures that could have deadlocks.
Change the interpretation of LTL and CTL by using complete
paths instead of infinite paths for the interpretation of formulas.
Moreover, add a new modality EG$^\infty$φ that requires
φ to hold on all states of an infinite path.
 Translate any LTS (possibly with deadlock) into a Kripke
structure without deadlock by adding a new state labelled with a
selfloop, labelled by a fresh proposition δ (deadlock)
and a transition to this state from any state in the
Kripke structure that otherwise would be a deadlock.
Then use the standard interpretation (in terms of infinite paths)
of the LTL or CTL operators on deadlockfree Kripke structures.
Now we have the following extensions of the results above:
Two processes $P$ and $Q$ (in an arbitrary LTS) satisfy the same LTL
formulas if P =_{CT}^{∞} Q.
For finitelybranching processes, we even have "iff".
Two processes $P$ and $Q$ (in an arbitrary LTS) satisfy the same LTL_{X}
formulas if P =_{WCT}^{∞} Q, that is,
if they have the same (possibly infinite) weak completed traces (obtained by
leaving out τ's).
Two processes $P$ and $Q$ (in an arbitrary LTS) satisfy the same CTL
formulas if they are strongly bisimilar. For finitelybranching processes, we even have "iff".
For general processes, we also have "iff", provided that we use CTL
with infinite conjunctions.
Two processes $P$ and $Q$ (in an arbitrary LTS) satisfy the same CTL_{X}
formulas if they are branching bisimilar with explicit divergence.
We even have "iff", provided that we use CTL_{X}
with infinite conjunctions.
The last result, however, only works with approach 3 or 4 above.
Otherwise we would get a weaker form of branching bisimilarity with
explicit divergence, which would identify deadlock and livelock.
Wednesday 2552016
I gave an overview of semantic equivalence relations
between process that to some extent take causal independence into
account. In one dimension semantic equivalences can be ordered
from lineartime to branchingtime semantics.
Typical examples of lineartime semantics are partial trace and
completed trace semantics. Typical branchingtime semantics are
strong bisimulation or branching bisimulation semantics.
The canonical equation that holds for
lineartime but not for branchingtime is a(b+c) = ab+ac.
Orthogonal to this classification is a spectrum that ranges
from interleaving semantics, in which parallelism is treated
by arbitrary interleaving of atomic actions, and causality respecting
semantics, in which causal relations between actions are explicitly
taken into account. A typical equation that holds in interleaving
semantics but not in causal semantics is ab = ab+ba.
It is rejected in causal semantics because in ab the two
actions a and b are causally independent, whereas
in ab+ba either a depends on b or vice versa.
A causal version of partial trace equivalence can be obtained by
taking partial orders of actions instead of sequences. This is why
causal semantics are sometimes called partial order semantics.
Between interleaving and causal semantics lays step semantics.
It differs from interleaving semantics by explicitly taking into
account the possibility that two concurrent actions a
and b by pure chance happen at the exact same (realtime) moment.
Here ab differs from ab+ba because only the former has
a trace where a and b happen at exactly then same time.
Between step semantics and causal semantics lays interval semantics.
It takes causality into account only to the extend that it manifest
itself by durational actions overlapping in time.
One argument to use at least interval semantics (and possibly causal
semantics) instead of interleaving semantics is realtime consistency.
If we imagine that actions take time to execute, interleaving
semantics may equate processes that have different running times (it
is not realtime consistent), whereas this cannot happen in interval
or causal semantics. An other argument is action refinement:
we want that two equivalent processes remain equivalent after
systematically splitting all occurrences of an action a
into a1;a2, or refining a into any more complicated
process. This works for interval or causal semantics, but not for
interleaving semantics.
A map of the equivalences discussed above appears on page 3 of
this paper.
Thursday 2652016
Rob Sison gave an introduction to event structures, following
this handout.
Afterwards I described the essence of safety properties, saying
that something bad will never happen, and liveness properties,
saying that something good will happen eventually. We formulated these
properties in LTL and CTL.
Safety properties are often established by means of invariants,
properties of states that hold in the initial state, and are
preserved under doing a transition. In the formulation of invariants,
states are often determined by the values of certain variables, and
the invariants are formulated in terms of these variables. Whether a
"bad" outgoing transition occurs in a state also depends on the values
of those variables, and the invariants we need says this never happens.
Whether liveness properties of systems hold depends often on whether
or not we make appropriate progress and fairness assumptions.
I discussed 4 such assumptions: progress, justness,
weak fairness and strong fairness. Please read page 7 of
this paper
for an informal description of these properties.
When assuming justness but not weak fairness, there are two bisimilar
systems with different liveness properties. Have a look at the section
"Process algebras without fairness assumptions, and their limitations"
in this paper.
Thus dealing with liveness properties under justness assumptions
(without assuming weak fairness) calls for a semantic equivalence
that distinguishes processes that are interleaving bisimilar.
In fact, this opens a new dimension in our lattice of equivalences,
to be revealed next week.
Wednesday 2552016
Today we further discussed the 4 progress and fairness assumptions
from last Thursday. An illustrative example appears in Figure 4 of
this paper.
That net displays a shop with two clerks I and II and two returning
customers A and B. There are 4 interactions between the clerks and the
customers: I serves A, II serves A, I serves B, II serves B.
In this net there are many traces that describe possible complete runs
of the systems. The stronger our fairness assumption, the fewer runs
are admissible. When assuming nothing, all partial traces model runs.
When assuming progress, this rules out all finite traces; now only
infinite traces model real completed runs. When assuming justness a
run that only contains "I serves A" is ruled out, because the
preconditions of "II serves B" are always met, and these tokens are
never used for anything else. However, a run that alternates between
"I serves A" and "II serves A" is still fine. Such a run is ruled out
by weak fairness however, as in each state "I serves B" is enabled,
yet customer B is never served. Weak fairness, however, allows the run
that alternates between "I serves A" and "I serves B", because "II
serves A" is not enabled in every state (due to customer A leaving
repeatedly). Yet, this run is ruled out by strong fairness.
This examples deals with global fairness assumption.
It is also possible to point at a Petri net (or some other system
description) and mark certain choices as fair, and others
as unfair; this gives local fairness assumptions.
Due to lack of time we do not treat those here.
My personal opinion is that it is often reasonable to assume (global)
progress. In the absence of that, no nontrivial liveness property can
be proven. When assuming progress I find it reasonable to also assume
justness (globally). However, the use of global (weak or strong)
fairness assumption should not be our default; it should be used only
if for some reason we are convinced that such an assumption is
warranted, or because we can only obtain a meaningful liveness
property conditionally on making such an assumption.
In the last part of the hour I explained STbisimulation equivalence,
which is the coarsest equivalence contained in interleaving
bisimulation equivalence that is preserved under refinement of actions.
It is also "real time consistent", meaning that if we assign durations
to actions, the minimal running times of equivalent processes are the same.
A formal definition can be found in Section 7 of
this paper.
Thursday 2652016
Today there was a presentation by Daniel Krajnik on Failures Semantics,
and by Ewan Scott on handling data in process algebra. Each had a handout.
I told myself that no Fair Scheduler can be modelled in
CCS/CSP/ACP or Petri nets, at least not without making a weak or
strong fairness assumption. This is an example showing that not
everything can be done in those formalism. A fair scheduler is a
mechanism for handling requests from two users, such that:
 a user can always make a new request,
 each request made will eventually be granted,
 requests not made will not be granted,
 and between granting any two requests occurs a separating action e.
Since Peterson's algorithm can be used to create a fair scheduler, it
follows that also that algorithm cannot be correctly modelled in
CCS/CSP/ACP or Petri nets, at least not without assuming fairness.
Handouts distributed in this course
(all fair game for exams)
The material treated only in week 13 is not examinable.
Please fill in
the CATEI evaluation for this course.