Usuario:Pau84/Lógica Temporal de Acciones (TLA)

En matemáticas, lógica, ciencias de la computación y ciencias relacionadas, la lógica temporal de las acciones (TLA) es una lógica que combina la lógica temporal y la lógica de acciones para la especificación y el razonamiento de sistemas concurrentes, originalmente desarrollada por Leslie Lamport.

Introducción[editar]

TLA se utiliza para la verificación de programas y la comprobación de la agilidad de las propiedades de los programas. TLA es simple, basa su teoría en que los sistemas y sus propiedades se representan en una misma lógica donde, su sintaxis y la semántica formal completas se resumen en una página aproximadamente. Sin embargo, a pesar de ser simple, TLA es muy potente, tanto en la teoría como en la práctica.

Semántica[editar]

En TLA, los algoritmos se representan con fórmulas y la semántica de fórmulas se basa en secuencias de estados. Todas las fórmulas elementales de TLA son acciones, y se pueden expresar en términos de operadores matemáticos conocidos (por ejemplo ∧), además de otras tres adicionales:

primero ( ' )
siempre ( □ ) y
cuantificador existencial ( ∃ ).

Ideas básicas[editar]

Las fórmulas de la lógica de las acciones se construyen usando los valores, las variables, los estados, las funciones estado y las acciones, y la lógica temporal es una clase de lógica que modela razonamientos sobre las secuencias de estados (la lógica del tiempo).

Un estado (o predicado) es una asignación de valores a las variables, por ejemplo, asignar el valor 22 a la variable hr es un estado en un sistema reloj.

Una acción es una expresión booleana que consta de variables, variables iniciadas y constantes. Una acción muestra la relación entre el estado anterior y uno nuevo, por ejemplo, hr'=hr+1.

Una función estado es una expresión no booleana, en este caso, pero construida también con constantes y simbolos, como por ejemplo x²+y-3.

Un ejemplo de un trozo de algoritmo, que en un lenguaje de programación convencional podría ser:

initially x = 0 ;

loop forever x := x + 1 end loop

en la especificación TLA es una fórmula π definida de la siguiente forma:

{\begin{aligned}\Pi {\overset {\vartriangle }{=}}&x=0\\&\land \Box [x'=x+1]_{x}\\&\land \mathrm {WF} _{x}(x'=x+1)\end{aligned}}

donde:

Sintácticamente, una fórmula TLA tiene una de las siguientes formas:

Operadores TLA

Herramientas[editar]

Referencias[editar]

Enlaces Externos[editar]