phmathВестник Государственного университета просвещения. Серия: Физика-МатематикаBulletin of Federal State University of Education. Series: Physics and Mathematics2949-50832949-5067Federal State University of Educationphmath-183Research ArticleСтатьиМОДИФИКАЦИЯ ОПЕРАТОРОВ CTL ЛОГИКИ И ИХ АЛГОРИТМЫ ПРОВЕРКИ НА СТРУКТУРЕ КРИПКЕUPDATING OF CTL OPERATORS AND THEIR CHECK ALGORITHMS ON KRIPKE STRUCTUREМазуровЮ. А.noemail@neicon.ruМосковский государственный социальный университетRussian Federation201030092022036674Copyright © Мазуров Ю.А., 20222022Мазуров Ю.А.Мазуров Ю.А.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.physmathmgou.ru/jour/article/view/183

В настоящей статье предложено расширение некоторых темпоральных операторов CTL логики, позволяющее явно указывать количество состояний системы или количество путей, в которых выполняется заданное свойство системы. Дается семантика, формальная грамматика, а так же соответствующие алгоритмы проверки выполнимости на структуре Крипке,расширенных темпоральных операторов.

In this article, extension of some temporal CTL logics operators is proposed, which enables explicit indication of the number of system states or the number of ways wherein the preset feature of the system is realized. Semantics, formal grammar, as well as relevant Kripke structure and extended temporal operators based feasibility check algorithms are given.

верификацияModel CheckingCTL логикаструктура КрипкеverificationModel CheckingCTL logicsKripke structureReferencesPnueli, A.. The temporal logic of programs [Text]. //Proc. of 18-th IEEE Symposium on Foundations of Computer Science, pp. 46-57, 1977.Pnueli, A.. The temporal logic of programs [Text]. //Proc. of 18-th IEEE Symposium on Foundations of Computer Science, pp. 46-57, 1977.Clarke, J.E.M., Emerson E.A. Design and synthesis of synchronization skeletons using branching time temporal logic [Text]. //A Series of Lecture Notes in Computer Science. - V. 131, pp.52-71, Springer, 1981.Clarke, J.E.M., Emerson E.A. Design and synthesis of synchronization skeletons using branching time temporal logic [Text]. //A Series of Lecture Notes in Computer Science. - V. 131, pp.52-71, Springer, 1981.Кларк, Э., Грамберг, О., Пелед, Д. Верификация моделей программ: Model Checking [Текст]. - М.: МЦНМО, 2002, с. 56-61.Кларк, Э., Грамберг, О., Пелед, Д. Верификация моделей программ: Model Checking [Текст]. - М.: МЦНМО, 2002, с. 56-61.Карпов, Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем[Текст]. - СПб.: БХВ-Петербург, 2010, с. 41-73.Карпов, Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем[Текст]. - СПб.: БХВ-Петербург, 2010, с. 41-73.

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