Counterexamples in probabilistic LTL model checking for Markov chains. (English) Zbl 1254.68155
Bravetti, Mario (ed.) et al., CONCUR 2009 – concurrency theory. 20th international conference, CONCUR 2009, Bologna, Italy, September 1–4, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-04080-1/pbk). Lecture Notes in Computer Science 5710, 587-602 (2009).
Summary: We propose a way of presenting and computing a counterexample in probabilistic LTL model checking for discrete-time Markov chains. In qualitative probabilistic model checking, we present a counterexample as a pair \((\alpha ,\gamma )\), where \(\alpha\), \(\gamma \) are finite words such that all paths that extend \(\alpha \) and have infinitely many occurrences of \(\gamma \) violate the specification. In quantitative probabilistic model checking, we present a counterexample as a pair \((W,R)\), where \(W\) is a set of such finite words \(\alpha \) and \(R\) is a set of such finite words \(\gamma \). Moreover, we suggest how the counterexample presented helps the user identify the underlying error in the system by means of an interactive game with the model checker.
For the entire collection see [Zbl 1173.68003].
For the entire collection see [Zbl 1173.68003].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
References:
| [1] | 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) · Zbl 1175.68239 · doi:10.1007/11603009_15 |
| [2] | 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) · Zbl 1141.68449 · doi:10.1007/11867340_4 |
| [3] | Aljazzar, H., Leue, S.: Counterexamples for model checking of Markov decision processes. Tech. Report soft-08-01, University of Konstanz, Germany (2007) · Zbl 1141.68449 |
| [4] | Aljazzar, H., Leue, S.: Debugging of dependability models using interactive visualization of counterexamples. In: QEST 2008, pp. 189–198. IEEE, Los Alamitos (2008) |
| [5] | Andrés, M., D’Argenio, P., van Rossum, P.: Significant diagnostic counterexamples in probabilistic model checking. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 129–148. Springer, Heidelberg (2008) · doi:10.1007/978-3-540-69369-7 |
| [6] | Breiman, L.: Probability. Addison Wesley, Reading (1968) · Zbl 0174.48801 |
| [7] | Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press, Cambridge (2001) · Zbl 1047.68161 |
| [8] | Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995) · Zbl 0885.68109 · doi:10.1145/210332.210339 |
| [9] | Damman, B., Han, T., Katoen, J.-P.: Regular expressions for PCTL counterexamples. In: QEST 2008, pp. 179–188. IEEE, Los Alamitos (2008) |
| [10] | de Alfaro, L.: Temporal logics for the specification of performance and reliability. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 165–176. Springer, Heidelberg (1997) · doi:10.1007/BFb0023457 |
| [11] | Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, vol. B, ch. 16, pp. 995–1072. Elsevier Science, Amsterdam (1990) · Zbl 0900.03030 |
| [12] | 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) · Zbl 1186.68293 · doi:10.1007/978-3-540-71209-1_8 |
| [13] | Han, T., Katoen, J.-P.: Providing evidence of likely being on time: Counterexample generation for CTMC model checking. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 331–346. Springer, Heidelberg (2007) · Zbl 1141.68470 · doi:10.1007/978-3-540-75596-8_24 |
| [14] | Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. 6(5), 512–535 (1994) · Zbl 0820.68113 · doi:10.1007/BF01211866 |
| [15] | Kemeny, J.G., Snell, J.L., Knapp, A.W.: Denumerable Markov Chains. Springer, Heidelberg (1976) · Zbl 0149.13301 · doi:10.1007/978-1-4684-9455-6 |
| [16] | Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46–57. IEEE, Los Alamitos (1977) |
| [17] | Ravi, K., Bloem, R., Somenzi, F.: A comparative study of symbolic algorithms for the computation of fair cycles. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 143–160. Springer, Heidelberg (2000) · doi:10.1007/3-540-40922-X_10 |
| [18] | Schmalz, M.: Extensions of an algorithm for generalised fair model checking. Diploma Thesis, Lübeck, Germany (2007), http://www.infsec.ethz.ch/people/mschmalz/dt.pdf |
| [19] | Schmalz, M., Völzer, H., Varacca, D.: Counterexamples in probabilistic LTL model checking for Markov chains. Technical Report 627, ETH Zürich, Switzerland (2009), http://www.inf.ethz.ch/research/disstechreps/techreports · Zbl 1254.68155 |
| [20] | Varacca, D., Völzer, H.: Temporal logics and model checking for fairly correct systems. In: LICS 2006, pp. 389–398. IEEE, Los Alamitos (2006) |
| [21] | Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS 1985, pp. 327–338. IEEE, Los Alamitos (1985) |
| [22] | Völzer, H., Varacca, D., Kindler, E.: Defining fairness. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 458–472. Springer, Heidelberg (2005) · Zbl 1134.68456 · doi:10.1007/11539452_35 |
| [23] | Wimmer, R., Braitling, B., Becker, B.: Counterexample generation for discrete-time Markov chains using bounded model checking. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 366–380. Springer, Heidelberg (2009) · Zbl 1206.68195 · doi:10.1007/978-3-540-93900-9_29 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
