
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Husain Aljazzar, Stefan Leue, "Directed Explicit StateSpace Search in the Generation of Counterexamples for Stochastic Model Checking," IEEE Transactions on Software Engineering, vol. 36, no. 1, pp. 3760, January/February, 2010.  
BibTex  x  
@article{ 10.1109/TSE.2009.57, author = {Husain Aljazzar and Stefan Leue}, title = {Directed Explicit StateSpace Search in the Generation of Counterexamples for Stochastic Model Checking}, journal ={IEEE Transactions on Software Engineering}, volume = {36}, number = {1}, issn = {00985589}, year = {2010}, pages = {3760}, 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 StateSpace Search in the Generation of Counterexamples for Stochastic Model Checking IS  1 SN  00985589 SP37 EP60 EPD  3760 A1  Husain Aljazzar, A1  Stefan Leue, PY  2010 KW  Directed explicit statespace search KW  heuristic search KW  counterexamples KW  stochastic model checking. VL  36 JA  IEEE Transactions on Software Engineering ER   
[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. AddisionWesley, 2003.
[3] E.M. Clarke and E.A. Emerson, "Design and Synthesis of Synchronization Skeletons Using BranchingTime Temporal Logic," Logic of Programs, pp. 5271, Springer, 1981.
[4] E. Clarke, S. Jha, Y. Lu, and H. Veith, "TreeLike Counterexamples in Model Checking," Proc. 17th Ann. IEEE Symp. Logic in Computer Science, pp. 1929, 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. 229247, 2006.
[6] A. Groce and W. Visser, "What Went Wrong: Explaining Counterexamples," Proc. Workshop Software Model Checking, pp. 121135, 2003.
[7] S. Edelkamp, S. Leue, and A. LluchLafuente, "Directed ExplicitState Model Checking in the Validation of Communication Protocols," Int'l J. Software Tools for Technology Transfer, vol. 5, nos. 2/3, pp. 247267, 2004.
[8] N.J. Nilsson, Principles of Artificial Intelligence. Tioga, 1980.
[9] J. Pearl, Heuristics—Intelligent Search Strategies for Computer Problem Solving. AddisionWesley, 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. 512535, 1994.
[12] A. Aziz, K. Sanwal, V. Singhal, and R. Brayton, "ModelChecking ContinuousTime Markov Chains," ACM Trans. Computational Logic, vol. 1, no. 1, pp. 162170, 2000.
[13] C. Baier, B. Haverkort, H. Hermanns, and J.P. Katoen, "ModelChecking Algorithms for ContinuousTime Markov Chains," IEEE Trans. Software Eng., vol. 29, no. 6, pp. 524541, 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. 441444, 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. 243244, 2005.
[16] H.L.S. Younes, "Ymer: A Statistical Model Checker," Proc. 17th Int'l Conf. Computer Aided Verification, pp. 429433, 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. 129130, 2006.
[18] C. Courcoubetis and M. Yannakakis, "Verifying Temporal Properties of FiniteState Probabilistic Programs," Proc. 29th Ann. Symp. Foundations of Computer Science, pp. 338345, 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. 336349, 1990.
[20] C. Courcoubetis and M. Yannakakis, "The Complexity of Probabilistic Verification," J. ACM, vol. 42, no. 4, pp. 857907, 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. 155165, 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. 499513, 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. 269276, 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. 177195, 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. 3351, 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. 241257, 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. 331346, 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. 169178, 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. 162175, 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 FiniteState Programs," Proc. 26th Ann. Symp. Foundations of Computer Science, pp. 327338, 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. 652673, 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. 1529, 1999.
[36] A. Martelli, "On the Complexity of Admissible Search Algorithms," Artificial Intelligence, vol. 8, no. 1, pp. 113, 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. 305310, 1998.
[38] R.E. Korf, M. Reid, and S. Edelkamp, "Time Complexity of IterativeDeepening${\rm A}^{\ast}$ ," Artificial Intelligence, vol. 129, nos. 1/2, pp. 199218, 2001.
[39] S. Kupferschmid, K. Dräger, J. Hoffmann, B. Finkbeiner, H. Dierks, A. Podelski, and G. Behrmann, "Uppaal/DMC—AbstractionBased Heuristics for Directed Model Checking," Proc. 13th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 679682, 2007.
[40] W.K. Grassmann, "Transient Solutions in Markovian Queuing Systems," Computers and OR, vol. 4, no. 1, pp. 4753, 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. 343361, 1984.
[43] R.E. Tarjan, "DepthFirst Search and Linear Graph Algorithms," SIAM J. Computing, vol. 1, no. 2, pp. 146160, 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. 228237, 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. 920, 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. 3247, 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. 239257, 2008.
[48] L. Benini, A. Bogliolo, G.A. Paleologo, and G.D. Micheli, "Policy Optimization for Dynamic Power Management," IEEE Trans. ComputerAided Design of Integrated Circuits and Systems, vol. 18, no. 6, pp. 813833, 1999.
[49] H. Hermanns, J.P. Katoen, J. MeyerKayser, and M. Siegle, "A Markov Chain Model Checker," Proc. Tools and Algorithms for Construction and Analysis of Systems, pp. 347362, 2000.