LTL-Specification of Counter Machines
| Autor: | Egor V. Kuzmin |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
Counter machine
Economics and Econometrics Correctness Computer science 0211 other engineering and technologies counter machines 02 engineering and technology Information technology computer.software_genre non-classical logic Turing machine symbols.namesake Linear temporal logic Computer Science::Logic in Computer Science 0202 electrical engineering electronic engineering information engineering Materials Chemistry Media Technology ltl-specification Software system 021110 strategic defence & security studies Computer program Programming language Forestry Non-classical logic linear temporal logic T58.5-58.64 Satisfiability symbols 020201 artificial intelligence & image processing computer |
| Zdroj: | Modelirovanie i Analiz Informacionnyh Sistem, Vol 28, Iss 1, Pp 104-119 (2021) |
| ISSN: | 2313-5417 1818-1015 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|