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.

Preview

PDF
274Kb

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
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Design and Analysis of Communication Systems (DACS) Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/19124
Official URL:	http://dx.doi.org/10.1007/3-540-45022-X_65
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 119647