Concurrency cannot be observed, asynchronously

摘要

The paper is devoted to an analysis of the concurrent features of asynchronous systems. Arnpreliminary step is represented by the introduction of a non-interleaving extension of barbedrnequivalence. This notion is then exploited in order to prove that concurrency cannot bernobserved through asynchronous interactions, i.e., that the interleaving and concurrentrnversions of a suitable asynchronous weak equivalence actually coincide. The theory isrnvalidated on some case studies, related to nominal calculi (π-calculus) and visualrnspecification formalisms (Petri nets). Additionally, we prove that a class of systems which isrndeemed (output-buffered) asynchronous, according to a characterization that was previouslyrnproposed in the literature, falls into our theory.