Logica temporal de tempo ramificado: CTL* e CTL. Comparação entre as lógicas CTL e LTL.

Especificação e verificação de propriedades LTL com a ferramenta Maria.

Exercícios sobre especificação de propriedades LTL.

Amanhã a aula teórica será dada antes da aula prática. Peço desculpa pelo aviso tardio.

Não houve aula. A mesma será compensada em data a combinar com os alunos.

No dia 19 de Abril não haverá aula teórica.

Foram publicados mais dois projectos com funcionalidades adicionais para a biblioteca Haskell de redes P/T. Recomenda-se aos grupos que ainda não escolheram projecto que o façam com a maior brevidade possível.

Exemplos de especificação com lógica LTL. Padrões de ocorrência em lógica temporal. Axiomas da LTL.

Introdução à lógica temporal. Estruturas de Kripke. Tempo linear vs tempo ramificado. Linear Temporal Logic.

Exercícios sobre redes coloridas: modelação e conversão para redes P/T.

Jornadas de Informática.

Na próxima Quarta, dia 5 de Abril, a aula teórica será nas Join.

Neste momento já todos os projectos foram escolhidos. Se mais alguém quiser realizar um projecto entre em contacto comigo para lhe propor um enunciado. Já agora, a entrega dos projectos deverá ser feita até ao dia 9 de Junho.

Conversão de redes coloridas para redes P/T. Modelação do alternating bit protocol usando redes coloridas.

Exercícios sobre redes P/T: verificação estrutural de propriedades. Cálculo de invariantes de lugar e armadilhas.