A spatial logic for concurrency - II

Luís Caires, Luca Cardelli

Research output: Contribution to journalConference article

46 Citations (Scopus)
15 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

Keywords

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

Fingerprint Dive into the research topics of 'A spatial logic for concurrency - II'. Together they form a unique fingerprint.

  • Cite this