Abstract
We study the behavioural theory of π P, a π-calculus in the tradition of Fusions and Chi calculi. In contrast with such calculi, reduction in π P generates a preorder on names rather than an equivalence relation. We present two characterisations of barbed congruence in π P: the first is based on a compositional LTS, and the second is an axiomatisation. The results in this paper bring out basic properties of π P, mostly related to the interplay between the restriction operator and the preorder on names.
Consequently, π P is a calculus in the tradition of Fusion calculi, in which both types and behavioural equivalences can be exploited in order to reason rigorously about concurrent and mobile systems.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proc. of POPL, pp. 104–115. ACM (2001)
Bengtson, J., Johansson, M., Parrow, J., Victor, B.: Psi-calculi: Mobile processes, nominal data, and logic. In: LICS, pp. 39–48. IEEE (2009)
Boreale, M., Buscemi, M.G., Montanari, U.: D-fusion: A distinctive fusion calculus. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 296–310. Springer, Heidelberg (2004)
Boreale, M., Buscemi, M.G., Montanari, U.: A general name binding mechanism. In: De Nicola, R., Sangiorgi, D. (eds.) TGC 2005. LNCS, vol. 3705, pp. 61–74. Springer, Heidelberg (2005)
Carpineti, S., Laneve, C., Padovani, L.: PiDuce - A project for experimenting Web services technologies. Sci. Comput. Program. 74(10), 777–811 (2009)
Deng, Y., Sangiorgi, D.: Towards an algebraic theory of typed mobile processes. Theor. Comput. Sci. 350(2-3), 188–212 (2006)
Ehrhard, T., Laurent, O.: Acyclic solos and differential interaction nets. Logical Methods in Computer Science 6(3) (2010)
Fu, Y.: The χ-calculus. In: APDC, pp. 74–81. IEEE Computer Society (1997)
Gardner, P., Laneve, C., Wischik, L.: The fusion machine (Extended abstract). In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 418–433. Springer, Heidelberg (2002)
Hirschkoff, D., Madiot, J.-M., Sangiorgi, D.: Name-passing calculi: From fusions to preorders and types. In: LICS, pp. 378–387. IEEE Computer Society (2013)
Hirschkoff, D., Madiot, J.-M., Xu, X.: Long version of this paper, http://madiot.org
Honda, K., Yoshida, N.: On reduction-based process semantics. Theor. Comp. Sci. 152(2), 437–486 (1995)
Laneve, C., Victor, B.: Solos in concert. Mathematical Structures in Computer Science 13(5), 657–683 (2003)
Liu, J., Lin, H.: Proof system for applied pi calculus. In: IFIP TCS. IFIP AICT, vol. 323, pp. 229–243. Springer, Heidelberg (2010)
Parrow, J., Sangiorgi, D.: Algebraic theories for name-passing calculi. Inf. Comput. 120(2), 174–197 (1995)
Parrow, J., Victor, B.: The fusion calculus: expressiveness and symmetry in mobile processes. In: LICS, pp. 176–185. IEEE (1998)
Pierce, B.C., Sangiorgi, D.: Typing and subtyping for mobile processes. Mathematical Structures in Computer Science 6(5), 409–453 (1996)
Sangiorgi, D., Walker, D.: The Pi-Calculus: a theory of mobile processes. Cambridge University Press (2001)
Victor, B., Parrow, J.: Concurrent constraints in the fusion calculus. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 455–469. Springer, Heidelberg (1998)
Wischik, L., Gardner, P.: Strong bisimulation for the explicit fusion calculus. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 484–498. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 IFIP International Federation for Information Processing
About this paper
Cite this paper
Hirschkoff, D., Madiot, JM., Xu, X. (2015). A Behavioural Theory for a π-calculus with Preorders. In: Dastani, M., Sirjani, M. (eds) Fundamentals of Software Engineering. FSEN 2015. Lecture Notes in Computer Science(), vol 9392. Springer, Cham. https://doi.org/10.1007/978-3-319-24644-4_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-24644-4_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24643-7
Online ISBN: 978-3-319-24644-4
eBook Packages: Computer ScienceComputer Science (R0)