Name
Abstract | ||
|---|---|---|
Providing evidence for the refutation of a property is an essential, if not the most important, feature of model checking. This paper considers algorithms for counterexample generation for probabilistic CTL formulae in discrete-time Markov chains. Finding the strongest evidence (i.e., the most probable path) violating a (bounded) until-formula is shown to be reducible to a single-source (hop-constrained) shortest path problem. Counterexamples of smallest size that deviate most from the required probability bound can be obtained by applying (small amendments to) k-shortest (hop-constrained) paths algorithms. These results can be extended to Markov chains with rewards, to LTL model checking, and are useful for Markov decision processes. Experimental results show that typically the size of a counterexample is excessive. To obtain much more compact representations, we present a simple algorithm to generate (minimal) regular expressions that can act as counterexamples. The feasibility of our approach is illustrated by means of two communication protocols: leader election in an anonymous ring network and the Crowds protocol. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1109/TSE.2009.5 | IEEE Trans. Software Eng. |
Keywords | Field | DocType |
single-source shortest path problem,probabilistic model checking,trees (mathematics),model checking,probable path,discrete-time markov chain,providing evidence,ltl model checking,probabilistic logic,property refutation,linear temporal logic,decision theory,temporal logic,strongest evidence,markov decision process,diagnostics,smallest size,markov processes,markov chain,computation tree logic,formal verification,counterexample generation,k-shortest path algorithm,probability,shortest path problem,quantum computing,shortest path,logic,leader election,protocols,communication protocol,feedback,ring network,regular expression,distributed computing | Computation tree logic,Markov process,Model checking,Computer science,Markov chain,Probabilistic CTL,Markov decision process,Algorithm,Theoretical computer science,Counterexample,Probabilistic logic | Journal |
Volume | Issue | ISSN |
35 | 2 | 0098-5589 |
Citations | PageRank | References |
55 | 1.58 | 42 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tingting Han | 1 | 98 | 7.34 |
| Joost-Pieter Katoen | 2 | 4444 | 289.65 |
| Damman Berteun | 3 | 55 | 1.58 |