This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model Checking
January/February 2010 (vol. 36 no. 1)
pp. 37-60
ASCII Text
x 
 
Husain Aljazzar, Stefan Leue, "Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model Checking," IEEE Transactions on Software Engineering, vol. 36, no. 1, pp. 37-60, January/February, 2010.
 
 
BibTex
x
 
@article{ 10.1109/TSE.2009.57,
author = {Husain Aljazzar and Stefan Leue},
title = {Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model Checking},
journal ={IEEE Transactions on Software Engineering},
volume = {36},
number = {1},
issn = {0098-5589},
year = {2010},
pages = {37-60},
doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2009.57},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model Checking
IS - 1
SN - 0098-5589
SP37
EP60
EPD - 37-60
A1 - Husain Aljazzar,
A1 - Stefan Leue,
PY - 2010
KW - Directed explicit state-space search
KW - heuristic search
KW - counterexamples
KW - stochastic model checking.
VL - 36
JA - IEEE Transactions on Software Engineering
ER -
 
Husain Aljazzar, University of Konstanz, Konstanz
Stefan Leue, University of Konstanz, Konstanz
Current stochastic model checkers do not make counterexamples for property violations readily available. In this paper, we apply directed explicit state-space search to discrete and continuous-time Markov chains in order to compute counterexamples for the violation of PCTL or CSL properties. Directed explicit state-space search algorithms explore the state space on-the-fly, which makes our method very efficient and highly scalable. They can also be guided using heuristics which usually improve the performance of the method. Counterexamples provided by our method have two important properties. First, they include those traces which contribute the greatest amount of probability to the property violation. Hence, they show the most probable offending execution scenarios of the system. Second, the obtained counterexamples tend to be small. Hence, they can be effectively analyzed by a human user. Both properties make the counterexamples obtained by our method very useful for debugging purposes. We implemented our method based on the stochastic model checker PRISM and applied it to a number of case studies in order to illustrate its applicability.

[1] E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking, third ed. MIT Press, 2001.
[2] G.J. Holzmann, The SPIN Model Checker: Primer and Reference Manual. Addision-Wesley, 2003.
[3] E.M. Clarke and E.A. Emerson, "Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic," Logic of Programs, pp. 52-71, Springer, 1981.
[4] E. Clarke, S. Jha, Y. Lu, and H. Veith, "Tree-Like Counterexamples in Model Checking," Proc. 17th Ann. IEEE Symp. Logic in Computer Science, pp. 19-29, 2002.
[5] A. Groce, S. Chaki, D. Kroening, and O. Strichman, "Error Explanation with Distance Metrics," Int'l J. Software Tools for Technology Transfer, vol. 8, no. 3, pp. 229-247, 2006.
[6] A. Groce and W. Visser, "What Went Wrong: Explaining Counterexamples," Proc. Workshop Software Model Checking, pp. 121-135, 2003.
[7] S. Edelkamp, S. Leue, and A. Lluch-Lafuente, "Directed Explicit-State Model Checking in the Validation of Communication Protocols," Int'l J. Software Tools for Technology Transfer, vol. 5, nos. 2/3, pp. 247-267, 2004.
[8] N.J. Nilsson, Principles of Artificial Intelligence. Tioga, 1980.
[9] J. Pearl, Heuristics—Intelligent Search Strategies for Computer Problem Solving. Addision-Wesley, 1986.
[10] W.J. Stewart, Introduction to the Numerical Solution of Markov Chains. Princeton Univ. Press, 1994.
[11] H. Hansson and B. Jonsson, "A Logic for Reasoning about Time and Reliability," Formal Aspects of Computing, vol. 6, no. 5, pp. 512-535, 1994.
[12] A. Aziz, K. Sanwal, V. Singhal, and R. Brayton, "Model-Checking Continuous-Time Markov Chains," ACM Trans. Computational Logic, vol. 1, no. 1, pp. 162-170, 2000.
[13] C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen, "Model-Checking Algorithms for Continuous-Time Markov Chains," IEEE Trans. Software Eng., vol. 29, no. 6, pp. 524-541, June 2003.
[14] A. Hinton, M.Z. Kwiatkowska, G. Norman, and D. Parker, "PRISM: A Tool for Automatic Verification of Probabilistic Systems," Proc. 12th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 441-444, 2006.
[15] J.-P. Katoen, M. Khattri, and I.S. Zapreev, "A Markov Reward Model Checker," Proc. Second Int'l Conf. Quantitative Evaluaiton of Systems, pp. 243-244, 2005.
[16] H.L.S. Younes, "Ymer: A Statistical Model Checker," Proc. 17th Int'l Conf. Computer Aided Verification, pp. 429-433, July 2005.
[17] T. Hérault, R. Lassaigne, and S. Peyronnet, "APMC 3.0: Approximate Verification of Discrete and Continuous Time Markov Chains," Proc. Third Int'l Conf. Quantitative Evaluation of Systems, pp. 129-130, 2006.
[18] C. Courcoubetis and M. Yannakakis, "Verifying Temporal Properties of Finite-State Probabilistic Programs," Proc. 29th Ann. Symp. Foundations of Computer Science, pp. 338-345, 1988.
[19] C. Courcoubetis and M. Yannakakis, "Markov Decision Processes and Regular Events (Extended Abstract)," Proc. 17th Int'l Colloquium Automata, Languages and Programming, pp. 336-349, 1990.
[20] C. Courcoubetis and M. Yannakakis, "The Complexity of Probabilistic Verification," J. ACM, vol. 42, no. 4, pp. 857-907, 1995.
[21] A. Aziz, V. Singhal, and F. Balarin, "It Usually Works: The Temporal Logic of Stochastic Systems," Proc. Seventh Int'l Conf. Computer Aided Verification, pp. 155-165, 1995.
[22] A. Bianco and L. de Alfaro, "Model Checking of Probabalistic and Nondeterministic Systems," Proc. 15th Conf. Foundations of Software Technology and Theoretical Computer Science, pp. 499-513, 1995.
[23] A. Aziz, K. Sanwal, V. Singhal, and R.K. Brayton, "Verifying Continuous Time Markov Chains," Proc. Eighth Int'l Conf. Computer Aided Verification, pp. 269-276, 1996.
[24] H. Aljazzar, H. Hermanns, and S. Leue, "Counterexamples for Timed Probabilistic Reachability," Proc. Third Int'l Conf. Formal Modeling and Analysis of Timed Systems, pp. 177-195, 2005.
[25] H. Aljazzar and S. Leue, "Extended Directed Search for Probabilistic Timed Reachability," Proc. Fourth Int'l Conf. Formal Modeling and Analysis of Timed Systems, pp. 33-51, 2006.
[26] T. Han, J.-P. Katoen, and B. Damman, "Counterexample Generation in Probabilistic Model Checking," IEEE Trans. Software Eng., vol. 35, no. 2, pp. 241-257, Mar./Apr. 2009.
[27] T. Han and J.-P. Katoen, "Providing Evidence of Likely Being on Time: Counterexample Generation for ctmc Model Checking," Proc. Fifth Int'l Symp. Automated Technology for Verification and Analysis, pp. 331-346, 2007.
[28] H. Fecher, M. Huth, N. Piterman, and D. Wagner, "Hintikka Games for PCTL on Labeled Markov Chains," Proc. Fifth Int'l Conf. Quantitative Evaluation of Systems, pp. 169-178, 2008.
[29] M.E. Andrés, P.R. D'Argenio, and P. van Rossum, "Significant Diagnostic Counterexamples in Probabilistic Model Checking," ACM Computing Research Repository, vol. abs/0806.1139, 2008.
[30] H. Hermanns, B. Wachter, and L. Zhang, "Probabilistic CEGAR," Proc. 20th Int'l Conf. Computer Aided Verification, pp. 162-175, 2008.
[31] H. Aljazzar and S. Leue, "Debugging of Dependability Models Using Interactive Visualization of Counterexamples," Proc. Fifth Int'l Conf. Quantitative Evaluation of Systems, 2008.
[32] M.Y. Vardi, "Automatic Verification of Probabilistic Concurrent Finite-State Programs," Proc. 26th Ann. Symp. Foundations of Computer Science, pp. 327-338, 1985.
[33] S.E. Dreyfus, "An Appraisal of Some Shortest Path Algorithms," Proc. Operations Research Soc. of Am./The Inst. of Management Sciences Joint Nat'l Mtg., vol. 16, p. 166, 1968.
[34] D. Eppstein, "Finding the $k$ Shortest Paths," SIAM J. Computing, vol. 28, no. 2, pp. 652-673, http://dx.doi.org/10.1137S0097539795290477 , 1998.
[35] V.M. Jiménez and A. Marzal, "Computing the k Shortest Paths: A New Algorithm and an Experimental Comparison," Algorithm Eng., pp. 15-29, 1999.
[36] A. Martelli, "On the Complexity of Admissible Search Algorithms," Artificial Intelligence, vol. 8, no. 1, pp. 1-13, 1977.
[37] R.E. Korf and M. Reid, "Complexity Analysis of Admissible Heuristic Search," Proc. 15th Nat'l Conf. Artificial Intelligence and 10th Innovative Applications of Artificial Intelligence Conf., pp. 305-310, 1998.
[38] R.E. Korf, M. Reid, and S. Edelkamp, "Time Complexity of Iterative-Deepening-${\rm A}^{\ast}$ ," Artificial Intelligence, vol. 129, nos. 1/2, pp. 199-218, 2001.
[39] S. Kupferschmid, K. Dräger, J. Hoffmann, B. Finkbeiner, H. Dierks, A. Podelski, and G. Behrmann, "Uppaal/DMC—Abstraction-Based Heuristics for Directed Model Checking," Proc. 13th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 679-682, 2007.
[40] W.K. Grassmann, "Transient Solutions in Markovian Queuing Systems," Computers and OR, vol. 4, no. 1, pp. 47-53, 1977.
[41] W.K. Grassmann, "Transient Solutions in Markovian Queuing Systems," Computers and OR, vol. 5, no. 2, p. 161, 1978.
[42] D. Gross and D.R. Miller, "The Randomization Technique as a Modeling Tool and Solution Procedure for Transient Markov Processes," Operations Research, vol. 32, no. 2, pp. 343-361, 1984.
[43] R.E. Tarjan, "Depth-First Search and Linear Graph Algorithms," SIAM J. Computing, vol. 1, no. 2, pp. 146-160, 1972.
[44] B.R. Haverkort, H. Hermanns, and J.-P. Katoen, "On the Use of Model Checking Techniques for Dependability Evaluation," Proc. 19th IEEE Symp. Reliable Distributed Systems, pp. 228-237, 2000.
[45] J. Muppala, G. Ciardo, and K. Trivedi, "Stochastic Reward Nets for Reliability Prediction," Comm. in Reliability, Maintainability and Serviceability, vol. 1, no. 2, pp. 9-20, July 1994.
[46] J. Heath, M.Z. Kwiatkowska, G. Norman, D. Parker, and O. Tymchyshyn, "Probabilistic Model Checking of Complex Biological Pathways," Proc. Int'l Conf. Computational Methods in Systems Biology, pp. 32-47, 2006.
[47] J. Heath, M.Z. Kwiatkowska, G. Norman, D. Parker, and O. Tymchyshyn, "Probabilistic Model Checking of Complex Biological Pathways," Theoretical Computer Science, vol. 391, no. 3, pp. 239-257, 2008.
[48] L. Benini, A. Bogliolo, G.A. Paleologo, and G.D. Micheli, "Policy Optimization for Dynamic Power Management," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 18, no. 6, pp. 813-833, 1999.
[49] H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle, "A Markov Chain Model Checker," Proc. Tools and Algorithms for Construction and Analysis of Systems, pp. 347-362, 2000.

Index Terms:
Directed explicit state-space search, heuristic search, counterexamples, stochastic model checking.
Citation:
Husain Aljazzar, Stefan Leue, "Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model Checking," IEEE Transactions on Software Engineering, vol. 36, no. 1, pp. 37-60, Jan.-Feb. 2010, doi:10.1109/TSE.2009.57
Usage of this product signifies your acceptance of the Terms of Use.