@techreport{RISC5595,author = {Wolfgang Schreiner and Tamás Bérczes and János Sztrik and Hamza Nemouchi},
title = {{On the Probabilistic Model Checking of Cognitive Radio Networks and Cognitive Infocommunication Systems}},
language = {english},
abstract = {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.},
number = {18-04},
year = {2018},
month = {February},
keywords = {formal methods, performance analysis, queueing systems},
sponsor = {Supported by the Stiftung Aktion Österreich-Ungarn project 96öu8 “Engineering Information Technology Modelling and Design of Cognitive Radio Networks”},
length = {24},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}