Fall 98, CSE 520: Assignment 4

Distributed: Published on the web on Nov. 18.
Due: Dec 8 (in class).
Total maximum score: 100 points.
The purpose of this assignment is to provide experience with CCS and the pi-calculus, and with the notion of bisimulation.

Please write your solutions as clearly and concisely as possible.

  1. (30 pts) For each of the following pairs of processes P and Q, say whether they are strongly / weakly bisimilar or not. (You don't need to write the justification)
    1. P =def= a.0 + a.P , Q =def= a.(0 + Q)
    2. P =def= a.0 + tau.P , Q =def= a.0
    3. P =def= a.(P | P) , Q =def= a.a.Q
    4. P =def= a.tau.c.0 + a.tau.d.0 , Q =def= a.(tau.c.0 + tau.d.0)
    5. P =def= a.R | a^.0 , Q =def= a.a^.R + a^.a.R + tau.R
    In the last pair, a^ represents the action complementary to a. (according to our convension, a is input and a^ is output).

  2. (10 pts) The Communicating Bit Protocol described in class (and in Chapter 6 of Milner89), is weakly bisimilar to a one-cell buffer. Suppose now that we change the protocol so that the acknowledgement is sent before delivery. Say whether the new system is weakly bisimilar to a
    1. one-cell buffer
    2. n-cells buffer (if this is the case, say what is n)
    3. unbounded buffer
    4. none of the above.
    You don't need to justify your answer.

  3. (25 pts) The "internal choice" between P and Q is defined as tau.P + tau.Q. Give a compositional encoding of this construct in CCS and in the pi-calculus, without using the + operator. The result of the encoding must be bisimilar to the original process. You don't need to prove the correctness of your encoding.

    Note: "Compositional encoding" means that the encoding of each compound process op(P1,...Pn) is defined in terms of the encodings of the components, i.e. the equations defining the encoding are of the form:

    [[ op(P1,...Pn) ]] = ... [[P1]] ... [[Pn]] ...

  4. (35 pts) In class we have seen how to encode compositionally the input and output prefix of the pi-calculus into the asynchronous polyadic pi-calculus (Honda-Tokoro encoding). Show that we don't need the "polyadic" feature for this purpose, i.e. give a compositional encoding of the input and output prefix of the pi-calculus into the "standard" (i.e. monadic) asynchronous pi-calculus, where only one name can be communicated at a time (i.e. the actions are of the form x(y) and x^y, where y is one single name.) The result of the encoding must be (weakly) bisimilar to the original process. You don't need to prove the correctness of your encoding.