Abstract
The computation of counterexamples for probabilistic model checking has been an area of active research over the past years. In spite of the achieved theoretical results in this field, there is no freely available tool that allows for the computation and representation of probabilistic counterexamples. We present an open source tool called DiPro that can be used with the PRISM and MRMC probabilistic model checkers. It allows for the computation of probabilistic counterexamples for discrete time Markov chains (DTMCs), continuous time Markov chains (CTMCs) and Markov decision processes (MDPs). The computed counterexamples can be rendered graphically.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aljazzar, H., Fischer, M., Grunske, L., Kuntz, M., Leitner-Fischer, F., Leue, S.: Safety analysis of an airbag system using probabilistic FMEA and probabilistic counterexamples. In: Proc. QEST 2009, pp. 299–308. IEEE Computer Society, Los Alamitos (2009)
Aljazzar, H., Kuntz, M., Leitner-Fischer, F., Leue, S.: Directed and heuristic counterexample generation for probabilistic model checking: a comparative evaluation. In: Proc. QUOVADIS 2010, pp. 25–32. ACM, New York (2010)
Aljazzar, H., Leue, S.: Debugging of dependability models using interactive visualization of counterexamples. In: Proc. QEST 2008. IEEE Computer Society Press, Los Alamitos (2008)
Aljazzar, H., Leue, S.: Generation of counterexamples for model checking of markov decision processes. In: Proc. QEST 2009, pp. 197–206. IEEE Computer Society, Los Alamitos (2009)
Aljazzar, H., Leue, S.: Directed explicit state-space search in the generation of counterexamples for stochastic model checking. IEEE Transactions on Software Engineering 36(1), 37–60 (2010)
Aljazzar, H., Leue, S.: K*: A heuristic search algorithm for finding the k shortest paths. Artificial Intelligence (2011) (accepted for publication)
Andrés, M., D’Argenio, P., van Rossum, P.: Significant diagnostic counterexamples in probabilistic model checking. Hardware and Software: Verification and Testing, 129–148 (2009)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering 29(7) (2003)
Han, T., Katoen, J., Berteun, D.: Counterexample Generation in Probabilistic Model Checking. IEEE Transactions on Software Engineering, 241–257 (2009)
Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)
Katoen, J.-P., Khattri, M., Zapreev, I.S.: A Markov Reward Model Checker. In: QEST 2005: Proceedings of the Second International Conference on Quantitative Evaluation of Systems, pp. 243–244. IEEE Computer Society, Los Alamitos (2005)
Kuntz, M., Leitner-Fischer, F., Leue, S.: From probabilistic counterexamples via causality to fault trees. Technical Report soft-11-02, Chair for Software Engineering, University of Konstanz (2011), http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-11-02.pdf
Leitner-Fischer, F., Leue, S.: QuantUM: Quantitative safety analysis of UML models. In: Proc. QAPL (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aljazzar, H., Leitner-Fischer, F., Leue, S., Simeonov, D. (2011). DiPro - A Tool for Probabilistic Counterexample Generation. In: Groce, A., Musuvathi, M. (eds) Model Checking Software. SPIN 2011. Lecture Notes in Computer Science, vol 6823. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22306-8_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-22306-8_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22305-1
Online ISBN: 978-3-642-22306-8
eBook Packages: Computer ScienceComputer Science (R0)