MPRI 2004/05 – Cours 2-3 (Concurrency)

Exam

17 February 2005

Part I - CCS

Question 1 For each of the following pairs of processes, say which is the strongest relation which relates them, among ∼, ≈ and ≅. Justify your answer, namely prove that the relation holds and that no stronger relation holds. Note: In some case, it may be that none of the relations holds

1. τ.P and P + τ.P

2. P and P | P

3. A and B, where A and B are defined recursively by A = a.A and B = a.B | a.B.

4. (νb)(a.b.c.0 | d.\overline{b}.e.0) and a.c.0 | d.e.0

5. P + Q and τ.P + τ.Q

6. (νa)(\overline{a} | (a.P + a.Q)) and τ.P + τ.Q Question 2 We say that P simulates Q, notation Q ⪯ P, if there exists a relation R such that (Q, P) ∈ R and for every (T, U) ∈ R we have:

T ⟶^{α} T′ implies ∃U′. U ⟶^{α} U′ and (T′, U′) ∈ R

Say whether it is the case that P ∼ Q if and only if P ⪯ Q and Q ⪯ P. Justify your answer, namely prove the above equivalence or find a counterexample

Part II - The Pi-calculus

1. The monadic synchronous π-calculus has the following grammar:

P ::= \overline{x}y.P | x(y).P | νx.P | 0 | P | P | !P

2. The following labelled transition rules give the behavior of replication:

\frac{P ⟶^{α} P′}{!P ⟶^{α} P′ |!P} if bn(α) ∩ fn(P) = ∅  (bang-spawn)
\frac{P ⟶^{\overline{x}y} P′  P ⟶^{xy} P′′}{!P ⟶^{τ} (P′ | P′′) |!P}  (bang-comm)
\frac{P ⟶^{\overline{x}(y)} P′  P ⟶^{xy} P′′}{!P ⟶^{τ} νy.(P′ | P′′) |!P} if y ∉ fn(P)  (bang-close)

Question 3 Define what it means for a relation to be a strong labelled bisimulation.

Question 4 In the monadic π-calculus, prove that strong labelled bisimilarity is preserved by replication, i.e. P ∼_{ℓ} Q implies !P ∼_{ℓ} !Q. To do this, construct an explicit relation R that contains the latter pairs (amongst others) and prove that it is a strong labelled bisimulation.

Note: You may use the fact that ∼_{ℓ} is preserved by parallel composition and by new binding, but if you do, cite the these results clearly.

You may use “up to” techniques; if so explain clearly how and where you use them.

Part III - The Asynchronous Pi-calculus

1. The monadic asynchronous π-calculus has the following grammar:

P ::= \overline{x}y | x(y).P | νx.P | 0 | P | P | !P

2. The set of evaluation contexts E is defined as

E = {νz⃗.(− | T) / T a process}

where the binding names of D = νz⃗.(− | T) ∈ E are bind(D) = {z⃗}.

3. Reduction and strong barbs are both characterisable in terms of evaluation contexts and structural congruence:

• P ⟶ P′ iff there exists D ∈ E, names x, v, and u, and a process P_{0} such that P ≡ D[\overline{x}v | x(u).P_{0}] and P′ ≡ D[\{v/u\}P_{0}].

• P ↓x iff there exists D ∈ E and names x and v such that P ≡ D[\overline{x}v] and x ∉ bind(D).

4. Weak barbed bisimulation ˙≈ is the largest relation R that is symmetric and for which for all (P, Q) ∈ R

• if P ⟶ P′, there exists Q′ such that Q ⟶^{∗} Q′ and (P′, Q′) ∈ R;

• if P ↓x then Q⇓x.

Question 5

1. Define the weak barb relation Q⇓x used above in the definition of ˙≈.

2. Show why ˙≈ is not preserved by parallel composition, i.e. find P, Q, R such that P ˙≈ Q but not P | R ˙≈ Q | R.

3. Prove that P ⟶ P′ implies {x/y}P ⟶ {x/y}P′.

4. Consider an equator process

E_{x,y} = !x(u).\overline{y}u |!y(u).\overline{x}u

5. Prove that E_{x,y} | D[\overline{x}v] ⟶ E_{x,y} | D[\overline{y}v] for x, y ∉ bind(D).

6. Show that equators can act like substitutions, i.e. νy.(E_{x,y} | P) ˙≈ {x/y}P. To do this, you need to demonstrate that there exists a weak barbed bisimulation containing the pair of processes in question.

7. Show that in the monadic synchronous π-calculus, i.e. the calculus where output prefixing \overline{w}z.Q is allowed, that this is false. To do this exhibit a concrete P for which the barbed behaviour of νy.(E_{x,y} | P) differs from that of {x/y}P.