@techreport{RISC5954,author = {Wolfgang Schreiner and János Sztrik},
title = {{On the Probabilistic Model Checking of a Retrial Queueing System with Unreliable Server, Collision, and Constant Time Impatience}},
language = {english},
abstract = {We report on initial experiments with the automated analysis of a finite-source queueing
system with an unreliable server and collisions of service requests that cause clients to be
moved to an orbit until they can be served. However, clients remain in the obit only for
some maximum amount of time before they run out of patience and unsuccessfully abort
their service request. In contrast to earlier investigations, the duration of their patience is
not exponentially distributed but constrained by a constant time bound, which imposes a
problem for both their manual and automatic analysis. In this paper we address how such
systems can be nevertheless approximately analyzed to a certain extent with the help of the
probabilistic model checker PRISM.},
year = {2019},
month = {July},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {formal methods, model checking, performance analysis},
sponsor = {Supported by the Austrian-Hungarian Bilateral Cooperation in Science and Technology project 2017-2.2.4-TeT- AT-2017-00010 and the Aktion Österreich-Ungarn project 101öu7.},
length = {21}
}