Model checking for performability

C. Baier, E.M. Hahn, B.R. Haverkort, H. Hermanns, J.-P. Katoen

Research output: Contribution to journalArticleAcademicpeer-review

14 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 languageEnglish
Pages (from-to)751-795
Number of pages45
JournalMathematical structures in computer science
Volume23
Issue numberSpecial Issue 04
DOIs
Publication statusPublished - Aug 2013

Fingerprint

Performability
Model checking
Model Checking
Evaluation
Temporal logic
Nondeterminism
Bisimulation
Stochastic models
Temporal Logic
Reward
Stochastic Model
Logic
Model

Keywords

  • EC Grant Agreement nr.: FP7/318490
  • EC Grant Agreement nr.: FP7/2007-2013

Cite this

Baier, C. ; Hahn, E.M. ; Haverkort, B.R. ; Hermanns, H. ; Katoen, J.-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",
author = "C. Baier and E.M. Hahn and B.R. Haverkort and H. Hermanns and J.-P. Katoen",
year = "2013",
month = "8",
doi = "10.1017/S0960129512000254",
language = "English",
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, B.R.; Hermanns, H.; Katoen, J.-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, B.R.

AU - Hermanns, H.

AU - Katoen, J.-P.

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

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 -