The COMICS Tool - Computing Minimal Counterexamples for Discrete-time Markov Chains

TL;DR

The paper introduces COMICS, a tool for model checking discrete-time Markov chains that computes minimal counterexamples through hierarchical abstraction and refinement, aiding in debugging probabilistic models.

Contribution

COMICS is the first tool to compute minimal counterexamples for DTMCs using hierarchical abstraction and interactive refinement.

Findings

Successfully computes minimal counterexamples for DTMCs

Supports hierarchical abstraction and refinement

Provides both command-line and GUI interfaces

Abstract

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.