Consider the paper  "A Calculus of Mobile Resources" handed out at the
lecture.


Exercise I (Warm up:)
Consider the transition rules in table 4 and describe the possible
transtions of the processes:


P  = (b)(a>co{b}.0 || b[*])

Q = a[b.0] || a\co{b}.c.0

where \co{b} denotes a b with a bar over.

(in both cases the transition systems are infinite, so you may want to use
symbolic processes/contexts ranging over all processes or specific contexts)


Exercise II (Bisimulation)
Verify the claim in section 6, i.e. that the set S is a bisimulation, by
checking that the condition in definition 3 is satisfied.

Exercise III (Speculative, Relationship to Ambients)
Sketch an encoding into the Mobile Resources Calculus of the following
fragment of Mobile Ambients calculus:


M:= out n | in m

A:= A || A   (parallel composition)
    |  n[A]     (ambient)
    |  M.A    (prefix)
    | 0          (inactive)


Please step by my office if you have any questions,