Disciplina Curricular
Lógica e Verificação de Modelos LVM
Mestrado Bolonha em Matemática Aplicada e Computação - MMAC 2021
Contextos
Grupo: MMAC 2021 > 2º Ciclo > Área Principal > Áreas de Especialização > Área de Especialização em Lógica e Computação > Área Científica de Lógica e Computação > Obrigatórias
Período:
Grupo: MMAC 2021 > 2º Ciclo > Área Principal > Áreas de Especialização > Área de Especialização em Lógica e Computação > Área Científica de Lógica e Computação > Obrigatórias
Período:
Peso
9.0 (para cálculo da média)
Objectivos
Os alunos devem conhecer lógica proposicional, conhecer os príncipais algorimtos SAT, conhecer lógica temporal, conhecer sisemas de transição para especificação de sistemas reactivos, conhecer os príncipais algoritmos usados em verificação de modelos. No fim do curso, espera-se que os alunos comperendam a teoria usada em SAT, sejam capazes modelar problemas simples em SAT, sejam capazes de usar a ferramenta Z3, para resolver esses problemas, compreender a teoria usada para verficação de modelos, sejam capazes de modelar sistemas reactivos simples, sejam capazes de especificar propriedades dos sistemas usando lógica temporal, sejam capazes de usar o verificador de modelos Spin para verificar sistemas reactivos simples.
Programa
Lógica proposicional. Problema SAT. Resolução proposicional. Algoritmos DPLL e CDCL. Sistemas concorrentes. Lógica temporal linear (LTL). Autómatos de Büchi para linguagens-ómega regulares. Verificação de modelos para LTL baseada em autómatos. Lógica temporal ramificada (CTL). Verificação de modelos para CTL. Caracterização dos operadores CTL por ponto fixo. Comparação entre LTL e CTL. Justiça forte e fraca. Diagramas de decisão binária. Verificação de modelos simbólica. Verificação de modelos limitada. Redução da verificação de modelos limitada a SAT.
Metodologia de avaliação
Exame (50%) e projetos computacionais com apresentação oral (50%).
Componente de Competências Transversais
A UC permite o desenvolvimento de competências transversais em Pensamento Crítico, Criatividade e Estratégias de Resoluções de Problemas, nas aulas, em trabalho autónomo e nas várias componentes de avaliação. A percentagem de avaliação associada a estas competências deverá ser da ordem dos 15%.
Componente Laboratorial
Utilização de SAT solvers e de verificadores de modelos.
Componente de Programação e Computação
Projetos computacionais.
Princípios Éticos
Todos os membros de um grupo são responsáveis pelo trabalho do grupo. Em qualquer avaliação, todo aluno deve divulgar honestamente qualquer ajuda recebida e fontes usadas. Numa avaliação oral, todo aluno deverá ser capaz de apresentar e responder a perguntas sobre toda a avaliação.