Advertisement

A Spatial Logic for Concurrency (Part I)

  • Luís Caires
  • Luca Cardelli
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2215)

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    G. Boudol. Asynchrony and the π-calculus (note). Rapport de Recherche 1702, INRIA Sofia-Antipolis, May 1992.Google Scholar
  2. 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. 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. 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. 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
  6. 6.
    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.CrossRefGoogle Scholar
  7. 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. 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. 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
  10. 10.
    J. Engelfriet and Tj. Gelsema. A Multiset Semantics for the π-calculus withReplication. Theoretical Computer Science, (152):311–337, 1999.CrossRefMathSciNetGoogle Scholar
  11. 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. 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
  13. 13.
    M. Hennessy and R. Milner. Algebraic laws for Nondeterminism and Concurrency. JACM, 32(1):137–161, 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  14. 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
  15. 15.
    D. Kozen. Results on the Propositional μ-Calculus. TCS, 27(3):333–354, 1983.zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    R. Milner. Communicating and Mobile Systems: the π-calculus. Cambridge University Press, 1999.Google Scholar
  17. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Luís Caires
    • 1
  • Luca Cardelli
    • 2
  1. 1.Departamento de Informática FCT/UNLLisboaPortugal
  2. 2.Microsoft ResearchCambridgeUK

Personalised recommendations