Guard-based partial-order reduction

Alfons Laarman (Corresponding Author), Elwin Pater, Jaco van de Pol, Henri Hansen

    Research output: Contribution to journalArticleAcademicpeer-review

    13 Citations (Scopus)
    82 Downloads (Pure)

    Abstract

    This paper aims at making partial-order reduction independent of the modeling language. To this end, we present a guard-based method which is a general-purpose implementation of the stubborn set method. We approach the implementation through so-called necessary enabling sets and do-not-accord sets, and give an algorithm suitable for an abstract model checking interface. We also introduce necessary disabling sets and heuristics to produce smaller stubborn sets and thus better reduction at low costs. We explore the effect of these methods using an implementation in the model checker LTSmin. We experiment with partial-order reduction on a number of Promela models, on benchmarks from the BEEM database in the DVE language, and with several with LTL properties. The efficiency of the heuristic algorithm is established by a comparison to the subset-minimal Deletion algorithm and the simple closure algorithm. We also compare our results to the Spin model checker. While the reductions take longer, they are consistently better than Spin ’s ample set and often surpass the upper bound for the process-based ample sets, established empirically earlier on BEEM models.
    Original languageEnglish
    Pages (from-to)427-448
    Number of pages22
    JournalInternational journal on software tools for technology transfer
    Volume18
    Issue number4
    DOIs
    Publication statusPublished - Aug 2016

    Keywords

    • EWI-23356
    • FMT-MC: MODEL CHECKING
    • Heuristic search
    • Partial order reduction
    • IR-94398
    • Ample set
    • Model Checking
    • Necessary disabling set
    • METIS-309547
    • Stubborn set

    Fingerprint

    Dive into the research topics of 'Guard-based partial-order reduction'. Together they form a unique fingerprint.

    Cite this