Husain Aljazzar
ABSTRACT
The generation of counterexamples for probabilistic model checking has been an area of active research over the past five years. Tangible outcome of this research are novel directed and heuristic algorithms for efficient generation of probabilistic counterexamples, such as K* and XBF. In this paper we present an empirical evaluation of the efficiency of these algorithms and the well-known Eppstein's algorithm. We will also evaluate the effect of optimisations applied to Eppstein, K* and XBF. Additionally, we will show, how information produced during model checking can be used to guide the search for counterexamples. This is a first step towards automatically generating heuristic functions. The experimental evaluation of the various algorithms is done by applying them to one case study, knwon from the literature on probabilistic model checking and one case study taken from the automotive industry.
- www.autosar.org, checked 16.12.2009.Google Scholar
- A. Aziz, K. Sanwal, V. Singhal, and R. K. Brayton. Verifying continuous-time Markov chains. In Rajeev Alur and Thomas A. Henzinger, editors, Eighth International Conference on Computer Aided Verification CAV, volume 1102, pages 269--276, New Brunswick, NJ, USA, 1996. Springer Verlag LNCS. Google ScholarDigital Library
- H. Aljazzar. Directed Diagnostics of System Dependability Models. PhD thesis, University of Konstanz, 2009. http://kops.ub.uni-konstanz.de/volltexte/2009/9188/.Google Scholar
- H. Aljazzar, M. Fischer, L. Grunske, M. Kuntz, F. Leitner-Fischer, and S. Leue. Safety analysis of an airbag system using probabilistic fmea and probabilistic counterexamples. Quantitative Evaluation of Systems, International Conference on, 0:299--308, 2009. Google ScholarDigital Library
- H. Aljazzar and S. Leue. Extended directed search for probabilistic timed reachability. In FORMATS '06, LNCS vol. 4202, pages 33--51. Springer, 2006. Google ScholarDigital Library
- H. Aljazzar and S. Leue. Debugging of dependability models using interactive visualization of counterexamples. In QEST '08. IEEE Computer Society Press, 2008. Google ScholarDigital Library
- H. Aljazzar and S. Leue. K*: A directed on-the-fly algorithm for finding the k shortest paths. Technical Report soft-08-03, Univ. of Konstanz, Gemany, March 2008. submitted for publication.Google Scholar
- H. Aljazzar and S. Leue. Directed explicit state-space search in the generation of counterexamples for stochastic model checking. IEEE Transactions on Software Engineering, 2009. Google ScholarDigital Library
- H. Aljazzar and S. Leue. Generation of counterexamples for model checking of markov decision processes. Quantitative Evaluation of Systems, International Conference on, 0:197--206, 2009. Google ScholarDigital Library
- H. Aljazzar and S. Leue. K*: Heuristics-guided, on-the-fly k shortest paths search. 2010. Submitted for publication. Under review.Google Scholar
- M. E. Andrés, P. R. D'Argenio, and P. van Rossum. Significant Diagnostic Counterexamples in Probabilistic Model Checking. In Haifa Verification Conference, volume 5394 of Lecture Notes in Computer Science, pages 129--148. Springer, 2008. Google ScholarDigital Library
- AUTOSAR GbR. Requirements on Memory Services v. 2.2.1. www.autosar.org/download/AUTOSAR_SRS_MemoryServices.pdf, checked 16.12.2009.Google Scholar
- C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model-checking algorithms for continuous-time Markov chains. IEEE Transions on Software Engineering, 29(7), 2003. Google ScholarDigital Library
- B. Damman, T. Han, and J.-P. Katoen. Regular Expressions for PCTL Counterexamples. In Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems, pages 179--188. IEEE Computer Society, 2008. Google ScholarDigital Library
- D. Eppstein. Finding the k shortest paths. SIAM J. Computing, 28(2):652--673, 1998. Google ScholarDigital Library
- H. Fecher, M. Huth, N. Piterman, and D. Wagner. Hintikka games for PCTL on labeled Markov chains. In Fifth International Conference on the Quantitative Evaluaiton of Systems (QEST 2008), pages 169--178, Washington, DC, USA, 2008. IEEE Computer Society. Google ScholarDigital Library
- L. Grunske, R. Colvin, and K. Winter. Probabilistic model-checking support for fmea. In QEST '07: Proceedings of the Fourth International Conference on Quantitative Evaluation of Systems, pages 119--128, Washington, DC, USA, 2007. IEEE Computer Society. Google ScholarDigital Library
- T. Han, J.-P. Katoen, and B. Damman. Counterexample generation in probabilistic model checking. IEEE Trans. Softw. Eng., 35(2):241--257, 2009. Google ScholarDigital Library
- H. Hermanns, B. Wachter, and L. Zhang. Probabilistic CEGAR. In Computer Aided Verification, 20th International Conference, CAV 2008, Proceedings, volume 5123 of Lecture Notes in Computer Science, pages 162--175. Springer, 2008. Google ScholarDigital Library
- A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker. PRISM: A tool for automatic verification of probabilistic systems. In TACAS'06, LNCS vol. 3920, pages 441--444. Springer, 2006. Google ScholarDigital Library
- V. M. Jiménez and A. Marzal. A lazy version of eppstein's shortest paths algorithm. In WEA '03, LNCS vol. 2647, pages 179--190. Springer, 2003. Google ScholarDigital Library
- J.-P. Katoen, M. Khattri, and I. S. Zapreev. A Markov Reward Model Checker. In QEST '05, pages 243--244. IEEE Computer Society, 2005. Google ScholarDigital Library
- J. Muppala, G. Ciardo, and K. Trivedi. Stochastic reward nets for reliability prediction. Communications in Reliability, Maintainability and Serviceability, 1(2):9--20, July 1994.Google Scholar
- J. Pearl. Heuristics -- Intelligent Search Strategies for Computer Problem Solving. Addision--Wesley, 1986. Google ScholarDigital Library
- M. Schmalz, D. Varacca, and H. Völzer. Counterexamples in Probabilistic LTL Model Checking for Markov Chains. In Proceedings of the 20th International Conference on Concurrency Theory, volume 5710 of Lecture Notes in Computer Science, pages 587--602. Springer, 2009. Google ScholarDigital Library
Index Terms
- Directed and heuristic counterexample generation for probabilistic model checking: a comparative evaluation
Recommendations
Accelerating counterexample detection in software model checking
ICSE '18: Proceedings of the 40th International Conference on Software Engineering: Companion ProceeedingsModel checking is an automatic approach in enhancing correctness of systems. However, when it is applied to discover flaws in software systems, most of the respective verification tools lack scalability due to the state-space explosion problem. ...
Counterexample Generation in Probabilistic Model Checking
Providing evidence for the refutation of a property is an essential, if not the most important, feature of model checking. This paper considers algorithms for counterexample generation for probabilistic CTL formulae in discrete-time Markov chains. ...
Genetic Algorithm for Generating Counterexample in Stochastic Model Checking
ICNCC '18: Proceedings of the 2018 VII International Conference on Network, Communication and ComputingCounterexamples are the most effective feature to convince system engineers about the value of formal verification. Generating the smallest counterexample in stochastic model checking has been proved to be NP-complete. In this paper, we apply the ...
Comments