A spatial logic for concurrency - II

Luís Caires, Luca Cardelli

Research output: Contribution to journalConference article

46 Citations (Scopus)
13 Downloads (Pure)

Abstract

We present a modal logic for describing the spatial organization and the behavior of distributed systems. In addition to standard logical and temporal operators, our logic includes spatial operations corresponding to process composition and name hiding, and a fresh name quantifier. In Part I of this work we study the fundamental semantic properties of our logic; the focus of the present Part II is on proof theory. The main contributions are a sequent-based proof system for our logic, and a proof of cut-elimination for its first-order fragment.

Original languageEnglish
Pages (from-to)517-565
Number of pages49
JournalTheoretical Computer Science
Volume322
Issue number3
DOIs
Publication statusPublished - 6 Sep 2004
EventFoundations of Wide Area Network Computing - Malaga, Spain
Duration: 12 Jul 200213 Jul 2002

Fingerprint

Concurrency
Semantics
Logic
Chemical analysis
Proof Theory
Cut-elimination
Proof System
Quantifiers
Modal Logic
Distributed Systems
Fragment
First-order
Operator

Keywords

  • Distributed systems
  • Proof systems
  • Spatial logics
  • Specification
  • Verification

Cite this

Caires, Luís ; Cardelli, Luca. / A spatial logic for concurrency - II. In: Theoretical Computer Science. 2004 ; Vol. 322, No. 3. pp. 517-565.
@article{be59b5c32c76435a9bda5ed80df8d8c9,
title = "A spatial logic for concurrency - II",
abstract = "We present a modal logic for describing the spatial organization and the behavior of distributed systems. In addition to standard logical and temporal operators, our logic includes spatial operations corresponding to process composition and name hiding, and a fresh name quantifier. In Part I of this work we study the fundamental semantic properties of our logic; the focus of the present Part II is on proof theory. The main contributions are a sequent-based proof system for our logic, and a proof of cut-elimination for its first-order fragment.",
keywords = "Distributed systems, Proof systems, Spatial logics, Specification, Verification",
author = "Lu{\'i}s Caires and Luca Cardelli",
year = "2004",
month = "9",
day = "6",
doi = "10.1016/j.tcs.2003.10.041",
language = "English",
volume = "322",
pages = "517--565",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "3",

}

A spatial logic for concurrency - II. / Caires, Luís; Cardelli, Luca.

In: Theoretical Computer Science, Vol. 322, No. 3, 06.09.2004, p. 517-565.

Research output: Contribution to journalConference article

TY - JOUR

T1 - A spatial logic for concurrency - II

AU - Caires, Luís

AU - Cardelli, Luca

PY - 2004/9/6

Y1 - 2004/9/6

N2 - We present a modal logic for describing the spatial organization and the behavior of distributed systems. In addition to standard logical and temporal operators, our logic includes spatial operations corresponding to process composition and name hiding, and a fresh name quantifier. In Part I of this work we study the fundamental semantic properties of our logic; the focus of the present Part II is on proof theory. The main contributions are a sequent-based proof system for our logic, and a proof of cut-elimination for its first-order fragment.

AB - We present a modal logic for describing the spatial organization and the behavior of distributed systems. In addition to standard logical and temporal operators, our logic includes spatial operations corresponding to process composition and name hiding, and a fresh name quantifier. In Part I of this work we study the fundamental semantic properties of our logic; the focus of the present Part II is on proof theory. The main contributions are a sequent-based proof system for our logic, and a proof of cut-elimination for its first-order fragment.

KW - Distributed systems

KW - Proof systems

KW - Spatial logics

KW - Specification

KW - Verification

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

U2 - 10.1016/j.tcs.2003.10.041

DO - 10.1016/j.tcs.2003.10.041

M3 - Conference article

VL - 322

SP - 517

EP - 565

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 3

ER -