Applying High Performance Computing to Analyzing by Probabilistic Model Checking Mobile Cellular Networks with Spectrum Renting
Sprache des Titels:
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.