LTL-specification of counter machines

E. V. Kuzmin

Modelirovanie i analiz informacionnyh sistem, Tome 28 (2021) no. 1, pp. 104-119.

Résumé

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 reflected 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.

Détail

Keywords: non-classical logic, linear temporal logic, counter machines, LTL-specification.

Bibliographie

[1] E. V. Kuzmin, Non-classical propositional logics, P.G. Demidov Yaroslavl State University, Yaroslavl, 2016, 160 (in Russian)

[2] G. Priest, An introduction to non-classical logic. From if to is, Cambridge University Press, 2008, 648 | MR

[3] M. Minsky, Computation: finite and infinite machines, Prentice-Hall, Inc., 1967 | MR | Zbl

[4] R. Schroeppel, A two counter machine cannot calculate $2^N$, Artificial Intelligence Memo No 257, Massachusetts Institute of Technology, Artificial Intelligence Laboratory, 1972, 32 pp.

[5] E. V. Kuzmin, Counter machines, Yaroslavl State University, Yaroslavl, 2010, 128 (in Russian)

[6] A. Pnueli, “The temporal logic of programs”, 18th annual symposium on foundations of computer science, SFCS 1977, IEEE Computer Society Press, 1977, 46-57 | MR

[7] E. M. Clarke, O. Grumberg, D. A. Peled, Model checking, The MIT Press, 2001 | MR

[8] C. Baier, J. Katoen, Principles of model checking, The MIT Press, 2008 | MR

[9] Cadence SMV, http://www.kenmcmil.com/smv.html

[10] E. Clarke, O. Grumberg, K. Hamaguchi, Another look at ltl model checking, Teh. Rep. CMU-CS-94-114, Carnegie Mellon University, 1994

[11] E. V. Kuzmin, V. A. Sokolov, “On construction and verification of PLC programs”, Automatic Control and Computer Sciences, 47:7 (2013), 443–451 | DOI

[12] E. V. Kuzmin, V. A. Sokolov, “Modeling, specification and construction of PLC-programs”, Automatic Control and Computer Sciences, 48:7 (2014), 554–563 | DOI

[13] E. V. Kuzmin, V. A. Sokolov, D. A. Ryabukhin, “Construction and verification of PLC-programs by LTL-specification”, Automatic Control and Computer Sciences, 49:7 (2015), 453–465 | DOI

[14] E. V. Kuzmin, V. A. Sokolov, D. A. Ryabukhin, “Construction and verification of plc ld programs by the ltl specification”, Automatic Control and Computer Sciences, 48:7 (2014), 424–436 | DOI

[15] E. V. Kuzmin, D. A. Ryabukhin, V. A. Sokolov, “Modeling a consistent behavior of plc-sensors”, Automatic Control and Computer Sciences, 48:7 (2014), 602–614 | DOI

[16] E. V. Kuzmin, D. A. Ryabukhin, V. A. Sokolov, “On the expressiveness of the approach to constructing PLC-programs by LTL-specification”, Automatic Control and Computer Sciences, 50:7 (2016), 510–519 | DOI | MR