Welcome to Francis Academic Press

Academic Journal of Computing & Information Science, 2020, 3(2); doi: 10.25236/AJCIS.2020.030212.

Runtime Probabilistic Model Checking Based on Incremental Method

Author(s)

Chao He

Corresponding Author:
Chao He
Affiliation(s)

Information Engineering, Nanjing University of Finance and Economics, Nanjing 210000, China
[email protected]

Abstract

Nowadays, more and more systems change dynamically during their life cycle, runtime probabilistic model checking is proposed to verify these system. An important challenge of runtime probabilistic model checking is its performance. It should be fast enough to respond to runtime requirements and continuously verify whether the current system meets system requirements when the system changes dynamically. In this paper, in view of the efficiency of the runtime probabilistic model checking, we propose a runtime probabilistic model checking based on incremental method. The method applies the ideal of incremental verification to reuse the calculated value of the previous model to reduce the number of iterations and improve their performance. We implement our method in model checking tool PRISM, and use a benchmark case model to perform model verification on its reachability properties. The results of the experiments show that the method proposed in this paper can reduce the system verification time of standard runtime probabilistic model checking by more than 45% in most of cases.

Keywords

Runtime probabilistic model checking, Incremental verification, Stochastic system, Discrete-Time Markov Chain

Cite This Paper

Chao He. Runtime Probabilistic Model Checking Based on Incremental Method. Academic Journal of Computing & Information Science (2020), Vol. 3, Issue 2: 85-95. https://doi.org/10.25236/AJCIS.2020.030212.

References

[1] Baier C, Katoen J P. Principles of model checking [M]. MIT press, 2008.
[2] LIU Yang, LI Xuan-Dong, MA Yan, WANG Lin-Zhang. Survey for stochastic model checking [J]. Chinese Journal of Computers, 2015, 000 (011): 2145-2162.
[3] Kwiatkowska M, Norman G, Parker D. PRISM 4.0: Verification of probabilistic real-time systems [C] //International conference on computer aided verification. Springer, Berlin, Heidelberg, 2011: 585-591.
[4] Dehnert C, Junges S, Katoen J P. A storm is coming: A modern probabilistic model checker [C] //International Conference on Computer Aided Verification. Springer, Cham, 2017: 592-600.
[5] Filieri A, Ghezzi C, Tamburrelli G. Run-time efficient probabilistic model checking [C] //2011 33rd International Conference on Software Engineering (ICSE). IEEE, 2011: 341-350.
[6] Christoph Prybila,Stefan Schulte,Christoph Hochreiner,Ingo Weber. Runtime verification for business processes utilizing the Bitcoin blockchain [J]. Future Generation Computer Systems,2020,107.
[7] Klein J, Baier C, Chrszon P. Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata [J]. International Journal on Software Tools for Technology Transfer, 2018, 20 (2): 179-194.
[8] Abrahám E, Jansen N, Wimmer R. DTMC model checking by SCC reduction [C] //2010 Seventh International Conference on the Quantitative Evaluation of Systems. IEEE, 2010: 37-46.
[9] Brázdil T, Chatterjee K, Chmelik M. Verification of Markov decision processes using learning algorithms [C] //International Symposium on Automated Technology for Verification and Analysis. Springer, Cham, 2014: 98-114.
[10] Kwiatkowska M, Parker D, Qu H. Incremental quantitative verification for Markov decision processes [C] //2011 IEEE/IFIP 41st International Conference on Dependable Systems & Networks (DSN). IEEE, 2011: 359-370.
[11] Forejt V, Kwiatkowska M, Parker D. Incremental runtime verification of probabilistic systems [C] //International Conference on Runtime Verification. Springer, Berlin, Heidelberg, 2012: 314-319.
[12] Sokolsky O V, Smolka S A. Incremental model checking in the modal mu-calculus [C] //International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg, 1994: 351-363.
[13] Conway C L, Namjoshi K S, Dams D. Incremental algorithms for inter-procedural analysis of safety properties [C] //International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg, 2005: 449-461.
[14] Heljanko K, Junttila T, Latvala T. Incremental and complete bounded model checking for full PLTL [C] //International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg, 2005: 98-111.
[15] Wongpiromsarn T, Ulusoy A, Belta C. Incremental temporal logic synthesis of control policies for robots interacting with dynamic agents [C] //2012 IEEE/RSJ International Conference on Intelligent Robots and Systems. IEEE, 2012: 229-236.
[16] Abrahám E, Jansen N, Wimmer R. DTMC model checking by SCC reduction [C] //2010 Seventh International Conference on the Quantitative Evaluation of Systems. IEEE, 2010: 37-46.
[17] Baier C, Klein J, Leuschner L. Ensuring the reliability of your model checker: Interval iteration for Markov decision processes [C] //International Conference on Computer Aided Verification. Springer, Cham, 2017: 160-180.
[18] Katoen J P. The probabilistic model checking landscape [C] //Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. 2016: 31-45.
[19] Elman H C, Saad Y, Saylor P E. A hybrid Chebyshev Krylov subspace algorithm for solving nonsymmetric systems of linear equations [J]. SIAM Journal on Scientific and Statistical Computing, 1986, 7 (3): 840-855.
[20] Sleijpen G L G, Van der Vorst H A. A Jacobi--Davidson iteration method for linear eigenvalue problems [J]. SIAM review, 2000, 42 (2): 267-293.
[21] Milaszewicz J P. Improving jacobi and gauss-seidel iterations [J]. Linear Algebra and Its Applications, 1987, 93: 161-170.
[22] Kohno T, Kotakemori H, Niki H, et al. Improving the modified Gauss-Seidel method for Z-matrices [J]. Linear Algebra and its Applications, 1997, 267: 113-123.
[23] Ortega J M, Rheinboldt W C. Monotone iterations for nonlinear equations with application to Gauss-Seidel methods [J]. SIAM Journal on Numerical Analysis, 1967, 4 (2): 171-190.