Beam Search: It is an optimization of the best-first search that uses the heuristic function to discard all but the m best candidate states at each depth, where m is the bound on the “width of the beam.” If more than m candidates exist, the worst candidates are discarded. This reduces the space requirements of best first search. Assigning a bound to the width of the search can also be applied to best-first, greedy best-first, and A*
searches.
When such a bound is used, termination of the search without discovering an error does not imply correctness of the system. However given that the advantage of heuristic search is its ability to quickly discover fairly short counterexamples, in practice use of such a bound is an effective bug-finding tactic.
We may have to run the model checker multiple times each time with a different and increasing value for m. This is called iterative widening.