Probabilistic Model Checking by Model Equivalent Reduction and Abstraction

Abstract:

In probabilistic model checking, use discrete time Markov chain (DTMCs) to represent the model and use a branch of the temporal logic called probabilistic computation tree(PCTL) to represent the properties of the model. In this paper, we presents several counterexample generation algorithms for DTMCs violating a PCTL formula, presented as follows: first, according to the transitive closure to reduce the model size against the specific properties of the model, second, using the minimal connected components to generate the equivalent acyclic graph, third, we use the algorithm of the operational research to obtain a shortest path between two points. Experimental results show that our algorithm greatly simplifies the model size and generate more reasonable counterexamples with least states and paths.

• Periodical: Advanced Materials Research (Volumes 989-994)
• Pages: 2474-2479
• DOI: https://doi.org/10.4028/www.scientific.net/AMR.989-994.2474
• Online since: July 2014
• Authors: Zhen Long Bai*, Lin Ying Xu, Zhan Shui Yu
• Keywords: Markov Chain, Minimal Connected Components, Model Checking, Shortest Path, Transitive Closure

References

[1] Erika Abrahám, Nils Jansen, Ralf Wimmer, J Katoen, and Bernd Becker. Dtmc model checking by scc reduction. In Quantitative Evaluation of Systems (QEST), 2010 Seventh International Conference on the, pages 37–46. IEEE, (2010).

DOI: 10.1109/qest.2010.13

[2] Tingting Han, J Katoen, and Damman Berteun. Counterexample generation in probabilistic model checking. Software Engineering, IEEE Transactions on, 35(2): 241–257, 2009. 14.

DOI: 10.1109/tse.2009.5

[3] Yo-Sub Han and Derick Wood. Obtaining shorter regular expressions from finite-state automata. Theoretical Computer Science, 370(1): 110–120, (2007).

DOI: 10.1016/j.tcs.2006.09.025

[4] NilsJansen, ErikaÁbrahám, J ensKatelaan, RalfWimmer, Joost-PieterKatoen, and BerndBecker. Hierarchical counterexamples for discrete-time markov chains. In Automated Technology for Verification and Analysis, pages 443–452. Springer, (2011).

[5] Nils Jansen, Ralf Wimmer, ErikaÁbrahám, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, and Johann Schuster. Symbolic counterexample generation for large discrete-time markov chains. Science of Computer Programming, (2014).

DOI: 10.1016/j.scico.2014.02.001

[6] HoonSang Jin, Kavita Ravi, and Fabio Somenzi. Fate and free will in error traces. International Journal on Software Tools for Technology Transfer, 6(2): 102–116, (2004).

DOI: 10.1007/s10009-004-0146-9

[7] Marta Kwiatkowska, Gethin Norman, and David Parker. Prism 4. 0: Verification of probabilistic real-time systems. In Computer Aided Verification, pages 585–591. Springer, (2011).

DOI: 10.1007/978-3-642-22110-1_47