
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Tingting Han, JoostPieter Katoen, Damman Berteun, "Counterexample Generation in Probabilistic Model Checking," IEEE Transactions on Software Engineering, vol. 35, no. 2, pp. 241257, March/April, 2009.  
BibTex  x  
@article{ 10.1109/TSE.2009.5, author = {Tingting Han and JoostPieter Katoen and Damman Berteun}, title = {Counterexample Generation in Probabilistic Model Checking}, journal ={IEEE Transactions on Software Engineering}, volume = {35}, number = {2}, issn = {00985589}, year = {2009}, pages = {241257}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2009.5}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Counterexample Generation in Probabilistic Model Checking IS  2 SN  00985589 SP241 EP257 EPD  241257 A1  Tingting Han, A1  JoostPieter Katoen, A1  Damman Berteun, PY  2009 KW  Model checking KW  Diagnostics VL  35 JA  IEEE Transactions on Software Engineering ER   
[1] PRISM Website, http:/www.prismmodelchecker.org, 2009.
[2] R.K. Ahuja, T.L. Magnanti, and J.B. Orlin, Network Flows: Algorithms, Theory and Applications. Prentice Hall, Inc., 1993.
[3] H. Aljazzar, H. Hermanns, and S. Leue, “Counterexamples for Timed Probabilistic Reachability,” Proc. Int'l Conf. Formal Modelling and Analysis of Timed Sequences, pp.177195, 2005.
[4] H. Aljazzar and S. Leue, “Extended Directed Search for Probabilistic Timed Reachability,” Proc. Int'l Conf. Formal Modelling and Analysis of Timed Sequences, pp.3351, 2006.
[5] C. Andersson, S. FischerHübner, and R. Lundin, “Enabling Anonymity for the Mobile Internet Using the Mcrowds System,” IFIP WG 9.2, 9.6/11.7 Summer School on Risks and Challenges of the Network Soc., p. 35, 2004.
[6] S. Andova, H. Hermanns, and J.P. Katoen, “DiscreteTime Rewards ModelChecked,” Proc. Int'l Conf. Formal Modelling and Analysis of Timed Sequences, pp.88104, 2003.
[7] M.E. Andrés, P. D'Argenio, and P. van Rossum, “Significant Diagnostic Counterexamples in Probabilistic Model Checking,” Proc. Fourth Haifa Verification Conf., to be published.
[8] M.E. Andrés and P. van Rossum, “Conditional Probabilities over Probabilistic and Nondeterministic Systems,” Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp.157172, 2008.
[9] C. Baier and J.P. Katoen, Principles of Model Checking. MIT Press, 2008.
[10] T. Ball, M. Naik, and S.K. Rajamani, “From Symptom to Cause: Localizing Errors in Counterexample Traces,” Proc. Symp. Principles of Programming Language, pp.97105, 2003.
[11] G. Behrmann, K.G. Larsen, and J.I. Rasmussen, “Optimal Scheduling Using Priced Timed Automata,” ACM SIGMETRICS Performance Evaluation Rev., vol. 32, no. 4, pp.3440, 2005.
[12] R. Bellman, “On a Routing Problem,” Quarterly Applications Math., vol. 16, no. 1, pp.8790, 1958.
[13] G. Berry and R. Sethi, “From Regular Expressions to Deterministic Automata,” Theoretical Computer Science, vol. 48, no. 3, pp.117126, 1986.
[14] J.A. Brzozowski, “Derivatives of Regular Expressions,” J. ACM vol. 11, no. 4, pp.481494, 1964.
[15] E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “CounterexampleGuided Abstraction Refinement,” Proc. Int'l Conf. Computer Aided Verification, pp.154169, 2000.
[16] E.M. Clarke, S. Jha, Y. Lu, and H. Veith, “TreeLike Counterexamples in Model Checking,” Proc. IEEE Symp. Logic in Computer Science, pp.1929, 2002.
[17] L. Comtet, Advanced Combinatorics: The Art of Finite and Infinite Expansion. D. Reidel Publishing Co., 1974.
[18] T.H. Cormen, C.E. Leiserson, R.L. Rivest, and C. Stein, “The BellmanFord Algorithm,” Introduction to Algorithms, chapter 24.1, pp.588592, MIT Press, 2001.
[19] B. Damman, T. Han, and J.P. Katoen, “Regular Expressions for PCTL Counterexamples,” Proc. Int'l Conf. Quantitative Evaluation of Systems, 2008.
[20] C. Daws, “Symbolic and Parametric Model Checking of DiscreteTime Markov Chains,” Proc. Int'l Colloquim Theoretical Aspects of Computing, pp.280294, 2004.
[21] L. de Alfaro, T.A. Henzinger, and F.Y. Mang, “Detecting Errors Before Reaching Them,” Proc. Int'l Conf. Computer Aided Verification, pp.186201, 2000.
[22] E. de Queirós Vieira Martins, M.M.B. Pascoal, and J.L.E. dos Santos, “Deviation Algorithms for Ranking Shortest Paths,” Int'l J. Foundations of Computer Science, vol. 10, no. 3, pp.247262, 1999.
[23] M. Delgado and J. Morais, “Approximation to the Smallest Regular Expression for a Given Regular Language,” Proc. Int'l Conf. Implementation and Application of Automata, pp.312314, 2004.
[24] E.W. Dijkstra, “A Note on Two Problems in Connexion with Graphs,” Numerische Mathematik, vol. 1, pp.269271, 1959.
[25] D.S. Du and K.I. Ko, Problem Solving in Automata, Languages, and Complexity. John Wiley and Sons, 2001.
[26] D. Eppstein, “Finding the $k$ Shortest Paths,” SIAM J. Computing, vol. 28, no. 2 pp.652673, 1998.
[27] M.R. Garey and D.S. Johnson, Computers and Intractability, A Guide to the Theory of NPCompleteness. Freeman, 1979.
[28] G. Gramlich and G. Schnitger, “Minimizing NFA's and Regular Expressions,” J. Computer Systems and Sciences vol. 73, no. 6, pp.908923, 2007.
[29] A. Gurfinkel and M. Chechik, “ProofLike CounterExamples,” Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp.160175, 2003.
[30] T. Han and J.P. Katoen, “Counterexamples in Probabilistic Model Checking,” Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp.7286, 2007.
[31] T. Han and J.P. Katoen, “Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking,” Proc. Int'l Symp. Automated Technology for Verification and Analysis, pp.331346, 2007.
[32] Y.S. Han, D. Wood, “Obtaining Shorter Regular Expressions from FiniteState Automata,” Theoretical Computer Science, vol. 370, nos.13, pp.110120, 2007.
[33] H. Hansson and B. Jonsson, “A Logic for Reasoning About Time and Reliability,” Proc. Int'l Workshop Formal Aspects of Component Software, vol. 6, no. 5, pp.512535, 1994.
[34] S. Hart, M. Sharir, and A. Pnueli, “Termination of Probabilistic Concurrent Programs.” ACM Trans. Programing Languages Systems, vol. 5, no. 3, pp.356380, 1983.
[35] H. Hermanns, B. Wachter, and L. Zhang, “Probabilistic CEGAR,” Proc. Int'l Conf. Computer Aided Verification, pp.162175, 2008.
[36] A. Itai and M. Rodeh, “Symmetry Breaking in Distributed Networks,” Information and Computation, vol. 88, no. 1, pp.6087, 1990.
[37] J.M. Jaffe, “Algorithms for Finding Paths with Multiple Constraints,” IEEE Network, vol. 14, pp.95116, 1984.
[38] V.M. Jiménez and A. Marzal, “Computing the $k$ Shortest Paths: A New Algorithm and an Experimental Comparison,” Proc. Workshop Algorithmic Eng., pp.1529, 1999.
[39] H. Jin, K. Ravi, and F. Somenzi, “Fate and Free Will in Error Traces,” Proc. Conf. Software Tools for Technology Transfer, vol. 6, no. 2, pp.102116, 2004.
[40] G.D.F. Jr, “The Viterbi Algorithm,” Proc. IEEE, vol. 61, no. 3, pp.268278, 1973.
[41] J.P. Katoen, T. Kemna, I. Zapreev, and D. Jansen, “Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking,” Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp.87101, 2007.
[42] J.P. Katoen, M. Khattri, and I.S. Zapreev, “A Markov Reward Model Checker,” Proc. Int'l Conf. Quantitative Evaluation of Systems, pp.243244, 2005.
[43] J.P. Katoen, D. Klink, M. Leucker, and V. Wolf, “ThreeValued Abstraction for ContinuousTime Markov Chains,” Proc. Int'l Conf. Computer Aided Verification, pp.311324, 2007.
[44] S.C. Kleene, Representation of Events in Nerve Nets and Finite Automata, pp.342, Princeton Univ. Press, 1956.
[45] F.A. Kuipers, T. Korkmaz, M. Krunz, and P. van Mieghem, “Performance Evaluation of ConstraintBased Path Selection Algorithms,” IEEE Network vol. 18, no. 5, pp.1623, 2004.
[46] M.Z. Kwiatkowska, G. Norman, and D. Parker, “Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach,” Proc. Conf. Software Tools for Technology Transfer vol. 6, no. 2, pp.128142, 2004.
[47] M.Z. Kwiatkowska, G. Norman, and D. Parker, “GameBased Abstraction for Markov Decision Processes,” Proc. Int'l Conf. Quantitative Evaluation of Systems, pp.157166, 2006.
[48] K.G. Larsen and A. Skou, “Bisimulation Through Probabilistic Testing,” Information and Computation, vol. 94, no. 1, pp.128, 1991.
[49] E. Lawler, Combinatorial Optimization: Networks and Matroids. Holt, Reinhart and Winston, 1976.
[50] H. le Guen and R.A. Marie, “Visiting Probabilities in NonIrreducible Markov Chains with Strongly Connected Components,” Proc. European Conf. Simulation and Modelling, pp.548552, 2002.
[51] P. Linz, An Introduction to Formal Languages and Automata. Jones and Bartless, 2001.
[52] G. Liu and K.G. Ramakrishnan, “A*prune: An Algorithm for Finding $k$ Shortest Paths Subject to Multiple Constraints,” Proc. INFOCOM, pp.743749, 2001.
[53] A. McIver, C. Morgan, and C. Gonzalia, “Proofs and Refutations for Probabilistic Systems,” Proc. Technical Conf. Formal Methods, pp.100115, 2008.
[54] K. Mehlhorn and M. Ziegelmann, “Resource Constrained Shortest Paths,” Proc. Int'l Conf. Embedded Systems and Applications, pp.326337, 2000.
[55] C. Neumann, “Converting Deterministic Finite Automata to Regular Expressions,” http://neumannhaus.com/christoph/ papers 20050316.DFA_to_RegEx.pdf, 2005.
[56] M.K. Reiter and A.D. Rubin, “Crowds: Anonymity for Web Transactions,” ACM Trans. Information and System Security, vol. 1, no. 1, pp.6692, 1998.
[57] V. Shmatikov, “Probabilistic Analysis of an Anonymity System,” J.Computer Security, vol. 12, nos.3/4, pp.355377, 2004.
[58] S. Shoham and O. Grumberg, “A GameBased Framework for CTL Counterexamples and 3Valued AbstractionRefinement,” Proc. Int'l Conf. Computer Aided Verification, pp.275287, 2003.
[59] A. VahaSipila and T. Virtanen, “BTCrowds: CrowdsStyle Anonymity with Bluetooth and Java,” Proc. Hawaii Int'l Conf. System Sciences, 2005.
[60] E. Vidal, F. Thollard, C. de la Higuera, F. Casacuberta, and R.C. Carrasco, “Probabilistic FiniteState MachinesPart I,” IEEE Trans. Pattern Analysis and Machine Intelligence, vol. 27, no. 7, pp.10131025, July 2005.
[61] A.J. Viterbi, “Error Bounds for Convolutional Codes and an Asymptotically Optimum Decoding Algorithm,” IEEE Trans. Information Theory, vol. 13, no. 2, pp.260269, 1967.