Comparing the Performance Modeling Environment MOSEL and the Probabilistic Model Checker PRISM for Modeling and Analyzing Retrial Queueing Systems

Tamas Berczes; Gabor Guta; Janos Sztrik; Wolfgang Schreiner; Gabor Kusper

Comparing the Performance Modeling Environment MOSEL and the Probabilistic Model Checker PRISM for Modeling and Analyzing Retrial Queueing Systems

Tamas Berczes, Gabor Guta, Janos Sztrik, Wolfgang Schreiner, Gabor Kusper

Research Institute for Symbolic Computation

Research output: Working paper and reports › Preprint

Abstract

We describe the results of analyzing the performance model of a retrial queueing system with the probabilistic model checker PRISM. The system has been previously analyzed with the help of the performance modeling environment MOSEL; we are able to accurately reproduce the results reported in literature. Furthermore, we compare PRISM and MOSEL with respect to their modeling languages and ways of specifying performance queries and benchmark the executions of the tools.

Original language	English
Place of Publication	Johannes Kepler University Linz, Altenbergerstraße 69, 4040 Linz, Austria
Publisher	RISC
Number of pages	40
Publication status	Published - 2007

Publication series

Name	RISC Report Series
No.	07-17

Fields of science

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

Cite this

@techreport{13e539e4ef954fa48d343f1a583f7864,

title = "Comparing the Performance Modeling Environment MOSEL and the Probabilistic Model Checker PRISM for Modeling and Analyzing Retrial Queueing Systems",

abstract = "We describe the results of analyzing the performance model of a retrial queueing system with the probabilistic model checker PRISM. The system has been previously analyzed with the help of the performance modeling environment MOSEL; we are able to accurately reproduce the results reported in literature. Furthermore, we compare PRISM and MOSEL with respect to their modeling languages and ways of specifying performance queries and benchmark the executions of the tools.",

author = "Tamas Berczes and Gabor Guta and Janos Sztrik and Wolfgang Schreiner and Gabor Kusper",

year = "2007",

language = "English",

series = "RISC Report Series",

publisher = "RISC",

number = "07-17",

type = "WorkingPaper",

institution = "RISC",

}

Comparing the Performance Modeling Environment MOSEL and the Probabilistic Model Checker PRISM for Modeling and Analyzing Retrial Queueing Systems. / Berczes, Tamas; Guta, Gabor; Sztrik, Janos et al.
Johannes Kepler University Linz, Altenbergerstraße 69, 4040 Linz, Austria: RISC, 2007. (RISC Report Series; No. 07-17).

Research output: Working paper and reports › Preprint

TY - UNPB

T1 - Comparing the Performance Modeling Environment MOSEL and the Probabilistic Model Checker PRISM for Modeling and Analyzing Retrial Queueing Systems

AU - Berczes, Tamas

AU - Guta, Gabor

AU - Sztrik, Janos

AU - Schreiner, Wolfgang

AU - Kusper, Gabor

PY - 2007

Y1 - 2007

N2 - We describe the results of analyzing the performance model of a retrial queueing system with the probabilistic model checker PRISM. The system has been previously analyzed with the help of the performance modeling environment MOSEL; we are able to accurately reproduce the results reported in literature. Furthermore, we compare PRISM and MOSEL with respect to their modeling languages and ways of specifying performance queries and benchmark the executions of the tools.

AB - We describe the results of analyzing the performance model of a retrial queueing system with the probabilistic model checker PRISM. The system has been previously analyzed with the help of the performance modeling environment MOSEL; we are able to accurately reproduce the results reported in literature. Furthermore, we compare PRISM and MOSEL with respect to their modeling languages and ways of specifying performance queries and benchmark the executions of the tools.

M3 - Preprint

T3 - RISC Report Series

BT - Comparing the Performance Modeling Environment MOSEL and the Probabilistic Model Checker PRISM for Modeling and Analyzing Retrial Queueing Systems

PB - RISC

CY - Johannes Kepler University Linz, Altenbergerstraße 69, 4040 Linz, Austria

ER -