A Markov Chain Model Checker

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

• Type: Conference
• Year: 2000
• Where: TACAS
• Authors: Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle
• Keywords: Algorithms, Markov Chain, Markov Chain Checker, TACAS 2000, Temporal Logic Formula