Guard-based partial-order reduction

Alfons Laarman, Elwin Pater, Jan Cornelis van de Pol, Henri Hansen

Research output: Contribution to journalArticle

  • 3 Citations

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.
LanguageUndefined
Pages427-448
Number of pages22
JournalInternational journal on software tools for technology transfer
Volume18
Issue number4
DOIs
StatePublished - 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

Cite this

Laarman, Alfons ; Pater, Elwin ; van de Pol, Jan Cornelis ; Hansen, Henri. / Guard-based partial-order reduction. In: International journal on software tools for technology transfer. 2016 ; Vol. 18, No. 4. pp. 427-448
@article{e731863b995044c5b45bafa658c37ff7,
title = "Guard-based partial-order reduction",
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.",
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",
author = "Alfons Laarman and Elwin Pater and {van de Pol}, {Jan Cornelis} and Henri Hansen",
note = "eemcs-eprint-23356",
year = "2016",
month = "8",
doi = "10.1007/s10009-014-0363-9",
language = "Undefined",
volume = "18",
pages = "427--448",
journal = "International journal on software tools for technology transfer",
issn = "1433-2779",
publisher = "Springer Berlin Heidelberg",
number = "4",

}

Guard-based partial-order reduction. / Laarman, Alfons; Pater, Elwin; van de Pol, Jan Cornelis; Hansen, Henri.

In: International journal on software tools for technology transfer, Vol. 18, No. 4, 08.2016, p. 427-448.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Guard-based partial-order reduction

AU - Laarman,Alfons

AU - Pater,Elwin

AU - van de Pol,Jan Cornelis

AU - Hansen,Henri

N1 - eemcs-eprint-23356

PY - 2016/8

Y1 - 2016/8

N2 - 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.

AB - 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.

KW - EWI-23356

KW - FMT-MC: MODEL CHECKING

KW - Heuristic search

KW - Partial order reduction

KW - IR-94398

KW - Ample set

KW - Model Checking

KW - Necessary disabling set

KW - METIS-309547

KW - Stubborn set

U2 - 10.1007/s10009-014-0363-9

DO - 10.1007/s10009-014-0363-9

M3 - Article

VL - 18

SP - 427

EP - 448

JO - International journal on software tools for technology transfer

T2 - International journal on software tools for technology transfer

JF - International journal on software tools for technology transfer

SN - 1433-2779

IS - 4

ER -