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

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2009.5

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.5REFERENCES

- [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.- [12] R. Bellman, “On a Routing Problem,”
Quarterly Applications Math., vol. 16, no. 1, pp.87-90, 1958.- [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.- [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.- [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.- [35] H. Hermanns, B. Wachter, and L. Zhang, “Probabilistic CEGAR,”
Proc. Int'l Conf. Computer Aided Verification, pp.162-175, 2008.- [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.- [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.- [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.- [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.- [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.
- [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. |