zbMATH — the first resource for mathematics

Linearity, persistence and testing semantics in the asynchronous pi-calculus. (English) Zbl 1277.68167
Amadio, Roberto (ed.) et al., Proceedings of the 14th international workshop on expressiveness in concurrency (EXPRESS 2007), Lisbon, Portugal, September 3, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 194, No. 2, 59-84 (2008).
Summary: In [“On the expressiveness of linearity vs persistence in the asynchronous pi calculus”, in: Proceedings of the 21st annual IEEE symposium on logic in computer science, LICS’2006. Los Alamitos: IEEE Press. 59–68 (2006)], C. Palamidessi et al. studied the expressiveness of persistence in the asynchronous \(\pi\)-calculus (A\(\pi\)) w.r.t 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 \(\pi\)-calculus (A\(\pi\)) w.r.t De Nicola and Hennessy’s testing scenario which is sensitive to divergence. Following [loc. cit.], we consider A\(\pi\) and three sub-languages of it, each capturing one source of persistence: the persistent-input calculus (PIA\(\pi\)), the persistent-output calculus (POA\(\pi\)) and persistent calculus (PA\(\pi\)). In [loc. cit.], Palamidessi et al. showed encodings from A\(\pi\) into the semi-persistent calculi (i.e., POA\(\pi\) and PIA\(\pi\)) correct w.r.t weak barbed congruence. In this paper we prove that, under some general conditions, there cannot be an encoding from A\(\pi\) into a (semi)-persistent calculus preserving the must testing semantics.
For the entire collection see [Zbl 1276.68007].

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI
[1] J. Alves-Foss. An Efficient Secure Authenticated Group Key Exchange Algorithm for Large and Dynamic Groups. In Proceedings of the 23rd National Information Systems Security Conference, 2000
[2] Amadio, R.; Lugiez, D.; Vanackere, V., On the symbolic reduction of processes with cryptographic functions, TCS: theoretical computer science, 290, (2003) · Zbl 1051.68054
[3] Best, E.; de Boer, F.; Palamidessi, C., Partial order and sos semantics for linear constraint programs, ()
[4] Blanchet, B., From linear to classical logic by abstract interpretation, Information processing letters, 95, 5, (2005) · Zbl 1185.68310
[5] Boreale, M.; Buscemi, M., A framework for the analysis of security protocols, Lecture notes in computer science, 2421, (2002) · Zbl 1012.68520
[6] Brinksma, E.; Rensink, A.; Vogler, W., Fair testing, (), 313-327
[7] Cacciagrano, D.; Corradini, F., On synchronous and asynchronous communication paradigms, (), 256-268 · Zbl 1042.68614
[8] Cacciagrano, D.; Corradini, F.; Palamidessi, C., Separation of synchronous and asynchronous communication via testing, Proc. of EXPRESS’05, Electr. notes theor. comput. sci., 154, 3, 95-108, (2006), An extended version will appear in Theoretical Computer Science · Zbl 1273.68251
[9] Carbone, M.; Maffeis, S., On the expressive power of polyadic synchronisation in pi-calculus, Nord. J. comput., 10, 2, 70-98, (2003) · Zbl 1062.68077
[10] Castellani, I.; Hennessy, M., Testing theories for asynchronous languages, (), 90-101
[11] F. Crazzolara. Language, Semantics, and Methods for Security Protocols. PhD Dissertation, University of Aarhus, Denmark, 2003
[12] Crazzolara, F.; Winskel, G., Events in security protocols, ()
[13] De Nicola, R.; Hennessy, M., Testing equivalence for processes, Theoretical computer science, 34, 83-133, (1984) · Zbl 0985.68518
[14] Fages, F.; Ruet, P.; Soliman, S., Linear concurrent constraint programming: operational and phase semantics, Information and computation, (2001) · Zbl 1003.68065
[15] Fiore, M.; Abadi, M., Computing symbolic models for verifying cryptographic protocols, ()
[16] D. Gorla: On the Relative Expressive Power of Asynchronous Communication Primitives. FoSSaCS 2006, 47-62, 2006 · Zbl 1180.68190
[17] D. Gorla: Synchrony vs Asynchrony in Communication Primitives Proc. of EXPRESS’06, 47-62, 2006
[18] S. Maffeis and I. Phillips. On the computational strength of pure ambient calculi. Proc. of EXPRESS ’03, 2003 · Zbl 1271.68190
[19] Milner, R., Communication and concurrency, (1989), Prentice-Hall International · Zbl 0683.68008
[20] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, part I and II, Information and computation, 100, 1-78, (1992)
[21] Merro, M.; Sangiorgi, D., On asynchrony in name-passing calculi, () · Zbl 0910.03019
[22] Nestmann, U., What is a ‘good’ encoding of guarded choice?, Information and computation, 156, 287-319, (2000) · Zbl 1046.68625
[23] Palamidessi, C., Comparing the expressive power of the synchronous and asynchronous π-calculus, Mathematical structures in computer science, 13, 5, 685-719, (2003), A preliminary version appeared in the proceedings of POPL ’97
[24] 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
[25] L.C. Paulson. Mechanized proofs for a recursive authentication protocol. In 10th Computer Security Foundations Workshop, 1997
[26] I. Phillips and M. Vigliotti Electoral Systems in Ambient Calculi. FoSSaCS’04. 2004 · Zbl 1126.68508
[27] Phillips, I.; Vigliotti, M., Leader election in rings of ambient processes, Electr. notes theor. comput. sci., 128, 2, 185-199, (2005) · Zbl 1272.68318
[28] Prasad, K.V.S., Broadcast calculus interpreted in CCS up to bisimulation, Proceedings of express’01, Electronic notes in theoretical computer science, 52, 83-100, (2002), Elsevier · Zbl 1260.68276
[29] Sangiorgi, D., The name discipline of uniform receptiveness, Theoretical computer science, 221, 1-2, 457-493, (1999) · Zbl 0930.68035
[30] Sangiorgi, D.; Walker, D., The π-calculus: A theory of mobile processes, (2001), Cambridge University Press · Zbl 0981.68116
[31] V. Saraswat and P. Lincoln. Higher-order linear concurrent constraint programming. Technical report, Xerox PARC, 1992
[32] Saraswat, V., Concurrent constraint programming, (1993), The MIT Press · Zbl 1002.68026
[33] Vigliotti, M.; Phillips, I.; Palamidessi, C., Separation results via leader election problems, (), 172-194 · Zbl 1196.68161
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.