Advertisement

A Stable Non-interleaving Early Operational Semantics for the Pi-Calculus

  • Thomas Troels Hildebrandt
  • Christian JohansenEmail author
  • Håkon Normann
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10168)

Abstract

We give the first non-interleaving early operational semantics for the pi-calculus which generalizes the standard interleaving semantics and unfolds to the stable model of prime event structures. Our starting point is the non-interleaving semantics given for CCS by Mukund and Nielsen, where the so-called structural (prefixing or subject) causality and events are defined from a notion of locations derived from the syntactic structure of the process terms. The semantics is conservatively extended with a notion of extruder histories, from which we infer the so-called link (name or object) causality and events introduced by the dynamic communication topology of the pi-calculus. We prove that the semantics generalises both the standard interleaving early semantics for the pi-calculus and the non-interleaving semantics for CCS. In particular, it gives rise to a labelled asynchronous transition system unfolding to prime event structures.

Keywords

Concurrency Non-interleaving Pi-calculus Early operational semantics Asynchronous transition systems Stability 

References

  1. 1.
    Bednarczyk, M.A.: Categories of asynchronous systems. Ph.D. thesis, University of Sussex (1988)Google Scholar
  2. 2.
    Bengtson, J., Johansson, M., Parrow, J., Victor, B.: Psi-calculi: a framework for mobile processes with nominal data and logic. Log. Methods Comput. Sci. 7(1), 1–44 (2011). http://dx.doi.org/10.2168/LMCS-7(1:11)2011 MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Best, E., Devillers, R., Kiehn, A., Pomello, L.: Concurrent bisimulations in petri nets. Acta Inform. 3(28), 231–264 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Boreale, M., Sangiorgi, D.: A fully abstract semantics for causality in the \(\pi \)-calculus. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 243–254. Springer, Heidelberg (1995). doi: 10.1007/3-540-59042-0_77 CrossRefGoogle Scholar
  5. 5.
    Boudol, G., Castellani, I., Hennessy, M., Kiehn, A.: A theory of processes with localities. Formal Asp. Comput. 6(2), 165–200 (1994)CrossRefzbMATHGoogle Scholar
  6. 6.
    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). doi: 10.1007/3-540-60218-6_11 CrossRefGoogle Scholar
  7. 7.
    Castellani, I.: Process algebras with localities. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 945–1045. Elsevier, Amsterdam (2001). Chap. 15CrossRefGoogle Scholar
  8. 8.
    Cattani, G.L., Sewell, P.: Models for name-passing processes: interleaving and causal. In: LICS, pp. 322–333. IEEE Computer Society (2000). http://dx.doi.org/10.1109/LICS.2000.855781
  9. 9.
    Clarke, E., Grumberg, O., Minea, M., Peled, D.: State space reduction using partial order techniques. Int. J. Softw. Tools Technol. Transf. 2(3), 279–287 (1999). http://dx.doi.org/10.1007/s100090050035 CrossRefzbMATHGoogle Scholar
  10. 10.
    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). doi: 10.1007/978-3-642-28729-9_15 CrossRefGoogle Scholar
  11. 11.
    Cristescu, I.: Operational and denotational semantics for the reversible \(\pi \)- calculus. Ph.D. thesis, Université Paris Diderot - Paris 7 - Sorbonne Paris Cité (2015). http://www.pps.univ-paris-diderot.fr/~ioana/these.pdf
  12. 12.
    Cristescu, I., Krivine, J., Varacca, D.: A compositional semantics for the reversible pi-calculus. In: ACM/IEEE Symposium on Logic in Computer Science, LICS. pp. 388–397. IEEE Computer Society (2013). http://dx.doi.org/10.1109/LICS.2013.45
  13. 13.
    Degano, P., Nicola, R., Montanari, U.: Partial orderings descriptions and observations of nondeterministic concurrent processes. In: Bakker, J.W., Roever, W.-P., Rozenberg, G. (eds.) REX 1988. LNCS, vol. 354, pp. 438–466. Springer, Heidelberg (1989). doi: 10.1007/BFb0013030 CrossRefGoogle Scholar
  14. 14.
    van Glabbeek, R., Goltz, U.: Refinement of actions and equivalence notions for concurrent systems. Acta Inform. 37(4/5), 229–327 (2001). http://link.springer.de/link/service/journals/00236/bibs/1037004/10370229.htm MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Hildebrandt, T.T.: Categorical models for concurrency: independence, fairness and dataflow. Ph.D. thesis, University of Aarhus, Denmark (1999)Google Scholar
  16. 16.
    Jategaonkar Jagadeesan, L., Jagadeesan, R.: Causality and true concurrency: a data-flow analysis of the pi-calculus. In: Alagar, V.S., Nivat, M. (eds.) AMAST 1995. LNCS, vol. 936, pp. 277–291. Springer, Heidelberg (1995). doi: 10.1007/3-540-60043-4_59 CrossRefGoogle Scholar
  17. 17.
    Lanese, I., Mezzina, C.A., Stefani, J.B.: Reversibility in the higher-order pi-calculus. Theoret. Comput. Sci. 625, 25–84 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Milner, R.: A Calculus of Communicating Systems, vol. 92. Springer, Berlin (1980)zbMATHGoogle Scholar
  19. 19.
    Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, I-II. Inf. Comput. 100(1), 1–77 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Montanari, U., Pistore, M.: Concurrent semantics for the pi-calculus. Electron. Notes Theoret. Comput. Sci. 1, 411–429 (1995). http://dx.doi.org/10.1016/S1571-0661(04)00024–6 MathSciNetCrossRefGoogle Scholar
  21. 21.
    Mukund, M., Nielsen, M.: CCS, locations and asynchronous transition systems. In: Shyamasundar, R. (ed.) FSTTCS 1992. LNCS, vol. 652, pp. 328–341. Springer, Heidelberg (1992). doi: 10.1007/3-540-56287-7_116 CrossRefGoogle Scholar
  22. 22.
    Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains. In: Kahn, G. (ed.) Semantics of Concurrent Computation. LNCS, vol. 70, pp. 266–284. Springer, Heidelberg (1979). doi: 10.1007/BFb0022474 CrossRefGoogle Scholar
  23. 23.
    Normann, H., Johansen, C., Hildebrandt, T.: Non-interleaving operational semantics for the pi-calculus (long version). Technical report 453, Department of Informatics, University of Oslo (2016). http://heim.ifi.uio.no/~cristi/papers/TR453.pdf
  24. 24.
    Rabinovich, A., Trakhtenbrot, B.: Behaviour structures and nets. Fundamenta Informaticae 4(XI), 357–404 (1988)zbMATHGoogle Scholar
  25. 25.
    Sangiorgi, D.: Locality and interleaving semantics in calculi for mobile processes. Theoret. Comput. Sci. 155(1), 39–83 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Sangiorgi, D., Walker, D.: The \(\pi \)-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)zbMATHGoogle Scholar
  27. 27.
    Shields, M.W.: Concurrent machines. Comput. J. 28(5), 449–465 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Ulidowski, I., Phillips, I., Yuen, S.: Concurrency and reversibility. In: Yamashita, S., Minato, S. (eds.) RC 2014. LNCS, vol. 8507, pp. 1–14. Springer, Heidelberg (2014). doi: 10.1007/978-3-319-08494-7_1 Google Scholar
  29. 29.
    Winskel, G., Nielsen, M.: Models for concurrency. In: Abramski, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, pp. 1–148. Oxford Universtiy Press, New York (1995)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Thomas Troels Hildebrandt
    • 1
  • Christian Johansen
    • 2
    Email author
  • Håkon Normann
    • 1
  1. 1.Department of Computer ScienceIT University of CopenhagenCopenhagenDenmark
  2. 2.Department of InformaticsUniversity of OsloOsloNorway

Personalised recommendations