Inproceedings3713957571: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Johannes Lehmann (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Christel |ErsterAutorNachname=Baier |FurtherAuthors=Boudewijn R. Haverkort; Holger Hermanns; Joost-Pieter Katoen}} {{Inproceedings |Booktitle=27th International Colloquium on Automata, Languages and Programming (ICALP) |Pages=780--792 |Publisher=Springer |Series=Lecture Notes in Computer Science |Title=On the Logical Characterisation of Performability Properties |Volume=1853 |Year=2000 }} {{Publi…“) |
Johannes Lehmann (Diskussion | Beiträge) K (Textersetzung - „Verifikation und formale quantitative Analyse“ durch „Algebraische und logische Grundlagen der Informatik“) |
||
| Zeile 15: | Zeile 15: | ||
|DOI Name=10.1007/3-540-45022-X_65 | |DOI Name=10.1007/3-540-45022-X_65 | ||
|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 [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. | |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 [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= | |Forschungsgruppe=Algebraische und logische Grundlagen der Informatik | ||
}} | }} | ||
Aktuelle Version vom 5. März 2025, 14:40 Uhr
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
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
@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}
}
