Skip to main content

2015 | OriginalPaper | Buchkapitel

Rigid Families for CCS and the \(\pi \)-calculus

verfasst von : Ioana Domnina Cristescu, Jean Krivine, Daniele Varacca

Erschienen in: Theoretical Aspects of Computing - ICTAC 2015

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

This paper presents a novel causal semantics for concurrency, based on rigid families. Instead of having causality as primitive notion, in our model causality and concurrency are derived from precedence, a partial order local to each run of a process. We show that our causal semantics can interpret CCS and \(\pi \)-calculus terms. We propose some criteria to evaluate the correctness of a causal semantics of process calculi and we argue that none of the previous models for the \(\pi \)-calculus satisfy them all.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Fußnoten
1
We let the reader refer to appendix for details. We also show in appendix how one can compile an event structure from rigid families and vice versa. Importantly, the category of Definition 2 and the category of event structures are not equivalent.
 
Literatur
1.
Zurück zum Zitat Aubert, C., Cristescu, I.: Reversible barbed congruence on configuration structures. In: 8th ICE, Satellite Workshop of DisCoTec 2015 (2015) Aubert, C., Cristescu, I.: Reversible barbed congruence on configuration structures. In: 8th ICE, Satellite Workshop of DisCoTec 2015 (2015)
2.
Zurück zum Zitat Boreale, M., Sangiorgi, D.: A fully abstract semantics for causality in the \(\pi \)-calculus. Acta. Inf. 35(5), 353–400 (1998)MathSciNetCrossRefMATH Boreale, M., Sangiorgi, D.: A fully abstract semantics for causality in the \(\pi \)-calculus. Acta. Inf. 35(5), 353–400 (1998)MathSciNetCrossRefMATH
3.
Zurück zum Zitat Boudol, G., Castellani, I.: Flow models of distributed computations: Three equivalent semantics for CCS. Inf. Comput. 114(2), 247–314 (1994)MathSciNetCrossRefMATH Boudol, G., Castellani, I.: Flow models of distributed computations: Three equivalent semantics for CCS. Inf. Comput. 114(2), 247–314 (1994)MathSciNetCrossRefMATH
4.
Zurück zum Zitat Bruni, R., Melgratti, H., Montanari, U.: Event structure semantics for nominal calculi. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 295–309. Springer, Heidelberg (2006) CrossRef Bruni, R., Melgratti, H., Montanari, U.: Event structure semantics for nominal calculi. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 295–309. Springer, Heidelberg (2006) CrossRef
5.
Zurück zum Zitat Busi, N., Gorrieri, R.: A petri net semantics for \(\pi \)-calculus. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 145–159. Springer, Heidelberg (1995) Busi, N., Gorrieri, R.: A petri net semantics for \(\pi \)-calculus. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 145–159. Springer, Heidelberg (1995)
6.
Zurück zum Zitat Castellan, S., Hayman, J., Lasson, M., Winskel, G.: Strategies as concurrent processes. Electron. Notes. Theor. Comput. Sci. 308, 87–107 (2014). Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX)MathSciNetCrossRef Castellan, S., Hayman, J., Lasson, M., Winskel, G.: Strategies as concurrent processes. Electron. Notes. Theor. Comput. Sci. 308, 87–107 (2014). Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX)MathSciNetCrossRef
7.
9.
Zurück zum Zitat Crafa, S., Varacca, D., Yoshida, N.: Event structure semantics of parallel extrusion in the \(\pi \)-calculus. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 225–239. Springer, Heidelberg (2012) CrossRef Crafa, S., Varacca, D., Yoshida, N.: Event structure semantics of parallel extrusion in the \(\pi \)-calculus. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 225–239. Springer, Heidelberg (2012) CrossRef
10.
Zurück zum Zitat Cristescu, I., Krivine, J., Varacca, D.: A compositional semantics for the reversible \(\pi \)-calculus. In: LICS 2013, pp. 388–397. IEEE Computer Society (2013) Cristescu, I., Krivine, J., Varacca, D.: A compositional semantics for the reversible \(\pi \)-calculus. In: LICS 2013, pp. 388–397. IEEE Computer Society (2013)
11.
Zurück zum Zitat Danos, V., Krivine, J.: Reversible communicating systems. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 292–307. Springer, Heidelberg (2004) CrossRef Danos, V., Krivine, J.: Reversible communicating systems. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 292–307. Springer, Heidelberg (2004) CrossRef
12.
13.
Zurück zum Zitat Eberhart, C., Hirschowitz, T., Seiller, T.: An intensionally fully-abstract sheaf model for \(\pi \). In: CALCO (2015) Eberhart, C., Hirschowitz, T., Seiller, T.: An intensionally fully-abstract sheaf model for \(\pi \). In: CALCO (2015)
14.
Zurück zum Zitat van Glabbeek, R.J., Plotkin, G.D.: Configuration structures, event structures and petri nets. Theor. Comput. Sci. 410(41), 4111–4159 (2009)MathSciNetCrossRefMATH van Glabbeek, R.J., Plotkin, G.D.: Configuration structures, event structures and petri nets. Theor. Comput. Sci. 410(41), 4111–4159 (2009)MathSciNetCrossRefMATH
15.
Zurück zum Zitat Hayman, J., Winskel, G.: Event structure semantics for security protocols (2013). submitted for publication Hayman, J., Winskel, G.: Event structure semantics for security protocols (2013). submitted for publication
16.
Zurück zum Zitat Krivine, J.: A verification algorithm for declarative concurrent programming. Technical Report 0606095, INRIA-Rocquencourt (2006) Krivine, J.: A verification algorithm for declarative concurrent programming. Technical Report 0606095, INRIA-Rocquencourt (2006)
17.
Zurück zum Zitat Milner, R.: Communication and Concurrency. Prentice-Hall Inc, Upper Saddle River (1989)MATH Milner, R.: Communication and Concurrency. Prentice-Hall Inc, Upper Saddle River (1989)MATH
18.
Zurück zum Zitat Milner, R.: Communicating and Mobile Systems: The \(\pi \)-calculus. Cambridge University Press, Cambridge (1999)MATH Milner, R.: Communicating and Mobile Systems: The \(\pi \)-calculus. Cambridge University Press, Cambridge (1999)MATH
19.
Zurück zum Zitat Phillips, I., Ulidowski, I.: Reversibility and models for concurrency. Electron. Notes Theor. Comput. Sci. 192(1), 93–108 (2007)MathSciNetCrossRefMATH Phillips, I., Ulidowski, I.: Reversibility and models for concurrency. Electron. Notes Theor. Comput. Sci. 192(1), 93–108 (2007)MathSciNetCrossRefMATH
20.
Zurück zum Zitat Sangiorgi, D., Walker, D.: PI-Calculus: A Theory of Mobile Processes. Cambridge University Press, New York (2001) MATH Sangiorgi, D., Walker, D.: PI-Calculus: A Theory of Mobile Processes. Cambridge University Press, New York (2001) MATH
21.
Zurück zum Zitat Sassone, V., Nielsen, M., Winskel, G.: Models for concurrency: towards a classification. Theor. Comput. Sci. 170(1–2), 297–348 (1996)MathSciNetCrossRefMATH Sassone, V., Nielsen, M., Winskel, G.: Models for concurrency: towards a classification. Theor. Comput. Sci. 170(1–2), 297–348 (1996)MathSciNetCrossRefMATH
22.
Zurück zum Zitat Winskel, G.: Event structure semantics for CCS and related languages. In: Proceedings of the 9th Colloquium on Automata, Languages and Programming, pp. 561–576 (1982) Winskel, G.: Event structure semantics for CCS and related languages. In: Proceedings of the 9th Colloquium on Automata, Languages and Programming, pp. 561–576 (1982)
23.
Zurück zum Zitat Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) Petri Nets: Applications and Relationships to Other Models of Concurrency. LNCS, vol. 255, pp. 325–392. Springer, Heidelberg (1987) CrossRef Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) Petri Nets: Applications and Relationships to Other Models of Concurrency. LNCS, vol. 255, pp. 325–392. Springer, Heidelberg (1987) CrossRef
24.
Zurück zum Zitat Yoshida, N.: Minimality and separation results on asynchronous mobile processes. Theor. Comput. Sci. 274(1–2), 231–276 (2002). Ninth International Conference on Concurrency Theory 1998CrossRefMATH Yoshida, N.: Minimality and separation results on asynchronous mobile processes. Theor. Comput. Sci. 274(1–2), 231–276 (2002). Ninth International Conference on Concurrency Theory 1998CrossRefMATH
Metadaten
Titel
Rigid Families for CCS and the -calculus
verfasst von
Ioana Domnina Cristescu
Jean Krivine
Daniele Varacca
Copyright-Jahr
2015
DOI
https://doi.org/10.1007/978-3-319-25150-9_14

Premium Partner