A Probabilistic Real-time Calculus for Performance Evaluation

systems, formal specification. In this paper we develop a probabilistic real-time calculus for performance evaluation. The calculus applies a simple gener-ative model of probabilities. Next to probabilistic action tran-sitions, probabilistic time transitions are supported. An opera-tional characterization is given in terms of a labelled transition system. The operational rules for the real-time part of the cal-culus are constructed in such a way, that the transition system can be interpreted as a discrete-time Markov chain. They fur-ther yield a constructive approach towards the efficient execu-tion 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 dif-ferent performance characteristics in terms of reward functions and prove that equivalent processes have an identical perfor-mance. Using an ergodic theorem of Markov chains, we further show how these performance figures can be computed in prac-tice. We introduce an experimental software tool and we show how it can be applied to calculate the performance of a non-trivial real-time data communication protocol.