Istituto di Scienza e Tecnologie dell'Informazione     
Degano P., De Nicola R., Montanari U. A distributed operational semantics for CCS based on condition/event systems. Internal note IEI-B4-21, 1987.
A new set of inference rules for the guarded version of Milner' s Calculus of Communicating Systems is proposed. They not only describe the actions agents may perform when a given state, but also say which parts of the agents move when the global state changes. From the transition relation a Condition/Event system, called ƩCCS, is immediately derived and two demonstrations are given of its adequacy as a truly concurrent and distributed CCS semantics. First, we prove that the abstract interleaving case graph of ƩCCS (i.e., the case graph with arcs labelled by single actions) is homomorphic to the transition system defined by Milner's inference rules. Since the homomorphisrn preserves transitions, we also have that the synchronization trees of two corresponding nodes are identical. Thus, our construction gives a semantics which is consistent with the original interleaving semantics of CCS whatever behavioural equivalence is chosen. Second, we prove that the transition system expressing a multiset semantics for CCS is transition-preserving hornornorphic to the abstract case graph of ƩCCS (i.e., the case graph with arcs labelled by multisets of actions) and thus that the amount of parallelism exhibited by ƩCCS and by multiset CCS is the same.

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional