DiPro
| swMATH ID: | 9744 |
| Software Authors: | Aljazzar, Husain; Leitner-Fischer, Florian; Leue, Stefan; Simeonov, Dimitar |
| Description: | 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. |
| Homepage: | http://link.springer.com/chapter/10.1007/978-3-642-22306-8_13 |
| Related Software: | PRISM; COMICS; z3; MRMC; CEGAR; Gurobi; SCIP; CPLEX; LTL2BA; cvc3; LiQuor |
| Cited in: | 4 Documents |
all
top 5
Cited by 10 Authors
| 2 | Ábrahám, Erika |
| 2 | Becker, Bernd |
| 2 | Jansen, Nils |
| 2 | Katoen, Joost-Pieter |
| 2 | Wimmer, Ralf D. |
| 1 | Baier, Christel |
| 1 | Debbi, Hichem |
| 1 | Dehnert, Christian |
| 1 | Funke, Florian |
| 1 | Jantsch, Simon |
Cited in 2 Serials
| 1 | Computing |
| 1 | Theoretical Computer Science |
Cited in 3 Fields
| 4 | Computer science (68-XX) |
| 2 | Probability theory and stochastic processes (60-XX) |
| 2 | Operations research, mathematical programming (90-XX) |
