A tool for model-checking Markov chains

Share/Save/Bookmark

Hermanns, H. and Katoen, J.P. and Meyer-Kayser, J. and Siegle, M. (2003) A tool for model-checking Markov chains. Int. Journal on Software Tools for Technology Transfer, 4 (2). pp. 153-172. ISSN 1433-2779

[img]
Preview
PDF
469Kb
Abstract:Markov chains are widely used in the context of the performance and reliability modeling of various systems. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both discrete [34, 10] and continuous time settings [7, 12]. In this paper, we describe a prototype model checker for discrete and continuous-time Markov chains, the Erlangen-Twente Markov Chain Checker EÎMC2, where properties are expressed in appropriate extensions of CTL. We illustrate the general benefits of this approach and discuss the structure of the tool. Furthermore, we report on successful applications of the tool to some examples, highlighting lessons learned during the development and application of EÎMC2.
Item Type:Article
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/66260
Official URL:http://dx.doi.org/10.1007/s100090100072
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page