A Spatial Logic for Concurrency (Part I)
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.
Unable to display preview. Download preview PDF.
- 1.G. Boudol. Asynchrony and the π-calculus (note). Rapport de Recherche 1702, INRIA Sofia-Antipolis, May 1992.Google Scholar
- 2.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.Google Scholar
- 3.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.Google Scholar
- 4.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.Google Scholar
- 5.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.Google Scholar
- 7.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.Google Scholar
- 8.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.Google Scholar
- 9.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.Google Scholar
- 11.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.Google Scholar
- 12.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.Google Scholar
- 14.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.Google Scholar
- 16.R. Milner. Communicating and Mobile Systems: the π-calculus. Cambridge University Press, 1999.Google Scholar
- 17.D. Sangiorgi. Extensionality and Intensionality of the Ambient Logics. In 28th Annual Symposium on Principles of Programming Languages, pages 4–13. ACM, 2001.Google Scholar