Model checking performability properties

Model checking has been introduced as an automated technique to verify, whether functional properties, expressed in a formal logic like computational tree logic (CTL), do hold in a formally-specified system. In recent years, we have extended CTL such that it allows for the specification of properties over finite-state continuous-time Markov chains (CTMCs). Computational techniques for model checking have been developed an successfully applied in the dependability context. Further work in this area has recently, led to the continuous stochastic reward logic (CSRL), a logic to specify, measures over CTMCs extended with a reward structure (so-called Markov reward models). Well-known performability measures, most notably, also Meyer's performability distribution, can be easily, defined with CSRL. However, using CSRL it is possible to specify performability measures that have not yet been addressed in the literature, hence, for which no computational procedures have been developed Yet. In this paper we present a number of computational procedures to perforin model checking of CSRL over finite Markov reward models, thereby, stressing their computational complexity, (time and space) and applicability, from a practical point of view (accuracy, stability). A case study, in the area of ad hoc mobile computing under power constraints shows the merits of CSRL and the new computational procedures.