Improving spin's partial-order reduction for breadth-first search
D Bošnački, GJ Holzmann - … SPIN Workshop on Model Checking of …, 2005 - Springer
International SPIN Workshop on Model Checking of Software, 2005•Springer
We describe an improvement of the partial-order reduction algorithm for breadth-first search
which was introduced in Spin version 4.0. Our improvement is based on the algorithm by
Alur et al. for symbolic state model checking for local safety properties [1]. The crux of the
improvement is an optimization in the context of explicit state model checking of the
condition that prevents action ignoring, also known as the cycle proviso. There is an
interesting duality between the cycle provisos for the breadth-first search (BFS) and depth …
which was introduced in Spin version 4.0. Our improvement is based on the algorithm by
Alur et al. for symbolic state model checking for local safety properties [1]. The crux of the
improvement is an optimization in the context of explicit state model checking of the
condition that prevents action ignoring, also known as the cycle proviso. There is an
interesting duality between the cycle provisos for the breadth-first search (BFS) and depth …
Abstract
We describe an improvement of the partial-order reduction algorithm for breadth-first search which was introduced in Spin version 4.0. Our improvement is based on the algorithm by Alur et al. for symbolic state model checking for local safety properties [1]. The crux of the improvement is an optimization in the context of explicit state model checking of the condition that prevents action ignoring, also known as the cycle proviso. There is an interesting duality between the cycle provisos for the breadth-first search (BFS) and depth first search (DFS) exploration of the state space, which is reflected in the role of the BFS queue and the DFS stack, respectively. The improved version of the algorithm is supported in the current version of Spin and can be shown to perform significantly better than the initial version.
Springer