Applying High Performance Computing to Analyzing by Probabilistic Model Checking Mobile Cellular Networks with Spectrum Renting

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.