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

80 Citations (Scopus)
30 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

Performability
Reward
Logic
Dependability
Specification
Continuous-time Markov Chain
Duality Theorems
Model Checking
Continuous Time
Markov chain
Express
Imply
Evaluation
Model

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
Baier, Christel ; Haverkort, Boudewijn ; Hermanns, Holger ; Katoen, Joost P. / On the Logical Characterisation of Performability Properties. Automata, Languages and Programming: 27th International Colloquium, ICALP 2000 Geneva, Switzerland, July 9–15, 2000 Proceedings. editor / Ugo Montanari ; José D.P. Rolin ; Emo Welzl. Berlin : Springer, 2000. pp. 780-792 (Lecture Notes in Computer Science).
@inproceedings{c5af6269d0cc48c0bc6e5535064e2744,
title = "On the Logical Characterisation of Performability Properties",
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.",
keywords = "FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, FMT-MC: MODEL CHECKING, METIS-119647, IR-19124, EWI-7915, FMT-PM: PROBABILISTIC METHODS",
author = "Christel Baier and Boudewijn Haverkort and Holger Hermanns and Katoen, {Joost P.}",
note = "Imported from research group DACS (ID number 477)",
year = "2000",
month = "7",
doi = "10.1007/3-540-45022-X_65",
language = "English",
isbn = "978-3-540-67715-4",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "780--792",
editor = "Ugo Montanari and Rolin, {Jos{\'e} D.P.} and Emo Welzl",
booktitle = "Automata, Languages and Programming",

}

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

On the Logical Characterisation of Performability Properties. / Baier, Christel; Haverkort, Boudewijn; Hermanns, Holger; Katoen, Joost P.

Automata, Languages and Programming: 27th International Colloquium, ICALP 2000 Geneva, Switzerland, July 9–15, 2000 Proceedings. ed. / Ugo Montanari; José D.P. Rolin; Emo Welzl. Berlin : Springer, 2000. p. 780-792 (Lecture Notes in Computer Science; Vol. 1853).

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

TY - GEN

T1 - On the Logical Characterisation of Performability Properties

AU - Baier, Christel

AU - Haverkort, Boudewijn

AU - Hermanns, Holger

AU - Katoen, Joost P.

N1 - Imported from research group DACS (ID number 477)

PY - 2000/7

Y1 - 2000/7

N2 - 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.

AB - 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.

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - FMT-MC: MODEL CHECKING

KW - METIS-119647

KW - IR-19124

KW - EWI-7915

KW - FMT-PM: PROBABILISTIC METHODS

U2 - 10.1007/3-540-45022-X_65

DO - 10.1007/3-540-45022-X_65

M3 - Conference contribution

SN - 978-3-540-67715-4

T3 - Lecture Notes in Computer Science

SP - 780

EP - 792

BT - Automata, Languages and Programming

A2 - Montanari, Ugo

A2 - Rolin, José D.P.

A2 - Welzl, Emo

PB - Springer

CY - Berlin

ER -

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