maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1051Research ArticleОригинальные статьиArticlesПроверка моделей распределенных систем с помощью аффинного представления данныхModel Checking of Distributed Systems with Affine Data StructuresГаранинаН. О.GaraninaN. O.garanina@iis.nsk.suИнститут систем информатики им. А.П. Ершова СО РАНRussian Federation2010201220101745259Copyright © Гаранина Н.О., 20102010Гаранина Н.О.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/1051

Предложено эффективное символьное представление распределенных систем, определяемых линейными функциями над целочисленными переменными.

A new data structure is suggested for symbolic model checking of distributed systems defined by linear functions of integer variables.

символьная проверка моделейраспределённые системыsymbolic model checkingdistributed systemsReferencesBoigelot B. and Wolper P. Symbolic Verification with Periodic Sets // Lect. Notes Comput. Sci. 1994. Vol. 818. P. 55-67.Boigelot B. and Wolper P. Symbolic Verification with Periodic Sets // Lect. Notes Comput. Sci. 1994. Vol. 818. P. 55-67.Bryant R.E. Symbolic boolean manipulation with ordered binary decision diagrams // IEEE Trans. Computers. 1986. Vol. C-35, N 8. P. 293-318.Bryant R.E. Symbolic boolean manipulation with ordered binary decision diagrams // IEEE Trans. Computers. 1986. Vol. C-35, N 8. P. 293-318.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.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.Kozen D. Results on the Propositional Mu-Calculus // Theor. Comput. Sci. 1983. Vol. 27, N 3. P. 333-354.Kozen D. Results on the Propositional Mu-Calculus // Theor. Comput. Sci. 1983. Vol. 27, N 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.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.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.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.Гаранина Н.О. Верификация распределенных систем с использованием аффинного представления данных, логик знаний и действий: Дис. ... канд. физ.- мат. наук. Новосибирск, 2004. 172 с.Гаранина Н.О. Верификация распределенных систем с использованием аффинного представления данных, логик знаний и действий: Дис. ... канд. физ.- мат. наук. Новосибирск, 2004. 172 с.Гаранина Н.О. Аффинное представление данных для проверки моделей программ. Новосибирск, 2004. 48 с. (Препр./ Сиб. отд-ние. РАН. ИСИ; N 116)Гаранина Н.О. Аффинное представление данных для проверки моделей программ. Новосибирск, 2004. 48 с. (Препр./ Сиб. отд-ние. РАН. ИСИ; N 116)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.