Abstract
This paper introduces a novel counterexample generation approach for the verification of discrete-time Markov chains (DTMCs) with two main advantages: (1) We generate abstract counterexamples which can be refined in a hierarchical manner. (2) We aim at minimizing the number of states involved in the counterexamples, and compute a critical subsystem of the DTMC whose paths form a counterexample. Experiments show that with our approach we can reduce the size of counterexamples and the number of computation steps by several orders of magnitude. © 2011 Springer-Verlag.
Cite
CITATION STYLE
Jansen, N., Ábrahám, E., Katelaan, J., Wimmer, R., Katoen, J. P., & Becker, B. (2011). Hierarchical counterexamples for discrete-time Markov chains. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6996 LNCS, pp. 443–452). https://doi.org/10.1007/978-3-642-24372-1_33
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
