Model checking for performability

作者:Baier C*; Hahn E M; Haverkort B R; Hermanns H; Katoen J P
来源:Mathematical Structures in Computer Science, 2013, 23(4): 751-795.
DOI:10.1017/S0960129512000254

摘要

This paper gives a bird%26apos;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.

  • 出版日期2013-8