Article2358732606: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Johannes Lehmann (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Christel |ErsterAutorNachname=Baier |FurtherAuthors=Ernst-Moritz Hahn; Boudewijn Haverkort; Holger Hermanns; Joost-Pieter Katoen}} {{Article |Journal=Mathematical Structures in Computer Science |Number=4 |Pages=751--795 |Title=Model Checking for Performability |Volume=23 |Year=2013 }} {{Publikation Details |DOI Name=10.1017/S0960129512000254 |Abstract=This paper gives a bird's-eye view of the va…“) |
Johannes Lehmann (Diskussion | Beiträge) K (Textersetzung - „Verifikation und formale quantitative Analyse“ durch „Algebraische und logische Grundlagen der Informatik“) |
||
Zeile 14: | Zeile 14: | ||
|DOI Name=10.1017/S0960129512000254 | |DOI Name=10.1017/S0960129512000254 | ||
|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. | |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. | ||
|Forschungsgruppe= | |Forschungsgruppe=Algebraische und logische Grundlagen der Informatik | ||
}} | }} |
Aktuelle Version vom 5. März 2025, 15:42 Uhr
Model Checking for Performability
Christel BaierChristel Baier, Ernst-Moritz HahnErnst-Moritz Hahn, Boudewijn HaverkortBoudewijn Haverkort, Holger HermannsHolger Hermanns, Joost-Pieter KatoenJoost-Pieter Katoen
Christel Baier, Ernst-Moritz Hahn, Boudewijn Haverkort, Holger Hermanns, Joost-Pieter Katoen
Model Checking for Performability
Mathematical Structures in Computer Science, 23(4):751--795, 2013
Model Checking for Performability
Mathematical Structures in Computer Science, 23(4):751--795, 2013
- KurzfassungAbstract
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. - Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science
@article{BHHHK2013,
author = {Christel Baier and Ernst-Moritz Hahn and Boudewijn Haverkort and
Holger Hermanns and Joost-Pieter Katoen},
title = {Model Checking for Performability},
journal = {Mathematical Structures in Computer Science},
volume = {23},
number = {4},
year = {2013},
pages = {751--795},
doi = {10.1017/S0960129512000254}
}