A compositional proof system for the modal μ-calculus

Henrik Reif Andersen; C. Stirling; G. Winskel,

doi:10.1109/LICS.1994.316076

A compositional proof system for the modal μ-calculus

Henrik Reif Andersen, C. Stirling, G. Winskel,

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

371 Downloads (Orbit)

Abstract

We present a proof system for determining satisfaction between processes in a fairly general process algebra and assertions of the modal μ-calculus. The proof system is compositional in the structure of processes. It extends earlier work on compositional reasoning within the modal μ-calculus and combines it with techniques from work on local model checking. The proof system is sound for all processes and complete for a class of finite-state processes

Original language	English
Title of host publication	Proceedings of the symposium of Logic in Computer Science
Publisher	IEEE
Publication date	1994
Pages	144-153
ISBN (Print)	08-18-66310-3
DOIs	https://doi.org/10.1109/LICS.1994.316076
Publication status	Published - 1994
Event	Ninth Annual Symposium on Logic in Computer Science - Paris, France Duration: 4 Jul 1994 → 7 Jul 1994

Conference

Conference	Ninth Annual Symposium on Logic in Computer Science
Country/Territory	France
City	Paris
Period	04/07/1994 → 07/07/1994

Bibliographical note

Copyright: 1994 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE

Access to Document

10.1109/LICS.1994.316076

RaifFinal published version, 892 KB

OpenUrl availability

Full text

Cite this

@inproceedings{a01e5c0805754644bd03636b1a6c7349,

title = "A compositional proof system for the modal μ-calculus",

abstract = "We present a proof system for determining satisfaction between processes in a fairly general process algebra and assertions of the modal μ-calculus. The proof system is compositional in the structure of processes. It extends earlier work on compositional reasoning within the modal μ-calculus and combines it with techniques from work on local model checking. The proof system is sound for all processes and complete for a class of finite-state processes",

author = "Andersen, {Henrik Reif} and C. Stirling and G. Winskel,",

note = "Copyright: 1994 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE; Ninth Annual Symposium on Logic in Computer Science, LICS '94 ; Conference date: 04-07-1994 Through 07-07-1994",

year = "1994",

doi = "10.1109/LICS.1994.316076",

language = "English",

isbn = "08-18-66310-3",

pages = "144--153",

booktitle = "Proceedings of the symposium of Logic in Computer Science",

publisher = "IEEE",

address = "United States",

}

TY - GEN

T1 - A compositional proof system for the modal μ-calculus

AU - Andersen, Henrik Reif

AU - Stirling, C.

AU - Winskel,, G.

N1 - Copyright: 1994 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE

PY - 1994

Y1 - 1994

N2 - We present a proof system for determining satisfaction between processes in a fairly general process algebra and assertions of the modal μ-calculus. The proof system is compositional in the structure of processes. It extends earlier work on compositional reasoning within the modal μ-calculus and combines it with techniques from work on local model checking. The proof system is sound for all processes and complete for a class of finite-state processes

AB - We present a proof system for determining satisfaction between processes in a fairly general process algebra and assertions of the modal μ-calculus. The proof system is compositional in the structure of processes. It extends earlier work on compositional reasoning within the modal μ-calculus and combines it with techniques from work on local model checking. The proof system is sound for all processes and complete for a class of finite-state processes

U2 - 10.1109/LICS.1994.316076

DO - 10.1109/LICS.1994.316076

M3 - Article in proceedings

SN - 08-18-66310-3

SP - 144

EP - 153

BT - Proceedings of the symposium of Logic in Computer Science

PB - IEEE

T2 - Ninth Annual Symposium on Logic in Computer Science

Y2 - 4 July 1994 through 7 July 1994

ER -

A compositional proof system for the modal μ-calculus

Abstract

Conference

Bibliographical note

Access to Document

OpenUrl availability

Fingerprint

Cite this