Esclarecimento de dúvidas sobre os projectos práticos.

Operações sobre Ordered Binary-Decision Diagrams: construção reduzida, operações binárias e restrição.

Exercícios sobre Ordered Binary-Decision Diagrams.

Introdução aos Ordered Binary-Decision Diagrams.

Exemplos de verificação simbólica para a lógica CTL.

Verificação por modelos usando a ferramenta SMV.

Introdução à verificação por modelos simbólica para a lógica CTL. Demonstração da ferramenta de verificação SMV.

Algoritmo linear para verificação directa de propriedades CTL. Verificação de modelos sob condições de justiça.

Exercícios sobre verificação directa de propriedades CTL usando o algoritmo de ponto fixo.

Introdução à verificação por modelos. Verificação directa de fórmulas CTL usando pontos fixos.