On the Logical Characterisation of Performability Properties

Christel Baier, Boudewijn Haverkort, Holger Hermanns, Joost P. Katoen

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    81 Citations (Scopus)
    46 Downloads (Pure)

    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
    Title of host publicationAutomata, Languages and Programming
    Subtitle of host publication27th International Colloquium, ICALP 2000 Geneva, Switzerland, July 9–15, 2000 Proceedings
    EditorsUgo Montanari, José D.P. Rolin, Emo Welzl
    Place of PublicationBerlin
    PublisherSpringer
    Pages780-792
    Number of pages13
    ISBN (Electronic)978-3-540-45022-1
    ISBN (Print)978-3-540-67715-4
    DOIs
    Publication statusPublished - Jul 2000
    Event27th International Colloquium on Automata, Languages and Programming, ICALP 2000 - Geneva, Switzerland
    Duration: 9 Jul 200015 Jul 2000
    Conference number: 27

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume1853
    ISSN (Print)0302-9743

    Conference

    Conference27th International Colloquium on Automata, Languages and Programming, ICALP 2000
    Abbreviated titleICALP
    CountrySwitzerland
    CityGeneva
    Period9/07/0015/07/00

      Fingerprint

    Keywords

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

    Cite this

    Baier, C., Haverkort, B., Hermanns, H., & Katoen, J. P. (2000). On the Logical Characterisation of Performability Properties. In U. Montanari, J. D. P. Rolin, & E. Welzl (Eds.), Automata, Languages and Programming: 27th International Colloquium, ICALP 2000 Geneva, Switzerland, July 9–15, 2000 Proceedings (pp. 780-792). (Lecture Notes in Computer Science; Vol. 1853). Berlin: Springer. https://doi.org/10.1007/3-540-45022-X_65