Título: Mu-calculus, CTL e outros fragmentos
Palestrante: Paulo de Tarso Guerra Oliveira

Resumo:

Mu-calculus é uma lógica modal cuja principal característica é possibilitar
definições indutivas através de operadores de ponto fixo. CTL, LTL e diversas
outras lógicas
temporais podem ser vistas como fragmentos do mu-calculus, no sentido que
podem ser traduzidas para sentenças nesta lógica. Assim, diversas propriedades
referentes ao 
mu-calculus também são válidas para CTL e outros de seus fragmentos. Neste
seminário faremos uma breve introdução sobre a lógica mu-calculus. 
Apresentaremos sua sintaxe, semântica e algumas propriedades lógicas. Também
descreveremos LTL, CTL e outras lógicas temporais como fragmentos do
mu-calculus. 
Por fim, mostraremos relações entre mu-calculus, teoria dos autômatos e teoria
dos jogos.