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, Boudewijn R.H.M.; Hermanns, H.; Katoen, Joost P. / Model checking for performability.

In: Mathematical structures in computer science, 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",
journal = "Mathematical structures in computer science",
issn = "0960-1295",
publisher = "Cambridge University Press",
number = "Special Issue 04",

}

Baier, C, Hahn, EM, Haverkort, BRHM, Hermanns, H & Katoen, JP 2013, 'Model checking for performability' Mathematical structures in computer science, 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.

In: Mathematical structures in computer science, 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

JO - Mathematical structures in computer science

T2 - Mathematical structures in computer science

JF - Mathematical structures in computer science

SN - 0960-1295

IS - Special Issue 04

ER -

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