The paper is devoted to an analysis of the concurrent features of asynchronous systems. A preliminary step is represented by the introduction of a non-interleaving extension of barbed equivalence. This notion is then exploited in order to prove that concurrency cannot be observed through asynchronous interactions, i.e., that the interleaving and concurrent versions of a suitable asynchronous weak equivalence actually coincide. The theory is validated on two case studies, related to nominal calculi (pi-calculus) and visual specification formalisms (Petri nets).
Concurrency Can't Be Observed, Asynchronously
BALDAN, PAOLO;
2010
Abstract
The paper is devoted to an analysis of the concurrent features of asynchronous systems. A preliminary step is represented by the introduction of a non-interleaving extension of barbed equivalence. This notion is then exploited in order to prove that concurrency cannot be observed through asynchronous interactions, i.e., that the interleaving and concurrent versions of a suitable asynchronous weak equivalence actually coincide. The theory is validated on two case studies, related to nominal calculi (pi-calculus) and visual specification formalisms (Petri nets).
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
APLAS10.pdf
Accesso riservato
Tipologia:
Published (Publisher's Version of Record)
Licenza:
Accesso privato - non pubblico
Dimensione
281.15 kB
Formato
Adobe PDF
|
281.15 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
