  It is well known that we can use structural proof theory to refine, or
generalize, existing paradigmatic computational primitives, or to discover new
ones. Under such a point of view we keep developing a programme whose goal is
establishing a correspondence between proof-search of a logical system and
computations in a process algebra. We give a purely logical account of a
process algebra operation which strictly includes the behavior of restriction
on actions we find in Milner CCS. This is possible inside a logical system in
the Calculus of Structures of Deep Inference endowed with a self-dual
quantifier. Using proof-search of cut-free proofs of such a logical system we
show how to solve reachability problems in a process algebra that subsumes a
significant fragment of Milner CCS.
