maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2021-1-104-119mais-1475Research ArticleTheory of ComputingLTL-спецификация счётчиковых машинLTL-Specification of Counter Machineshttps://orcid.org/0000-0003-0500-306XКузьминЕгор ВладимировичKuzminEgor V.

Профессор, доктор физико-математических наук

ул. Советская, д. 14, г. Ярославль, 150003

Professor, Doctor of Science

14 Sovetskaya str., Yaroslavl 150003

kuzmin@uniyar.ac.ruЯрославский государственный университет им. П. Г. ДемидоваРоссияP. G. Demidov Yaroslavl State UniversityRussian Federation202123032021281104119Copyright © Кузьмин Е.В., 20212021Кузьмин Е.В.Kuzmin E.V.Данная работа распространяется под лицензией 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/1475

Статья написана в поддержку учебной дисциплины “Неклассические логики”. В рамках этой дисциплины объектами изучения являются базовые принципы и конструктивные элементы, с помощью которых происходит формальное построение различных неклассических логик высказываний. Несмотря на абстрактность теории неклассических логик, в которой основное внимание уделяется строгой математической формализации логических рассуждений, существуют реальные прикладные области применения теоретических результатов. В частности, языки темпоральных модальных логик широко используются для моделирования, спецификации и верификации (анализа корректности) программных систем логического управления. В этой статье на примере линейной темпоральной логики LTL демонстрируется, как абстрактные понятия неклассических логик могут находить отражение на практике в области информационных технологий и программирования. Показывается возможность представления поведения программной системы в виде набора LTL-формул и использования этого представления для проверки выполнимости программных свойств системы через процедуру доказательства справедливости логических выводов, выраженных в терминах линейной темпоральной логики LTL. В качестве программных систем, для спецификации поведения которых будет применяться логика LTL, рассматриваются счётчиковые машины Минского. Счётчиковые машины Минского — один из способов формализации интуитивного понятия алгоритма. Они обладают той же вычислительной мощностью, что и машины Тьюринга. Счётчиковая машина имеет вид компьютерной программы, написанной на языке высокого уровня, поскольку содержит переменные, называемые счётчиками, и операторы условного и безусловного перехода, позволяющие строить конструкции циклов. Известно, что любой алгоритм (гипотетически) может быть реализован в виде трёхсчётчиковой машины Минского.

The article is written in support of the educational discipline “Non-classical logics”. Within the framework of this discipline, the objects of study are the basic principles and constructive elements, with the help of which the formal construction of various non-classical propositional logics takes place. Despite the abstractness of the theory of non-classical logics, in which the main attention is paid to the strict mathematical formalization of logical reasoning, there are real practical areas of application of theoretical results. In particular, languages of temporal modal logics are widely used for modeling, specification, and verification (correctness analysis) of logic control program systems. This article demonstrates, using the linear temporal logic LTL as an example, how abstract concepts of non-classical logics can be reƒected in practice in the field of information technology and programming. We show the possibility of representing the behavior of a software system in the form of a set of LTL-formulas and using this representation to verify the satisfiability of program system properties through the procedure of proving the validity of logical inferences, expressed in terms of the linear temporal logic LTL. As program systems, for the specification of the behavior of which the LTL logic will be applied, Minsky counter machines are considered. Minsky counter machines are one of the ways to formalize the intuitive concept of an algorithm. They have the same computing power as Turing machines. A counter machine has the form of a computer program written in a high-level language, since it contains variables called counters, and conditional and unconditional jump operators that allow to build loop constructions. It is known that any algorithm (hypothetically) can be implemented in the form of a Minsky three-counter machine.

неклассическая логикалинейная темпоральная логикасчётчиковые машиныLTL-спецификацияnon-classical logiclinear temporal logiccounter machinesLTL-specificationРабота выполнена в рамках инициативной НИР ЯрГУ им. П. Г. Демидова № VIP-016This work was supported by P. G. Demidov Yaroslavl State University Project № VIP-016ReferencesE. V. Kuzmin, Non-Classical Propositional Logics, in Russian. Yaroslavl: P.G. Demidov Yaroslavl State University, 2016, p. 160.E. V. Kuzmin, Non-Classical Propositional Logics, in Russian. Yaroslavl: P.G. Demidov Yaroslavl State University, 2016, p. 160.G. Priest, An Introduction to Non-Classical Logic. From if to is. Cambridge University Press, 2008, p. 648.G. Priest, An Introduction to Non-Classical Logic. From if to is. Cambridge University Press, 2008, p. 648.M. Minsky, Computation: Finite and Infinite Machines. Prentice-Hall, Inc., 1967.M. Minsky, Computation: Finite and Infinite Machines. Prentice-Hall, Inc., 1967.R. Schroeppel, “A Two Counter Machine Cannot Calculate 2N”, Massachusetts Institute of Technology, Artificial Intelligence Laboratory, Artificial Intelligence Memo #257, 1972, p. 32.R. Schroeppel, “A Two Counter Machine Cannot Calculate 2N”, Massachusetts Institute of Technology, Artificial Intelligence Laboratory, Artificial Intelligence Memo #257, 1972, p. 32.E. V. Kuzmin, Counter Machines, in Russian. Yaroslavl: Yaroslavl State University, 2010, p. 128.E. V. Kuzmin, Counter Machines, in Russian. Yaroslavl: Yaroslavl State University, 2010, p. 128.A. Pnueli, “The temporal logic of programs”, in 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), IEEE Computer Society Press, 1977, pp. 46–57.A. Pnueli, “The temporal logic of programs”, in 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), IEEE Computer Society Press, 1977, pp. 46–57.E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking. The MIT Press, 2001.E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking. The MIT Press, 2001.C. Baier and J.-P. Katoen, Principles of Model Checking. The MIT Press, 2008.C. Baier and J.-P. Katoen, Principles of Model Checking. The MIT Press, 2008.Cadence SMV. [Online]. Available: http://www.kenmcmil.com/smv.html.Cadence SMV. [Online]. Available: http://www.kenmcmil.com/smv.html.E. Clarke, O. Grumberg, and K. Hamaguchi, “Another Look at LTL Model Checking”, Carnegie Mellon University, Tech. Rep. CMU-CS-94-114, 1994.E. Clarke, O. Grumberg, and K. Hamaguchi, “Another Look at LTL Model Checking”, Carnegie Mellon University, Tech. Rep. CMU-CS-94-114, 1994.E. V. Kuzmin and V. A. Sokolov, “On Construction and Verification of PLC Programs”, Automatic Control and Computer Sciences, vol. 47, no. 7, pp. 443–451, 2013.E. V. Kuzmin and V. A. Sokolov, “On Construction and Verification of PLC Programs”, Automatic Control and Computer Sciences, vol. 47, no. 7, pp. 443–451, 2013.E. V. Kuzmin and V. A. Sokolov, “Modeling, Specification and Construction of PLC-programs”, Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 554–563, 2014.E. V. Kuzmin and V. A. Sokolov, “Modeling, Specification and Construction of PLC-programs”, Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 554–563, 2014.E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, “Construction and Verification of PLC-programs by LTL-specification”, Automatic Control and Computer Sciences, vol. 49, no. 7, pp. 453–465, 2015.E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, “Construction and Verification of PLC-programs by LTL-specification”, Automatic Control and Computer Sciences, vol. 49, no. 7, pp. 453–465, 2015.E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, “Construction and Verification of PLC LD Programs by the LTL Specification”, Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 424–436, 2014.E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, “Construction and Verification of PLC LD Programs by the LTL Specification”, Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 424–436, 2014.E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, “Modeling a Consistent Behavior of PLC-Sensors”, Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 602–614, 2014.E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, “Modeling a Consistent Behavior of PLC-Sensors”, Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 602–614, 2014.E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, “On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification”, Automatic Control and Computer Sciences, vol. 50, no. 7, pp. 510–519, 2016.E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, “On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification”, Automatic Control and Computer Sciences, vol. 50, no. 7, pp. 510–519, 2016.

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