Partial model checking

Henrik Reif Andersen

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

    462 Downloads (Pure)

    Abstract

    A major obstacle in applying finite-state model checking to the verification of large systems is the combinatorial explosion of the state space arising when many loosely coupled parallel processes are considered. The problem also known as the state-explosion problem has been attacked from various sides. This paper presents a new approach based on partial model checking where parts of the concurrent system are gradually removed while transforming the specification accordingly. When the intermediate specifications constructed in this manner can be kept small, the state-explosion problem is avoided. Experimental results with a prototype implemented in Standard ML, shows that for Milner's Scheduler-an often used benchmark-this approach improves on the published results on binary decision diagrams and is comparable to results obtained using generalized decision diagrams. Specifications are expressed in a variant of the modal μ-calculus
    Original languageEnglish
    Title of host publicationLogic in Computer Science, 1995. LICS '95. Proceedings., Tenth Annual IEEE Symposium on
    PublisherIEEE
    Publication date1995
    Pages398-407
    ISBN (Print)0-8186-7050-9
    DOIs
    Publication statusPublished - 1995
    EventLogic in Computer Science, 1995. LICS '95. Proceedings., Tenth Annual IEEE Symposium on -
    Duration: 1 Jan 1995 → …

    Conference

    ConferenceLogic in Computer Science, 1995. LICS '95. Proceedings., Tenth Annual IEEE Symposium on
    Period01/01/1995 → …

    Bibliographical note

    Copyright: 1995 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 'Partial model checking'. Together they form a unique fingerprint.

    Cite this