Guard-based Partial-Order Reduction

Alfons Laarman, Elwin Pater, Jan Cornelis van de Pol, M. Weber

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    8 Citations (Scopus)
    454 Downloads (Pure)

    Abstract

    This paper aims at making partial-order reduction independent of the modeling language. Our starting point is the stubborn set algorithm of Valmari (see also Godefroid's thesis), which relies on necessary enabling sets. We generalise it to a guard-based algorithm, which can be implemented on top of an abstract model checking interface. We extend the generalised algorithm by introducing necessary disabling sets and adding a heuristics to improve state space reduction. The effect of the changes to the algorithm are measured using an implementation in the LTSmin model checking toolset. We experiment with partial-order reduction on a number of Promela models, some with LTL properties, and on benchmarks from the BEEM database in the DVE language. We compare our results to the SPIN model checker. While the reductions take longer, they are consistently better than SPIN's ample set and even often surpass the ideal upper bound for the ample set, as established empirically by Geldenhuys, Hansen~and~Valmari on BEEM models.
    Original languageUndefined
    Title of host publicationProceedings of the 20th International SPIN Symposium on Model Checking of Software, SPIN 2013
    EditorsE. Bartocci, C.R. Ramakrishnan
    Place of PublicationLondon
    PublisherSpringer
    Pages227-245
    Number of pages18
    ISBN (Print)978-3-642-39175-0
    DOIs
    Publication statusPublished - 8 Jul 2013
    Event20th International SPIN Symposium on Model Checking of Software, SPIN 2013 - Stony Brook, NY, USA
    Duration: 8 Jul 20139 Jul 2013

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume7976
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference20th International SPIN Symposium on Model Checking of Software, SPIN 2013
    Period8/07/139/07/13
    Other8-9 July 2013

    Keywords

    • FMT-MC: MODEL CHECKING
    • METIS-297622
    • LTSMIN
    • necessary disabling sets
    • necessary enabling sets
    • Partial order reduction
    • Stubborn set
    • optimal reductions
    • EWI-23303
    • proviso
    • IR-86105
    • Ample set
    • Model Checking
    • DVE
    • Heuristics
    • SPIN
    • Promela
    • LTL

    Cite this