Pruning state spaces with extended beam search

M. Torabi Dashti, A.J. Wijs

Research output: Book/ReportReportAcademic

1 Downloads (Pure)


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.
Original languageEnglish
Place of PublicationAmsterdam
PublisherCentrum voor Wiskunde en Informatica
Number of pages19
Publication statusPublished - 2006

Publication series

NameCWI report. SEN-R : software engineering
ISSN (Print)1386-369X


Dive into the research topics of 'Pruning state spaces with extended beam search'. Together they form a unique fingerprint.

Cite this