Métodos de prova para propriedades à espera de

Neste método serão apresentados métodos de prova para propriedades do tipo à espera de, cuja forma mais geral é dada pela fórmula

onde p, q₀, q₁, ..., q_m são fórmulas de estado. Esta fórmula é válida numa computação se todos os estados onde se verifica p dão início a uma sequência de intervalos onde se verificam sucessivamente q_m a q₀. Cada um destes intervalos pode ser vazio ou extender-se até ao infinito. Esta fórmula é um caso particular de uma propriedade de segurança, mas que envolve operadores sobre o passado (não podendo ser provada com os métodos do capítulo anterior).