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.

Specification Patterns

 Abstract

The software design patterns (Design Patterns) are considered since the 90s, as the ideal solution for the construction of computer applications, in this sense, under a general approach, reusable and with the potential to be applied to different problems of computer science nature, is shown as the most favorable solution when designing software, it is mainly templates, which help us to identify potential situations of failure in software design, likewise, provide solutions to general and specific problems faced by programmers during the phases of software development.

Key words

Linear Temporal Logic (LTL), Pattern Design, Formal Methods, Temporal Logic.

Context

In the 1990s, four great thinkers (Erich Gamma, Richard Helm, Ralph Johnson and John Vlissides), known as the Gang of Four (GoF), came together and published a book entitled "Design Patterns: Elements of Reusable Object-Oriented Software", in which they proposed the need to incorporate reusable object-oriented software elements.

This led to the initiation of the design pattern concept in software development, which includes 23 common design patterns. Each of them defines the solution to solve a given problem, facilitating the reuse of source code, Wikipedia (2022).

According to Rodríguez Cruz Abeyro, A. J. (2020), the constant growth of the information technology sector has led to the evolution of software development practices. Previously, all software was required to be completed before testing, which meant encountering programming and design problems.

To mitigate such situations, which in turn lead to high costs in time and in returning to development stages once it has been completed, a practice currently known as Testing was introduced during the development phase.

This practice is used to identify error conditions and problems in the code, which may not be evident during the execution of the application. Relying on verification patterns and error detection through models and techniques, procedural, which ultimately make the design patterns help you to be sure of the validity of our code.

In this sense, design patterns based on linear temporal logic (LTL or PLTL), have time as a base model, they are considered as a numerable set of instances organized in a linear way, easy to debug and decompose, the LTL temporal logic is considered clear and intuitive (Vardi 2001), for the description of processes in a natural and understandable way.

Considering that each pattern is considered a time scope, they seek to relate each problem from a conceptual logical point of view, which allows to diagram such situations in a predetermined way, and with moderately pre-established solutions, which allow to have an initial framework for the detection of possible causes, effects and potential solutions.

Conclusions

Design patterns have been the most versatile tools when developing computer applications. Likewise, their incorporation as software construction patterns in Linear Temporal Logic (LTL) provides programmers with an important programming tool, since they facilitate the understanding of the input and output processes in a system and help mitigate the risk of potential errors during the development of the systems.

Bibliography

• Rosales Morales, V. Y., Alor-Hernández, G., & Mejia-Miranda, J. (2017). "Development of a software platform for code generation for multi-device applications from image processing" (Doctoral dissertation, Instituto Tecnológico de Orizaba).
• Rodríguez Cruz Abeyro, A. J. (2020). Pattern detection in gaze using model checking (Doctoral dissertation, Universidad Veracruzana. Faculty of Statistics and Informatics. Xalapa Region).
• Muñoz Gutierrez, C. (2000). Non-Classical Logics. Apunte de Cátedra, Lógica y Computación, Departamento de Lógica y Filosofía de la Ciencia, Universidad Complutense de Madrid, Spain.

Introduction to Formal Methods

 Abstract

Formal verification has been very useful in highly critical computer systems, ranging from air traffic systems to microcircuit design. When we talk about verification techniques of symbolic models of linear temporal logic (LTL), we must take into account that this technique helps us to represent in a natural way and by means of human logic, the correct development of processes that seem complex, but that through the use of mathematical symbologies, we can express in an understandable way.

Key words: Linear temporal logic (LTL), Formal methods.

Context

According to AF Domínguez (2018), temporal logic (TL, Temporal Logic) is a variant of modal logic that has as its focus the succession of events over time (Markey 2015). It extends propositional logic with modal and temporal operators such as: never, always, sometimes, sometimes, eventually, among others.

TL allows specifying qualitative properties (Konur 2013) -using standard TL- or quantitative properties -using TL with timed extensions- of the dynamic knowledge of a system to represent desirable behaviors. It even allows reasoning about how such behaviors change over time.

The standard TL expresses restrictions on the relative order of events or cases (for example:, in the expression "Every time (1) a customer requests to reserve an entity, (2) an employee must check the availability of the entity", it can be observed that for event 2 to occur, event 1 must always occur first, i.e., 1 is before 2 and therefore 2 is after 1), by means of timed extensions the TL adds real time restrictions that relate the exact occurrence of those events - Domínguez, A. F. (2018). Master's Thesis.

As in modal logic, the semantics of TL is defined in Kripke structures (a variation of transition systems to represent behaviors of a system) (Laroussinie & Schnoebelen 1995). These structures are used in model checking.

The TL comprises two main frames: linear time and branched time. In a Kripke structure, the linear time frame aims to express the properties along each individual or group trajectory as the case may be, while the branched time frame adds quantification over the possible trajectories.

Its routine application to represent and reason about temporal information, to specify desirable behaviors of computer systems is very useful, and in turn, its ability to verify that certain behavior is fulfilled, as established by a particular specification, is significant during the process of conception of the functional logic of computational processes.

According to Domínguez, A. F. (2018). Master's Thesis, additional applications include the specification of reactive and concurrent systems, formal verification of hardware/software protocols, manual and automatic program composition support, as well as verification of documents and hypermedia applications.

Conclusions

The linear time logic (LTL) modeling is very helpful when diagramming specific processes, where the realization of flows is required in a natural and understandable way, and with the ability to extrapolate to a computational language.

Bibliography

• Garis, A. G. (2010). Temporal logic in software model checking. Origin and evolution to current times. Foundations in Humanities, 11(21), 151-161.
• Kristin Y. Rozier, Linear Temporal Logic Symbolic Model Checking, Computer Science Review, Volume 5, Issue 2, 2011, Pages 163-203, ISSN 1574-0137.
• DOMÍNGUEZ, Alejandro Fernández. Master's Thesis. 2018.

PhD in Informatics

 Already 2 months ago I started to realize a pending dream, which is to start my doctorate, and with it help to improve the world.