author = {Wolfgang Schreiner},
title = {{Initial Results on Modeling in PRISM Mobile Cellular Networks with Spectrum Renting}},
language = {english},
abstract = {We report in this paper on our initial results on modeling in the probabilistic model checker PRISM the system described in the paper \enquote{A New Finite-Source Queueing Model for Mobile Cellular Networks Applying 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 results are there produced with the MOSEL-2 tool. Our results show that the model can be described and analyzed in PRISM in a very transparent way; however, due to an apparent system bug we are not yet able to check models of the same size as in MOSEL-2.},
year = {2013},
month = {April 9},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
sponsor = {Supported by the project HU 10/2012 of the Austrian Academic Exchange Service (ÖAD).},
length = {18}