Classes e exemplos de fórmulas temporais

As fórmulas da lógica temporal linear podem ser agrupadas em classes de acordo com o seu poder expressivo. Nas fórmulas seguintes prepresenta uma fórmula temporal sobre o passado^2.1. Podemos definir as seguintes classes de fórmulas temporais, caracterizadas pelos seus operadores mais externos:

• $\Box p$. Proriedade de segurança ou invariância. Impõe que p se verifique sempre durante a execução do programa.
• $\Diamond p$. Propriedade de animação ou garantia. Garante que p se verificará algures no furuto.
• $\Box \Diamond p$. Propriedade de resposta. Indica que p ocorre um número infinito de vezes durante a execução do programa.
• $\Diamond \Box p$. Propriedade de persistência. Garante que p será sempre válida a partir de um determinado instante de tempo no futuro.

A seguir apresentamos alguns exemplos de fórmulas temporais e o respectivo significado informal (p, q e r são fórmulas de estado):

• $p \supset \Diamond q$. Se p se verificar no início da execução então q será eventualmente verdadade. Propriedade de animação.
• $(p \Rightarrow \Diamond q)$. Qualquer estado onde p se verifique coincide ou é seguido por um estado onde q também se verifica. Propriedade de resposta.
• $\lnot q \mathcal{W} p$. O ocorrência de q deve ser antecedida pela ocorrência de p. Propriedade de segurança.
• $p \Rightarrow \Diamond \Box q$. Um estado onde se verifique p é eventualmente seguido de um estado a partir do qual q é sempre verdade. Propriedade de persistência.
• $(p \Rightarrow q \mathcal{W} r)$. A ocorrência de p despoleta uma sequência de estados onde q se verifica, eventualmente terminada pela ocorrência de r.
• $\Box \exists u \cdot (x = u \land \Circle(x = u + 1))$. Nesta fórmula u é uma variável rígida e x uma variável flexível e o seu significado é o seguinte: o valor de x é incrementado de uma unidade em todos os estados.
• $\forall u \cdot (x = u \Rightarrow \Diamond(y = u))$. Nesta fórmula u é uma variável rígida e x e y são variáveis flexíveis e o seu significado é o seguinte: qualquer valor que x possa assumir é eventualmente assumido por y.