A spatial logic for concurrency - II

被引：40

作者：

Caires, L ^{[1
]}

Cardelli, L

机构：

[1] Univ Nova Lisboa, FCT, P-1200 Lisbon, Portugal

[2] Microsoft Res, Cambridge, England

来源：

THEORETICAL COMPUTER SCIENCE | 2004年 / 322卷 / 03期

关键词：

spatial logics; distributed systems; proof systems; specification; verification;

D O I：

10.1016/j.tcs.2003.10.041

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 [计算机软件与理论];

摘要：

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. (C) 2004 Elsevier B.V. All rights reserved.

引用

页码：517 / 565

页数：49

共 24 条

[1]

[Anonymous], 14 ANN S LOG COMP SC

[2]

[Anonymous], ACM WORKSH TYP LANG

[3]

[Anonymous], 2000, BASIC PROOF THEORY

[4]

[Anonymous], LECT NOTES COMPUTER

[5]

[Anonymous], LECT NOTES COMPUT SC

[6]

[Anonymous], 28 ANN S PRINC PROGR

[7]

[Anonymous], 27 ACM S PRINC PROGR

[8]

[Anonymous], LECT NOTES COMPUTER

[9]

A spatial logic for concurrency (part I) [J].

Caires, L ;

Cardelli, L .

INFORMATION AND COMPUTATION, 2003, 186 (02) :194-235

[10]

Caires L, 1998, LECT NOTES COMPUT SC, V1381, P42, DOI 10.1007/BFb0053562

← 1 2 3 →