@article{RISC5058,author = {Wolfgang Schreiner and Tamas Berczes and Janos Sztrik},
title = {{Probabilistic Model Checking on HPC Systems for the Performance Analysis of Mobile Networks}},
language = {english},
abstract = {We report on the use of HPC resources for the performance analysis of the mobile
cellular network model described in “A New Finite-Source Queueing Model for
Mobile Cellular Networks Applying Spectrum Renting” by Tien Van Do et al. That
paper proposed a new finite-source retrial queueing model with spectrum renting that
was analyzed with the MOSEL-2 tool. Our results show how this model can be also
appropriately described and analyzed with the probabilistic model checker PRISM, although
at some cost considering the formulation of the model; in particular, we are able
to accurately reproduce most of the analytical results presented in that paper and thus
increase the confidence in the previously presented results. However, we also outline
some discrepancies which may hint to deficiencies of the original analysis. Moreover,
by applying a parallel computing framework developed for this purpose, we are able
to considerably speed up studies performed with the PRISM tool. The investigations
are illustrated by figures and conclusions are drawn.},
journal = {Annales Mathematicae et Informaticae},
volume = {43},
pages = {123--144},
publisher = {Líceum University Press},
isbn_issn = {ISSN 1787-5021, ISSN 1787-6117},
year = {2014},
refereed = {yes},
length = {22}
}