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.