Extended beam search for non-exhaustive state space analysis

State space explosion is a major problem in both qualitative and quantitative model checking. This article focuses on using beam search, a heuristic search algorithm, for pruning weighted state spaces while generating. The original beam search is adapted to the state space generation setting and two new variants, motivated by practical case studies, are devised. These beam searches have been implemented in the μμCRL toolset and applied on several case studies reported in the article.

► We extend detailed and priority beam search for general state space exploration.
► A new class of searches called multi-phase best-first search is described.
► The extended beam searches use flexible beam widths and multiple guiding functions.
► We implemented particular search setups in the μμCRL toolset.
► Results of multiple experiments with scheduling and planning models are reported.