Model Checking for Performability

Publikation: Beitrag in FachzeitschriftForschungsartikelBeigetragenBegutachtung

Beitragende

  • Christel Baier - , Professur für Algebraische und logische Grundlagen der Informatik (Autor:in)
  • Ernst Moritz Hahn - , Universität des Saarlandes (Autor:in)
  • Boudewijn R. Haverkort - , Eindhoven University of Technology, University of Twente (Autor:in)
  • Holger Herrmanns - , Universität des Saarlandes (Autor:in)
  • Jost-Pieter Katoen - , University of Twente, Rheinisch-Westfälische Technische Hochschule Aachen (Autor:in)

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.

Details

OriginalspracheEnglisch
Seiten (von - bis)751-795
Seitenumfang45
FachzeitschriftMathematical Structures in Computer Science
Jahrgang23
Ausgabenummer4
PublikationsstatusVeröffentlicht - 2013
Peer-Review-StatusJa

Externe IDs

Scopus 84880212844
ORCID /0000-0002-5321-9343/work/142236666

Schlagworte

Schlagwörter

  • Model Checking, Performability