Abstract:
(see also RR-2276)
The distributed structure of CCS processes can be made
explicit by assigning different locations to their parallel
components. The assignment of locations may be done statically, or
dynamically as the execution proceeds. The dynamic approach was
developed first, by Boudol et al., as it appeared more convenient for
defining notions of location equivalence and preorder. Extending
previous work by L. Aceto we study here the static approach, which is
more natural from an intuitive point of view, and more manageable for
verification purposes. We define static notions of location
equivalence and preorder, and show that they coincide with the dynamic
ones. To establish the equivalence of the two location semantics, we
introduce an intermediate transition system called occurrence system,
which incorporates both notions of locality. This system supports a
definition of local history preserving bisimulation for CCS, which is
a third formulation of location equivalence.