On the Logical Characterisation of Performability Properties

Christel Baier, Boudewijn Haverkort, Holger Hermanns, Joost P. Katoen, Ugo Montanari (Editor), José D.P. Rolin (Editor), Emo Welzl (Editor)

Research output: Other contribution

82 Citations (Scopus)

Abstract

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 [#!ASS+96!#,#!BKH99!#], 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 continuo us-time Markov chain, so that model checking procedures for CSL [#!BKH99!#,#!BHHK00!#] can be employed.
Original languageEnglish
PublisherSpringer
Number of pages13
Place of PublicationBerlin
ISBN (Print)978-3-540-67715-4
DOIs
Publication statusPublished - Jul 2000
Externally publishedYes

Keywords

  • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
  • FMT-MC: MODEL CHECKING
  • METIS-119647
  • IR-19124
  • EWI-7915
  • FMT-PM: PROBABILISTIC METHODS

Fingerprint Dive into the research topics of 'On the Logical Characterisation of Performability Properties'. Together they form a unique fingerprint.

Cite this