In the context of a multi-disciplinary project, where we contribute with formal methods for reasoning about energy-awareness and other quantitative aspects of low-level resource management protocols, we made a series of interesting observations on the strengths and limitations of probabilistic model checking. To our surprise, the operating-system experts identified several relevant quantitative measures that are not supported by state-of-the-art probabilistic model checkers. Most notably are conditional probabilities and quantiles. Both are standard in mathematics and statistics, but research on them in the context of probabilistic model checking is rare. Another deficit of standard probabilistic model-checking techniques was the lack of methods for establishing properties imposing constraints on the energy-utility ratio.

In this article, we will present formalizations of the above mentioned quantitative measures, illustrate their significance by means of examples and sketch computation methods that we developed in our recent work.