Wolfgang Schreiner, Tamas Berczes, Janos Sztrik,
"Probabilistic Model Checking on HPC Systems for the Performance Analysis of Mobile Networks"
, Serie Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria, RISC, JKU, Hagenberg, 9-2013
Probabilistic Model Checking on HPC Systems for the Performance Analysis of Mobile Networks
Sprache des Titels:
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 v. 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 validate the previously presented results. However, we also outline some discrepancies with 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.
Sprache der Kurzfassung:
Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria