Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-22306-8_13 | SPIN |
Keywords | Field | DocType |
available tool,open source tool,discrete time markov chain,markov decision process,probabilistic model checking,active research,probabilistic counterexample generation,computed counterexamples,mrmc probabilistic model checker,continuous time markov chain,probabilistic counterexamples,counterexamples | Computer science,Markov chain,Markov decision process,Probabilistic CTL,Algorithm,Statistical model,Counterexample,Discrete time and continuous time,Probabilistic logic,Computation | Conference |
Citations | PageRank | References |
13 | 0.59 | 13 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Husain Aljazzar | 1 | 212 | 9.05 |
| Florian Leitner-Fischer | 2 | 119 | 7.38 |
| Stefan Leue | 3 | 1199 | 108.55 |
| Dimitar Simeonov | 4 | 17 | 1.13 |