A probabilistic real-time calculus for performance evaluation

In this paper we develop a probabilistic real-time calculus for performance evaluation. The calculus applies a simple generative model of probabilities. Next to probabilistic action transitions, probabilistic time transitions are supported. An operational characterization is given in terms of a labelled transition system. The operational rules for the real-time part of the calculus are constructed in such a way, that the transition system can be interpreted as a discrete-time Markov chain. They further yield a constructive approach towards the efficient execution of processes and generation of transition graphs. On top of the operational rules, bisimulation equivalence is defined and proven to be a congruence for all operators. We define three different performance characteristics in terms of reward functions and prove that equivalent processes have an identical performance. Using an ergodic theorem of Markov chains, we further show how these performance figures can be computed in practice. We introduce an experimental software tool and we show how it can be applied to calculate the performance of a nontrivial real-time data communication protocol.