CS 352.      Homework given on April 29, and elaborated on May 1, 1997

A.  Winskel's parallel composition is given by the following
    structural operational rules:

         x -a-> x'	  x -a-> x'  y -b-> y'        y -b-> y'
    -------------------   --------------------   -------------------
    x||y -(a,*)-> x'||y   x||y -(a,b)-> x'||y'   x||y -(*,b)-> x||y'

    In untyped CSP parallel compositions |H| (with H a set of actions)
    is used given by the rules 

    x -a-> x' (a not in H) x -a-> x'  y -a-> y' (a in H) y -b-> y' (b not in H)
    ---------------        --------------------          -------------------
    x||y -a-> x'||y          x||y -a-> x'||y'            x||y -b-> x||y'

    (In "Notes" and in the original variant of CSP only two parallel
    compositions occur, namely the one with H=Act (denoted ||) and the
    one with H empty (denoted |||).)
						x -a-> x' ((a,b) in R)
    Relational renaming is given by the rule ---------------
                                             x[R] -b-> y'[R]

    Relational renaming extends (functional) renaming, in that R is
    allowed to be a binary relation over Act, instead of a function.
    Note that restriction is a special case of relational renaming.

    a) show that every parallel composition |H| is expressible in
       terms of Winskels ||, restriction and renaming.
    b) show that Winskels || can be expressed in terms of the
       operators |H| and relational renaming.

B.  Show that for every failure set satisfying the four closure
    properties of the handout ("Notes ..."), there is a process graph
    G where F(G) is that failure set.

C.  Consider the CSP-like syntax P ::= 0 | aP | P+P | P|H|P | P[R]
    with a an action and R a relational renaming.
    
       Give a `definition' of this language on the model of failure
       sets that is consistent with the given structural operational
       semantics. In other words, express F(P+Q) as obtained from the
       transition system generated by the SOS in terms of F(P) and
       F(Q) obtained in the same way, and likewise for the other operators.