Tampere University of Technology

TUTCRIS Research Portal

Guard-based Partial Order Reduction

Research output: Contribution to journalArticleScientificpeer-review

Details

Original languageEnglish
Pages (from-to)427-448
JournalInternational Journal on Software Tools for Technology Transfer
Volume18
Issue number4
DOIs
Publication statusPublished - Dec 2014
Publication typeA1 Journal article-refereed

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.

Publication forum classification

Field of science, Statistics Finland