The COMICS Tool - Computing Minimal Counterexamples for Discrete-time Markov Chains
This work addresses the need for efficient counterexample generation in model checking for discrete-time Markov chains, but it appears incremental as it builds on existing abstraction and refinement techniques.
The authors tackled the problem of generating counterexamples for discrete-time Markov chains by developing the COMICS tool, which computes an abstract system and refines it hierarchically to produce critical subsystems, resulting in a tool with both command-line and graphical interfaces for interactive refinement.
This report presents the tool COMICS, which performs model checking and generates counterexamples for DTMCs. For an input DTMC, COMICS computes an abstract system that carries the model checking information and uses this result to compute a critical subsystem, which induces a counterexample. This abstract subsystem can be refined and concretized hierarchically. The tool comes with a command-line version as well as a graphical user interface that allows the user to interactively influence the refinement process of the counterexample.