T13 - Diagramas de decisão binários.

6 dezembro 2012, 15:00 • Jaime Ramos

Diagramas de decisão binários para representação de funções Booleanas (OBDD). Função determinada por OBDD. Diagramas de decisão binários reduzidos (ROBDD). Existência e unicidade de ROBDD para uma funçã Booleana. Regras de redução. Correcção e completude das regras.

Algumas formas de justiça. Justiça em LTL e em CTL.

Comparação entre a verificação de modelos em LTL e em CTL. vantagens e desvantagens.