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

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

Publication series

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

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

Laarman, A., Pater, E., van de Pol, J. C., & Weber, M. (2013). Guard-based Partial-Order Reduction. In E. Bartocci, & C. R. Ramakrishnan (Eds.), Proceedings of the 20th International SPIN Symposium on Model Checking of Software, SPIN 2013 (pp. 227-245). (Lecture Notes in Computer Science; Vol. 7976). London: Springer. https://doi.org/10.1007/978-3-642-39176-7_15
Laarman, Alfons ; Pater, Elwin ; van de Pol, Jan Cornelis ; Weber, M. / Guard-based Partial-Order Reduction. Proceedings of the 20th International SPIN Symposium on Model Checking of Software, SPIN 2013. editor / E. Bartocci ; C.R. Ramakrishnan. London : Springer, 2013. pp. 227-245 (Lecture Notes in Computer Science).
@inproceedings{276a95168e9b48fb8a7f2f81ededc712,
title = "Guard-based Partial-Order Reduction",
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.",
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",
author = "Alfons Laarman and Elwin Pater and {van de Pol}, {Jan Cornelis} and M. Weber",
note = "eemcs-eprint-23303",
year = "2013",
month = "7",
day = "8",
doi = "10.1007/978-3-642-39176-7_15",
language = "Undefined",
isbn = "978-3-642-39175-0",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "227--245",
editor = "E. Bartocci and C.R. Ramakrishnan",
booktitle = "Proceedings of the 20th International SPIN Symposium on Model Checking of Software, SPIN 2013",

}

Laarman, A, Pater, E, van de Pol, JC & Weber, M 2013, Guard-based Partial-Order Reduction. in E Bartocci & CR Ramakrishnan (eds), Proceedings of the 20th International SPIN Symposium on Model Checking of Software, SPIN 2013. Lecture Notes in Computer Science, vol. 7976, Springer, London, pp. 227-245. https://doi.org/10.1007/978-3-642-39176-7_15

Guard-based Partial-Order Reduction. / Laarman, Alfons; Pater, Elwin; van de Pol, Jan Cornelis; Weber, M.

Proceedings of the 20th International SPIN Symposium on Model Checking of Software, SPIN 2013. ed. / E. Bartocci; C.R. Ramakrishnan. London : Springer, 2013. p. 227-245 (Lecture Notes in Computer Science; Vol. 7976).

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

TY - GEN

T1 - Guard-based Partial-Order Reduction

AU - Laarman, Alfons

AU - Pater, Elwin

AU - van de Pol, Jan Cornelis

AU - Weber, M.

N1 - eemcs-eprint-23303

PY - 2013/7/8

Y1 - 2013/7/8

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

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

KW - FMT-MC: MODEL CHECKING

KW - METIS-297622

KW - LTSMIN

KW - necessary disabling sets

KW - necessary enabling sets

KW - Partial order reduction

KW - Stubborn set

KW - optimal reductions

KW - EWI-23303

KW - proviso

KW - IR-86105

KW - Ample set

KW - Model Checking

KW - DVE

KW - Heuristics

KW - SPIN

KW - Promela

KW - LTL

U2 - 10.1007/978-3-642-39176-7_15

DO - 10.1007/978-3-642-39176-7_15

M3 - Conference contribution

SN - 978-3-642-39175-0

T3 - Lecture Notes in Computer Science

SP - 227

EP - 245

BT - Proceedings of the 20th International SPIN Symposium on Model Checking of Software, SPIN 2013

A2 - Bartocci, E.

A2 - Ramakrishnan, C.R.

PB - Springer

CY - London

ER -

Laarman A, Pater E, van de Pol JC, Weber M. Guard-based Partial-Order Reduction. In Bartocci E, Ramakrishnan CR, editors, Proceedings of the 20th International SPIN Symposium on Model Checking of Software, SPIN 2013. London: Springer. 2013. p. 227-245. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-39176-7_15