DTMC Model Checking by SCC Reduction

9 years 11 months ago
DTMC Model Checking by SCC Reduction
Discrete-Time Markov Chains (DTMCs) are a widely-used formalism to model probabilistic systems. On the one hand, available tools like PRISM or MRMC offer efficient model checking algorithms and thus support the verification of DTMCs. However, these algorithms do not provide any diagnostic information in the form of counterexamples, which are highly important for the correction of erroneous systems. On the other hand, there exist several approaches to generate counterexamples for DTMCs, but all these approaches require the model checking result for completeness. In this paper we introduce a model checking algorithm for DTMCs that also supports the generation of counterexamples. rithm, based on the detection and abstraction of strongly d components, offers abstract counterexamples, which can be interactively refined by the user.
Erika Ábrahám, Nils Jansen, Ralf Wim
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where QEST
Authors Erika Ábrahám, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
Comments (0)