On the Logical Characterisation of Performability Properties

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

DOI Link

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

Details
Bibtex

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