On the Logical Characterisation of Performability Properties


Baier, Christel and Haverkort, Boudewijn and Hermanns, Holger and Katoen, Joost-Pieter (2000) On the Logical Characterisation of Performability Properties. In: 27th International Colloquium on Automata, Languages and Programming, ICALP 2000, Geneva, Switzerland (pp. pp. 780-792).

open access
Abstract:Markov-reward models, as extensions of continuous-time Markov chains, have received increased attention for the speci cation and evaluation of performance and dependability properties of systems. Until now, however, the speci cation 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 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
Item Type:Conference or Workshop Item
Copyright:© 2000 Springer-Verlag
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/19124
Official URL:https://doi.org/10.1007/3-540-45022-X_65
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 119647