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 some case studies, related to nominal calculi (pi-calculus) and visual specification formalisms (Petri nets). Additionally, we prove that a class of systems which are (output-buffered) asynchronous according to a characterisation previously proposed in the literature falls into our theory.
Concurrency Can't Be Observed, Asynchronously
BALDAN, PAOLO;
2015
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 some case studies, related to nominal calculi (pi-calculus) and visual specification formalisms (Petri nets). Additionally, we prove that a class of systems which are (output-buffered) asynchronous according to a characterisation previously proposed in the literature falls into our theory.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
