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

    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 languageEnglish
    Title of host publicationProceedings of the symposium of Logic in Computer Science
    PublisherIEEE
    Publication date1994
    Pages144-153
    ISBN (Print)08-18-66310-3
    DOIs
    Publication statusPublished - 1994
    EventNinth Annual Symposium on Logic in Computer Science - Paris, France
    Duration: 4 Jul 19947 Jul 1994

    Conference

    ConferenceNinth Annual Symposium on Logic in Computer Science
    Country/TerritoryFrance
    CityParis
    Period04/07/199407/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

    Fingerprint

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

    Cite this