LTL-Specification of Counter Machines
https://doi.org/10.18255/1818-1015-2021-1-104-119
Abstract
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.
Supporting agencies: This work was supported by P. G. Demidov Yaroslavl State University Project № VIP-016
About the Author
Egor V. Kuzmin
P. G. Demidov Yaroslavl State University
Russian Federation
Russian Federation
Professor, Doctor of Science
14 Sovetskaya str., Yaroslavl 150003
References
1. E. V. Kuzmin, Non-Classical Propositional Logics, in Russian. Yaroslavl: P.G. Demidov Yaroslavl State University, 2016, p. 160.
2. G. Priest, An Introduction to Non-Classical Logic. From if to is. Cambridge University Press, 2008, p. 648.
3. M. Minsky, Computation: Finite and Infinite Machines. Prentice-Hall, Inc., 1967.
4. R. Schroeppel, “A Two Counter Machine Cannot Calculate 2N”, Massachusetts Institute of Technology, Artificial Intelligence Laboratory, Artificial Intelligence Memo #257, 1972, p. 32.
5. E. V. Kuzmin, Counter Machines, in Russian. Yaroslavl: Yaroslavl State University, 2010, p. 128.
6. 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.
7. E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking. The MIT Press, 2001.
8. C. Baier and J.-P. Katoen, Principles of Model Checking. The MIT Press, 2008.
9. Cadence SMV. [Online]. Available: http://www.kenmcmil.com/smv.html.
10. E. Clarke, O. Grumberg, and K. Hamaguchi, “Another Look at LTL Model Checking”, Carnegie Mellon University, Tech. Rep. CMU-CS-94-114, 1994.
11. 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.
12. 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.
13. 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.
14. 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.
15. 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.
16. 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.
Review
For citations:
Kuzmin E.V. LTL-Specification of Counter Machines. Modeling and Analysis of Information Systems. 2021;28(1):104-119. (In Russ.) https://doi.org/10.18255/1818-1015-2021-1-104-119
Views:
570
Email this article 