Geodesic
LTL-specification of bounded counter machines
Modelirovanie i analiz informacionnyh sistem, Tome 29 (2022) no. 1, pp. 44-59.

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: non-classical logic, linear temporal logic, counter machines, LTL-specification. 
@article{MAIS_2022_29_1_a3,
     author = {E. V. Kuzmin},
     title = {LTL-specification of bounded counter machines},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {44--59},
     publisher = {mathdoc},
     volume = {29},
     number = {1},
     year = {2022},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2022_29_1_a3/}
}
TY  - JOUR
AU  - E. V. Kuzmin
TI  - LTL-specification of bounded counter machines
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2022
SP  - 44
EP  - 59
VL  - 29
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2022_29_1_a3/
LA  - ru
ID  - MAIS_2022_29_1_a3
ER  - 
%0 Journal Article
%A E. V. Kuzmin
%T LTL-specification of bounded counter machines
%J Modelirovanie i analiz informacionnyh sistem
%D 2022
%P 44-59
%V 29
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2022_29_1_a3/
%G ru
%F MAIS_2022_29_1_a3
E. V. Kuzmin. LTL-specification of bounded counter machines. Modelirovanie i analiz informacionnyh sistem, Tome 29 (2022) no. 1, pp. 44-59. http://geodesic.mathdoc.fr/item/MAIS_2022_29_1_a3/

[1] E. V. Kuzmin, “LTL-Specification of Counter Machines”, Modeling and Analysis of Information Systems, 28:1 (2021), 104–119 (in Russian) | DOI | MR

[2] M. Minsky, Computation: Finite and Infinite Machines, Prentice-Hall, Inc, 1967 | MR | Zbl

[3] R. Schroeppel, A Two Counter Machine Cannot Calculate $2^N$, Artificial Intelligence Memo #257, Massachusetts Institute of Technology, Artificial Intelligence Laboratory, 1972, 32 pp.

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

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

[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. P. Katoen, Principles of Model Checking, The MIT Press, 2008 | MR

[9] G. Priest, An Introduction to Non-Classical Logic. From if to is, Cambridge University Press, 2008, 648 | MR

[10] E. V. Kuzmin, Non-Classical Propositional Logics, P.G. Demidov Yaroslavl State University, Yaroslavl, 2016, 160 (in Russian)

[11] E. Clarke, O. Grumberg, K. Hamaguchi, Another Look at LTL Model Checking, Tech. Rep. CMU-CS-94-114, Carnegie Mellon University, 1994