TY - JOUR
T1 - Extended beam search for non-exhaustive state space analysis
AU - Wijs, A.J.
AU - Torabi Dashti, M.
PY - 2012
Y1 - 2012
N2 - 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.
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.
U2 - 10.1016/j.jlap.2011.06.002
DO - 10.1016/j.jlap.2011.06.002
M3 - Article
SN - 1567-8326
VL - 81
SP - 46
EP - 69
JO - Journal of Logic and Algebraic Programming
JF - Journal of Logic and Algebraic Programming
IS - 1
ER -