Abstract
Spatial logics have been proposed to reason locally and modularly on algebraic models of distributed systems. In this paper we define the spatial equational logic AπL whose models are processes of the applied π-calculus. This extension of the π-calculus allows term manipulation and records communications as active substitutions in a frame, thus augmenting the underlying predefined equational theory. Our logic allows one to reason locally either on frames or on processes, thanks to static and dynamic spatial operators. We study the logical equivalences induced by various relevant fragments of AπL, and show in particular that the whole logic induces a coarser equivalence than structural congruence. We give characteristic formulae for some of these equivalences and for static equivalence. Going further into the exploration of AπL’s expressivity, we also show that it can eliminate standard term quantification.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 55–74 (2002)
Ishtiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL 2001, pp. 14–26 (2001)
Gordon, A., Cardelli, L.: Anytime, anywhere: Modal logics for mobile ambients. In: Press, A. (ed.) POPL 2000, pp. 365–377 (2000)
Caires, L., Cardelli, L.: A spatial logic for concurrency (part I). Journal of Information and Computation 186(2) (2003)
Hirschkoff, D., Lozes, É., Sangiorgi, D.: Minimality results for spatial logics. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 252–264. Springer, Heidelberg (2003)
Hirschkoff, D., Lozes, É., Sangiorgi, D.: On the expressiveness of the ambient logic. Logical Methods in Computer Science 2(2) (March 2006)
Hirschkoff, D.: An extensional spatial logic for mobile processes. In: Jin, H., Pan, Y., Xiao, N., Sun, J. (eds.) CONCUR 2002. LNCS, vol. 3252. Springer, Heidelberg (2004)
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL 2001, pp. 104–115 (2001)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, i. Inf. Comput. 100(1), 1–40 (1992)
Dawar, A., Gardner, P., Ghelli, G.: Expressiveness and complexity of graph logic. Inf. Comput. 205(3), 263–310 (2007)
Calcagno, C., Gardner, P., Hague, M.: From separation logic to first-order logic. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 395–409. Springer, Heidelberg (2005)
Kuncak, V., Rinard, M.: On spatial conjunction as second-order logic. Technical report, MIT CSAIL (October 2004)
Hüttel, H., Pedersen, M.D.: A logical characterisation of static equivalence. Electron. Notes Theor. Comput. Sci. 173, 139–157 (2007)
Sangiorgi, D.: Extensionality and intensionality of the ambient logics. In: POPL (2001)
Caires, L., Lozes, É.: Elimination of quantifiers and undecidability in spatial logics for concurrency. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 240–257. Springer, Heidelberg (2004)
Villard, J., Lozes, É., Treinen, R.: A spatial equational logic for the applied pi-calculus. Research Report LSV-08-10, LSV, ENS Cachan, France, 44 pages (March 2008)
Pym, D., Tofts, C.: A Calculus and logic of resources and processes. Formal Aspects of Computing 18(4), 495–517 (2006)
Mardare, R.: Observing distributed computation. a dynamic-epistemic approach. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol. 4624, pp. 379–393. Springer, Heidelberg (2007)
Kramer, S.: Logical Concepts in Cryptography. PhD thesis, École Polytechnique Fédérale de Lausanne (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lozes, É., Villard, J. (2008). A Spatial Equational Logic for the Applied π-Calculus. In: van Breugel, F., Chechik, M. (eds) CONCUR 2008 - Concurrency Theory. CONCUR 2008. Lecture Notes in Computer Science, vol 5201. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85361-9_31
Download citation
DOI: https://doi.org/10.1007/978-3-540-85361-9_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85360-2
Online ISBN: 978-3-540-85361-9
eBook Packages: Computer ScienceComputer Science (R0)