A short bibliography on Spatial Logics for Concurrency

Suggestions, corrections, and additions are very welcome. Electronic version of the papers can, in general, be found in the respective author's web site.

[L04] Expressivité des logiques d'espaces

Étienne Lozes.
PhD Thesis (in French).

Gives a complete survey on the expressiveness of spatial logics, namely what properties can be specified, up to what point can the logic distinguish between elements of the model, what are the minimal operations in the logic that provide this expressiveness and what is the complexity of the associated algorithms.

[TV04] An Observational Model for Spatial Logics

Emilio Tuosto and Hugo Torres Vieira.
To appear in VODCA'2004 Proceedings.

Characterizes the semantics of a spatial logic through a labelled transition system.

[H04] An Extensional Spatial Logic for Mobile Processes

Daniel Hirschkoff.
Appears in CONCUR'2004 Proceedings, #3170 of Lecture Notes in Computer Science, Springer-Verlag, 2004.

[CL04] Elimination of Quantifiers and Decidability in Spatial Logics for Concurrency

Luís Caires and Étienne Lozes.
Appears in CONCUR'2004 Proceedings, #3170 of Lecture Notes in Computer Science, Springer-Verlag, 2004. (ps)
and
To appear in Theoretical Computer Science. (ps)

Shows that spatial logics for concurrency with contextual observations based on the composition adjunct are essentially undecidable, both with relation to model-checking and validity, even in the absence of first-order quantifiers.

[C04] Behavioral and Spatial Observations in a Logic for the Pi-Calculus

Luís Caires.
Appears in ETAPS/FOSSACS'2004 Proceedings, #2987 of Lecture Notes in Computer Science, Springer-Verlag, 2004. (ps)

Studies a spatial logic with behavioral and spatial operators. Characterizes logical equivalence on processes, and shows that model-checking is decidable.

[CG04] Decidability of Freshness, Undecidability of Revelation

Giovanni Conforti and Giorgio Ghelli.
Appears in ETAPS/FOSSACS'2004 Proceedings, #2987 of Lecture Notes in Computer Science, Springer-Verlag, 2004.

[CGC03] Deciding validity in a spatial logic for trees

Cristiano Calcagno, Luca Cardelli and Andrew D. Gordon.
Proceedings of the ACM Workshop on Types in Language Design and Implementation, pp 62-73. ACM, 2003.

Shows that the validity and model-checking problems for the static ambient logic is decidable.

[HLS03] Minimality results for the spatial logics

Daniel Hirschkoff, Étienne Lozes and Davide Sangiorgi.
Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science, pp 252-264.
#2914 of Lecture Notes in Computer Science, Springer-Verlag, 2003.

Studies minimality of spatial logics, and shows that behavioral modalities can be encoded into spatial logics for the pi-calculus that include adjunct and revelation operators.

[L04] Adjunct Elimination in the Static Ambient Logic

Étienne Lozes.
Proceedings of the 10th International Workshop on Expressiveness in Concurrency, pp 51-72.
#96 of Electronic Notes in Theoretical Computer Science, Elsevier, 2004.

Shows that adjuncts do not add to the expressive power of static spatial logics.

[CC02,04] A Spatial Logic for Concurrency (Part II)

Luís Caires and Luca Cardelli.
Appears in CONCUR'2002 Proceedings, #2421 of Lecture Notes in Computer Science, Springer-Verlag, 2002. (ps)
and
Appears in Theoretical Computer Science, 322(3), 2004. (ps)

Defines a proof theory for spatial logic of [CC01] based on a sequent calculus, that enjoys the cut-elimination property. The logic is extended with explicit permutations.

[HLS02] Separability, expressiveness, and decidability in the Ambient Logic

Daniel Hirschkoff, Étienne Lozes and Davide Sangiorgi.
Proceedings of the 17th IEEE Symposium on Logic in Computer Science, pp 423-432. IEEE Computer Society Press, 2002.

Studies expressiveness and separation results for the ambient logic.

[CC01,03] A Spatial Logic for Concurrency (Part I)

Luís Caires and Luca Cardelli.
Appears in TACS 2001 Proceedings, Lecture Notes in Computer Science, Springer-Verlag, 2001. (ps.gz)
and
Appears in Journal of Information and Computation, 186(2), 2003. (ps.gz)

Introduces a mature semantic model for a spatial logic for concurrent systems modeled in the pi-calculus, presenting freshness and hidden name quantifiers and recursion as properly defined logical primitives.

[CG01] Logical Properties of Name Restriction

Luca Cardelli and Andrew D. Gordon.
Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications, pp 46-60.
#2044 of Lecture Notes in Computer Science, Springer-Verlag, 2001.

Adds to the ambient logic of [CG00] two operators to deal with restricted names, the revelation operator and the freshness quantifier, which is defined here as a metalevel abbreviation. Shows that the hidden name quantifier can be analyzed by decomposition into these two operations, and derives many fundamental properties of these conectives.

[CT01] The Decidability of Model Checking Mobile Ambients

Witold Charatonik and Jean-Marc Talbot.
Proceedings of the 15th Annual Conference of the European Association for Computer Science Logic, pp 339-354.
#2142 of Lecture Notes in Computer Science, Springer-Verlag, 2001.

Shows that model-checking and validity checking of spatial logics with quantifiers over names is undecidable.

[S01] Extensionality and Intensionality of the Ambient Logics

Davide Sangiorgi.
Proceedings of the 28th ACM Annual Symposium on Principles of Programming Languages, pp 4-13. ACM, 2001.

Studies the logical equivalence induced on the ambient calculus without restricted names by the ambient logic, and concludes that it coincides with structural congruence.

[CG00] Anytime, Anywhere. Modal Logics for Mobile Ambients

Luca Cardelli and Andrew D. Gordon.
Proceedings of the 27th ACM Annual Symposium on Principles of Programming Languages, pp 365-377. ACM, 2000.

Introduces the ambient logic, a spatial logic for the ambient calculus with public names, and shows the derivation of several interesting properties. The ambient logic includes adjuncts, powerful operators that allow the expression of security properties. Shows that model-checking of spatial logics without adjunct is decidable.

[C99] A Model for Declarative Programming and Specification with Concurrency and Mobility

Luís Caires.
PhD Thesis. (ps.gz)

Includes (Chap 5) a generalization of the spatial logic in [CM98] with definitions by recursion, and interpreted in an action-calculus based compositional semantics. Presents a sound proof system, and several examples of derivable properties.

[GP99] A New Approach to Abstract Syntax Involving Binders

Murdoch Gabbay and Andrew M. Pitts.
Proceedings of the 14th IEEE Annual Symposium on Logic in Computer Science, pp 214-224. IEEE Computer Society Press, 1999.

Introduces the freshness quantifier, which was used in [CG01], and then also in [CC01] to give a semantics to freshness and hidden name quantification in spatial logics.

[CM98] Verifiable and Executable Logic Specifications of Concurrent Objects in Lpi

Luís Caires and Luís Monteiro.
Appears in the ETAPS/ESOP98 proceedings. #1381 of Lecture Notes in Computer Science, Springer-Verlag, 1998. (ps.gz)

Introduces a logic for a nominal process calculus that includes void, composition, and the hidden name quantifier as primitive spatial connectives. This logic is then used to encode a specification language for concurrent objects, supporting some form of local reasoning.