Abstract
In addition to behavioral properties, spatial logics can talk about other key properties of concurrent systems such as secrecy, freshness, usage of resources, and distribution. We study an expressive spatial logic for systems specified in the synchronous π-calculus with recursion, based on a small set of behavioral and spatial observations. We give coinductive and equational characterizations of the equivalence induced on processes by the logic, and conclude that it strictly lies between structural congruence and strong bisimulation. We then show that model-checking is decidable for a useful class of processes that includes the finite-control fragment of the π-calculus.
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.
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Amadio, R., Cardelli, L.: Subtyping recursive types. ACM Transactions on Programming Languages and Systems 15(4), 575–631 (1993)
Caires, L.: A Model for Declarative Programming and Specification with Concurrency and Mobility. PhD thesis, Dept. de Informática, FCT, Universidade Nova de Lisboa (1999)
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, p. 209. Springer, Heidelberg (2002)
Caires, L., Cardelli, L.: A Spatial Logic for Concurrency (Part I). Information and Computation 186(2), 194–235 (2003)
Cardelli, L., Gardner, P., Ghelli, G.: Manipulating trees with hidden labels. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 216–232. Springer, Heidelberg (2003)
Cardelli, L., Gordon, A.D.: Anytime, Anywhere. Modal Logics for Mobile Ambients. In: 27th ACM Symp. on Principles of Programming Languages, pp. 365–377. ACM, New York (2000)
Cardelli, L., Gordon, A.D.: Logical properties of name restriction. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, p. 46. Springer, Heidelberg (2001)
Charatonik, W., Gordon, A.D., Talbot, J.-M.: Finite-control mobile ambients. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 295–313. Springer, Heidelberg (2002)
Charatonik, W., Talbot, J.-M.: The decidability of model-checking mobile ambients. In: Metayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, Springer, Heidelberg (2002)
Dal-Zilio, S.: Spatial congruence for ambients is decidable. In: He, J., Sato, M. (eds.) ASIAN 2000. LNCS, vol. 1961, pp. 365–377. Springer, Heidelberg (2000)
Dam, M.: Model checking mobile processes. Information and Computation 129(1), 35–51 (1996)
Dam, M.: Proof systems for π-calculus logics. In: de Queiroz (ed.) Logic for Concurrency and Synchronisation, Studies in Logic and Computation, Oxford University Press, Oxford (to appear)
Engelfriet, J., Gelsema, T.: Multisets and Structural Congruence of the π- calculus with Replication. Theoretical Computer Science (211), 311–337 (1999)
Gabbay, M., Pitts, A.: A New Approach to Abstract Syntax with Variable Binding. Formal Aspects of Computing 13(3-5), 341–363 (2002)
Ghelli, G., Conforti, G.: Decidability of freshness, undecidability of revelation. Technical Report 03–11, Dipartimento di Informatica, Universita di Pisa (2003)
Hirschkoff, D., Lozes, E., Sangiorgi, D.: Separability, Expressiveness and Decidability in the Ambient Logic. In: Proc. LICS, Copenhagen, Denmark, IEEE Computer Society, Los Alamitos (2002)
Hirschkoff, D., Lozes, É., Sangiorgi, D.: Minimality results for the spatial logics. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 252–264. Springer, Heidelberg (2003)
Ishtiaq, S., O’Hearn, P.: BI as an Assertion Language for Mutable Data Structures. In: 28th ACM Symp. on Principles of Programming Languages (2001)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Milner, R.: Communicating and Mobile Systems: the π-calculus. CUP (1999)
Milner, R., Parrow, J., Walker, D.: Modal logics for mobile processes. Theoretical Computer Science 114, 149–171 (1993)
Montanari, U., Pistore, M.: Pi-Calculus, Structured Coalgebras, and Minimal HD-Automata. In: MFCS: Symp. on Mathematical Foundations of Computer Science, pp. 569–578 (2000)
O’Hearn, P., Pym, D.: The Logic of Bunched Implications. The Bulletin of Symbolic Logic 5(2), 215–243 (1999)
Sangiorgi, D.: Extensionality and Intensionality of the Ambient Logics. In: 28th Annual Symposium on Principles of Programming Languages, pp. 4–13. ACM, New York (2001)
Sangiorgi, D., Walker, D.: The π-calculus: A Theory of Mobile Processes. CUP (2001)
Winskel, G.: A note on model checking the modal ν-calculus. In: Ausiello, G., Dezani-Ciancaglini, M., Rocca, S.R.D. (eds.) ICALP 1989. LNCS, vol. 372, pp. 761–772. Springer, Heidelberg (1989)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Caires, L. (2004). Behavioral and Spatial Observations in a Logic for the π-Calculus. In: Walukiewicz, I. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2004. Lecture Notes in Computer Science, vol 2987. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24727-2_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-24727-2_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21298-0
Online ISBN: 978-3-540-24727-2
eBook Packages: Springer Book Archive