Pruning state spaces with extended beam search
Mohammad Torabi Dashti, Anton Wijs · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 2006
Abstract. State space explosion is still the main problem in the area of model checking. This paper focuses on using beam search, a heuristic search algorithm, for pruning state spaces while generating. Original beam search is adapted to the state space generation setting and two new variants, motivated by some practical case studies, are devised. Remarkably, the resulting framework is shown to encompass A � search and some partial order reduction algorithms. These beam searches have all been implemented in the µCRL toolset. Case studies and comparisons with SPIN are also presented. 1