In this paper we investigate the generation of counterexamples for discrete-time Markov chains (DTMCs) and PCTL properties. Whereas most available methods use explicit representations for at least some intermediate results, our aim is to develop fully symbolic algorithms. As in most related work, our counterexample computations are based on path search. We first adapt bounded model checking as a path search algorithm and extend it with a novel SAT-solving heuristics to prefer paths with higher probabilities. As a second approach, we use symbolic graph algorithms to find counterexamples. Experiments show that our approaches, in contrast to other existing techniques, are applicable to very large systems with millions of states. © 2013 Springer-Verlag.
CITATION STYLE
Jansen, N., Ábrahám, E., Zajzon, B., Wimmer, R., Schuster, J., Katoen, J. P., & Becker, B. (2013). Symbolic counterexample generation for discrete-time Markov chains. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7684 LNCS, pp. 134–151). https://doi.org/10.1007/978-3-642-35861-6_9
Mendeley helps you to discover research relevant for your work.