A spatial logic for concurrency (part I)

Luís Caires, Luca Cardelli

Research output: Contribution to journalArticlepeer-review

131 Citations (Scopus)
10 Downloads (Pure)

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 fresh name quantifier. Properties can also be defined by recursion; a central aim of this paper is then the combination of a logical notion of freshness with inductive and coinductive definitions of properties.

Original languageEnglish
Pages (from-to)194-235
Number of pages42
JournalInformation and Computation
Volume186
Issue number2
DOIs
Publication statusPublished - 1 Nov 2003
Event4th Symposium on Theoretical Aspects of Computer Software - Sendai, Japan
Duration: 29 Oct 200131 Oct 2001

Keywords

  • Semantics
  • Models
  • Bigraphical reactive

Fingerprint

Dive into the research topics of 'A spatial logic for concurrency (part I)'. Together they form a unique fingerprint.

Cite this