Estendendo a revisão de modelos CTL para modelos parciais de Kripke

• Processo: 12/16308-1
• Modalidade de apoio: Auxílio à Pesquisa - Pesquisador Visitante - Brasil
• Data de Início da vigência: 20 de agosto de 2012
• Data de Término da vigência: 19 de agosto de 2013
• Área do conhecimento: Ciências Exatas e da Terra - Ciência da Computação - Metodologia e Técnicas da Computação
• Pesquisador responsável: Renata Wassermann
• Beneficiário: Renata Wassermann
• Pesquisador visitante: Aline Maria Santos Andrade
• Instituição do Pesquisador Visitante: Universidade Federal da Bahia (UFBA). Instituto de Matemática, Brasil
• Instituição Sede: Instituto de Matemática e Estatística (IME). Universidade de São Paulo (USP). São Paulo , SP, Brasil
• Palavra(s)-Chave do Pesquisador: Modelos do Mu-calculus | Revisão e atualização de crenças | Revisão e atualização de modelos | Revisão e atualização de modelos parciais | Sistemas de transições modais de Kripke | Verificação de Modelos | Métodos Formais

Resumo

As estruturas modais de Kripke são modelos adequados para representar sistemas com informações parcias, como especificações de software com requisitos ainda não elicitados e abstração de modelos CTL. As estruturas modais de Kripke são modelos para o Mu-calculus modal e podem ser submetidas à verificação de modelos. Na verificação de modelos quando uma propriedade desejada não é verificada, o modelo deve ser alterado para satisfazer a propriedade. A alteração automática de modelos é um desafio de pesquisa atualmente e existem algumas propostas para alteração de modelos CTL baseadas em revisão e atualização de crenças. Este projeto se propõe a investigar o problema de revisão e atualização sobe estruturas modais de Kripke a partir dos resultados existentes sobre revisão e atualização de modelos CTL. (AU)