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

220 Downloads (Pure)

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	Symposium on Logic in Computer Science - Paris, France Duration: 1 Jan 1994 → …

Conference

Conference	Symposium on Logic in Computer Science
City	Paris, France
Period	01/01/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

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; Symposium on Logic in Computer Science, LICS '94 ; Conference date: 01-01-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 - Symposium on Logic in Computer Science

Y2 - 1 January 1994

ER -