Experiments with Measuring Time in PRISM 4.0 (Addendum)

Research output: Working paper and reportsPreprint

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.
Original languageEnglish
Place of PublicationHagenberg
PublisherRISC Hagenberg
Number of pages14
Publication statusPublished - Apr 2013

Publication series

NameRISC Report Series

Fields of science

  • 101001 Algebra
  • 101002 Analysis
  • 101 Mathematics
  • 102 Computer Sciences
  • 102011 Formal languages
  • 101009 Geometry
  • 101013 Mathematical logic
  • 101020 Technical mathematics
  • 101025 Number theory
  • 101012 Combinatorics
  • 101005 Computer algebra
  • 101006 Differential geometry
  • 101003 Applied geometry
  • 102025 Distributed systems

JKU Focus areas

  • Computation in Informatics and Mathematics

Cite this