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

Jansen, Nils; Scheffler, Maik; Volk, Matthias; Vorpahl, Andreas; Ábrahám, Erika; Becker, Bernd; Katoen, Joost-Pieter; Wimmer, Ralf D.

Record: found
Abstract: found
Article: found

Is Open Access

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

Preprint

Author(s): Nils Jansen, Maik Scheffler, Matthias Volk, Andreas Vorpahl, Erika Ábrahám, Bernd Becker, Joost-Pieter Katoen, Ralf D. Wimmer

Publication date: 2012-06-04

Read this article at

ScienceOpen ArXiv

There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

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.