Model Checking of Distributed Systems with Affine Data Structures
Abstract
A new data structure is suggested for symbolic model checking of distributed systems
defined by linear functions of integer variables.
defined by linear functions of integer variables.
About the Author
N. O. Garanina
Институт систем информатики им. А.П. Ершова СО РАН
Russian Federation
Russian Federation
References
1. Boigelot B. and Wolper P. Symbolic Verification with Periodic Sets // Lect. Notes Comput. Sci. 1994. Vol. 818. P. 55-67.
2. Bryant R.E. Symbolic boolean manipulation with ordered binary decision diagrams // IEEE Trans. Computers. 1986. Vol. C-35, N 8. P. 293-318.
3. Bultan T., Gerber R., and Pugh W. Model Checking Concurrent Systems With Unbounded Integer Variables: Symbolic Representations, Approximations and Experimental Results // ACM Trans. Progr. Lang, and Systems. 1999. Vol. 21, N 4. P. 747-789.
4. Kozen D. Results on the Propositional Mu-Calculus // Theor. Comput. Sci. 1983. Vol. 27, N 3. P. 333-354.
5. McMillan K.L. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993. 216 p.
6. Shilov N.V., Garanina N.O. A Polynomial Approximations for Model Checking // Lect. Notes Comput. Sci. 2003. Vol. 2890. P. 395-400.
7. Shilov N.V., Garanina N.O., Kalinina N.A. Model checking knowledge, actions and fixpoints // Proc. Int. Workshop on Concurrency, Specification and Programming. Caputh, Germany, 2004. V. 2. P. 351-357.
8. Гаранина Н.О. Верификация распределенных систем с использованием аффинного представления данных, логик знаний и действий: Дис. ... канд. физ.- мат. наук. Новосибирск, 2004. 172 с.
9. Гаранина Н.О. Аффинное представление данных для проверки моделей программ. Новосибирск, 2004. 48 с. (Препр./ Сиб. отд-ние. РАН. ИСИ; N 116)
10. http://www.cs.umd.edu/projects/omega/
Review
For citations:
Garanina N.O. Model Checking of Distributed Systems with Affine Data Structures. Modeling and Analysis of Information Systems. 2010;17(4):52-59. (In Russ.)
Views:
540
Email this article 