@techreport{RISC4705,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}
}