A spatial logic for concurrency (part I)

Luís Caires; Luca Cardelli

doi:10.1016/S0890-5401(03)00137-8

A spatial logic for concurrency (part I)

Luís Caires, Luca Cardelli

DI - Departamento de Informática

Research output: Contribution to journal › Article › peer-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 language	English
Pages (from-to)	194-235
Number of pages	42
Journal	Information and Computation
Volume	186
Issue number	2
DOIs	https://doi.org/10.1016/S0890-5401(03)00137-8
Publication status	Published - 1 Nov 2003
Event	4th Symposium on Theoretical Aspects of Computer Software - Sendai, Japan Duration: 29 Oct 2001 → 31 Oct 2001

Keywords

Semantics
Models
Bigraphical reactive

Access to Document

10.1016/S0890-5401(03)00137-8Licence: CC BY-NC-ND

A spatial logic for concurrency (part I)Final published version, 400 KBLicence: CC BY-NC-ND

Cite this

@article{3a2b046312cf4cb4bf469b519048230e,

title = "A spatial logic for concurrency (part I)",

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.",

keywords = "Semantics, Models, Bigraphical reactive",

author = "Lu{\'i}s Caires and Luca Cardelli",

year = "2003",

month = nov,

day = "1",

doi = "10.1016/S0890-5401(03)00137-8",

language = "English",

volume = "186",

pages = "194--235",

journal = "Information and Computation",

issn = "0890-5401",

publisher = "ACADEMIC PRESS INC ELSEVIER SCIENCE",

number = "2",

note = "4th Symposium on Theoretical Aspects of Computer Software ; Conference date: 29-10-2001 Through 31-10-2001",

}

TY - JOUR

T1 - A spatial logic for concurrency (part I)

AU - Caires, Luís

AU - Cardelli, Luca

PY - 2003/11/1

Y1 - 2003/11/1

N2 - 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.

AB - 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.

KW - Semantics

KW - Models

KW - Bigraphical reactive

UR - http://www.scopus.com/inward/record.url?scp=0142121530&partnerID=8YFLogxK

U2 - 10.1016/S0890-5401(03)00137-8

DO - 10.1016/S0890-5401(03)00137-8

M3 - Article

AN - SCOPUS:0142121530

VL - 186

SP - 194

EP - 235

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

IS - 2

T2 - 4th Symposium on Theoretical Aspects of Computer Software

Y2 - 29 October 2001 through 31 October 2001

ER -

A spatial logic for concurrency (part I)

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this