author = {Wolfgang Schreiner and Nikolaj Popov and Tamas Berczes and Janos Sztrik and Gabor Kusper},
title = {{Applying High Performance Computing to Analyzing by Probabilistic Model Checking Mobile Cellular Networks with Spectrum Renting}},
language = {english},
abstract = {We report on the use of high performance computing in order to analyze with the proba- bilistic model checker PRISM mobile cellular networks, in particular the system described in the paper “A New Finite-Source Queueing Model for Mobile Cellular Networks Apply- ing Spectrum Renting” by Tien v. Do et al. That paper proposes a new finite-source retrial queueing model to consider spectrum renting in mobile cellular networks; numerical re- sults are there produced with the MOSEL-2 tool. Our results show that the model can be also appropriately described and analyzed in PRISM, but that modeling becomes compar- atively more cumbersome due to the lack of zero-time/infinite-rate transitions in PRISM. By using a massively parallel non-uniform memory architecture (NUMA), we are able to considerably speed up the analysis of large scale models.},
year = {2013},
month = {July},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {performance modeling, probabilistic model checking, parallel computing},
sponsor = {Supported by the European project FIRST (TÁMOP-4.4.2.C) and by the project 85öu8 of the Stiftung Aktion Österreich-Ungarn},
length = {24}