Linearity, Persistence and Testing Semantics in the Asynchronous Pi-Calculus
Diletta Cacciagrano, Flavio Corradini, Jesús Aranda, Frank Valencia · Electronic Notes in Theoretical Computer Science · 2008
In [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59–68 , 2006] the authors studied the expressiveness of persistence in the asynchronous π -calculus (A π ) wrt weak barbed congruence. The study is incomplete because it ignores the issue of divergence. In this paper, we present an expressiveness study of persistence in the asynchronous π -calculus (A π ) wrt De Nicola and Hennessy's testing scenario which is sensitive to divergence. Following [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59–68 , 2006], we consider A π and three sub-languages of it, each capturing one source of persistence: the persistent-input calculus (PIA π ), the persistent-output calculus (POA π ) and persistent calculus (PA π ). In [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59–68 , 2006] the authors showed encodings from A π into the semi-persistent calculi (i.e., POA π and PIA π ) correct wrt weak barbed congruence. In this paper we prove that, under some general conditions, there cannot be an encoding from A π into a (semi)-persistent calculus preserving the must testing semantics.