Abstract
We present a logic that can express properties of freshness, secrecy, structure, and behavior of concurrent systems. In addition to standard logical and temporal operators, our logic includes spatial operations corresponding to composition, local name restriction, and a primitive freshname quantifier. Properties can also be defined by recursion; a central theme of this paper is then the combination of a logical notion of freshness with inductive and coinductive definitions of properties.
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
G. Boudol. Asynchrony and the π-calculus (note). Rapport de Recherche 1702, INRIA Sofia-Antipolis, May 1992.
L. Caires. A Model for Declarative Programming and Specification with Concurrency and Mobility. PhD thesis, Departamento de Informática, Faculdade de Ciências e Tecnologia, Universidade Nova de Lisboa, 1999.
L. Caires and L. Monteiro. Verifiable and Executable Specifications of Concurrent Objects in L π. In C. Hankin, editor, Programming Languages and Systems: Proceedings of the 7th European Symposium on Programming (ESOP 1998), number 1381 in Lecture Notes in Computer Science, pages 42–56. Springer-Verlag, 1998.
L. Cardelli and G. Ghelli. A Query Language Based on the Ambient Logic. In David Sands, editor, Programming Languages and Systems: Proceedings of the 10th European Symposium on Programming (ESOP 2001), volume 2028 of Lecture Notes in Computer Science, pages 1–22. Springer-Verlag, 2001.
L. Cardelli and A. D. Gordon. Anytime, Anywhere. Modal Logics for Mobile Ambients. In 27th ACM Symposium on Principles of Programming Languages, pages 365–377. ACM, 2000.
L. Cardelli and A. D. Gordon. Logical Properties of Name Restriction. In S. Abramsky, editor, Typed Lambda Calculi and Applications, number 2044 in Lecture Notes in Computer Science. Springer-Verlag, 2001.
W. Charatonik and J.-M. Talbot. The decidability of model checking mobile ambients. In Proceedings of the 15th Annual Conference of the European Association for Computer Science Logic, Lecture Notes in Computer Science. Springer-Verlag, 2001. To appear.
S. Dal-Zilio. Spatial Congruence for Ambients is Decidable. In Proceedings of ASIAN’00-6th Asian Computing Science Conference, number 1961 in Lecture Notes in Computer Science, pages 365–377. Springer-Verlag, 2000.
M. Dam. Relevance Logic and Concurrent Composition. In Proceedings, Third Annual Symposium on Logic in Computer Science, pages 178–185, Edinburgh, Scotland, 5-8 July 1988. IEEE Computer Society.
J. Engelfriet and Tj. Gelsema. A Multiset Semantics for the π-calculus withReplication. Theoretical Computer Science, (152):311–337, 1999.
M. J. Gabbay and A. M. Pitts. A New Approachto Abstract Syntax Involving Binders. In 14th Annual Symposium on Logic in Computer Science, pages 214–224. IEEE Computer Society Press, Washington, 1999.
P. Gardner. From Process Calculi to Process Frameworks. In Catuscia Palamidessi, editor, CONCUR 2000: Concurrency Theory (11th International Conference, University Park, PA, USA), volume 1877 of Lecture Notes in Computer Science, pages 69–88. Springer, August 2000.
M. Hennessy and R. Milner. Algebraic laws for Nondeterminism and Concurrency. JACM, 32(1):137–161, 1985.
K. Honda and M. Tokoro. On Asynchronous Communication Semantics. In M. Tokoro, O. Nierstrasz, and P. Wegner, editors, Object-Based Concurrent Computing 1991, number 612 in Lecture Notes in Computer Science, pages 21–51. Springer-Verlag, 1992.
D. Kozen. Results on the Propositional μ-Calculus. TCS, 27(3):333–354, 1983.
R. Milner. Communicating and Mobile Systems: the π-calculus. Cambridge University Press, 1999.
D. Sangiorgi. Extensionality and Intensionality of the Ambient Logics. In 28th Annual Symposium on Principles of Programming Languages, pages 4–13. ACM, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Caires, L., Cardelli, L. (2001). A Spatial Logic for Concurrency (Part I). In: Kobayashi, N., Pierce, B.C. (eds) Theoretical Aspects of Computer Software. TACS 2001. Lecture Notes in Computer Science, vol 2215. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45500-0_1
Download citation
DOI: https://doi.org/10.1007/3-540-45500-0_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42736-0
Online ISBN: 978-3-540-45500-4
eBook Packages: Springer Book Archive