A compositional proof system for the modal μ-calculus

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

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    362 Downloads (Pure)


    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 languageEnglish
    Title of host publicationProceedings of the symposium of Logic in Computer Science
    Publication date1994
    ISBN (Print)08-18-66310-3
    Publication statusPublished - 1994
    EventSymposium on Logic in Computer Science - Paris, France
    Duration: 1 Jan 1994 → …


    ConferenceSymposium on Logic in Computer Science
    CityParis, France
    Period01/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


    Dive into the research topics of 'A compositional proof system for the modal μ-calculus'. Together they form a unique fingerprint.

    Cite this