Pruning state spaces with extended beam search

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.