Adaptive partial order reduction methods

Authors

Pierre Parutto

Type

techreport

Year

2013

Number

1213

Abstract

Explicit model checking of concurrent systems suffers from the exponential blow-up in the number of states of the represented system. The partial order reduction methods are a set of methods to tackle this problem. They act by preventing the generation of redundant states while creating the state space. Among all these methods are the two phase and ample set algorithms that serve as the basis for our investigations. We implemented those algorithms in Spot, the C++, model-checking library developed at the LRDE, using the Divine interface. Building on these classical methods and taking advantadge of the on-the-fly property of Spot's algorithms, it is possible to devise a new class of methods called adaptive partial order methods that use the current state of the formula automaton and not the whole formula. This new method gives better results than the classical partial order methods on our test suite.