Non-Markovian systems are usually difficult to represent and analyse using currently available stochastic process calculi. By relying on a combination between the newly introduced process algebra PHASE and the probabilistic model checker PRISM, we examine the dynamics of one such system, which involves a collaborative text review performed by two manuscript editors, and focus on the derivation of quantitative performance measures. We find that approximating non-Markovian transitions through single Markovian transitions is fast, but inaccurate, while employing more complex phase-type approximations is somewhat slow, but considerably more precise.
展开▼
