Métodos de prova para propriedades de invariância

Neste capítulo são apresentados métodos de prova para provar fórmulas do tipo

$$\Box p$$

onde p é uma fórmula de estado (i.é, sem conectivas temporais). Como já foi visto no capítulo 2, estas fórmulas são designadas propriedades de invariância pois implicam que p seja vardadeira em todos os estados acessíveis de um programa.