# Course notes for COMP6752: Comparative Concurrency Semantics

This file contains an inventory of potential material to be covered, and lists handouts to be distributed. It is gathered from offerings of the course in prior years and will be fine-tuned later on.

## Monday 26-2-2018: Specification and Implementation

Today I will introduce 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 definitions below.

Another way to represent concurrent systems is by means of process algebraic expressions.

These concepts will be 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 to determine if they match. I will discuss a criterion based on bisimulation, that matched the states of the related LTSs. I show 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.

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.

• ε 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 IG --a--> s in G, where IG denotes the initial state of G, there will be an extra transition root --a--> s, and likewise, for each transition IH --a--> s in H, where IH denotes the initial state of H, there will be an extra transition root --a--> s.
root is labelled with ✔ if either IG or IH is.
• G||H is obtained by taking the Cartesian product of the states of G and H; that is, the states of G|H are pairs (s,t) with s a state from G and t a state from H. The initial state of G||H 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, G||H 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 τ.

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 will draw 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 τ.

## Tuesday 27-2-2018: The process algebra ACP

Today I presented the syntax and 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 ✔.

## Monday 5-3-2018: Spectrum of semantic equivalences

I discussed 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 ≡.

In this course I will present a lattice of semantic equivalence relations on process graphs. These represent different points of view on whether two processes are roughly the same. In such a lattice, equivalences are classified with respect to their discriminating power.

As part of this lattice of semantic equivalences I presented 8=2x2x2 versions of trace semantics, all defined on process graphs G=(S,T,I) that are not equipped with a termination predicate (=final states).

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.

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). I this class I defined CT(p) to mean CTfin(p).

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 or just P =CT 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 =PT Q, if PT(P) = PT(Q).

Together, these four equivalence notion form a square when ordered w.r.t. discriminating power.

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 definitions of weak partial trace equivalence (=WPT or =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 (finitary or infinitary) weak partial trace equivalent if they have the same (finite or possibly infinite) weak partial traces. Weak completed trace equivalence, and its infinitary version, can be defined in the same vein.

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}.

In addition, two processes are called language equivalent if they have the same traces leading to terminating states. In automata theory such traces are called words, accepted by s. The set of all words accepted by s is the language accepted by s. It turns out that language equivalence is coarser than partial trace equivalence, whereas completed trace equivalence is finer than partial trace equivalence.

My paper The Linear Time - Branching Time Spectrum I is a small encyclopedia of (strong, or concrete) equivalence relations; language equivalence appears in Section 19.

## Tuesday 6-3-2018: Linear time versus branching time

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.

I discussed 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.

For the same reason, one would want to distinguish the systems Q := τ.(b + c) and P:= τ.b+τ.c. However, these two systems are equivalence under each of the 8 variants of trace equivalence discussed above. For this reason we need 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.

The definition of bisimulation equivalence, also called bisimilarity, can be found in this handout, which you should read entirely, except for the sections "Modal logic", "Non-well-founded sets" and "Concurrency". 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,→,✔). More commonly, one ignores the component ⊨ or ✔ completely.

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.

I 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.

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 saw 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. I presented the definition of weak bisimilarity in class.

I treated weak and branching bisimulation equivalence, from this handout; read the section "Abstraction". I also characterised branching bisimilarity in terms of consistent colourings:

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.

Strong bisimilarity can be characterised in the same way; the only difference is that no actions count as inert. Thus a potential (a,C) simply means one can do an a-transition to a state with colour C.

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.

## Tuesday 13-3-2018: Recursion, and CCS

In order to describe infinite processes in a language like ACP, we add a bunch of constants X,Y,Z to the language, 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.

An alternative approach is to introduce variables X,Y,Z to the language, as well as recursion constructs <X|S>. Here S is a set of recursive equations X = PX, and <X|S> specifies "the process X that satisfies the equations S". We normally restrict attention to the guarded case, in which there is only one process X satisfying S.

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.
6. P[f] (relabelling) for each function f:A -> 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 a-labelled transition from this new state to the initial state of G (which is no longer initial in a.G).
• G+H is obtained by taking the union of copies of G and H with disjoint sets of states, and adding a fresh state root, which will be the initial state of G+H. For each transition IG --a--> s in G, where IG denotes the initial state of G, there will be an extra transition root --a--> s, and likewise, for each transition IH --a--> s in H, where IH 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 statesWPTfin (roots) of G and H, and then gluing together these roots to form the new initial state of G+H.
• G|H is obtained by taking the Cartesian product of the states of G and H; that is, the states of G|H are pairs (s,t) with s a state from G and t a state from H. The initial state of G|H 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, G|H 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.WPTfin
It is used to remove the remnants of unsuccessful communication, so that the synchronisation that is enabled by parallel composition, is enforced.
• G[f] is the graph G in which each label a is replaced by f(a), and likewise a by f(a).
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. These operators do not occur in CCS.
• 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 τ.WPTfin
• 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 γ.

## Monday 12-3-2018: Deadlock, livelock and divergence

A liveness property says that something good will eventually happen. The following concepts are important when formulating (or proving) liveness properties.
A progress assumption roughly states that if we are in a state with an outgoing transition, we will not stay in that state forever. A fairness assumption roughly 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. Progress and sometimes fairness assumptions are often made when proving liveness properties.
I discussed deadlock, livelock and (possibly fair) divergence, versus normal progress under a progress assumption. Some formal definitions are in
this handout, which you should read. 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.

 WPTfin P normal progress a.b.0 $\{ab,a,\epsilon\}$ Q fair divergence a.Δb.0 $\{ab,a,\epsilon\}$ R livelock a.(b.0+ τ.Δ0) $\{ab,a,\epsilon\}$ S deadlock a.(b.0 + τ.0) $\{ab,a,\epsilon\}$

In the above table, the unary operator $\Delta$ appends a $\tau$-loop at the beginning of its argument. Formally, $\Delta G$ is the process graph created out of $G$ by adding a fresh initial state $I$, together with a fresh $\tau$-loop I --$\tau$--> I, and a transition I --$\alpha$--> s for each transition IG --$\alpha$--> s from $G$. Process graphs of the 4 processes in the above table were drawn in class. If we assume fairness, "normal progress" may be identified with "fair divergence", but in the absence of a fairness assumption only "normal progress" satisfies the liveness property that b will happen eventually. In weak partial trace semantics, deadlock, livelock, divergence and normal progress are all identified. The weak partial traces of all four processes are the same. This week it is homework to invent definitions of completed trace equivalence that make different choices in this matter.

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 ($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:

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.

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.

(State s is divergent if there is an infinite path of τ-transitions starting from s. A colouring preserves divergence if for any colour either all states of that colour are divergent, or none are. Now two states are weakly divergence preserving branching bisimilar if they receive the same colour by some consistent colouring that preserves divergence. I showed by a proof and a counterexample that this notion is strictly weaker than divergence preserving branching bisimilarity.)

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 τ.

### Tutorial

Answer to HW3, Q1: I only consider process graphs G without a termination predicate. A rooted path of G is an alternating WPTfin-sequence of states and transitions, starting from the initial state of G and either infinite or ending in a state, such that each transition goes from the state before it to the state after it. For π such a path, let l(π) be the (finite or infinite) sequence of labels of the transitions of π, in the order in which these transitions occur in π. Let wl(π) be the same sequence after omitting all τs.

A state s is a deadlock state if it has no outgoing transitions.
A finite path π is a deadlock path if its last state is a deadlock state.
A state s is a livelock state if from s we can not reach a deadlock state, nor a state from which a visible action can be performed.
A finite path π is a livelock path if its last state is a livelock state.
A state s is a divergence state if it is the beginning of an infinite path of τ-transitions.
A finite path π is a divergence path if its last state is a divergence state.

Let WCTδ(G) := {wl(π) | π is a deadlock path of G}.
Let WCTλ(G) := {wl(π) | π is a livelock path of G}.
Let WCTΔ(G) := {wl(π) | π is a divergence of G}.
Note that WCTλ(G) always is a subset of WCTΔ(G).

These sets are illustrated on the examples given earlier:

 WPTfin WCTδ WCTλ WCTΔ normal progress a.b.0 $\{ab,a,\epsilon\}$ $\{ab\}$ $\emptyset$ $\emptyset$ fair divergence a.Δb.0 $\{ab,a,\epsilon\}$ $\{ab\}$ $\emptyset$ $\{a\}$ livelock a.(b.0+ τ.Δ0) $\{ab,a,\epsilon\}$ $\{ab\}$ $\{a\}$ $\{a\}$ deadlock a.(b.0 + τ.0) $\{ab,a,\epsilon\}$ $\{ab,a\}$ $\emptyset$ $\emptyset$

The question was: Modify the definition of weak completed trace semantics in six different ways, namely such that

1. deadlock = livelock and fair divergence = normal progress,
2. fair divergence = normal progress, and livelock differs from deadlock and from normal progress,
3. deadlock = livelock and fair divergence differs from livelock and from normal progress,
4. livelock = fair divergence, different from deadlock and progress,
5. deadlock = livelock = fair divergence, different from progress,
6. all four phenomena are distinguished.
The answers:
1. Let $G =_{\rm WCT}^a H$ if WPTfin(G) = WPTfin(H) and WCTδ(G) $\cup$ WCTλ(G) = WCTδ(H) $\cup$ WCTλ(H).
2. Let $G =_{\rm WCT}^b H$ if WPTfin(G) = WPTfin(H) and WCTδ(G) = WCTδ(H) and WCTλ(G) = WCTλ(H).
3. Let $G =_{\rm WCT}^c H$ if WPTfin(G) = WPTfin(H) and WCTδ(G) $\cup$ WCTλ(G) = WCTδ(H) $\cup$ WCTλ(H) and WCTδ(G) $\cup$ WCTΔ(G) = WCTδ(H) $\cup$ WCTΔ(H)
4. Let $G =_{\rm WCT}^d H$ if WPTfin(G) = WPTfin(H) and WCTδ(G) = WCTδ(H) and WCTΔ(G) = WCTΔ(H).
5. Let $G =_{\rm WCT}^e H$ if WPTfin(G) = WPTfin(H) and WCTδ(G) $\cup$ WCTΔ(G) = WCTδ(H) $\cup$ WCTΔ(H).
6. Let $G =_{\rm WCT}^f H$ if WPTfin(G) = WPTfin(H) and WCTδ(G) = WCTδ(H) and WCTλ(G) = WCTλ(H) and WCTΔ(G) = WCTΔ(H).

### 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.

 WCTfin 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 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).

## Monday 23-4-2018: Congruence I

I defined 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. It also fails for the parallel composition of CSP. A counterexample: the processes $ab+ac$ and $a(b+c)$ are completed trace equivalent, but after placing them in a context $\partial_{\{b\}}(\_)$ or $\_\backslash b$ or $\_\|_{\{b\}}0$ they are not. 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.

The congruence closure ~c of ~ (w.r.t. a language L) is defined by

P ~c Q if and only if C[P] ~ C[Q] for any L-context C[ ].

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

The congruence closure of strong completed trace equivalence can be characterised as strong failures equivalence (not defined yet). It is finer than strong completed trace equivalence, but finer than strong bisimilarity. A similar thing applies to weak equivalences.

## Thursday 14-4-2016: Equational axiomatisations

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.

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: the processes $ab+ac$ and $a(b+c)$ are completed trace equivalent, but after placing them in a context $\partial_{\{b\}}(\_)$ or $\_\backslash b$ or $\_\|_{\{b\}}0$ they are not. This problem can be solved by
• giving up on full equational logic,
• giving up on $=_{WB}$
• or giving up on the +.
Whereas the process algebras ACP and CCS follow the second approach, the process algebra CSP follows the last approach.

## Monday 23-4-2018: Congruence II and CSP

Weak and branching bisimilarity fail to be congruences for the choice operator (+) of ACP or CCS. A counterexample is presented above. There are two ways to remedy such a situation: to change the equivalence (by taking instead its congruence closure) or to change the language (by dropping the offending operator).

Weak bisimulation congruence, the congruence closure of weak bisimilarity, is the default semantic equivalence used in the language CCS. It can 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.

Likewise, branching bisimulation congruence, the congruence closure of branching bisimilarity, is the default semantic equivalence used in the language ACP. It can be characterised as rooted branching bisimilarity.

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:

• 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 a-labelled transition from this new state to the initial state of G (which is no longer initial in a.G).
• GH 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||SH is obtained by taking the Cartesian product of the states of G and H; that is, the states of G||H are pairs (s,t) with s a state from G and t a state from H. The initial state of G||H 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 τ.

### Thursday 21-4-2016

Today I returned 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 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.

### Thursday 21-4-2016

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

• 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'.

## Wednesday 27-4-2016: Equational axiomatisations II

On Monday 7-4-2014 we discussed a complete equational axiomatisation of strong bisimilarity on recursion-free CCS. To axiomatise rooted weak bisimilarity =RWB we need three extra axioms: $$\begin{array}{c} (T1) & \alpha.\tau.P = \alpha.P \\ (T2) & \tau.P = \tau.P + P \\ (T3) & \alpha.(\tau.P + Q) = \alpha.(\tau.P + Q) +\alpha.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.

Delay bisimilarity and η-bisimilarity are semantic equivalences intermediate between weak and branching bisimilarity, defined in the handouts. Rooted delay bisimilarity is axiomatised by (T1) and (T2); rooted η-bisimilarity by (T1) and (T3). Rooted branching bisimilarity is completely axiomatised by $$\alpha.(\tau.(P+Q)+Q) = \alpha.(P+Q)$$ on top the of axioms for strong bisimilarity. This axiom is a strengthening of (T1). There does not exists a congruence that is axiomatised by (T1) plus the axioms of strong bisimilarity alone. In this direction, rooted branching bisimilarity is at good as it gets.

When using equational reasoning to verify that a specification is equivalent to an implementation we use, in addition to the machinery of equational logic, the recursive definition principle (RDP) and the recursive specification principle (RSP). RDP says that a system satisfies its recursive definition; RSP says that two processes satisfying the same guarded recursive equation, must be equal. It holds for strong and rooted weak or branching bisimilarity. These principles are applied in last week's handout on the verification of correctness of the alternating bit protocol.

## Monday 19-3-2018: Operational semantics

In the denotational semantics we saw before, the denotation of an expression is a process graph (an LTS with initial state) and the meaning of a composed expression like P|Q is a process graph obtained in a particular way from the process graphs of the arguments P and Q.

In the operational framework we drop the distinction between processes and states. There will be one humongous LTS (without initial state) whose states are all possible closed process expressions, and the transitions between states are given by certain operational rules. To get an idea of the difference between process graphs and LTSs, read the definitions in this handout, and especially note how Definition 3 of bisimulation avoids having the clause on initial states.

Today I presented the theory of structural operational semantics, as described in this handout. (The handout, however, deals also with negative premises, which were not treated in class yet.) I also covered the structural operational semantics of CCS, given here. (Only read the first section.) What is called $\textbf{fix}_XS$ in the handout was called <X|S> in class. The rule for recursion involves substitution. (The operational rules for basic CCS are given in Example 1 of this handout. (In class I wrote P and Q for x1 and x2, and P' for y1.))

I also explained a theorem in Structured Operational Semantics, saying that strong bisimulation is a congruence as soon as all operators concerned have operational rules in the GSOS format. See the handout on structural operational semantics for details. We covered a few examples illustrating a failure of bisimulation being a congruence when we deviate from this format.

As a consequence of this result, strong bisimilarity is a congruence for all operators of ACP, CCS and CSP.

Today I extended the theory of structural operational semantics (see handout above) and the GSOS format with negative premises, using the priority operator that is sometimes added to ACP as an example.

### 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.

## Monday 26-3-2018 to Tuesday 10-4-2018: SOS and mutex

See this page, also for homework.

## Monday 30-4-2018

Then I presented the Hennessy-Milner logic (HML), following this handout. (In the section "modal logic" take polymodal logic with an empty set of propositions.) The syntax of HML is given by: $\varphi,\psi ::= {\color{green} \top} \mid {\color{red} \bot} \mid \color{green} \varphi \color{green}\wedge \color{green}\psi \mid \color{red} \varphi \color{red}\vee \color{red}\psi \mid \neg\varphi \mid \color{green} \langle \color{green}\alpha \color{green}\rangle \color{green}\phi \mid \color{red}[\color{red}\alpha\color{red}] \color{red}\phi$ Infinitary HML (HML$^\infty$) moreover has an infinitary conjunction $\bigwedge_{i\in I}\phi_i$.
By Theorems 1 and 2 in the handout, two processes are strong bisimulation equivalent iff they satisfy the same infinitary HML-formulas. Thus, to show that two processes are not strongly bisimilar, it suffices to find an infinitary HML-formulas that is satisfies by one, but not by the other. Moreover, if we know that at least one of the processes is image-finite, we do not need infinite conjunction.

Above, the red connectives and modalities are redundant, because they are expressible in the green connectives and negation. Likewise, the green connectives are expressible in terms of the red ones and negation. Finally, if we keep both the red and the green connectives and modalities, then negation is redundant. It is the latter form we need to extend HML into the modal $\mu$-calculus. It additionally has modalities $\mu X.\phi(X)$ and $\nu X.\phi(X)$. Here $\phi(X)$ is a modal $\mu$-formula that may contain the variable $X$. $\mu X.\phi(X)$ denotes the least fixed point of the equation $X=\phi(X)$, and $\nu X.\phi(X)$ the greatest. For these fixed points to exist, the formulas $\phi(X)$ need to be monotone in $X$, and to achieve that we needed to eliminate negation.

A formal denotational semantics of the modal $\mu$-calculus can be found in wikipedia. There, negatation is not eleminated, but instead a variable needs to be under an even number of negation operators. This treatment is equivalent.

## Wednesday 16-3-2016 (by P. Höfner): Logics

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   a∈K} . F ⊨ Φ E ⊨ Φ iff ∃F∈{E':E--a-->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 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).

## Monday 16-4-2018 by Peter Höfner: Temporal logic

Today I introduced the logics CTL and CTL*. The syntax and the semantics can be found in any text book on temporal logic, e.g. [HR04]. For CTL I explained how fixed points can be used to check whether a given Kripke structure satisfies E_U_ and E_U_.
I then continued the lecture by discussing how 2 different logics can be compared w.r.t. expressiveness. As a trivial example, we showed LTL ⊆ CTL* and CTL ⊂ CTL* .

A superset of today's contents can be found at the slides of COMP3153/9153. In particular, Lecture 3 (Syntax and Semantics of LTL/CTL and CTL*) and Lecture 5 (calculating fixed point of E_U_ and E_U_).

[HR04] Michael Huth and Mark Ryan. Logic in Computer Science (2nd edition). Cambridge University Press, 2004.
As we taught you to compare logics yesterday, we showed that LTL and CTL are incomparable. We did this by proving that there cannot exist an LTL-formula that is equivalent to the CTL-formula AG EF a, and by showing that there cannot exist a CTL-formula equivalent to FG a (see e.g. [BK08].

At the end of the lecture we discussed how Kripke structures can be translated into LTSs, and vice versa.

[BK08] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. ISBN 978-0-262-02649-9

### Note on structural induction

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 20-4-2016: Deciding bisimilarity

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.

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.

### 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. Or (better) Section 1, 2, 3 and 7 of the published version. 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.

### Monday 7-5-2018

Today, Joshua Lau gave a presentation on Algorithms for Strong Bisimilarity on Finite Transition Systems. He gave detailed description of the partition refinement algorithm by Kanellakis & Smolka, as improved by Paige & Tarjan. It has complexity $O(m.(log(n)+log(l))$, where $m$ is the number of transitions, $n$ is the number of states, and $l$ is the number of different action labels in a finite system (when assuming n < m+2, which can be achieved by collapsing deadlock states). (Often $l$ is taken to be a constant, and not counted.)

### Monday 19-5-2014

Japeth give detailed accounts and a complexity analysis of the partition refinement algorithms for deciding (strong weak and branching) bisimilarity on finite-state transition systems. He also commented on the EXPTIME complexity for such equivalences when the input is a process algebra expression (of a not too complex kind). This is because an LTS can be exponentially larger than its generating expression. Finally, he made some remarks on the use of bisimulations in contemporary verification.
To decide weak bisimilarity for finite transition systems we first compute the transitive closure: add a transition $p \stackrel{\alpha}\longrightarrow r$ whenever we have $p \stackrel{\tau}\longrightarrow q \stackrel{\alpha}\longrightarrow r$ or $p \stackrel{\alpha}\longrightarrow q \stackrel{\tau}\longrightarrow r$; also add a $\tau$-loop in every state. After this transformation weak bisimilarity coincides with strong bisimilarity, and we can use the algorithm to decide the latter. But the complexity of performing the above transitive closure is higher than that of partition refinement; the total complexity of deciding weak bisimilarity is $O(l.n^{2.376})$.

## Wednesday 4-5-2016: Alternating bit protocol; tools

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).

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.

## Wednesday 25-5-2016: Non-interleaving semantics

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.

I indicated how causal trace semantics can be represented in terms of pomsets, partial ordered multisets. The process $a(b||(c+de)))$ for instance has two completed pomsets, which were drawn in class. A normal trace can be regarded as a totally ordered multiset of actions.

### Monday 12-5-2014

Nicholas Turner introduced event structures as a model of concurrency different from LTSs. He also explained some of their use in modelling bits of game theory.

In this handout the definition of a labelled prime event structure with binary conflict can be found, as well as its translation into a process graph.

Here is a more thorough account of event structures. In class I told how operators of CCS and related languages can be interpreted in terms of event structures. This corresponds with Section 2.3 of that paper.

### Wednesday 14-5-2014

I completed the story about interpreting process algebras like CCS in terms of event structures. Then I explained how event structures can be translated in process graphs and vice versa, without loss of essential information. See the above handout for details.

I also gave a Game theoretical characterisation of strong bisimilarity. The details are in wikipedia.

Finally, I introduced Petri nets, and gave an interpretation of the operators of CCS etc. in terms of nets. Thus also Petri nets can be used as semantic model of such languages.

On Petri nets and event structures it is common to not use interleaving equivalences that identify a|b and ab+ba. Reasons to distinguish these processes are preservation of semantic equivalence under action refinement and real-time consistency.

## Thursday 26-5-2016: Progress, Justness and Fairness

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. The terminology "liveness" used here stems from Lamport 1977, who was inspired by the older use of the term "liveness" in Petri nets, whose meaning however is different. 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.

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. The notions of (rooted) branching (or weak) bisimulation equivalence with explicit divergence do not make fairness of justness assumptions. A progress assumption is build in in the logics CTL and LTL (for they work with infinite paths rather than partial paths).

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.

## Course evaluation

Please fill in the course and instructor evaluation forms. (The school holds it against the instructor if there are not enough responses.)

## Monday 21-5-2018

Today, Quac-An Ho spoke on Safety and Liveness properties in labelled transition systems, based on the first 9 pages of this paper.

After the break, Patrick Gilfillan presented Chu spaces.

In the last 10 minutes I presented "reactive CTL/LTL". A few weeks ago we say how to interpret CTL and LTL on process graphs (or states in labelled transition systems) with deadlocks. We discussed 3 methods to deal with deadlock. In the context of CTL or LTL minus the next-state operator, the 3rd method was the best. But when using full CTL or LTL, with the next-state operator, the 2nd method is just as good, and this is what I use today. In a deadlock state in a Kripke structure (a state without outgoing transitions), the CTL formula AXfalse holds, and in a state with an outgoing transition it does not hold. Hence this formula could be used to describe deadlock.

We use the De Nicola-Vaandrager translation from process graphs to Kripke structures. Formally, 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. The associated Kripke structure is $(S',I,\rightarrow',\models)$, where $S' := S \cup\{(s,a,t)\in{\rightarrow}\mid a\neq \tau\}$, and ${\rightarrow'} := \{(s,(s,a,t)),((s,a,t),t) \mid (s,a,t)\in S'\} \cup \{(s,t)\mid (s,\tau,t) \in {\rightarrow}\}$. This Kripke structure has the same states and transitions as the process graph, except that a new state $(s,a,t)$ is added halfway a transition from $s$ to $t$ labelled $a\neq\tau$. As atomic propositions we take the set Act of actions, except for $\tau$, and declare that a state satisfies the atomic proposition $a\in Act$ iff that state has the form $(s,a,t)$. So $r \models a$ iff $r=(s,a,t)$.

Now we consider all possible subsets $B$ of $Act\setminus\{\tau\}$. $B$ contains the actions that may be blocked by the environment. We define a $B$-complete path of a process graph as a path that is either infinite or ends in a state of which all outgoing transitions have a label from $B$. A $B$-complete path in a Kripke structure that arises as the De Nicola-Vaandrager translation of a process graph is a path that ends in a state, all of whose successor states are labelled with atomic propositions from $B$. Thus, the De Nicola-Vaandrager translation maps $B$-complete paths in process graphs to $B$-complete paths in the associated Kripke structures. An LTL formula $\phi$ is said to hold for the Kripke structure $K$ when the actions from $B$ might be blocking, notation $K \models_B \phi$, iff each $B$-complete path from the initial state of $K$ satisfies $\phi$. Likewise, $\models_B$ can be defined for CTL by simply replacing all references to infinite paths by $B$-complete paths.

As an example, consider a vending machine that takes in a coin $c$ and produces a pretzel $p$. We assume that taking in the coin requires cooperation from the environment, but producing the pretzel does not. A process algebraic specification is $$VM=a.p.VM$$ In old-fashioned LTL we have $VM \models G(c\Rightarrow Fp)$. This formula says that whenever a coin is inserted, eventually a pretzel is produced. This formula is intuitively true indeed. But we also have $VM \models G(p\Rightarrow Fc)$. This formula says that whenever a pretzel is produced, eventually a new coin will be inserted. This formula is intuitively false. This example shows that old-fashioned LTL is not suitable to describe the behaviour of this vending machine. Instead we use reactive LTL, and take $B=\{c\}$. This choice of $B$ says that the environment may bock the action $c$, namely by not inserting a coin; however, the environment may not block $p$. As intuitively expected, we have $VM \models_B G(c\Rightarrow Fp)$ but $VM \not\models_B G(p\Rightarrow Fc)$.

Note that the old-fashioned LTL/CTL interpretation $\models$ is simply $\models_\emptyset$, obtained by taking the empty set of blocking actions.

There are 3 ways to incorporate the above idea.

• One is to pick a set $B$ that is fixed for a given application. In case of the vending machine above, we take $B=\{c\}$. Then we can leave out the subscript $B$ from $\models$.
• Alternatively, we use a specification of our system that is neutral on which actions are blocking, and instead use subscripts $B$ with $\models$. A formula $P \models_B \phi$ then simply says that "under the assumption that actions from $B$ may block, process $P$ satisfies formula $\phi$". Thus, information about blocking is taken aboard only when writing down the validity of temporal formulae.
• The third option is to stick to old-fashioned CTL or LTL, and instead add a $\tau$-loop to each state that intuitively has only blocking outgoing actions. This approach says that we assume that any system will make progress, unless we explicitly indicate that it can stay in a state by means of a $\tau$-loop. In this approach our vending machine would have to be adapted to $VM=\tau.VM + a.p.VM$.

### Thursday 26-5-2016

I told 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.

## Wednesday 21-5-2014

Today I treated value-passing process algebras. These are variants of standard process algebras like CCS, CSP or ACP, with the following modifications.
• Behind the process algebra sits a well chosen data structures. It consists of data types, like the integers, queues of integers, Booleans, or whatever we need in a given application. Within each data type we provide constants. For instance T and F are two constants of type Booleans, and 0 and 1 are constants of type Integer. The empty queue [] is a constant of type queues. On each data type there are also operators or functions, each with a given arity. For instance, negation is a unary function on the type of the Booleans, whereas conjunction is a binary function on the Booleans. Successor is a unary function on the integers, whereas addition and multiplication are binary functions on the integers. In addition, there can be functions whose arguments belongs to different data types and whose output again is of a different type. For instance, "is-empty" could be a function whose single argument is a queue (of integers) and whose output is a Boolean. append is a binary function whose arguments are an integer and a queue of integers, and whose output is a queue of integers.

Now a data expression is made from these constants and from variables ranging over a particular data type by applying the functions or operators specified by the data structure. For instance append(8+n,q) is a data expression of type queue. It is built from the constant 8 of type integer, the variable n of type integer, the binary operator + of type integer, the variable q of type queues of integers, and the operator append mentioned above.

Instead of atomic actions like a and b, we use actions that model the transmission of data over certain channels. In value-passing ACP there may be actions sc(d) indicating the sending of data (d) over the channel c. In value-passing CCS, the action a(d) denotes the sending of data d on the channel c. Here c is a taken from a set of channels names, where each channel comes with a certain data type, and d is a data expression of that type. The action c(x) represents the receipt of some data on some channel c. Here x is a variable of the data type required by c. The structural operational semantics is the same as before, except that the rule for communication now is $$\frac{P \stackrel{\bar c(d)}\longrightarrow P' \qquad Q \stackrel{c(x)}\longrightarrow Q'}{P | Q \stackrel{\tau}\longrightarrow P'|Q'\{v/x\}}$$ Here $d$ denotes a data expression of the data type specified by the channel c and $Q'\{d/x\}$ denotes the process $Q$ with $d$ substituted for all free occurrences of the variable $x$. There are different ways in which this can be made more precise; due to lack of time I will not do this here.

• Instead of recursive constants X that come with defining equations like X = a.X, we use parametrized recursive constants like X(n,q) where the parameters are variables ranging over certain data types. These parameters may be used in the body of the recursive equations. Such an equation could be $X(n,q) = c(x).X(x,append(n,q))$ for example. Here the process $X$ stores a number and a queue in the variables $n$ and $q$. It can read a number $x$ on channel $c$ and change its state by appending $n$ to its queue and storing $x$ instead of $n$.
• (not treated) Often there also are guards: expressions like $[x>5].P$. In case the variable $x$ evaluates to a number larger than 5, this guard evaluates to true and the process will behave like $P$. In case the guard evaluates to false the process behaves like the CCS constant 0. Now one can model an "if $x>5$ then $P$ else $Q$" statement like $[x>5].P + [x \leq 5].Q$.
I indicated how a value-passing process algebra could be translated into the standard process algebra with infinite sums.

## Handouts distributed in this course (2016)

(all fair game for exams)
The material treated only in week 13 is not examinable.
See also A HREF=2012leftovers.html>2012 leftovers.
 Rob van Glabbeek homework rvg@cse.unsw.edu.au