Abstract
Probabilistic model checkers typically provide a list of individual state probabilities on the refutation of a temporal logic formula. For large state spaces, this information is far too detailed to act as useful diagnostic feedback. For quantitative (constrained) reachability problems, sets of paths that carry enough probability mass are more adequate. We recently have shown that in the context of discrete-time probabilistic processes, such sets of smallest size can be efficiently computed by (hop-constrained) k-shortest path algorithms. This paper considers the problem of generating counterexamples for continuous-time Markov chains. The key contribution is a set of approximate algorithms for computing small sets of paths that indicate the violation of time-bounded (constrained) reachability probabilities.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aljazzar, H., Hermanns, H., Leue, S.: Counterexamples for timed probabilistic reachability. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 177–195. Springer, Heidelberg (2005)
Aljazzar, H., Leue, S.: Extended directed search for probabilistic timed reachability. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 33–51. Springer, Heidelberg (2006)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Model-checking continous-time Markov chains. ACM Trans. Comput. Log. 1(1), 162–170 (2000)
Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524–541 (2003)
Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: LICS, pp. 19–29 (2002)
Dijkstra, E.W.: A note on two problems in connection with graphs. Num. Math. 1, 395–412 (1959)
Eppstein, D.: Finding the k shortest paths. SIAM J. Comput. 28(2), 652–673 (1998)
Fox, B.L., Glynn, P.W.: Computing Poisson probabilities. Comm. ACM 31(4), 440–445 (1988)
Gurfinkel, A., Chechik, M.: Proof-like counter-examples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 160–175. Springer, Heidelberg (2003)
Han, T., Katoen, J.-P.: Counterexamples in probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 72–86. Springer, Heidelberg (2007)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. 6(5), 512–535 (1994)
Jensen, A.: Markoff chains as an aid in the study of Markoff processes. Skand. Aktuarietidskrift 36, 87–91 (1953)
Katoen, J.-P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: QEST 2005, pp. 243–244. IEEE Computer Society Press, Los Alamitos (2005)
Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 2.0: A tool for probabilistic model checking. In: QEST 2004, pp. 322–323. IEEE Computer Society Press, Los Alamitos (2004)
Marie, R.A., Reibman, A.L., Trivedi, K.S.: Transient analysis of acyclic Markov chains. Perform. Eval. 7(3), 175–194 (1987)
Neuts, M.F.: Matrix-Geometric Solutions in Stochastic Models: An Algorithmic Approach. The Johns Hopkins Univ. Press (1981)
Qureshi, M., Sanders, W.: A new methodology for calculating distributions of reward accumulated during a finite interval. In: FTCS, pp. 116–125. IEEE Computer Society, Los Alamitos (1996)
Shoham, S., Grumberg, O.: A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 275–287. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Han, T., Katoen, JP. (2007). Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds) Automated Technology for Verification and Analysis. ATVA 2007. Lecture Notes in Computer Science, vol 4762. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75596-8_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-75596-8_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75595-1
Online ISBN: 978-3-540-75596-8
eBook Packages: Computer ScienceComputer Science (R0)