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.
Original language | English |
---|---|
Pages (from-to) | 153-172 |
Number of pages | 20 |
Journal | International journal on software tools for technology transfer |
Volume | 4 |
Issue number | 2 |
DOIs | |
Publication status | Published - 2003 |
Keywords
- FMT-MC: MODEL CHECKING
- FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
- FMT-PM: PROBABILISTIC METHODS
- Markov chain
- Model checking
- Numerical mathematics
- Performance evaluation
- Probabilistic systems
- Temporal logic