Distribution and Locality of Concurrent Systems

A new semantics for process description languages that discriminates according to the distribution in space of processes is proposed. The semantics is based on a set of distributed transition rules that record spatial information and on a notion of equivalence that discriminates according to which actions processes can perform and where these actions are performed. The new semantics is proven to coincide with the locality equivalence of Boudol, Castellani, Hennessy and Kiehn. Over the latter, it has the advantage of not requiring explicit introduction of a (infinite) space of locations; this makes the new equivalence amenable to a mechanical treatment in the same vein as the classical bisimulation-based equivalences. Indeed, we propose a polynomial time algorithm for checking locality equivalence of processes