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

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

    Conference

    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

    Cite this