Impementacao de Revisão de Modelos CTL
Prof.ª Renata Wassermann
Paulo de Tarso Guerra Oliveira
Lógica Temporal é um tipo de lógica modal que nos permite fazer proposições relacionadas a tempo, assim como operar sobre elas. Em lógica temporal é possível, por exemplo, expressar sentenças como "Eu estou sempre com fome" ou "Eu estarei com fome até comer algo". Em computação, ela é muito utilizada para declarar requerimentos de hardwares e softwares, assim como na construção de modelos dos mesmos.
Uma importante Lógica temporal é a Lógica de Árvore Computacional (ou Computation Tree Logic - CTL). CTL é uma lógica que modela o tempo em uma estrutura de árvore, ou seja, os nós de um ramo denotam os possíveis futuros que o estado representado poderá ter. Em suas aplicações computacionais, a CTL pode quantificar sobre os diversos caminhos que uma execução pode tomar, ou seja, ela pode determinar se existe a possibilidade de um estado ocorrer (como por exemplo, se dois processos utilizarão o mesmo recurso ao mesmo tempo) e assim, podemos tomar decisões que evitem ou não tais estados.
Algumas vezes, nossas quantificaçãos sobre os caminhos de execução se mostram incorretas. Por isso, dentro da área de inteligência artificial, a teoria de revisão de crenças é relacionada ao modo que um agente inteligente age frente à necessidade de incorporar novas informações. Isso significa que ela descreve modos de tratar informação conflitante e de como manter a base de crenças consistente. No contexto de lógicas temporais, revisão de crenças pode ser utilizada para reparar modelos temporais, assim como mantê-los consistentes frente a novas acerções.
Atualmente, sabe-se da importância de revisão e atualização de crenças tanto na área de inteligência artificial quanto em outras áreas da computação. Vários estudos foram feitos nessa área e alguns algoritmos foram propostos para alguns dos principais problemas (expansão, contração e revisão de bases de crenças), porém existem poucas implementações destes algoritmos.
A proposta deste trabalho é implementar um algoritmo de revisão de crenças CTL como apresentado por Paulo de Tarso Guerra em sua tese de mestrado Revisão de Modelos CTL (II) tendo como base o framework de revisão de crenças desenvolvido por Renato Urquiza Lundeberg sob supervisão da prof.ª Renata (III) (Tese disponível aqui). O algoritmo será implementado em Java e tem como principais vantagens ser determinístico e apenas iterar sobre elementos finitos.
| Atividade\Mês
| Mar
| Abr
| Mai
| Jun
| Jul
| Ago
| Set
| Out
| Nov
| Dez
|
| Estudo Preliminar |
|
|
|
|
|
|
|
|
|
|
| Estudo sobre o algoritmo |
|
|
|
|
|
|
|
|
|
|
| Implementação |
|
|
|
|
|
|
|
|
|
|
| Monografia |
|
|
|
|
|
|
|
|
|
|
| Apresentação |
|
|
|
|
|
|
|
|
|
|
| Entrega Final |
|
|
|
|
|
|
|
|
|
|
| Legenda |
| |
Tarefa concluída no prazo |
| |
Prazo da tarefa |
| |
Atraso |
| Estudo Preliminar |
Estudo básico de lógicas, CTL e revisão de crenças |
| Estudo sobre o algoritmo |
Estudo aprofundado sobre o algoritmo proposto e tópicos diretamente relacionados |
| Implementação |
Implentação do algoritmo (parte foco do TCC) |
| Monografia |
Desenvolvimento do texto de monografia |
| Apresentação |
Desenvolvimento da apresentação oral |
| Entrega Final |
Ajustes para a entrega final |
