Optimization Procedures in Affine Model Checking
Abstract
Symbolic model checking is based on a compact representation of sets of states and transition relations. At present there are three basic approaches of symbolic model checking: BDD-methods, bounded model checking using SAT-solvers, and various algebraic techniques, for example, constraint based model checking and regular model checking. In this paper we suggest improved algorithms for an algebraic data representation, namely, optimization algorithms for affine data structures.
About the Author
N. O. Garanina
Институт систем информатики им. А.П. Ершова СО РАН
Russian Federation
Russian Federation
References
1. Abdulla P.A., Jonsson B., Nilsson M., Saksena M. A Survey of Regular Model Checking. Proc. of CONCUR'04 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004 // Lect. Notes Comput. Sci. 2004. Vol. 3170. P. 35-48.
2. Bartzis C., Bultan T. Efficient Symbolic Representations for Arithmetic Constraints in Verification // Int. J. Found. Comput. Sci. 2003. Vol. 4. P. 605-624.
3. Boigelot B., Wolper P. Symbolic Verification with Periodic Sets // Lect. Notes Comput. Sci. 1994. Vol. 818. P. 55-67.
4. Boigelot B., Legay A., Wolper P. Iterating transducers in the large // Proc. 15th Int. Conf. on Computer Aided Verification. 2003. Lecture Notes in Computer Science. Vol. 2725. P. 223-235.
5. Bryant R.E. Symbolic boolean manipulation with ordered binary decision diagrams // IEEE Trans. Computers. 1986. Vol. C-35, №8. P. 293-318.
6. Bultan T., Gerber R., 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, №4. P. 747-789.
7. Bultan T. BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems. Proc. of Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Berlin, Germany, March 25 - April 2, 2000 // Lect. Notes Comput. Sci. 2000. Vol. 1785. P. 441-455.
8. Clarke E.M., Grumberg O., Peled D. Model Checking. London: MIT Press, 1999. 314 p.
9. Kozen D. Results on the Propositional Mu-Calculus // Theor. Comput. Sci. 1983. Vol. 27, №3. P. 333-354.
10. McMillan K.L. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993. 216 p.
11. McMillan K.L. Applying SAT Methods in Unbounded Symbolic Model Checking. Proc. of 14th International Conference, CAV'02, Copenhagen, Denmark, July 27-31, 2002 // Lect. Notes Comput. Sci. 2002. Vol. 2404. P. 250-264.
12. Shilov N.V., Garanina N.O. A Polynomial Approximations for Model Checking // Lect. Notes Comput. Sci. 2003. Vol. 2890. P. 395-400.
13. Yavuz-Kahveci T., Bultan T. Heuristics for Efficient Manipulation of Composite Constraints. Proc. of Frontiers of Combining Systems, 4th International Workshop, FroCoS 2002, Santa Margherita Ligure, Italy, April 8-10, 2002 // Lect. Notes Comput. Sci. 2002. Vol. 2309. P. 57-71.
14. Гаранина Н.О. Верификация распределенных систем с использованием аффинного представления данных, логик знаний и действий: дис. ... канд. физ.- мат. наук. Новосибирск, 2004. 172 с.
15. Гаранина Н.О. Аффинное представление данных для проверки моделей программ. Новосибирск, 2004. 48 с. (Препр./ Сиб. отд-ние. РАН. ИСИ; №116.)
16. Гаранина Н.О. Проверка моделей распределенных систем с помощью аффинного представления данных // Моделирование и анализ информационных систем. 2010. Т. 17, №4. С.52-59.
17. http://www.cs.umd.edu/projects/omega/
Review
For citations:
Garanina N.O. Optimization Procedures in Affine Model Checking. Modeling and Analysis of Information Systems. 2011;18(4):56-67. (In Russ.)
Views:
435
Email this article 