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.
CITATION STYLE
Caires, L., & Cardelli, L. (2001). A spatial logic for concurrency (Part I). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2215). Springer Verlag. https://doi.org/10.1007/3-540-45500-0_1
Mendeley helps you to discover research relevant for your work.