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.