DiPro - A Tool for Probabilistic Counterexample Generation. The computation of counterexamples for probabilistic model checking has been an area of active research over the past years. In spite of the achieved theoretical results in this field, there is no freely available tool that allows for the computation and representation of probabilistic counterexamples. We present an open source tool called DiPro that can be used with the PRISM and MRMC probabilistic model checkers. It allows for the computation of probabilistic counterexamples for discrete time Markov chains (DTMCs), continuous time Markov chains (CTMCs) and Markov decision processes (MDPs). The computed counterexamples can be rendered graphically.
Keywords for this software
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- Á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)
- Wimmer, Ralf; Jansen, Nils; Ábrahám, Erika; Katoen, Joost-Pieter; Becker, Bernd: Minimal counterexamples for linear-time probabilistic verification (2014)
- Jansen, Nils; Ábrahám, Erika; Volk, Matthias; Wimmer, Ralf; Katoen, Joost-Pieter; Becker, Bernd: The COMICS tool -- computing minimal counterexamples for DTMCs (2012) ioport
- Aljazzar, Husain; Leitner-Fischer, Florian; Leue, Stefan; Simeonov, Dimitar: Dipro -- A tool for probabilistic counterexample generation (2011) ioport