maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1098Research ArticleОригинальные статьиArticlesОптимизационные процедуры в аффинной проверке моделейOptimization Procedures in Affine Model CheckingГаранинаНаталья ОлеговнаGaraninaN. O.garanina@iis.nsk.suИнститут систем информатики им. А.П. Ершова СО РАНRussian Federation2011201220111845667Copyright © Гаранина Н.О., 20112011Гаранина Н.О.Garanina N.O.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1098

Символьная проверка на модели основана на компактном представлении множеств. На данный момент есть три основных направления символьной проверки моделей: методы, основанные на бинарных разрешающих диаграммах, ограниченная проверка моделей, использующая SAT-решатели, и различные алгебраические подходы к эффективному представлению данных. В данной работе предлагается рассмотреть улучшенные алгоритмы манипуляции с алгебраическим представлением данных, а именно алгоритмы оптимизации аффинных представлений данных.

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.

символьная проверка моделейалгебраические представления данныхраспределенные системыsymbolic model checkingalgebraic data representationdistributed systemsReferencesAbdulla 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.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.Bartzis C., Bultan T. Efficient Symbolic Representations for Arithmetic Constraints in Verification // Int. J. Found. Comput. Sci. 2003. Vol. 4. P. 605-624.Bartzis C., Bultan T. Efficient Symbolic Representations for Arithmetic Constraints in Verification // Int. J. Found. Comput. Sci. 2003. Vol. 4. P. 605-624.Boigelot B., Wolper P. Symbolic Verification with Periodic Sets // Lect. Notes Comput. Sci. 1994. Vol. 818. P. 55-67.Boigelot B., Wolper P. Symbolic Verification with Periodic Sets // Lect. Notes Comput. Sci. 1994. Vol. 818. P. 55-67.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.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.Bryant R.E. Symbolic boolean manipulation with ordered binary decision diagrams // IEEE Trans. Computers. 1986. Vol. C-35, №8. P. 293-318.Bryant R.E. Symbolic boolean manipulation with ordered binary decision diagrams // IEEE Trans. Computers. 1986. Vol. C-35, №8. P. 293-318.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.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.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.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.Clarke E.M., Grumberg O., Peled D. Model Checking. London: MIT Press, 1999. 314 p.Clarke E.M., Grumberg O., Peled D. Model Checking. London: MIT Press, 1999. 314 p.Kozen D. Results on the Propositional Mu-Calculus // Theor. Comput. Sci. 1983. Vol. 27, №3. P. 333-354.Kozen D. Results on the Propositional Mu-Calculus // Theor. Comput. Sci. 1983. Vol. 27, №3. P. 333-354.McMillan K.L. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993. 216 p.McMillan K.L. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993. 216 p.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.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.Shilov N.V., Garanina N.O. A Polynomial Approximations for Model Checking // Lect. Notes Comput. Sci. 2003. Vol. 2890. P. 395-400.Shilov N.V., Garanina N.O. A Polynomial Approximations for Model Checking // Lect. Notes Comput. Sci. 2003. Vol. 2890. P. 395-400.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.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.Гаранина Н.О. Верификация распределенных систем с использованием аффинного представления данных, логик знаний и действий: дис. ... канд. физ.- мат. наук. Новосибирск, 2004. 172 с.Гаранина Н.О. Верификация распределенных систем с использованием аффинного представления данных, логик знаний и действий: дис. ... канд. физ.- мат. наук. Новосибирск, 2004. 172 с.Гаранина Н.О. Аффинное представление данных для проверки моделей программ. Новосибирск, 2004. 48 с. (Препр./ Сиб. отд-ние. РАН. ИСИ; №116.)Гаранина Н.О. Аффинное представление данных для проверки моделей программ. Новосибирск, 2004. 48 с. (Препр./ Сиб. отд-ние. РАН. ИСИ; №116.)Гаранина Н.О. Проверка моделей распределенных систем с помощью аффинного представления данных // Моделирование и анализ информационных систем. 2010. Т. 17, №4. С.52-59.Гаранина Н.О. Проверка моделей распределенных систем с помощью аффинного представления данных // Моделирование и анализ информационных систем. 2010. Т. 17, №4. С.52-59.http://www.cs.umd.edu/projects/omega/http://www.cs.umd.edu/projects/omega/

The authors declare that there are no conflicts of interest present.