Model checking for performability

C Baier, E.M. Hahn, Boudewijn R.H.M. Haverkort, H. Hermanns, Joost P. Katoen

Research output: Contribution to journalArticleAcademicpeer-review

13 Citations (Scopus)

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
Publication statusPublished - Aug 2013

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. 2013 ; Vol. 23, No. Special Issue 04. pp. 751-795.
@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",
language = "Undefined",
volume = "23",
pages = "751--795",
journal = "Mathematical structures in computer science",
issn = "0960-1295",
publisher = "Cambridge University Press",
number = "Special Issue 04",

}

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: Contribution to journalArticleAcademicpeer-review

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

JF - Mathematical structures in computer science

SN - 0960-1295

IS - Special Issue 04

ER -