COmputing MInimal CounterexamleS 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.

Getting COMICS

Please go to the download page for binaries and sources as well as short instructions on how to start and compile COMICS.

Documentation

The user manual is available here.

Benchmarks

For a number of benchmarks, follow this link.

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.