Performance Analysis and Formal Verification of Cognitive Wireless Networks

Cognitive Networks are a class of communication networks, in which nodes can learn how to adjust their behaviour according to the present and past network conditions. In this paper we introduce a formal probabilistic model for the analysis of wireless networks in which nodes are seen as processes capable of adapting their course of action to the environmental conditions. In particular, we model a network made of mobile nodes using the gossip protocol, and we study how the energy performance of the network varies, according to the topology changes and the transmission power. The stochastic process underlying the model is a discrete time Markov chain. We use the PRISM model checker to obtain, through Monte-Carlo simulation, numerical results for our analysis, which show how the learning-driven dynamic adjustment of transmission power can improve the energy performance while preserving connectivity.