Exercícios sobre Model Checking

Instale a ferramenta de model checking NuSMV e utilize-a para resolver os seguintes exercícios:

1. Verifique que o algoritmo de Peterson para exclusão mútua entre 2 processos satisfaz as seguintes propriedades:
   • Exclusão mútua: os processos não estão simultaneamente na região crítica;
   • Ausência de starvation: um processo que pretenda aceder à região crítica eventualmente conseguirá;
   • Prioridade: o primeiro processo a requisitar o acesso à região crítica é o sempre o primeiro a aceder à dita.
2. As seguintes propriedades em lógica temporal não são equivalentes. Tente encontrar sistemas de transição (o mais simples possíveis) que confirmem isso:
   • AG p e EG p
   • AF p e EF p
   • AG (p -> p) e AG (p -> AF p)
   • AG (p -> p) e AG (p -> AG p)
   • AF (p & q) e AF p & AF q
   • AG (p | q) e AG p | AG q
   • AF AX p e F X p
   • G F p -> G F q e AG AF p -> AG AF q