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  and the continuous time setting , . In this short paper, we describe the prototype model checker $E \vdash M C^2$ for discrete and continuous-time Markov chains, where properties are expressed in appropriate extensions of CTL.We illustrate the general benefits of this approach and discuss the structure of the tool.
|Title of host publication||Proceedings of the 2nd PROGRESS Workshop on Embedded Systems 2001|
|Place of Publication||Veldhoven, the Netherlands|
|Number of pages||6|
|Publication status||Published - 2001|
|Event||2nd PROGRESS Workshop on Embedded Systems 2001 - Veldhoven, Netherlands|
Duration: 18 Oct 2001 → 18 Oct 2001
Conference number: 2
|Workshop||2nd PROGRESS Workshop on Embedded Systems 2001|
|Period||18/10/01 → 18/10/01|
- FMT-PM: PROBABILISTIC METHODS
- FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
- FMT-MC: MODEL CHECKING
- FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
Hermanns, H., Karelse, F. (Ed.), Katoen, J. P., Meyer-Kayser, J., & Siegle, M. (2001). A model checker for performance and dependability properties. In Proceedings of the 2nd PROGRESS Workshop on Embedded Systems 2001 (pp. 83-88). Veldhoven, the Netherlands: STW.