Abstract (click to show/hide)
We
introduce a novel stochastic process algebra, called PHASE, which
directly supports phasetype distributions, useful for approximating
the dynamics of nonMarkovian HCI systems. In order to encourage the
effective use of PHASE, we give a step by step account of how PHASE
processes can be implemented in PRISM, one of the most powerful and
popular probabilistic model checkers currently available. Furthermore,
we provide a case study involving a nonMarkovian interactive system,
as a means of highlighting the advantages of phasetype approximations,
in comparison to approximating nonMarkovian transitions through single
Markovian transitions.
