T10 - Conclusão da aula anterior. Lógica temporal ramificada

15 novembro 2012, 15:00 • Jaime Ramos

Conclusão da aula anterior. Exemplo da construção do autómato de Buchi para a fórmula (pUq).

Lógica temporal ramificada: motivação, Computation Tree Logic (CTL), sintaxe e semântica.

Exemplos. Equivalência de fórmulas. Forma normal existêncial (ENF). Equivalência entre fórmulas CTL e fórmulas LTL.

P07 - SPIN e LTL

12 novembro 2012, 09:00 • David João Barros Henriques

Timeouts, processos activos, justiça fraca e forte em SPIN. Especificação e verificação de propriedades LTL em SPIN. Resolução dos exercícios 5.5 e 5.6 das folhas da cadeira.

T09 - Verificação de modelos para LTL

8 novembro 2012, 15:00 • Jaime Ramos

Estrutura genérica do algoritmo de verificação de modelos para LTL. Conjunto elementar. Existência de autómato de Buchi generalizado que reconhece o conjunto de modelos de uma fórmula LTL. Aplicação deste resultado à verificação de modelos para fórmulas LTL.

P06 - Exercícios sobre Lógica Temporal Linear

5 novembro 2012, 09:00 • David João Barros Henriques

Resolução dos exercícios 5.1, 5.2.1, 5.2.1, 5.2.2, 5.2.3, 5.2.5, 5.3, 5.4, 4.10 das folhas da cadeira.

P05 - Exercícios sobre Propriedades Regulares

29 outubro 2012, 09:00 • David João Barros Henriques

Resolução dos exercícios 4.1, 4.2, 4.3, 4.4, 4.5, 4.6, 4.7, 4.8 das folhas da cadeira.