Other formats:
BibTeX
LaTeX
RIS
@inproceedings{371573,
author = {Brim, Luboš and Černá, Ivana and Nečesal, Martin},
address = {Berlin Heidelberg New York},
booktitle = {Process Algebra and Probabilistic Methods. Proceedings of PAPM-PROBMIV 2001},
keywords = {Model checking; randomized algorithm; depth-first search},
language = {eng},
location = {Berlin Heidelberg New York},
isbn = {3-540-42556-X},
pages = {105-119},
publisher = {Springer},
title = {Randomization Helps in LTL Model Checking},
year = {2001}
}
TY - JOUR
ID - 371573
AU - Brim, Luboš - Černá, Ivana - Nečesal, Martin
PY - 2001
TI - Randomization Helps in LTL Model Checking
VL - LNCS 2165
PB - Springer
CY - Berlin Heidelberg New York
SN - 354042556X
KW - Model checking
KW - randomized algorithm
KW - depth-first search
N2 - We present and analyze a new probabilistic method for automata based LTL model checking of non-proba\-bi\-listic systems with intention to reduce memory requirements. The main idea of our approach is to use randomness to decide which of the needed information (visited states) should be stored during a computation and which could be omitted. We propose two strategies of probabilistic storing of states. The algorithm never errs, i.e. it always delivers correct results. On the other hand the computation time can increase. The method has been embedded into the SPIN model checker and a series of experiments has been performed. The results confirm that randomization can help to increase the applicability of model checkers in practice.
ER -
BRIM, Luboš, Ivana ČERNÁ and Martin NEČESAL. Randomization Helps in LTL Model Checking. In \textit{Process Algebra and Probabilistic Methods. Proceedings of PAPM-PROBMIV 2001}. Berlin Heidelberg New York: Springer, 2001, p.~105-119. LNCS 2165. ISBN~3-540-42556-X.
|
