The automated quantitative system analysis in terms of probabilistic model checking (PMC) is nowadays well-established and has been applied successfully in various areas. Recently, we showed how PMC can be applied for the trade-off analysis between several cost and reward functions, such as energy and utility. Besides utility, also the resilience of a system, i.e., the systems capability to operate successfully even in unfavorable conditions, crucially depends on costs invested: It is well-known that better resilience can be achieved, e.g., through introducing redundant components, which however may yield higher energy consumption.

In this paper, we focus on the interplay energy, utility and resilience. The formalization of the resulting trade-offs requires several concepts like quantiles, conditional probabilities and expectations and ratios of cost or reward functions. We present an overview how these quantitative measures for resilience mechanisms can be computed when the resilient systems are modeled either as discrete or continuous-time Markov chains. All the presented concepts of multi-objective reasoning are not supported by state-of-the-art probabilistic model checkers yet. By means of a small case study following the modular redundancy principle, we exemplify a resilience analysis within our prototype implementations.