Evaluating a Probabilistic Model Checker for Modeling and Analyzing Retrial Queueing Systems
Sprache des Titels:
We describe the results of analyzing the performance model of a retrial queueing system with the PRISM (PRobabIlistic Symbolic Model checker). The system has been previously analyzed with the help of the performance modeling environment MOSEL (Modeling, Specification and Evaluation Language). In our paper we are able to accurately reproduce the results reported in literature. Furthermore, we compare PRISM and MOSEL with respect to their modeling languages and ways of specifying performance queries and benchmark the executions of the tools. Several numerical examples illustrate the comparisons resulting in various tables and figures.