The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.02 - March/April (2009 vol.35)
pp: 241-257
Tingting Han , RWTH Aachen University, Aachen and University of Twente, Enschede
Joost-Pieter Katoen , RWTH Aachen University, Aachen and University of Twente, Enschede
Damman Berteun , RWTH Aachen University, Aachen and University of Twente, Enschede
ABSTRACT
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. Finding the strongest evidence (i.e., the most probable path) violating a (bounded) until-formula is shown to be reducible to a single-source (hop-constrained) shortest path problem. Counterexamples of smallest size that deviate most from the required probability bound can be obtained by applying (small amendments to) k-shortest (hop-constrained) paths algorithms. These results can be extended to Markov chains with rewards, to LTL model checking, and are useful for Markov decision processes. Experimental results show that typically the size of a counterexample is excessive. To obtain much more compact representations, we present a simple algorithm to generate (minimal) regular expressions that can act as counterexamples. The feasibility of our approach is illustrated by means of two communication protocols: leader election in an anonymous ring network and the Crowds protocol.
INDEX TERMS
Model checking, Diagnostics
CITATION
Tingting Han, Joost-Pieter Katoen, Damman Berteun, "Counterexample Generation in Probabilistic Model Checking", IEEE Transactions on Software Engineering, vol.35, no. 2, pp. 241-257, March/April 2009, doi:10.1109/TSE.2009.5
REFERENCES
[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.177-195, 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.33-51, 2006.
[5] C. Andersson, S. Fischer-Hü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, “Discrete-Time Rewards Model-Checked,” Proc. Int'l Conf. Formal Modelling and Analysis of Timed Sequences, pp.88-104, 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.157-172, 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.97-105, 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.34-40, 2005.
[12] R. Bellman, “On a Routing Problem,” Quarterly Applications Math., vol. 16, no. 1, pp.87-90, 1958.
[13] G. Berry and R. Sethi, “From Regular Expressions to Deterministic Automata,” Theoretical Computer Science, vol. 48, no. 3, pp.117-126, 1986.
[14] J.A. Brzozowski, “Derivatives of Regular Expressions,” J. ACM vol. 11, no. 4, pp.481-494, 1964.
[15] E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “Counterexample-Guided Abstraction Refinement,” Proc. Int'l Conf. Computer Aided Verification, pp.154-169, 2000.
[16] E.M. Clarke, S. Jha, Y. Lu, and H. Veith, “Tree-Like Counterexamples in Model Checking,” Proc. IEEE Symp. Logic in Computer Science, pp.19-29, 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 Bellman-Ford Algorithm,” Introduction to Algorithms, chapter 24.1, pp.588-592, 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 Discrete-Time Markov Chains,” Proc. Int'l Colloquim Theoretical Aspects of Computing, pp.280-294, 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.186-201, 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.247-262, 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.312-314, 2004.
[24] E.W. Dijkstra, “A Note on Two Problems in Connexion with Graphs,” Numerische Mathematik, vol. 1, pp.269-271, 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.652-673, 1998.
[27] M.R. Garey and D.S. Johnson, Computers and Intractability, A Guide to the Theory of NP-Completeness. Freeman, 1979.
[28] G. Gramlich and G. Schnitger, “Minimizing NFA's and Regular Expressions,” J. Computer Systems and Sciences vol. 73, no. 6, pp.908-923, 2007.
[29] A. Gurfinkel and M. Chechik, “Proof-Like Counter-Examples,” Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp.160-175, 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.72-86, 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.331-346, 2007.
[32] Y.-S. Han, D. Wood, “Obtaining Shorter Regular Expressions from Finite-State Automata,” Theoretical Computer Science, vol. 370, nos.1-3, pp.110-120, 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.512-535, 1994.
[34] S. Hart, M. Sharir, and A. Pnueli, “Termination of Probabilistic Concurrent Programs.” ACM Trans. Programing Languages Systems, vol. 5, no. 3, pp.356-380, 1983.
[35] H. Hermanns, B. Wachter, and L. Zhang, “Probabilistic CEGAR,” Proc. Int'l Conf. Computer Aided Verification, pp.162-175, 2008.
[36] A. Itai and M. Rodeh, “Symmetry Breaking in Distributed Networks,” Information and Computation, vol. 88, no. 1, pp.60-87, 1990.
[37] J.M. Jaffe, “Algorithms for Finding Paths with Multiple Constraints,” IEEE Network, vol. 14, pp.95-116, 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.15-29, 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.102-116, 2004.
[40] G.D.F. Jr, “The Viterbi Algorithm,” Proc. IEEE, vol. 61, no. 3, pp.268-278, 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.87-101, 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.243-244, 2005.
[43] J.-P. Katoen, D. Klink, M. Leucker, and V. Wolf, “Three-Valued Abstraction for Continuous-Time Markov Chains,” Proc. Int'l Conf. Computer Aided Verification, pp.311-324, 2007.
[44] S.C. Kleene, Representation of Events in Nerve Nets and Finite Automata, pp.3-42, Princeton Univ. Press, 1956.
[45] F.A. Kuipers, T. Korkmaz, M. Krunz, and P. van Mieghem, “Performance Evaluation of Constraint-Based Path Selection Algorithms,” IEEE Network vol. 18, no. 5, pp.16-23, 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.128-142, 2004.
[47] M.Z. Kwiatkowska, G. Norman, and D. Parker, “Game-Based Abstraction for Markov Decision Processes,” Proc. Int'l Conf. Quantitative Evaluation of Systems, pp.157-166, 2006.
[48] K.G. Larsen and A. Skou, “Bisimulation Through Probabilistic Testing,” Information and Computation, vol. 94, no. 1, pp.1-28, 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 Non-Irreducible Markov Chains with Strongly Connected Components,” Proc. European Conf. Simulation and Modelling, pp.548-552, 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.743-749, 2001.
[53] A. McIver, C. Morgan, and C. Gonzalia, “Proofs and Refutations for Probabilistic Systems,” Proc. Technical Conf. Formal Methods, pp.100-115, 2008.
[54] K. Mehlhorn and M. Ziegelmann, “Resource Constrained Shortest Paths,” Proc. Int'l Conf. Embedded Systems and Applications, pp.326-337, 2000.
[55] C. Neumann, “Converting Deterministic Finite Automata to Regular Expressions,” http://neumannhaus.com/christoph/ papers 2005-03-16.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.66-92, 1998.
[57] V. Shmatikov, “Probabilistic Analysis of an Anonymity System,” J.Computer Security, vol. 12, nos.3/4, pp.355-377, 2004.
[58] S. Shoham and O. Grumberg, “A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement,” Proc. Int'l Conf. Computer Aided Verification, pp.275-287, 2003.
[59] A. Vaha-Sipila and T. Virtanen, “BT-Crowds: Crowds-Style 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 Finite-State Machines-Part I,” IEEE Trans. Pattern Analysis and Machine Intelligence, vol. 27, no. 7, pp.1013-1025, 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.260-269, 1967.
20 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool