Blog
About

35
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

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

      Preprint

      Read this article at

      Bookmark
          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.

          Related collections

          Most cited references 5

          • Record: found
          • Abstract: not found
          • Article: not found

          A logic for reasoning about time and reliability

            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            The ins and outs of the probabilistic model checker MRMC

              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              Counterexample Generation in Probabilistic Model Checking

                Bookmark

                Author and article information

                Journal
                04 June 2012
                Article
                1206.0603

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                Custom metadata
                cs.SE

                Comments

                Comment on this article