LTL-Specification of Bounded Counter Machines
https://doi.org/10.18255/1818-1015-2022-1-44-59
Abstract
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.
References
1. E. V. Kuzmin, “LTL-Specification of Counter Machines”, in Russian, Modeling and Analysis of Information Systems, vol. 28, no. 1, pp. 104-119, 2021.
2. M. Minsky, Computation: Finite and Infinite Machines. Prentice-Hall, Inc., 1967.
3. R. Schroeppel, “A Two Counter Machine Cannot Calculate 2N ”, Massachusetts Institute of Technology, Artificial Intelligence Laboratory, Artificial Intelligence Memo #257, 1972, p. 32.
4. E. V. Kuzmin, Counter Machines, in Russian. Yaroslavl: Yaroslavl State University, 2010, p. 128.
5. Cadence SMV. [Online]. Available: http://www.kenmcmil.com/smv.html.
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. G. Priest, An Introduction to Non-Classical Logic. From if to is. Cambridge University Press, 2008, p. 648.
10. E. V. Kuzmin, Non-Classical Propositional Logics, in Russian. Yaroslavl: P.G. Demidov Yaroslavl State University, 2016, p. 160.
11. E. Clarke, O. Grumberg, and K. Hamaguchi, “Another Look at LTL Model Checking”, Carnegie Mellon University, Tech. Rep. CMU-CS-94-114, 1994.
Review
For citations:
Kuzmin E.V. LTL-Specification of Bounded Counter Machines. Modeling and Analysis of Information Systems. 2022;29(1):44-59. (In Russ.) https://doi.org/10.18255/1818-1015-2022-1-44-59
Views:
494
Email this article 