Programa

Lógica e Verificação de Modelos

Mestrado Bolonha em Matemática e Aplicações e Computação

Mestrado Bolonha em Engenharia Informática e de Computadores - Alameda

Programa

Lógica proposicional. Diagramas de decisão binária. Lógica CTL. Verificação de modelos. Fairness. Caracterização dos operadores CTL como pontos fixos. Outras lógicas temporais. Verificação de sistemas concorrentes e distribuídos. Simulação e bi-simulação de modelos. Lógica de Hoare. Lógica modal e agentes. Lógica dinâmica. Lógica de 1a ordem, teorias decidíveis e aplicações.