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 2-3-2016

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

  1. ε (successful termination)       (only present in the optional extension ACPε)
  2. δ (deadlock)
  3. a (action constant) for each action a.
  4. P.Q (sequential composition)
  5. P+Q (summation, choice or alternative composition)
  6. P||Q (parallel composition)
  7. H(P) (restriction, or encapsulation) for each set of visible actions H.
  8. τ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.


Here is the example of the relay race presented in class.

There are two runners R1 and R1 participating in the relay race, and while running they carry a baton. Runner 1 starts running, and at the halfway-point 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:

R1 = start.give
R2 = receive.finish
Here start is the action of runner 1 starting the race,
give is the finish of runner 1 at the halfway-point, where R1 gives the baton to R2,
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(R1 || R2))
with H={give,receive} and I={hand-over}. Here the communication function γ is given by γ(give,receive) = γ(receive,give) = hand-over. 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 3-3-2016

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 9-3-2016

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 above-linked handout.

Thursday 10-3-2016

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 = PX where PX 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 PX lays within the scope of a subexpression a.P'X of PX, 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
  1. 0 (inaction)
  2. a.P (action prefix) for each action a.
  3. P+Q (summation, choice or alternative composition)
  4. P|Q (parallel composition)
  5. 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:

Processes with loops are specified by means of recursive specifications, just as for ACP (see above).

The main differences between ACP and CCS are:


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 16-3-2016 (by P. Höfner)

Today we looked at the Hennessy-Milner 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':E--a-->E'  and   aK} . F ⊨ Φ
E ⊨ <K>Φ   iff   F∈{E':E--a-->E'  and   aK} . 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 17-3-2016 (by P. Höfner)

In today's lecture we continued to discuss Hennessy-Milner 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 Linear-time Temporal Logic (LTL).

Wednesday 23-3-2016 to Thursday 7-4-2016 (by K. Engelhardt)

See this page, also for homework.

Note on structural induction

Wednesday 13-4-2016

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 L-expression 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 L-context C[ ].

It can be shown that ~L is the coarsest congruence finer than ~. (Note that there are three statements in that last sentence.)

Thursday 14-4-2016

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 recursion-free 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 recursion-free 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 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

  1. 0 (inaction, originally written STOP)
  2. a.P (action prefix, originally written a→P) for each visible action a.
  3. PQ (external choice)
  4. P⊓Q (internal choice)
  5. P||SQ (parallel composition, enforcing synchronisation over the set S of visible actions)
  6. 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:

Wednesday 20-4-2016

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 13-4-2016 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 (root-unwinding) 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 21-4-2016

I presented another characterisation of =WBC, and illustrate it with examples:

Two processes P and Q are RWB equivalent iff

Crucial here is that the mimicked a-step 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 (root-unwinding) 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

Next, I explained the partition refinement algorithm for deciding (strong) bisimulation equivalence on finite-state 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 27-4-2016

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 28-4-2016

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 Hennessy-Milner Logic (HML), but restricted to the syntax $$\phi ::= \langle a \rangle \phi ~~\mid~~ \phi \wedge \phi ~~\mid~~ \neg a ~(a\mathbin\in A).$$ For infinite-state 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 4-5-2016

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 92-95 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 5-5-2016

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 CTfin(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 PTfin(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 PTfin(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 =CTfin Q, if CTfin(p) = CTfin(q) and PTfin(p) = PTfin(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 =CTfin Q, if PTfin(p) = PTfin(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 9-5-2016

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 (WCTfin) 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 WCTfin. This is shown in the following table: WCTfin distinguishes deadlock from livelock, whereas WCT does not.

WCTfinWCTWCTΔWCTλ
normal progressa.b.0$\{ab\}$$\{ab\}$$\{ab\}$$\{ab\}$
fair divergencea.Δb.0$\{ab\}$$\{ab,a\}$$\{ab,a\Delta\}$$\{ab\}$
livelocka.(b.0+ τ.Δ.0)$\{ab\}$$\{ab,a\}$$\{ab,a\Delta\}$$\{ab,a\}$
deadlocka.(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 divergence-preserving (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/livelock-trace 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/livelock-trace of p. Two processes p and q are deadlock/livelock-preserving (finitary) completed trace equivalent, notation P =WCTλ Q, if WCTλ(p) = WCTλ(q) and also WPTfin(p) = WPTfin(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 11-5-2016

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 12-5-2016

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 18-5-2016

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 non-inert a-transition 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 19-5-2016

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 state-labels 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 deadlock-free LTS) satisfy the same LTL formulas if they have the same infinite traces. For finitely-branching processes, we even have "iff".

Two processes (states in a deadlock-free 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 deadlock-free LTS) satisfy the same CTL formulas if they are bisimilar. For finitely-branching 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 deadlock-free 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:

  1. Translate any LTS (possibly with deadlock) into a Kripke structure without deadlock by adding a self-loop 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 deadlock-free Kripke structures.
  2. 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.
  3. 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.
  4. Translate any LTS (possibly with deadlock) into a Kripke structure without deadlock by adding a new state labelled with a self-loop, 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 deadlock-free 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 finitely-branching 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 finitely-branching 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 25-5-2016

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 linear-time to branching-time semantics. Typical examples of linear-time semantics are partial trace and completed trace semantics. Typical branching-time semantics are strong bisimulation or branching bisimulation semantics. The canonical equation that holds for linear-time but not for branching-time 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 a||b = ab+ba. It is rejected in causal semantics because in a||b 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 (real-time) moment. Here a||b 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 real-time consistency. If we imagine that actions take time to execute, interleaving semantics may equate processes that have different running times (it is not real-time 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 26-5-2016

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 25-5-2016

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 non-trivial 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 ST-bisimulation 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 26-5-2016

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:

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.
Rob van Glabbeek homework rvg@cse.unsw.edu.au