Top

Automatic Control and Computer Sciences

Published in:

01-12-2023

Linear Temporal Logic Specification of Bounded Counter Machines

Author: E. V. Kuzmin

Published in: Automatic Control and Computer Sciences | Issue 7/2023

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

This article revises the results of work devoted to representing the behavior of a program system as a set of formulae of linear temporal logic (LTL), followed by the use of this representation to verify the satisfiability of the program properties of the system by proving the validity of logical inferences expressed in terms of the LTL. This logic is applied to bounded Minsky counter machines considered as program systems whose behavior must be specified. Earlier on, a special pseudooperator was introduced for referring to previous values of variables used in elementary propositions when working with the LTL temporal logic as a program logic. Even though this pseudooperator is easy to implement in the Cadence SMV verifier when proving the validity of logical LTL inferences, the classical definition of the LTL does not imply its presence. This article will use only binary variables to build the LTL specification for the behavior of a bounded counter machine. Previous values of these variables will be tracked through the appropriate formulas exclusively within the LTL itself.

previous article Recursive-Parallel Algorithm for Solving the Graph-Subgraph Isomorphism Problem

next article Methods for Changing Parallelism in the Process of High-Level VLSI Synthesis

Kuzmin, E.V., LTL-specification of counter machines, Autom. Control Comput. Sci., 2022, vol. 56, pp. 711–722. https://doi.org/10.3103/S0146411622070112CrossRef

Minsky, M., Computation: Finite and Infinite Machines, Prentice-Hall, 1967.

Schroeppel, R., A two counter machine cannot calculate 2^N, Artificial Intelligence Memo, Artificial Intelligence Laboratory, 1972, no. 257, p. 32.

Kuzmin, E.V., Schetchikovye mashiny (Counter Machines), Yaroslavl: Yaroslavl. Gos. Univ., 2010.

Cadence SMV. http://www.kenmcmil.com/smv.html.

Pnueli, A., The temporal logic of programs, 18th Annu. Symp. on Foundations of Computer Science (sfcs 1977), Providence, R.I., 1977, IEEE, 1977, pp. 46–57. https://doi.org/10.1109/sfcs.1977.32

Clarke, E.M., Grumberg, O., and Peled, D.A., Model Checking, Cambridge, Mass.: MIT Press, 2001.CrossRef

Baier, C. and Katoen, J.-P., Principles of Model Checking, Cambridge, Mass.: MIT Press, 2008.

Priest, G., An Introduction to Non-Classical Logic. From If to Is, Cambridge Introductions to Philosophy, Cambridge Univ. Press, 2008, 2nd ed.

10.

Kuzmin, E.V., Neklassicheskie logiki vyskazyvanii (Nonclassical Propositional Logics), Yaroslavl: Yaroslavl. Gos. Univ. im. P.G. Demidova, 2016.

11.

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

Title: Linear Temporal Logic Specification of Bounded Counter Machines
Author: E. V. Kuzmin
Publication date: 01-12-2023
Publisher: Pleiades Publishing
Published in: Automatic Control and Computer Sciences / Issue 7/2023
Print ISSN: 0146-4116
Electronic ISSN: 1558-108X
DOI: https://doi.org/10.3103/S0146411623070064

Springer Professional

Abstract

Please log in to get access to your license.

Other articles of this Issue 7/2023

Neural Network Sentiment Classification of Russian Sentences into Four Classes

An Algorithm of Angular Superresolution Using the Cholesky Decomposition and Its Implementation Based on Parallel Computing Technology

Recursive Sentiment Detection Algorithm for Russian Sentences

Research of Models of Topological Relations of Spatial Features

Transformation of C Programming Language Memory Model into Object-Oriented Representation of EO Language

Text Model for the Automatic Scoring of Business Letter Writing