Título: Verificação de modelos com jogos

 Palestrante: Aline Andrade (UFBA)

 Resumo:

Estruturas de Kripke podem ser compactadas em Estruturas Modais de Kripke
(KMTS), que tem expressividade para  representar informação parcial explícita,
sendo modelo para o Mu-calculus modal. A revisão de modelos de Kripke através
de KMTS pode ser feita com algoritmos de verificação de modelos para
Mu-calculus. 

Esta palestra apresentará a verificação de modelos para Mu-calculus  baseada
em jogos para lógica de 2 e 3 valores (a verificação de propriedades sobre
KMTS raciocina com lógica de 3 valores) e dará uma idéia da revisão de modelos
KMTS utilizando o jogo de 3 valores.