On the Logical Characterisation of Performability Properties

From International Center for Computational Logic

Toggle side column

On the Logical Characterisation of Performability Properties

Christel BaierChristel Baier,  Boudewijn R. HaverkortBoudewijn R. Haverkort,  Holger HermannsHolger Hermanns,  Joost-Pieter KatoenJoost-Pieter Katoen
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen
On the Logical Characterisation of Performability Properties
27th International Colloquium on Automata, Languages and Programming (ICALP), volume 1853 of Lecture Notes in Computer Science, 780--792, 2000. Springer
  • KurzfassungAbstract
    Markov-reward models, as extensions of continuous-time Markov chains, have received increased attention for the specification and evaluation of performance and dependability properties of systems. Until now, however, the specification of reward-based performance and dependability measures has been done manually and informally. In this paper, we change this undesirable situation by the introduction of a continuous-time, reward-based stochastic logic. We argue that this logic is adequate for expressing performability measures of a large variety. We isolate two important sub-logics, the logic CSL [1,3], and the novel logic CRL that allows one to express reward-based properties. These logics turn out to be complementary, which is formally established in our main duality theorem. This result implies that reward-based properties expressed in CRL for a particular Markov reward model can be interpreted as CSL properties over a derived continuous-time Markov chain, so that model checking procedures for CSL [3,2] can be employed.
  • Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science
The final publication is available at Springer via http://dx.doi.org/10.1007/3-540-45022-X_65.
@inproceedings{BHHK2000,
  author    = {Christel Baier and Boudewijn R. Haverkort and Holger Hermanns and
               Joost-Pieter Katoen},
  title     = {On the Logical Characterisation of Performability Properties},
  booktitle = {27th International Colloquium on Automata, Languages and
               Programming (ICALP)},
  series    = {Lecture Notes in Computer Science},
  volume    = {1853},
  publisher = {Springer},
  year      = {2000},
  pages     = {780--792},
  doi       = {10.1007/3-540-45022-X_65}
}