[BaierHHHK13] Model Checking for Performability Baier, C.; Hahn, E. M.; Haverkort, B. R. and Katoen, H. H. J.-P. In Mathematical Structures in Computer Science, 23: 751-795, 2013.
Downloads: pdf, bibURL: http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=8951476 Abstract. This paper gives a bird's-eye view of the various ingredients that make up a modern, model-checking-based approach to performability evaluation: Markov reward models, temporal logics and continuous stochastic logic, model-checking algorithms, bisimulation and the handling of non-determinism. A short historical account as well as a large case study complete this picture. In this way, we show convincingly that the smart combination of performability evaluation with stochastic model-checking techniques, developed over the last decade, provides a powerful and unified method of performability evaluation, thereby combining the advantages of earlier approaches.