Modeling RF Communication in Sensor Networks by Probabilistic Model Checking

Wolfgang Schreiner; Tamas Berczes; Janos Sztrik; Adam Toth

Modeling RF Communication in Sensor Networks by Probabilistic Model Checking

Wolfgang Schreiner
, Tamas Berczes
, Janos Sztrik
, Adam Toth

Research Institute for Symbolic Computation

Research output: Working paper and reports › Preprint

Abstract

We report in this paper our results of modeling and analyzing with the probabilistic model checker PRISM a system of radio frequency (RF) transmission in sensor networks which has previously been studied in literature by using finite-source retrial queueing systems. We are able to validate with a small and quite transparent PRISM model the previously reported results (and also exhibit a minor error). Furthermore, we extend the model by also considering infinite sources and show that a previously suggested optimization has in this model beneficial effects only in a comparatively small parameter range.

Original language	English
Place of Publication	RISC Hagenberg
Publisher	RISC
Number of pages	25
Publication status	Published - Oct 2015

Publication series

Name	RISC Report Series
No.	15-21

Fields of science

101 Mathematics
101001 Algebra
101005 Computer algebra
101009 Geometry
101012 Combinatorics
101013 Mathematical logic
101020 Technical mathematics

JKU Focus areas

Computation in Informatics and Mathematics

Cite this

@techreport{e3bef82acbfb4837b6c6d20ac8e185a5,

title = "Modeling RF Communication in Sensor Networks by Probabilistic Model Checking",

abstract = "We report in this paper our results of modeling and analyzing with the probabilistic model checker PRISM a system of radio frequency (RF) transmission in sensor networks which has previously been studied in literature by using finite-source retrial queueing systems. We are able to validate with a small and quite transparent PRISM model the previously reported results (and also exhibit a minor error). Furthermore, we extend the model by also considering infinite sources and show that a previously suggested optimization has in this model beneficial effects only in a comparatively small parameter range.",

author = "Wolfgang Schreiner and Tamas Berczes and Janos Sztrik and Adam Toth",

year = "2015",

month = oct,

language = "English",

series = "RISC Report Series",

publisher = "RISC",

number = "15-21",

type = "WorkingPaper",

institution = "RISC",

}

TY - UNPB

T1 - Modeling RF Communication in Sensor Networks by Probabilistic Model Checking

AU - Schreiner, Wolfgang

AU - Berczes, Tamas

AU - Sztrik, Janos

AU - Toth, Adam

PY - 2015/10

Y1 - 2015/10

N2 - We report in this paper our results of modeling and analyzing with the probabilistic model checker PRISM a system of radio frequency (RF) transmission in sensor networks which has previously been studied in literature by using finite-source retrial queueing systems. We are able to validate with a small and quite transparent PRISM model the previously reported results (and also exhibit a minor error). Furthermore, we extend the model by also considering infinite sources and show that a previously suggested optimization has in this model beneficial effects only in a comparatively small parameter range.

AB - We report in this paper our results of modeling and analyzing with the probabilistic model checker PRISM a system of radio frequency (RF) transmission in sensor networks which has previously been studied in literature by using finite-source retrial queueing systems. We are able to validate with a small and quite transparent PRISM model the previously reported results (and also exhibit a minor error). Furthermore, we extend the model by also considering infinite sources and show that a previously suggested optimization has in this model beneficial effects only in a comparatively small parameter range.

M3 - Preprint

T3 - RISC Report Series

BT - Modeling RF Communication in Sensor Networks by Probabilistic Model Checking

PB - RISC

CY - RISC Hagenberg

ER -