MAC499 - Trabalho de Formatura Supervisionado

Aluno: Bruno Vercelino da Hora
Orientador: Marcelo Finger

   Nosso trabalho pretende aplicar técnicas de Revisão de Crenças [1], que consiste em analisar um modelo abstrato de um sistema atrás de inconsistências, sugerindo alterações afim de torná-lo consistente. Iremos utilizar como linguagem de entrada o SMV [5], que é uma forma de modelar abstratamente um sitema. Esta linguagem tem como base a CTL [3], uma lógica temporal com ramificações, para representar as propriedados do sistema.

   A idéia do algoritmo é originário de [4], onde foi provado que é possível executar o processo de Revisão de Crenças para a lógica CTL e mostrado um algoritmo para tal. O algoritmo consiste em utilziar uma técnica de verificação de modelos chamada Bounded Model Checking [2], onde ocorre uma tradução do modelo para lógica clássica, executando a revisão em lógica clássica.

   As traduções serão baseadas em [6], onde foi mostrado a tradução de um modelo em ACTL (fragmento universal da CTL). Utilizaremos tal algoritmo de tradução para a ida, e se baseando no mesmo para gerar a tradução de volta, gerando as sugestões no modelo original.

   Algoritmos de Revisão de Crenças para CTL já foram desenvolvidos utilizando diferentes estratégias, porém com algumas restrições indesejáveis. Pretendemos utilizar a abordagem de Revisão de Crenças com BMC, a fim de averiguar uma alternativa e avaliar sua eficácia. A técnica de BMC foi originalmente desenvolvido para LTL, lógica temporal linear, sendo posteriormente aplicado para CTL com as traduções citadas.

   Nosso objetivo é implementar tal algoritmo de Revisão de Crenças e avaliá-lo. Assim teremos uma nova abordagem para o problema e uma possível melhora. Outro objetivo é encontrar uma tradução capaz de trazer de volta o modelo da lógica clássica para CTL, gerando as sugestões no modelo original.

   Até o exato momento, foram estudados as diversas áreas abordadas pelo projeto. Toda a teoria de revisão de crenças como as bases para BMC e CTL foram estudados afim de obter o conhecimento necessário sobre o tema. Também foram executadas pesquisas atrás de uma tradução de CTL para lógica clássica, e a análise de tais traduções.

   A monografia será dividida em duas partes:

Parte técnica
1. Introdução: Descrição do problema, motivação e proposta
2. Revisão de Crenças: Descrição teórica do processo de Revisão de Crenças
3. Lógica Temporal: Decrição teórica da Lógica Temporal, especificamente da CTL
4. Verificação de Modelos: Descrição teórica das técnicas de Model Checking, especificamente de BMC
5. Algoritmo: Metodologia utilizada para criação do algoritmo e explicação do mesmo
6. Conclusões: Conclusões obtidas de acordo com os resultados obtidos da execução do program gerado
7. Apêndices: Sintaxe do SMV, código fonte do programa criado e resultado dos testes
8. Bibliografia

Parte subjetiva
1. Desafios vencidos: Desafios encontrados durante o desenvolvimento e o aprendizado adquirido através do desenvolvimento do projeto e da superação desses desafios
2. Desafios por vencer: Obstáculos encontrados e que ainda não foram ultrapassados neste projeto
3. Disciplinas relacionadas: Listagem e explicação das matérias cursadas relevantes para o desenvolvimento do projeto, relacionando-as com os conceitos aprendidos e aplicados no projeto.
4. Próximas etapas: Próximas etapas para dar prosseguimento ao projeto e para aprimorar os conhecientos na área.

[1] C. E. Alchourròn, P. Gärdenfors, and D. Makinson. On the logic of theory change: Partial meet contraction and revision functions. Journal of Symbolic Logic, 50:510-530, 1985.

[2] Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. Symbolic model checking without bdds. Lecture Notes in Computer Science, 1579:193-207, 1999.

[3] Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, Workshop, pages 52-71, London, UK, 1982. Springer-Verlag.

[4] Marcelo Finger and Renata Wassermann. Revising specifications with ctl properties using bounded model checking. In SBIA '08: Proceedings of the 19th Brazilian Symposium on Artificial Intelligence, pages 157-166, Berlin, Heidelberg, 2008. Springer-Verlag.

[5] K. L. Mcmillan. The smv system, 1992.

[6] W. Penczek, B. Wo'zna, and A. Zbrzezny. Bounded model checking for the universal fragment of ctl, 2002.