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,
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.
|Name||CWI report. SEN-R : software engineering|