The COMICS tool -- computing minimal counterexamples for DTMCs This paper presents the tool COMICS 1.0, 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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 3 articles , 1 standard article )

Showing results 1 to 3 of 3.
Sorted by year (citations)

  1. Ábrahám, Erika; Becker, Bernd; Dehnert, Christian; Jansen, Nils; Katoen, Joost-Pieter; Wimmer, Ralf: Counterexample generation for discrete-time Markov models: an introductory survey (2014)
  2. Wimmer, Ralf; Jansen, Nils; Ábrahám, Erika; Katoen, Joost-Pieter; Becker, Bernd: Minimal counterexamples for linear-time probabilistic verification (2014)
  3. Jansen, Nils; Ábrahám, Erika; Volk, Matthias; Wimmer, Ralf; Katoen, Joost-Pieter; Becker, Bernd: The COMICS tool -- computing minimal counterexamples for DTMCs (2012) ioport