Name
Abstract | ||
|---|---|---|
This paper presents several symbolic counterexample generation algorithms for discrete-time Markov chains (DTMCs) violating a PCTL formula. A counterexample is (a symbolic representation of) a sub-DTMC that is incrementally generated. The crux to this incremental approach is the symbolic generation of paths that belong to the counterexample. We consider two approaches. First, we extend bounded model checking and develop a simple heuristic to generate highly probable paths first. We then complement the SAT-based approach by a fully (multi-terminal) BDD-based technique. All symbolic approaches are implemented, and our experimental results show a substantially better scalability than existing explicit techniques. In particular, our BDD-based approach using a method called fragment search allows for counterexample generation for DTMCs with billions of states (up to 1015). |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1016/j.scico.2014.02.001 | Science of Computer Programming |
Keywords | Field | DocType |
Markov chain,Counterexample,Model checking,Binary decision diagram | Heuristic,Model checking,Computer science,Markov chain,Algorithm,Binary decision diagram,Theoretical computer science,Discrete time and continuous time,Counterexample,Symbolic trajectory evaluation,Bounded function | Journal |
Volume | ISSN | Citations |
91 | 0167-6423 | 7 |
PageRank | References | Authors |
0.44 | 39 | 7 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Nils Jansen | 1 | 284 | 27.77 |
| Ralf Wimmer | 2 | 407 | 34.28 |
| Erika Ábrahám | 3 | 830 | 63.17 |
| Barna Zajzon | 4 | 11 | 0.84 |
| Joost-Pieter Katoen | 5 | 4444 | 289.65 |
| Bernd Becker | 6 | 855 | 73.74 |
| Johann Schuster | 7 | 28 | 3.69 |