A Case Study on Exploring the Performance Limits of PRISM
Sprache des Titels:
Englisch
Original Kurzfassung:
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.
Forschungs-