 Solution

ID: past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/concurrency/1/b/solution

h

P = (h \to P) ∖ {h} .

The apparent guard is removed by CSP hiding. Each unfolding can perform a CSP internal action and return to the same situation without any visible CSP event. Operationally this is an infinite internal loop, a CSP divergence, so the equation is not a guarded recursion. This is precisely why a syntactic test that counts every occurrence of

\to

would be wrong.

 New to topics? Read the docs here!