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 in a given state, but also say which parts of the agents move when the global state changes. From the transition relation a particular Petri Net, namely a Condition/Event system called ?_ccs, is immediately derived. Our construction gives a semantics which is consistent with the interleaving semantics of CCS and exhibits full parallelism. The proof consists of relating the case graph of ?_CCS with the original and with the multiset (step) transition systems of the calculus.
A distributed operational semantics for CCS based on condition/event systems
De Nicola R;
1988
Abstract
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 in a given state, but also say which parts of the agents move when the global state changes. From the transition relation a particular Petri Net, namely a Condition/Event system called ?_ccs, is immediately derived. Our construction gives a semantics which is consistent with the interleaving semantics of CCS and exhibits full parallelism. The proof consists of relating the case graph of ?_CCS with the original and with the multiset (step) transition systems of the calculus.| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_419429-doc_148224.pdf
solo utenti autorizzati
Descrizione: A distributed operational semantics for CCS based on condition/event systems
Tipologia:
Versione Editoriale (PDF)
Dimensione
4.39 MB
Formato
Adobe PDF
|
4.39 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
