Lógica temporal de ações

Lógica temporal de ações (LTA) é uma lógica desenvolvida por Leslie Lamport, que combina a Lógica temporal com a lógica de ações. É usada para descrever comportamentos de sistemas concorrentes.

Detalhes

Declarações na lógica temporal são da forma $[A{]}_t$, onde A é a ação e t contem um subconjunto de variáveis ocorrendo em A. Uma ação é uma expressão contendo variáveis primas e não primas, assim como $x+x^{\prime }*y=y^{\prime }$. O significado de variável não-prima é o valor da variável neste estado. O significado de variável prima é o valor da variável no próximo estado. A expressão acima significa o valor de x agora, mais o valor de x depois vezes o valor de y agora, igual ao valor de y depois.

O significado de $[A{]}_t$ é que ou A é válida agora, ou as variáveis que ocorrem em t não mudam. Isto possibilita para os passos, no qual nenhuma das variáveis de programa mudam o seus valores.

Editores

Alguns editores TLA+ incluem:

• TLA+ Toolbox (Uma IDE Eclipse para ferramentas TLA+, incluindo o tradutor PlusCal, Modelo TLC de verificação e Sistema de prova TLA+)
• Eclipse TLA+ Plugin
• VisualTLA
• TLA Editor
• TLA# Plugin para Microsoft Visual Studio 2005

Ver também

• Lógica temporal
• PlusCal

• Predefinição:Citar livro
• Predefinição:Citation

Ligações externas

• Lamport's page no TLA
• Official TLA+ site
• O sistema de prova TLA+