The truth of a spatial formula depends on its location
Spatial logics are specification logics for describing the behavior and spatial structure of concurrent systems. Logics for concurrent systems are certainly not new, but the intent to describe spatial properties, and in particular the spatial structure of distributed and mobile systems, seems to have arisen only recently. The spatial properties we consider are essentially of two kinds: whether a system is composed of two or more identifiable subsytems, possibly including hierarchies of named locations, and whether a system restricts the use of certain resources to certain subsytems. The latter, in particular, concerns specifying systems that deal with fresh or secret resources such as keys, nonces, channels, or locations.
A logic for studying distributed processes requires both spatial and temporal modalities. By removing the temporal modalities we obtain "pure" spatial logics. These describe simple arrangements such as trees and graphs that are static in time, but using a very rich vocabulary. Pure spatial logics have been found useful in the study of semistructured data and related query languages.
For Process Calculi
A Spatial Logic for Concurrency (Part II) (TCS) - A Spatial Logic for Concurrency (Part I) (I&C)
-
A Specification
Logic for Mobility.
Luis Caires. (DI/FCT/UNL Technical Report 4/2000) - Verifiable and
Executable Logic Specifications of Concurrent Objects in Lpi. Luis Caires and Luis Monteiro.
(ETAPS/ESOP98)
For Ambient Calculus
- Anytime, Anywhere (POPL'00)
- Logical Properties of Name Restriction (TLCA'01)
- Ambient Logic (MSCS)
For Trees
- Manipulating Trees with Hidden Labels (PlotkinVolume'06)
- Deciding Validity in a Spatial Logic for Trees (JFP)
- Describing Semistructured Data (SIGMOD Record)
- A Query Language Based on the Ambient Logic (MSCS)
For Graphs
A Spatial Logic for Querying Graphs (ICALP'02) Closely Related Work
