Departamento de Informática (UM)

Página de Unidade Curricular

DesignaçãoCódigoCursoRegimeRegente

Lógica Computacional

10862 [8505O5]

Licenciatura em Ciências da Computação [CCOM]

S5

Maria João Gomes Frade

Objetivos

A UC é estrutural porque fornece a experiência, em ferramentas conceptuais e computacionais, necessárias à especificação e verificação automática de grandes sistemas definidos por regras lógicas complexas.
Pretende-se atingir familiaridade com um conjunto de problemas lógicos "standard" aos quais muitos sistemas concretos podem ser reduzidos e fornecer proficiência com as ferramentas computacionais usadas na construção das suas soluções.

Programa

1. Optimização. Problemas de "programação inteira" (IP), "programação inteira híbrida" (MIP) e "programação com restrições" (CP). Algoritmos de otimização em MIP e CP. Problemas Knapsack, Set Cover, Point Cover. Alguns problemas de Grafos.
2. Satisfação Proposicional (SAT). Algoritmo de Davis Putman e suas oprimizações. Problemas MAXSAT.
3. "Satisfatiability Model Theories" (SMT). Algoritmos base de verificação SMT. As principais teorias SMT. Verificação da correcção de programas imperativos. Sistemas de Transição de 1ª Ordem (FOTS) e sua codificação em SMT's. Sistemas ciber-físicos (autómatos híbridos) e a sua codificação em SMT's.
4. Verificação de Modelos Finitos ("Model Checking"). Lógicas temporais LTL e CTL. Estruturas de Kripke. BDD's ("binary decision diagrams") e os seus algoritmos. "Model Checking" usando BDD's.
5. "Bounded Model Checking" (BMC). Verificação de modelos infinitos. Descrição do comportamento limitado de sistemas infinitos. Codificação da LTL e verificação de fórmulas LTL num comportamento infinito usando SMT's.

Bibliografia

Integer Programming, Conforti, Michele, Cornuejols, Gerard, Zambelli, Giacomo, Springer-Verlag.

Biere, A. (ed). Handbook of Satisfiability. IOS Press.

Manuais dos sistemas SCIP, Gurobi, MiniSat, Z3, SMTLIB, NuSMV, XuSMV.

Resultados da aprendizagem

- Desenvolver conhecimento na modelação lógica de sistemas dinâmicos e das suas propriedades.
- Desenvolver conhecimento na modelação de propriedades de sistemas estáticos e construção de soluções ótimas para a verificação dessas propriedades.
- Desenvolver conhecimento sobre o processo interno de construção de soluções para os problemas de verificação quer de sistemas estáticos como de sistemas dinâmicos.
- Demonstrar capacidade de usar as ferramentas computacionais mais apropriadas à representação dos sistemas dinâmicos e verificação automática das suas propriedades comportamentais.
- Demonstrar capacidade de adequar as ferramentas computacionais a cada sistema concreto e combinar várias ferramentas quando uma só não basta para resolver o problema.
- Demonstrar capacidade para a construção de algoritmos e flexibilidade para os programar nas linguagens que forem necessárias.
Pré-requisitos recomendados

Noções elementares de Matemática Discreta e Lógica.

Método de avaliação

Avaliação contínua formada por um teste teórico e um conjunto de trabalhos individuais.
O teste teórico dirige-se a avaliar os dois primeiros RA's enquanto os trabalhos avaliam os dois últimos RA's.
O peso destas duas componentes na nota final varia com o número de trabalhos mas está sempre contido no intervalo [0.4,0.6].

Funcionamento

Turno: T 1; Docente: José Manuel Esgalhado Valença; Dep.: DI; Horas: 30.
Turno: TP 1; Docente: Manuel Alcino Pereira Cunha; Dep.: DI; Horas: 30.
Turno: TP 2; Docente: Maria João Gomes Frade; Dep.: DI; Horas: 30.

[ Outras UCs do Departamento ]