CIS 650 -- Models of Concurrent Systems

Assignment 3

Due Monday, October 5

1. In lecture we proved most of the cases of Proposition 12 of Section 4 (see pages 99--101). Complete the case where G has form G1\ L.

2. The rest of this assignment concerns getting familiar with the Concurrency Workbench (CWB). CWB is a computer-based tool that supports reasoning about CCS agents, including (among other things) their possible tranitions, equivalence among agents, and their satisfaction of various temporal-logic formulae.

   You should first read/browse through the local introduction to CWB, as well as the portions of the CWB user's manual that it recommends. The local guide includes information on running CWb as well as a sample session.

   Use CWB to answer the following questions and submit a transcript of the execution (if you run CWB from inside emacs, cut-and-paste from the buffer is fine). You'll probably find the CWB commands strongeq, transitions, derivatives, and sort.

   Note: These questions are primarily intended to get you working with CWB and to make sure that things have been set up correctly (and that my instructions make sense). Please let me know if you run into problems.

   1. Define the following agents:

      	    A0 =def a.A0 + b.A1 + tau.A1
      	    A1 =def a.A1 + tau.A2
      	    A2 =def b.A0
      	    B1 =def a.B1 + tau.B2 + b.B1
      	    B2 =def b.B1
      

      (Note that =def is an attempt to simulate Milner's notation in pure ASCII; it is not CWB syntax.)
      Are A0 and B1 strongly equivalent?

   2. Are

      	    a.(b.0 + c.0 + d.0)
      	    

      and

      	    a.(b.0 + c.0) + a. (c.0 + d.0) + a.(b.0 + d.0)
      	    

      strongly bisimlar?

   3. Recall the agents A, B and C of Problem 4 in Assignment 1.

      What are the immediate derivatives of C?

      What are the syntactic sorts of A, B, and C?

   4. What are the immediate b-derivatives of the following agent:

      	    B =def (('a.0 + b.B) | ('b.0 + a.B))[f] \{a,c}
      	    

      where the relabeling function f maps a to b, b to c and for all other labels (i.e., not a,b,'a,'b) behaves like the identity.