COMICS: Computing Minimal Counterexamples for Discrete-Time Markov Chains

COMICS is a stand-alone tool which performs model checking and the generation of counterexamples for discrete-time Markov Chains (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 which allows the user to interactively influence the refinement process of the counterexample.

Documentation

The user manual is available here.

Authors

COMICS was developed and is maintained by Nils Jansen, Erika Ábrahám, Jens Katelaan, Maik Scheffler, Matthias Volk and Andreas Vorpahl.

Contact

For any questions, feedback and support requests regarding COMICS, please contact Nils Jansen.