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.},
number = {19-11},
year = {2019},
month = {July},
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},
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)}