Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
Guard-Based Partial-Order Reduction
verfasst von : Alfons Laarman, Elwin Pater, Jaco van de Pol, Michael Weber
Erschienen in: Model Checking Software
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.