Model Checking Performability Properties

Boudewijn R. HaverkortBoudewijn R. Haverkort, Lucia ClothLucia Cloth, Holger HermannsHolger Hermanns, Joost-Pieter KatoenJoost-Pieter Katoen, Christel BaierChristel Baier

DOI Link

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

Details
Bibtex

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}
}