A Markov Chain Model Checker


Share/Save/Bookmark

Hermanns, Holger and Katoen, Joost-Pieter and Meyer-Kayser, Joachim and Siegle, M. (2000) A Markov Chain Model Checker. In: 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000, 27-31 March 2000, Berlin, Germany.

[img]
Preview
PDF
522Kb
Abstract:Markov chains are widely used in the context of performance and reliability evaluation of systems of various nature. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both the discrete [17,6] and the continuous time setting [4,8]. In this paper, we describe a prototype model checker for discrete and continuous-time Markov chains, the Erlangen Twente Markov Chain Checker $(E    \vdash MC^2$), where properties are expressed in appropriate extensions of CTL. We illustrate the general bene ts of this approach and discuss the structure of the tool. Furthermore we report on first successful applications of the tool to non-trivial examples, highlighting lessons learned during development and application of $(E \vdash MC^2$).
Item Type:Conference or Workshop Item
Copyright:© 2000 Springer
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/66266
Official URL:http://dx.doi.org/10.1007/3-540-46419-0
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 119649