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
editarTLA 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
editarEn 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
editarLas 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:
donde:
Sintácticamente, una fórmula TLA tiene una de las siguientes formas:
Herramientas
editar- TLA+ Toolbox
- Plugin TLA+ para Eclipse
- VisualTLA
- TLA Editor
- TLA# Plugin for Microsoft Visual Studio 2005
Referencias
editar- The Temporal Logic of Actions (Microsoft)
- Presentación (The Temporal Logic of Actions) Autor:Massimiliano Menarini
- Introducción a TLA (Compac)