@techreport{RISC4820,author = {Wolfgang Schreiner and Tamas Berczes and Janos Sztrik and Gabor Kusper},
title = {{A Case Study on Exploring the Performance Limits of PRISM}},
language = {english},
abstract = {We investigate based on a simple system model the range of applicability of the probabilistic
model checker PRISM. In particular, we analyze the effect of the choice of the
checking engine, of the numerical equation solver, and of other settings on the time and
memory required for the analysis of the model by PRISM. The results demonstrate that not
always the same engine is the fastest one but that for large models an otherwise slow engine
may show superior performance; furthermore, the appropriate choice of the termination
criterium can make the crucial difference between the success and the failure of an analysis.},
year = {2013},
month = {September},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
length = {13}
}