Informatics and Applications
2014, Volume 8, Issue 4, pp 58-69
A METHOD OF ENHANCING PROBABILISTIC VERIFICATION EFFICIENCY FOR COMPUTER AND TELECOMMUNICATION SYSTEMS
- A. M. Mironov
- S. L. Frenkel
Abstract
The paper considers the problem of reduction of probabilistic transition systems (PTS) in order to reduce the complexity of model checking of such systems. The problem of model checking of a PTS is to calculate truth values of formulas of temporal probabilistic computational tree logic (PCTL) in the initial state of the PTS. The
paper introduces the concept of equivalence of states of a PTS and represents an algorithm for removing equivalent states. The result of this algorithm is a PTS such that all its properties expressed by formulas of PCTL coincide with those of the original PTS.
[+] References (22)
- Karpov, Yu. G. 2010. Model checking. Verification of paral-lel and distributed systems. St. Petersburg.: BHV-Peterburg. 560 p.
- Kemeny, J.G., and J. L. Snell. 1976. Finite Markov chains. New York - Berlin - Heidelberg - Tokyo: Springer-Verlag. 225 p.
- Bukharaev, R. G. 1985. Foundations of probabilistic au-tomata theory. Moscow: Nauka. 288 p.
- Hansson, H., and B. Jonsson. 1994. A logic for reasoning about time and reliability. Formal Aspects Computing 6(5):512-535.
- Kwiatkowska, M., and D. Parker. 2012. Advances in prob-abilistic model checking. NATO Science for Peace and Security Series, Information and Communication Security 33:126-151.
- Clarke, E. M., O. Grumberg, and D. Peled. 1999. Model checking. MIT Press. 314 p.
- Mironov, A.M., and S.L. Frenkel. 2014. Minimization of probabilistic models of programs. Fundamental Applied Mathematics 19(1):121-163.
- Baier, C., M. Groesser, and F Ciesinski. 2004. Partial order reduction for probabilistic systems. 1st Conference (Inter-national) on Quantitative Evaluation of Systems (QEST'04) Proceedings. IEEE Computer Society Press. 230-239.
- D'Argenio, P., and P. Niebert. 2004. Partial order reduction on concurrent probabilistic programs. 1st Conference (International) on Quantitative Evaluation of Systems (QEST'04) Proceedings. IEEE Computer Society Press. 240-249.
- Kwiatkowska, M., G. Norman, and D. Parker. 2006. Symmetry reduction for probabilistic model checking. Computer aided verification. Eds. T. Ball and R. B. Jones. Lecture notes in computer science ser. 4144:234-248.
- Donaldson, A., and A. Miller. 2006. Symmetry reduction for probabilistic model checking using generic represen-tatives. Automated technology for verification and analysis. Eds. S. Graf and W. Zhang. Lecture notes in computer science ser. 4218:9-23.
- Hart, S., M. Sharir, and A. Pnueli. 1983. Termination of probabilistic concurrent programs. ACM Trans. Program-ming Languages Syst. 5(3):356-380.
- Vardi, M. 1985. Automatic verification of probabilistic concurrent finite state programs. 26th Annual Symposium
on Foundations of Computer Science (FOCS'85) Proceed-ings. IEEE Computer Society Press. 327-338.
- Courcoubetis, C., and M. Yannakakis. 1988. Verifying temporal properties of finite state probabilistic programs. 29th Annual Symposium on Foundations of Computer Sci-ence (FOCS'88) Proceedings. IEEE Computer Society Press. 338-345.
- Bianco, A., and L. de Alfaro. 1995. Model checking of probabilistic and nondeterministic systems. Foundations of software technology and theoretical computer science. Ed. P. S. Triagarejan. Lecture notes in computer science ser. 1026:499-513.
- Baier, C., B. Haverkort, H. Hermanns, and J.-P. Ka- toen. 2003. Model-checking algorithms for continuoustime Markov chains. IEEE Trans. Software Engineering 29(6):524-541.
- Hansson, H. 1994. Time and probability in formal design of distributed systems. Elsevier. 304 p.
- Baier, C., E. Clarke, V. Hartonas-Garmhausen, M. Kwiatkowska, and M. Ryan. 1997. Symbolic model checking for probabilistic processes. Automata, languages and programming. Eds. P. Degano, R. Gorrieri, and A. Marinetti-Spaccamela. Lecture notes in computer science ser. 1256:430-440.
- Hermanns, H., J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. 2000. A Markov chain model checker. Tools and algorithms for the construction and analysis ofsystems. Eds. S. Graf and M. I. Schwartzbach. Lecture notes in computer science ser. 1785:347-362.
- De Alfaro, L., M. Kwiatkowska, G. Norman, D. Parker, and R. Segala. 2000. Symbolic model checking of proba-bilistic processes using MTBDDs and the Kronecker rep-resentation. Tools and algorithms for the construction and analysis of systems. Eds. S. Graf and M. I. Schwartzbach. Lecture notes in computer science ser. 1785:395-410.
- Kwiatkowska, M., G. Norman, and D. Parker. 2005. Probabilistic model checking in practice: Case studies with PRISM. ACM SIGMETRICS Performance Evaluation Review. 32(4):16-21.
- Kwiatkowska, M., G. Norman, and D. Parker. 2011. PRISM 4.0: Verification of probabilistic real-time sys- terns. Computer aided verification. Eds. G. Gopalakrish- nan and S. Qadeer. Lecture notes in computer science ser. 6806:585-591.
[+] About this article
Title
A METHOD OF ENHANCING PROBABILISTIC VERIFICATION EFFICIENCY FOR COMPUTER AND TELECOMMUNICATION SYSTEMS
Journal
Informatics and Applications
2014, Volume 8, Issue 4, pp 58-69
Cover Date
2014-10-30
DOI
10.14357/19922264140408
Print ISSN
1992-2264
Publisher
Institute of Informatics Problems, Russian Academy of Sciences
Additional Links
Key words
verification; model checking; probabilistic transition systems; probabilistic temporal logic; reduction of probabilistic models
Authors
A. M. Mironov  and
S. L. Frenkel , 
Author Affiliations
Institute of Informatics Problems, Russian Academy of Sciences, 44-2 Vavilov Str., Moscow 119333, Russian Federation
Moscow Institute of Radio, Electronics, and Automation (MIREA), 78 Prosp. Vernadskogo, Moscow 119454, Russian Federation
|