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.
| Original language | English |
|---|
| Place of Publication | Hagenberg |
|---|
| Publisher | RISC Hagenberg |
|---|
| Number of pages | 18 |
|---|
| Publication status | Published - Apr 2013 |
|---|
- 101001 Algebra
- 101002 Analysis
- 101 Mathematics
- 102 Computer Sciences
- 102011 Formal languages
- 101009 Geometry
- 101013 Mathematical logic
- 101020 Technical mathematics
- 101025 Number theory
- 101012 Combinatorics
- 101005 Computer algebra
- 101006 Differential geometry
- 101003 Applied geometry
- 102025 Distributed systems
- Computation in Informatics and Mathematics