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.
Original languageUndefined
Pages (from-to)751-795
Number of pages45
JournalMathematical structures in computer science
Volume23
Issue numberSpecial Issue 04
DOIs
StatePublished - Aug 2013

Fingerprint

Model checking
Temporal logic
Stochastic models

Keywords

  • EC Grant Agreement nr.: FP7/318490
  • EC Grant Agreement nr.: FP7/2007-2013
  • IR-87378
  • METIS-299989
  • EWI-23612

Cite this

Baier, C., Hahn, E. M., Haverkort, B. R. H. M., Hermanns, H., & Katoen, J. P. (2013). Model checking for performability. 23(Special Issue 04), 751-795. DOI: 10.1017/S0960129512000254

Baier, C; Hahn, E.M.; Haverkort, Boudewijn R.H.M.; Hermanns, H.; Katoen, Joost P. / Model checking for performability.

Vol. 23, No. Special Issue 04, 08.2013, p. 751-795.

Research output: Scientific - peer-reviewArticle

@article{5e6edea216bd4c24a2ab1e3e10f3f979,
title = "Model checking for performability",
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.",
keywords = "EC Grant Agreement nr.: FP7/318490, EC Grant Agreement nr.: FP7/2007-2013, IR-87378, METIS-299989, EWI-23612",
author = "C Baier and E.M. Hahn and Haverkort, {Boudewijn R.H.M.} and H. Hermanns and Katoen, {Joost P.}",
note = "eemcs-eprint-23612",
year = "2013",
month = "8",
doi = "10.1017/S0960129512000254",
volume = "23",
pages = "751--795",
number = "Special Issue 04",

}

Baier, C, Hahn, EM, Haverkort, BRHM, Hermanns, H & Katoen, JP 2013, 'Model checking for performability' vol 23, no. Special Issue 04, pp. 751-795. DOI: 10.1017/S0960129512000254

Model checking for performability. / Baier, C; Hahn, E.M.; Haverkort, Boudewijn R.H.M.; Hermanns, H.; Katoen, Joost P.

Vol. 23, No. Special Issue 04, 08.2013, p. 751-795.

Research output: Scientific - peer-reviewArticle

TY - JOUR

T1 - Model checking for performability

AU - Baier,C

AU - Hahn,E.M.

AU - Haverkort,Boudewijn R.H.M.

AU - Hermanns,H.

AU - Katoen,Joost P.

N1 - eemcs-eprint-23612

PY - 2013/8

Y1 - 2013/8

N2 - 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.

AB - 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.

KW - EC Grant Agreement nr.: FP7/318490

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - IR-87378

KW - METIS-299989

KW - EWI-23612

U2 - 10.1017/S0960129512000254

DO - 10.1017/S0960129512000254

M3 - Article

VL - 23

SP - 751

EP - 795

IS - Special Issue 04

ER -

Baier C, Hahn EM, Haverkort BRHM, Hermanns H, Katoen JP. Model checking for performability. 2013 Aug;23(Special Issue 04):751-795. Available from, DOI: 10.1017/S0960129512000254