Concurrency 5

CCS - Up-to bisimulation. Weak bisimulation. Axiomatizations.

Catuscia Palamidessi

INRIA Futurs and LIX - Ecole Polytechnique

The other lecturers for this course:

Jean-Jacques Lévy (INRIA Rocquencourt)

James Leifer (INRIA Rocquencourt) Eric Goubault (CEA)

http://pauillac.inria.fr/˜ leifer/teaching/mpri-concurrency-2005/

Outline

2

A brief summary: Syntax of CCS

(channel, port) names: a, b, c, … co-names: \overline{a}, \overline{b}, \overline{c}, … Note: \overline{\overline{a}} = a silent action: τ

actions, prefixes: μ ::= a | \overline{a} | τ

processes: P, Q ::= 0  inaction | μ.P  prefix | P | Q parallel | P + Q (external) choice | (νa)P restriction | K (a⃗) process name with parameters

Process definitions: D ::= K (x⃗) =^{def} P where fn(P) ⊆ x⃗

fn(P) is the set of free (channel) names in P (occurrences not in the scope of ν) conversely, bn(P) is the set of bound names in P (occurrences in the scope of ν)

A brief summary: Labeled transition system for CCS

We assume a given set of definitions D

[Act] _{\overline{μ.P →^{μ} P}}  [Res] \frac{P →^{μ} P′ μ≠a,\overline{a}}{(νa)P →^{μ} (νa)P′}
[Sum1] \frac{P →^{μ} P′}{P+Q →^{μ} P′}  [Sum2] \frac{Q →^{μ} Q′}{P+Q →^{μ} Q′}
[Par1] \frac{P →^{μ} P′}{P|Q →^{μ} P′|Q}  [Par2] \frac{Q →^{μ} Q′}{P|Q →^{μ} P|Q′}
[Com] \frac{P →^{a} P′ Q →^{\overline{a}} Q′}{P|Q →^{τ} P′|Q′}  [Rec] \frac{P[a⃗/x⃗] →^{μ} P′ K (x⃗)=^{def}P ∈ D}{K (a⃗) →^{μ} P′}

A brief summary: (Strong) Bisimulation and Bisimilarity

Definition We say that a relation R on processes is a bisimulation if P R Q implies that ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′ ifQ →^{μ} Q′ then ∃P′ s.t. P →^{μ} P′ and P′ R Q′

Note that this property does not uniquely defines R. There may be several relations that satisfy it. Definition (Bisimilarity) ∼ = ⋃{R | R is a bisimulation} Theorem ∼ is a bisimulation. P ∼ Q (P is bisimilar to Q) intuitively means that Q can do everything that P can do, and vice versa, at every step of the computation.

A brief summary: The coinductive method

Bisimilarity is a coinductive definition. In order to prove that P ∼ Q it is sufficient to find a bisimulation R such that P R Q

Bisimilarity is a congruence

Bisimilarity in CCS is a congruence

Definition A relation R on a language is a congruence if

R is an equivalence relation (i.e. it is reflexive, symmetric, and transitive), and R is preserved by all the operators of the language, namely if P R Q then op(P_{1}, …, P, …, P_{n}) R op(P_{1}, …, Q, …, P_{n})

Theorem ∼ is a congruence relation

This is an important property as it allows to prove equivalence in a modular way.

Proof of the congruence theorem

Bisimilarity is an equivalence relation.

Reflexivity. Let R = {(P, P) | P is a CCS process }. Then R is a bisimulation (Immediate). Symmetry. If P R Q, with R bisimulation, then Q R^{−1} P holds and R^{−1} is a bisimulation (Immediate). Transitivity. If P R Q and Q S R, with R, S bisimulations, then P R ∘ S R holds and R ∘ S is a bisimulation (Proof: exercise).

We have to prove now that ∼ is preserved by the operators of CCS. We prove it for the most complicated case, the parallel operator, and we leave the others as exercise.

Proof of the congruence theorem: case of the parallel operator

Assume P ∼ Q. We prove that for any R, P | R ∼ Q | R holds. (The case R | P ∼ R | Q is analogous). Let

R = {(P′ | R′, Q′ | R′) | P′, Q′, R′ are CCS processes and P′ ∼ Q′ }

We only need to prove that R is a bisimulation.

(Decomposition phase) Assume P′ | R′ →^{μ} P′′ | R′′. There are three cases, corresponding to the three rules for parallel composition.

(Rule Par1) In this case P′ →^{μ} P′′ and R′′ = R′. Since P′ ∼ Q′, there exists Q′′ such that Q′ →^{μ} Q′′ and P′′ ∼ Q′′. (Rule Par2) In this case P′′ = P′ and R′ →^{μ} R′′. Take Q′′ = Q′. (Rule Com) In this case P′ →^{a} P′′, R′ →^{\overline{a}} R′′, and μ = τ. Since P′ ∼ Q′, there exists Q′′ such that Q′ →^{a} Q′′ and P′′ ∼ Q′′.

(Composition phase) In each of the three cases, Q′ | R′ →^{μ} Q′′ | R′′ for some Q′′ such that P′′ ∼ Q′′, and therefore P′′ | R′′ R Q′′ | R′′ holds.

Some interesting bisimilarities

Some interesting bisimilarities

The following bisimilarities hold

P + 0 ∼ P  P | 0 ∼ P
P + Q ∼ Q + P  P | Q ∼ Q | P
(P + Q) + R ∼ P + (Q + R)  (P | Q) | R ∼ Q | (P | R)
P + P ∼ P
(νa)0 ∼ 0
(νa)(P | Q) ∼ P | (νa)Q if a ∉ fn(P)
(νa)(P + Q) ∼ P + (νa)Q if a ∉ fn(P)
(νa)(νb)P ∼ (νb)(νa)P
(νa)(P) ∼ (νb)P[b/a] if a not in the scope of (νb) in P (α conversion)
(νa)b.P ∼ 0  if b = a or b = \overline{a}
(νa)b.P ∼ b.(νa)P  if b ≠ a and b ≠ \overline{a}
K (a⃗) ∼ P[a⃗/x⃗]  ifK (x⃗) =^{def} P

Proof: Exercise

Some interesting bisimilarities

Some interesting bisimilarities: The Expansion Laws

The following bisimilarities hold

a.P | b.Q ∼ a.(P | b.Q) + b.(a.P | Q) ifb ≠ \overline{a}
a.P | \overline{a}.Q ∼ a.(P | \overline{a}.Q) + \overline{a}.(a.P | Q) + τ.(P | Q)

More in general:

(P | Q) ∼ (μ. ∑_{P →^{μ} P′} P′ | Q) + (μ. ∑_{Q →^{μ} Q′} P | Q′) + (τ. ∑_{Q →^{\overline{a}} Q′^{P \underrightarrow{a} P′}} P′ | Q′)

Proof: Exercise

Axiomatization of strong bisimilarity

An equational theory for CCS: the axioms are the “=” version of the bisimilarities seen in previous pages. That is:

P + 0 = P  P | 0 = P
P + Q = Q + P  P | Q = Q | P
(P + Q) + R = P + (Q + R)  (P | Q) | R = Q | (P | R)
P + P = P
(νa)0 = 0
(νa)(P | Q) = P | (νa)Q if a ∉ fn(P)
(νa)(P + Q) = P + (νa)Q if a ∉ fn(P)
(νa)(νb)P = (νb)(νa)P
(νa)(P) = (νb)P[b/a] if a not in the scope of (νb) in P (α conversion)
(νa)b.P = 0  if b = a or b = \overline{a}
(νa)b.P = b.(νa)P  if b ≠ a and b ≠ \overline{a}
K (a⃗) = P[a⃗/x⃗]  ifK (x⃗) =^{def} P
(P | Q) = (μ. ∑_{P →^{μ} P′} P′ | Q) + (μ. ∑_{Q →^{μ} Q′} P | Q′) + (τ. ∑_{Q →^{\overline{a}} Q′^{P \underrightarrow{a} P′}} P′ | Q′)

Axiomatization of strong bisimilarity

To prove equivalence of recursive processes, it is convenient to introduce also the following conditional axiom (Unique solution of equations):

Given a context C[ ] (that is, a term with some “holes” [ ]), in which all the holes are guarded (that is, occur in the context of a prefix), then, for every P and Q

if P = C[P] and Q = C[Q] then P = Q

Definition We write Ax ⊢ P = Q iff P = Q is derivable from the above axioms Ax and the usual rules for equality

Theorem (Soundness of the axiomatization) If Ax ⊢ P = Q then P ∼ Q.

The converse of the above theorem does not hold, i.e. the axiomatization is not complete. Note that the existence of a sound and complete axiomatization would imply the decidability of bisimilarity (because the complement of the bisimarity relation is semidecidable). However, bisimilarity is not decidable in CCS.

The characterization of subsets of CCS in which bisimulation is decidable is an important research field in Concurrency Theory.

Bisimulation up-to ∼

The axiomatization can be combined with the coinductive method to ease proving bisimilarity. The idea is based on the so-called “bisimulation up-to ∼” technique.

Definition We say that a relation R on processes is a bisimulation up-to ∼ if

P R Q implies that ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ ∼ R ∼ Q′ ifQ →^{μ} Q′ then ∃P′ s.t. P →^{μ} P′ and P′ ∼ R ∼ Q′

Notation: P′ ∼ R ∼ Q′ means: ∃P′′, Q′′ s.t. P′ ∼ P′′, P′′ R Q′′, and Q′′ ∼ Q′. Note that in order to prove P′ ∼ P′′ and Q′′ ∼ Q′, it is sufficient to prove Ax ⊢ P′ = P′′ and Ax ⊢ Q′′ = Q′ .

Theorem If there exists R such that R is a bisimulation up-to ∼, and P R Q holds, then P ∼ Q holds.

The advantage of the above technique is that it is usually easier to define a relation that is a bisimulation up-to ∼, rather than a bisimulation.

Exercises

Prove that A ∼ B where A =^{def} a.A and B =^{def} a.B + a.a.B

Prove that the two definitions of semaphores given in previous lecture are equivalent (that is, the semaphores given by those two definitions are bisimilar)

Value-passing CCS

In pure CCS processes communicate via channel (or port) names, but the communication does not carry data (or values). We now illustrate how we can modify CCS so that processes can send (and receive) values.

(data) variables: y, z, … (data) values: v, w, … (channel, port) names: a, b, c, … co-names: \overline{a}, \overline{b}, \overline{c}, … silent action: τ actions, prefixes: μ ::= a⟨y⃗⟩ | \overline{a}⟨v⃗⟩ | τ

processes: P, Q ::= 0  inaction | μ.P  prefix | P | Q  parallel | P + Q  (external) choice | (νa)P  restriction | {K (a⃗) \atop ⟨v⃗⟩} process name with parameters

Process definitions: D ::= K (x⃗)⟨y⃗⟩ =^{def} P where fn(P) ⊆ x⃗

The labeled transition system for value-passing CCS

We assume a given set of definitions D

[Send] _{\overline{\overline{a}⟨v⃗⟩.P →^{a⟨v⃗⟩} P}}
[Receive ] _{\overline{a⟨y⃗⟩.P →^{a⟨v⃗⟩} P[v⃗/y⃗]}}  [Res] \frac{P →^{μ} P′ μ≠a,\overline{a}}{(νa)P →^{μ} (νa)P′}
[Sum1] \frac{P →^{μ} P′}{P+Q →^{μ} P′}  [Sum2] \frac{Q →^{μ} Q′}{P+Q →^{μ} Q′}
[Par1] \frac{P →^{μ} P′}{P|Q →^{μ} P′|Q}  [Par2] \frac{Q →^{μ} Q′}{P|Q →^{μ} P|Q′}
[Com] \frac{P →^{a⟨v⃗⟩} P′ Q →^{\overline{a}⟨v⃗⟩} Q′}{P|Q →^{τ} P′|Q′}  [Rec] \frac{P[a⃗/x⃗][v⃗/y⃗] →^{μ} P′ K (x⃗)⟨y⃗⟩=^{def}P ∈ D}{K (a⃗)⟨v⃗⟩ →^{μ} P′}

Bisimulation and bisimilarity are defined as usual, considering as labels those of the form a⟨v⃗⟩ and \overline{a}⟨v⃗⟩

Translating value-passing CCS into pure CCS

If the domain V of values is finite, we can emulate value-passing CCS by translating it into pure CCS in the following way. We denote this translation by

[[·]] : value-passing CCS → pure CCS

For simplicity we assume channel arity 1.

[[0]] = 0
[[\overline{a}⟨v⟩.P]] = \overline{a_{v}}.[[P]]
[[a⟨y⟩.P]] = ∑_{v∈V} a_{v}.[[P[v/y]]]
[[P | Q]] = [[P]] | [[Q]]
[[P + Q]] = [[P]] + [[Q]]
[[(νa)P]] = (νa)[[P]]
[[K (a⃗)⟨v⟩]] = K_{v}(a⃗)

Furthermore, each definition K (x⃗)⟨y⃗⟩ =^{def} P is replaced by the following set of definitions, one for each v ∈ V :

K_{v}(x⃗) =^{def} [[P[v/y]]]

Weak Bisimulation and Weak Bisimilarity

Motivation: abstract from internal actions (i.e. τ actions) We introduce the following notation

P( →^{τ} )^{∗}Q iff P = P_{0} →^{τ} P_{1} →^{τ} … →^{τ} P_{n} = Q

P ⇒^{μ⃗} Q iff

P = P_{0} ( →^{τ} )^{∗} →^{μ_{1}} ( →^{τ} )^{∗} P_{1} ( →^{τ} )^{∗} →^{μ_{2}} ( →^{τ} )^{∗} … ( →^{τ} )^{∗} →^{μ_{n}} ( →^{τ} )^{∗} P_{n} = Q

and μ⃗ = μ_{1}μ_{2} … μ_{n} P \underrightarrow{μ̂} Q iff P ⇒^{μ⃗} Q and μ̂ is obtained from μ⃗ by removing all the τ’s

Examples: â = a, τ̂aτ = a, τ̂ = ε (empty string), âτb = ab. Note:

P \underrightarrow{â} Q means P ( →^{τ} )^{∗} →^{a} ( →^{τ} )^{∗} Q, P \underrightarrow{τ̂} Q means P ⇒^{ε} Q, namely P ( →^{τ} )^{∗} Q, P ⇒^{τ} Q means P ( →^{τ} )^{∗} →^{τ} ( →^{τ} )^{∗} Q, namely P ( →^{τ} )^{+} Q (at least one τ-step).

Weak Bisimulation and Weak Bisimilarity

Definition We say that a relation R on processes is a weak bisimulation if

P R Q implies that ifP →^{μ} P′ then ∃Q′ s.t. Q \underrightarrow{μ̂} Q′ and P′ R Q′ ifQ →^{μ} Q′ then ∃P′ s.t. P \underrightarrow{μ̂} P′ and P′ R Q′

Note that this property does not uniquely defines R. There may be several relations that satisfy it.

Definition (Bisimilarity) ≈ = ⋃{R | R is a weak bisimulation}

Theorem ≈ is a weak bisimulation.

P ≈ Q (P is weakly bisimilar to Q) intuitively means that at every step of the computation Q can do everything that P can do, and vice versa, if we ignore the internal actions.

Observation congruence

Unfortunately ≈ is not a congruence. Example: a.P ≈ τ.a.P but a.P + b.Q ≉ τ.a.P + b.Q

Definition We say that P and Q are observation-congruent (notation P ≅ Q) iff

ifP →^{μ} P′ then ∃Q′ s.t. Q ⇒^{μ} Q′ and P′ ≈ Q′
ifQ →^{μ} Q′ then ∃P′ s.t. P ⇒^{μ} P′ and P′ ≈ Q′

The difference between ≈ and ≅ is when the first step is a τ-step. If P →^{τ} P′ and P ≈ Q, then we can take Q′ = Q provided that P′ ≈ Q′. On the contrary, if P ≅ Q, then we are obliged to find a Q′ such that Q ⇒^{τ} Q′ (which means, at least one τ-step from Q to Q′), and P′ ≈ Q′.

Theorem ∼ ⊆ ≅ ⊆ ≈

Proof: exercise.

Theorem ≅ is a congruence, and more precisely, it is the largest congruence on CCS contained in ≈.

Properties of observation congruence

Properties of observation congruence

Proposition The following properties hold:

μ.τ.P ≅ μ.P
P + τ.P ≅ τ.P
μ.(P + τ.Q) + μ.Q ≅ μ.(P + τ.Q)

Proof: exercise. The above properties are used to give an axiomatization observation congruence. The “=” version of the above are called τ-laws:

μ.τ.P = μ.P
P + τ.P = τ.P
μ.(P + τ.Q) + μ.Q = μ.(P + τ.Q)

Definition We write Ax_{τ} ⊢ P = Q iff P = Q can be derived from the axioms Ax, the τ-laws, and the usual rules for equality. Theorem (Soundness) If Ax_{τ} ⊢ P = Q then P ≅ Q.

Properties of observation congruence

Properties of observation congruence

The following properties that can be useful to prove observation congruence If P ≈ Q then μ.P ≅ μ.Q P ≈ Q iff P ≅ Q or P ≅ τ.Q or τ.P ≅ Q

Exercise:

Assume A =^{def} a.b.0 + a.c.0 and B =^{def} a.(τ.b.0 + τ.c.0). Prove that A ≅ B. Assume A =^{def} (νb)(a.b.c.0 + a.b̄.c.0) and B =^{def} a.a.c.c.0. Prove that A ≅ B.

Example: FIFO Queues

Two equivalent definitions of FIFO Queues

Consider the following definitions of a FIFO queue with 2 positions in value-passing CCS

First definition

Q_{2}(in, out) =^{def} in(y).Q_{1}(in, out)⟨y⟩
Q_{1}(in, out)⟨y⟩ =^{def} in(z).Q_{0}(in, out)⟨z, y⟩ + \overline{out}⟨y⟩.Q_{2}(in, out)
Q_{0}(in, out)⟨z, y⟩ =^{def} \overline{out}⟨y⟩.Q_{1}(in, out)⟨z⟩

Second definition Here we define a 2-positions queue as the concatenation of two 1-position buffers

B(in, out) =^{def} in(y).B′(in, out)⟨y⟩
B′(in, out)⟨y⟩ =^{def} \overline{out}⟨y⟩.B(in, out)
Queue (in, out) =^{def} (νc)(B(in, c) | B(c, out))

Exercise Prove that Q_{2}(in, out) is observation-congruent to Queue (in, out).