Sciweavers

SPIN
2005
Springer

Improving Spin's Partial-Order Reduction for Breadth-First Search

13 years 9 months ago
Improving Spin's Partial-Order Reduction for Breadth-First Search
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.
Dragan Bosnacki, Gerard J. Holzmann
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where SPIN
Authors Dragan Bosnacki, Gerard J. Holzmann
Comments (0)