### Abstract

Original language | Undefined |
---|---|

Title of host publication | Proceedings of the 20th International SPIN Symposium on Model Checking of Software, SPIN 2013 |

Editors | E. Bartocci, C.R. Ramakrishnan |

Place of Publication | London |

Publisher | Springer |

Pages | 227-245 |

Number of pages | 18 |

ISBN (Print) | 978-3-642-39175-0 |

DOIs | |

State | Published - 8 Jul 2013 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Verlag |

Volume | 7976 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Fingerprint

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

*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. DOI: 10.1007/978-3-642-39176-7_15

}

*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. DOI: 10.1007/978-3-642-39176-7_15

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

Research output: Scientific - peer-review › Conference contribution

TY - CHAP

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

PB - Springer

ER -