Partial Model Checking with ROBDDs

Henrik Reif Andersen, Niels Maretti, Jørgen Staunstrup

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

    Abstract

    This paper introduces a technique for localizing model checking of concurrent state-based systems. The technique, called partial model checking, isfully automatic and performs model checking by gradually specializing the specification with respect to the concurrent components one by one,computing a `concurrent weakest precondition.' Specifications are invariance properties and the concurrent components sets of transitions. Bothare expressed as predicates represented by Reduced Ordered Binary Decision Diagrams (ROBDDs). The self-reducing properties of ROBDDs areimportant for the success of the technique. We describe experimental results obtained on four different examples.
    Original languageEnglish
    Title of host publicationProceedings of TACAS'97, LNCS 1217
    Place of PublicationBerlin,Heidelberg
    PublisherSpringer Verlag
    Publication date1997
    Pages35-49
    Publication statusPublished - 1997
    EventTACAS'97, Tools and Algorithms for the Construction and Analysis of Systems - Enschede, Netherlands
    Duration: 1 Jan 1997 → …

    Conference

    ConferenceTACAS'97, Tools and Algorithms for the Construction and Analysis of Systems
    CityEnschede, Netherlands
    Period01/01/1997 → …

    Cite this

    Andersen, H. R., Maretti, N., & Staunstrup, J. (1997). Partial Model Checking with ROBDDs. In Proceedings of TACAS'97, LNCS 1217 (pp. 35-49). Springer Verlag.