Observing distribution in processes

Abstract

The distributed structure of CCS processes can be made explicit by assigning different locations to their parallel components. These locations then become part of what is observed of a process. The assignment of locations may be done statically, or dynamically as the execution proceeds. The dynamic approach was developed first, by Boudol et al. in [BCHK91a], [BCHKSlb], as it seemed more convenient for defining notions of location equivalence and preorder. However, it has the drawback of yielding infinite transition system representations. The static approach, which is more intuitive but technically more elaborate, was later developed by L. Aceto [Ace91] for nets of automata, a subset of CCS where parallelism is only allowed at the top level. In this approach each net of automata has a finite representation, and one may derive notions of equivalence and preorder which coincide with the dynamic ones. The present work generalizes the static treatment of Aceto to full CCS. The result is a distributed semantics which yields finite transition systems for all CCS processes with a regular behaviour and a finite degree of parallelism.

This work has been partly supported by the Project 502-1 of the Indo-French Centre for the Promotion of Advanced Research.