Abstract
A spatial logic consists of four groups of operators: standard propositional connectives; spatial operators; a temporal modality; calculus-specific operators. The calculus-specific operators talk about the capabilities of the processes of the calculus, that is, the process constructors through which a process can interact with its environment. We prove some minimality results for spatial logics. The main results show that in the logics for π-calculus and asynchronous π-calculus the calculus-specific operators can be eliminated. The results are presented under both the strong and the weak interpretations of the temporal modality. Our proof techniques are applicable to other spatial logics, so to eliminate some of – if not all – the calculus-specific operators. As an example of this, we consider the logic for the Ambient calculus, with the strong semantics.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Busi, N., Zavattaro, G.: On the expressiveness of Movement in Pure Mobile Ambients. ENTCS 66(3) (2002)
Caires, L., Cardelli, L.: A Spatial Logic for Concurrency (Part I). In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, p. 1. Springer, Heidelberg (2001)
Caires, L., Cardelli, L.: A Spatial Logic for Concurrency (Part II). In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 209–225. Springer, Heidelberg (2002)
Cardelli, L., Gordon, A.: Mobile Ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998)
Cardelli, L., Gordon, A.: Anytime, Anywhere, Modal Logics for Mobile Ambients. In: Proc. of POPL 2000, pp. 365–377. ACM Press, New York (2000)
Cardelli, L., Gordon, A.: Logical Properties of Name Restriction. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, p. 46. Springer, Heidelberg (2001)
Hirschkoff, D., Lozes, E., Sangiorgi, D.: Separability, Expressiveness and Decidability in the Ambient Logic. In: 17th IEEE Symposium on Logic in Computer Science, pp. 423–432. IEEE Computer Society Press, Los Alamitos (2002)
Hirschkoff, D., Lozes, E., Sangiorgi, D.: Minimality Results for the Spatial Logics. Technical report, LIP – ENS Lyon (2003), in–preparation available from http://www.ens-lyon.fr/~elozes
Nestmann, U., Pierce, B.: Decoding choice encodings. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, Springer, Heidelberg (1996)
Pierce, B.C., Turner, D.N.: Pict: A programming language based on the picalculus. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language and Interaction: Essays in Honour of Robin Milner, MIT Press, Cambridge (2000)
Sangiorgi, D.: Extensionality and Intensionality of the Ambient Logic. In: Proc. of 28th POPL, pp. 4–17. ACM Press, New York (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hirschkoff, D., Lozes, É., Sangiorgi, D. (2003). Minimality Results for the Spatial Logics. In: Pandya, P.K., Radhakrishnan, J. (eds) FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2003. Lecture Notes in Computer Science, vol 2914. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24597-1_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-24597-1_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20680-4
Online ISBN: 978-3-540-24597-1
eBook Packages: Springer Book Archive