Model Checking Performability Properties
From International Center for Computational Logic
Model Checking Performability Properties
Boudewijn R. HaverkortBoudewijn R. Haverkort, Lucia ClothLucia Cloth, Holger HermannsHolger Hermanns, Joost-Pieter KatoenJoost-Pieter Katoen, Christel BaierChristel Baier
Boudewijn R. Haverkort, Lucia Cloth, Holger Hermanns, Joost-Pieter Katoen, Christel Baier
Model Checking Performability Properties
International Conference on Dependable Systems and Networks (DSN), 103--112, 2002. IEEE Computer Society
Model Checking Performability Properties
International Conference on Dependable Systems and Networks (DSN), 103--112, 2002. IEEE Computer Society
- KurzfassungAbstract
Model checking has been introduced as an automated technique to verify whether functional properties, expressed in a formal logic like computational tree logic (CTL), do hold in a formally-specified system. We present a number of computational procedures to perform model checking of continuous stochastic reward logic (CSRL) over finite Markov reward models, thereby stressing their computational complexity (time and space) and applicability from a practical point of view (accuracy, stability). A case study in the area of ad hoc mobile computing under power constraints shows the merits of CSRL and the new computational procedures. - Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science
@inproceedings{HCHKB2002,
author = {Boudewijn R. Haverkort and Lucia Cloth and Holger Hermanns and
Joost-Pieter Katoen and Christel Baier},
title = {Model Checking Performability Properties},
booktitle = {International Conference on Dependable Systems and Networks (DSN)},
publisher = {IEEE Computer Society},
year = {2002},
pages = {103--112},
doi = {10.1109/DSN.2002.1028891}
}