On the Probabilistic Model Checking of Cognitive Radio Networks and Cognitive Infocommunication Systems

We report on the usage of the probabilistic model checker PRISM to validate respectively falsify previously published results on the performance of cognitive radio networks and other cognitive infocommunication systems. For this purpose, we construct formal system models in the PRISM modeling language as Continuous Time Markov Chains (CTMCs) that are analyzed with the help of queries formulated in a variant of continuous stochastic logic (CSL). It is shown that many results can be accurately reproduced but also that a few previously reported results are clearly erroneous. Furthermore, we report several deviations from previously reported results where the reasons are unclear and need further investigation. Here a major problem is that the systems that have been analyzed in literature are usually just described in informal language which leaves ample room for interpretation. This makes the reconstruction of corresponding formal system models and the reproduction of performance measures a difficult task and limits the long-term scientific value of the reported results.