Turing Machine

What does the Church-Turing Thesis postulate?

Salinas Molina, M. A. (2011), proposes that the Church-Turing thesis defines the computability of a computable function, an important result in computer science because it helped to formulate a discipline of human knowledge: Computer science.

His real success was to bring out the compiler theory, whose object is to make the programs that run on computers closely related to the concepts of algorithm and recursion, its statement is presented as follows: A function is effectively computable if only if it is Turing computable. This includes two concepts, the first on the effectively computable function that refers to the recursive functions that are an effective computation, stated by Church in the lambda calculus; the second on the effective procedure, definition given by Turing in the sense of successfully executing a sequence of instructions in a Turing machine.

Vargas, C., & de Costa Rica, I. T. (1996), establishes that the Church-Turing thesis deals with the algorithm for the calculation of a mathematical function, which is impossible to demonstrate mathematically, since the concept is of an intuitive nature. In this sense, we can establish that the computable coincides with the Turing-Computable (computable by means of MT).

What is the difference between a search problem and a decision problem?

When we talk about a search problem, the Turing Machine understands that it receives an input of information and returns an output depending on what is supplied, on the other hand, when the MT is confronted with a decision problem, where the input data can be a value from 1 to 'n' values, the expected results would be presented in a binary form, that is, ones and zeros, understanding that its output would be a value between 'True' or 'False', Martínez, G. D. J. R. (2016).

Why in the case of decision problems, can we refer interchangeably to problems and languages?

The execution process of a Turing Machine, starts initially from a tape that forms a Tuple of values, which are represented, as a language of sets of strings, Favio Perea (2013).

For example: we can represent the execution of values in a TM, by means of the following set of strings

T = (Σ, Q, q0, qf, δ)

Where:

Σ = ∅ is a finite alphabet containing a distinguished symbol, called the white symbol,

Q = ∅ is the finite set of states, which includes q0 and qf, q0 is the initial state,

qf is the final state of acceptance

δ is a transition function whose domain is a subset of Q × Σ and whose contradomain is Q × Σ × M. Such that if δ is defined for the pair (l, s) ∈ Q × Σ and δ (l, s) = (l', s', m).

Then:

(l) is the current state,

(s) the symbol being read by the head, 

(l') the state to which the transition will take us (s') the symbol to be written,

(m) the movement that the head will make.

Bibliography

• Salinas Molina, M. A. (2011). Computability and Turing machine.
• Muro, V. (2018, January). Computability, randomness and the Church-Turing Physics Thesis. I Jornadas de Estudiantes del Departamento de Filosofía.
• Vargas, C., & de Costa Rica, I. T. (1996). Artificial Intelligence (AI) and Cognitive Science be known and discussed in. Memoria, 348.
• Martínez, G. D. J. J. R. (2016). Some challenges to the Turing test. Luxiérnaga-Philosophy Student Journal, 6(11), 21-21.

GOAL Tool, Büchi Automatons

 Abstract

Büchi automata and linear logic formulas are very useful for verification and validation of software requirements, as well as for multiple tasks that require analysis and measurement of future time parameters. However, in order to perform these tasks accurately, it is recommended to have a technological instrument that allows the graphical representation of these models in a legible and understandable way, in view of the specialist in charge of collecting such information.

Key words

Linear Temporal Logic (LTL), Büchi Automata and Arithmetic Operators.

Context

Linear-Time Temporal Logic (LTL) was born in 1977 by Amir Pnuli for the verification of sequential and parallel programs [Pnueli, 1977], and later, together with Zohar Manna, presented a methodology based on this logic for the specification and verification of reactive systems [Manna and Pnueli, 1992; Manna and Pnueli, 1995]. LTL has the temporal operators; (P) (Current Time), (F) (Future Time) and (U) (Until) that allow us to characterize properties about the execution of the system, that is, we can refer to what can happen in the future time.

According to, R. Degiovanni (2015), as we already mentioned, the temporal organization of LTL is linear. That is, time is modeled as an infinite sequence of states where each one has a unique successor, modeling how propositions change value along the execution of the system.

The graphical presentation of a linear time execution process can be represented by using the GOAL technology tool, which stands for "Graphical Tool for Omega Automata and Logics", launched in 2007, and its main developers were Yih-Kuen Tsay, Ming-Hsien Tsai, Shi-Shian and Jie Lin.

GOAL is an interactive graphical tool (developed with the JAVA programming language) for defining and manipulating Büchi automata, and formulas of temporal logic. Chicano (2007) defines a Büchi automaton as a tuple A = (S, Q, D, Q0, F), where ∑ is a finite alphabet, Q is a finite set of states, D ∈ Q x ∑ x Q is a transition relation, Q 0 ∈ Q is the set of initial states and F ∈ Q is the set of accepting states.

Amir Pnueli (1977), established linear time temporal logic, as a tool capable of making references to time by encoding future paths.

According to Wikipedia (2022), LTLs were constructed from a finite set of propositional variables AP , the logical operators and the temporal modal operators X (some literature uses O or N ) and U. They form the set of LTL formulas over AP.

It is defined inductively as follows:

- if p ∈ AP then p is an LTL formula;

- if ψ and φ are LTL formulas, then ¬ψ, φ ∨ ψ, X ψ and φ U ψ are LTL formulas.

In such sense, in this paper, we can observe different models generated through the GOAL application, in which by means of LTL, we can see generated Büchi automata, according to their specification pattern and corresponding formula.

Conclusions

Before analyzing, interpreting and verifying a given model of a system, it is necessary to transform it into a structure, from which the verification algorithm can be applied. Through Kripke's structure and Büchi's automata, the formalization of the properties of a system is achieved.

Bibliography

• Lisboa, J. L. C., Hernández, M. D. M., Ramos, P. N. B., & Klimkiewicz, A. G. (2019). Modelo teórico para la especificación y gestión de procesos de negocio, sustentado en el uso de Big Data e Internet de las Cosas (IoT)/Conceptual theoric model for the specification and management of the business process, based on the use of Big Data and Inte. La Revista Argentina de Investigación en Negocios (RAIN), 5(2), 141-160.
• Schapachnik, F. (2007). Verification of timed automata in single-processor and multiprocessor architectures (Doctoral dissertation, Universidad de Buenos Aires. Faculty of Exact and Natural Sciences).
• Lacerda, B., & Lima, P. (2008). Linear-time temporal logic control of discrete event models of cooperative robots.