maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2022-1-44-59mais-1607Research ArticleTheory of ComputingLTL-спецификация ограниченных счётчиковых машинLTL-Specification of Bounded Counter Machineshttps://orcid.org/0000-0003-0500-306XКузьминЕгор ВладимировичKuzminEgor V.kuzmin@uniyar.ac.ruЯрославский государственный университет им. П. Г. ДемидоваРоссияP. G. Demidov Yaroslavl State UniversityRussian Federation2022170320222914459Copyright © Кузьмин Е.В., 20222022Кузьмин Е.В.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/1607

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

The article revises the results of the work devoted to the problem of representing the behaviour of a program system as a set of formulas of the linear temporal logic LTL, followed by the use of this representation to verify the satisfiability of the program system properties through the procedure of proving the validity of logical inferences, expressed in terms of the LTL logic. The LTL logic is applied to bounded Minsky counter machines that are considered as program systems of which we need to get the specification of its behaviour. Earlier, when working with the temporal logic LTL as a program logic, a special pseudo-operator was actually introduced to refer to the previous values of variables involved in elementary propositions. Despite the fact that this pseudo-operator is easily implemented in the Cadence SMV verifier when proving the validity of logical LTL-inferences, the classical definition of the LTL logic does not imply its presence. In this article, only binary variables will be used to build an LTL-specification for the behaviour of a bounded counter machine, and tracking of previous values of these variables will be carried out exclusively within the LTL logic itself through the appropriate formulas.

неклассическая логикалинейная темпоральная логикасчётчиковые машиныLTL-спецификацияnon-classical logiclinear temporal logiccounter machinesLTL-specificationReferencesE. V. Kuzmin, “LTL-Specification of Counter Machines”, in Russian, Modeling and Analysis of Information Systems, vol. 28, no. 1, pp. 104-119, 2021.E. V. Kuzmin, “LTL-Specification of Counter Machines”, in Russian, Modeling and Analysis of Information Systems, vol. 28, no. 1, pp. 104-119, 2021.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.Cadence SMV. [Online]. Available: http://www.kenmcmil.com/smv.html.Cadence SMV. [Online]. Available: http://www.kenmcmil.com/smv.html.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.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.E. 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.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.

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