Fall 2001, CSE 520: Assignment 6

Distributed: Published on the web on Nov 22.
Due: Dec 4 (in class).
Total maximum score: 100 points.
The purpose of this assignment is to provide experience with Concurrency.

Please write your solutions as clearly and concisely as possible.

Definition of a queue in CCS

Note: This exercise corresponds to Exercise 4 in the pages that were distributed in class on Tuesday 20 November (Exercise 4 at pages 134-135 in the book "Communication and Concurrency" by Robin Milner).

Consider the following specification of an unbounded queue, where ":" stands for the concatenation operation of an element to a sequence, and "e" stands for the empty sequence. 

   Queue(e)    =def=  in(x).Queue(x) + empty.Queue(e)
   Queue(s:v)  =def=  in(x).Queue(x:s:v) + ^out(v).Queue(s)

The exercise consists in defining an "implementation" for the queue that corresponds (i.e. is weakly bisimilar to) the above specification. The implementation should be done similarly to the implementation of the Stack illustrated in the pages distributed in class (page 134 in the book "Communication and Concurrency" by Robin Milner).

Please add some comments to explain your solution so that the TA and I can understand it more easily.