Midterm Exam

MPRI – Cours 2-3

30 November 2005

Question 1 (5 points)

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. A | B and C, where A =^{def} a.A, B =^{def} b.B and C =^{def} a.C + b.C.

2. τ.(P | P) and P | τ.P.

3. (νa)(νb)(ā.0 | b̄.0 | a.b.P | b.a.Q) and τ.P + τ.Q.

4. a.0 and (νb)(A | B), where A =^{def} b.A + a.0 and B =^{def} b̄.B + τ.0.

5. a.0 and A, where A =^{def} τ.B + a.0 and B =^{def} τ.B.

Question 2 (5 points)

In a ceramic workshop there are two workers that are specialized in painting: each worker W receives an unpainted item u, paints it using its own brush, gives back the painted item p̄, and starts the cycle again. Formally the production unit U can be described as follows:

U =^{def} W | W where W =^{def} u.p̄.W

One day, one of the brushes breaks, and while waiting for a new one, the two workers decide to share the remaining one, after establishing some simple synchronization rules. More precisely, each of them will signal with ā his “take brush” action, and with b̄ his “release brush” action. The new production unit U′ can then be described as follows:

U′ =^{def} (νa)(νb)(W′ | B | W′) where W′ =^{def} u.ā.b̄.p̄.W′ and B =^{def} a.b.B

The question is: is the new production unit U′ observation congruent to the old one U? Prove or disprove the statement.

Question 3

Consider the following specification of an unbounded buffer B_{k}(empty, in, out) in CCS, where k represents the number of elements that are in the buffer at the moment, and empty, in, \overline{out} represent the possible actions of the buffer:

• empty: signal that the buffer is empty. Possible only for B_{0}

• in: insert an element

• \overline{out}: output an element. Possible only for B_{k} with k > 0.

For simplicity, we abstract from the value of the elements. Furthermore, we omit the parameters when they are clear from context, i.e. we write B_{k} instead of B_{k}(empty, in, out).

B_{0}  =^{def} empty.B_{0} + in.B_{1}
B_{k+1} =^{def} \overline{out}.B_{k} + in.B_{k+2}

We want to implement the buffer using a concatenation of cells, where each cell C(empty, in, out, e, i, o) will contain just one element. A special process E(empty, in, out, e, i, o) will represent the empty buffer. These processes are specified as follows (again, we omit the parameters for simplicity):

E =^{def} empty.E + in.(C ▷ E)
C =^{def} \overline{out}.C′ + in.(C ▷ C)
C′ =^{def} o.C + \overline{e}.E

where C ▷ E is defined by

C ▷ E =^{def} (νe′)(νi′)(νo′)(C(empty, in, out, e′, i′, o′) | E(e′, i′, o′, e, i, o))

and analogously for C ▷ C, C ▷ C′, etc.

It is known that ▷ is associative modulo ∼. Namely, (P ▷ Q) ▷ R ∼ P ▷ (Q ▷ R). Hence in the following we can omit the parentheses and write P ▷ Q ▷ R.

Question 3.1 (3 points) Prove that C′ ▷ C ≈ C ▷ C′, C′ ▷ E ≈ E ▷ E, and E ▷ E ∼ E.

Note: You can use the fact that if P has only one transition of the form P ⟶^{τ} Q, then P ≈ Q.

Question 3.2 (2 points) Define C^{(k)} (for k ≥ 0) as follows:

C^{(k)} =^{def} C ▷ C ▷ … ▷ C ▷ E (with C repeated k times)

Using the relations in previous question, prove that for any k ≥ 0, C′ ▷ C^{(k)} ≈ C^{(k)}.

Note: You can use the fact that ≈ is preserved by ▷, i.e. P ≈ Q implies P ▷ R ≈ Q ▷ R.

Question 3.3 (5 points) Using the result established in previous question, prove that for every k ≥ 0, C^{(k)} ≈ B_{k}.

Note: You can use the expansion theorem and the unique fixed-point theorem for weak bisimulation.

The expansion theorem (in its most general form) says that for any process process P we have

P = ∑_{P ⟶^{α}P′} α.P′

The unique fixed-point theorem for weak bisimulation says the following: Consider two (possibly infinite) families of processes P⃗ = P_{1}, P_{2}, …, Q⃗ = Q_{1}, Q_{2}, …, and a family of contexts C⃗[ ] = C_{1}[ ], C_{2}[ ], . . .. Assume that each “hole” in the contexts is strongly guarded (i.e. in the scope of a non-τ prefix). We have that, if P⃗ and Q⃗ satisfy P⃗ ≈ C⃗[P⃗] and Q⃗ ≈ C⃗[Q⃗], then P⃗ ≈ Q⃗.

Bonus question (2 points)

A professor announces in class:

Next week there will be a surprise test.

The students reply:

Impossible. You cannot give us a surprise test. In fact, you cannot give it on Friday, because it is the last day of the week, and we would know by the end of Thursday that it is going to be on Friday, so it would not be a surprise. Analogously you cannot give it on Thursday, because we know it cannot be on Friday, and so by the end of Wednesday we would know that it would be on Thursday, etc.

The professor remains silent. The students think that they have won the argument and they are happy imagining of all the fun things they can do next week instead of preparing for the test. Then, the following week, on Wednesday, the professor gives the test, and takes everybody by surprise.

How would you explain the above apparent paradox?