DTMC Model Checking by SCC Reduction


Nils Jansen, Theorie Hybrider Systeme

Title DTMC Model Checking by SCC Reduction
When 22.04.2010
Where Lecture Room Informatik 11
Abstract 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.

We introduce a model checking algorithm for DTMCs that also supports the generation of counterexamples. Our algorithm, based on the detection and abstraction of strongly connected components, offers abstract counterexamples, which can be interactively refined by the user.