author = {Wolfgang Schreiner},
title = {{Experiments with Measuring Time in PRISM 4.0 (Addendum)}},
language = {english},
abstract = { In our previous paper “Experiments with Measuring Time in PRISM 4.0” we have re- ported on experiments with the probabilistic symbol model checker PRISM 4.0 on evalu- ating the response times of client/server system models. In that report some questions re- mained unresolved, in particular an unexpected result in the analysis of Probabilistic Timed Automata (PTA) in PRISM, and an unexplained discrepancy between explicit time mea- surement and results derived from queueing theory (by application of Little’s Law) in the analysis of a simple client/server model. In this addendum to that paper these open ques- tions are addressed and (essentially) solved. In particular, it is shown that expected time analysis by explicit time measurement in PRISM is more complex than previously thought such that the application of Little’s Law still has its merit. },
year = {2013},
month = {April},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {Supported by the project HU 10/2012 of the Austrian Academic Exchange Service (ÖAD).},
length = {14}