RISC RISC Research Institute for Symbolic Computation  
  • @techreport{RISC4749,
    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}