Paper announcement: A Spatial Logic for Concurrency (Part I)

["Luca Cardelli" <luca@xxxxxxxxxxxxx>]

(To appear in TACS'01)
A Spatial Logic for Concurrency (Part I)
Luís Caires and Luca Cardelli
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
fresh name 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.

Available from <http://www.luca.demon.co.uk/>, or directly:

.ps:
<http://research.microsoft.com/Users/luca/Papers/A%20Spatial%20Logic%20F
or%20Concurrency%20(Part%20I)%20TACS01.A4.ps>

.pdf:
<http://research.microsoft.com/Users/luca/Papers/A%20Spatial%20Logic%20F
or%20Concurrency%20(Part%20I)%20TACS01.A4.pdf>

  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html