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.

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.

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

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.

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.

Redes de arcos constantes e coloridas. Demonstração com o PEP.

Verificação estrutural: cálculo de invariantes de lugar e armadilhas.

Exercícios sobre redes P/T: cálculo de grafos de acessibilidade e de cobertura, eliminação de contactos e arcos inibidores e verificação por enumeração de propriedades de segurança e animação.

Verificação de propriedades de animação por enumeração. Verificação estrutural: matrizes de incidência e invariantes de lugar.

Grafo de cobertura. Propriedades básicas de redes de Petri: finitude, animação, invertibilidade e exclusão mútua. Verificação por enumeração de propriedades de segurança.

Exercícios sobre modelação com redes P/T.

Redes P/T: formalização, condição de activação e disparo e grafo de acessibilidade. Redes com capacidades explícitas e eliminação de contactos. Arcos inibidores.

Aplicações de redes elementares: exclusão mútua (incluindo algoritmo de Peterson) e protocolos (conversa cruzada).

Exercícios sobre redes elementares: cálculo de grafos de acessibilidade, detecção e eliminação de contactos, semântica não-entrelaçada e detecção de conflitos.

Noção de conflito, contacto e confusão. Cálculo do grafo de acessibilidade usando semântica entrelaçada e não-entrelaçada. Eliminação de contactos.

Formalização do conceito de rede. Definição de rede simples e pura. Introdução às redes elementares: activação, disparo, e concorrência.

Introdução à ferramenta DaNAMiCS. Exercícios sobre modelação com redes elementares.

Introdução às redes de Petri.

Operações sobre sistema de transição: restrição, renomeação, produto, composição paralela. Modelos da concorrência entrelaçados e não entrelaçados.

Exercícios sobre sistemas de transição.

Introdução aos sistemas de transição.

Apresentação da disciplina.

Não houve aula.