@Article{	  wijs.ea:extended:2012,
  author	= {Anton Wijs and Mohammad Torabi Dashti},
  journal	= {The Journal of Logic and Algebraic Programming},
  language	= {USenglish},
  month		= {January},
  number	= 1,
  pages		= {46--69},
  title		= {Extended beam search for non-exhaustive state space
		  analysis},
  volume	= 81,
  year		= 2012,
  user		= {torabidm}
}




TY  - JOUR
T1  - Extended beam search for non-exhaustive state space analysis
JO  - Journal of Logic and Algebraic Programming
VL  - 81
IS  - 1
SP  - 46
EP  - 69
PY  - 2012/1//
T2  - Special Issue on Quantitative Formal Methods: Theory and Application
AU  - Wijs, A.J.
AU  - Torabi Dashti, M.
SN  - 1567-8326
M3  - doi: 10.1016/j.jlap.2011.06.002
UR  - http://www.sciencedirect.com/science/article/pii/S1567832611000609
KW  - Model checking
KW  - Formal analysis
KW  - State space generation
KW  - Heuristics
KW  - Guided traversal
AB  - 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.
ER  -