Uma Solução para o Refinamento de Modelos KMTS Baseado em Verificação de Modelos com Jogos

Abstract

A revisão de modelos é uma técnica baseada na teoria de revisão de crenças, que tem como princípio modificar minimamente os modelos de forma a satisfazer uma dada propriedade. A revisão de modelos pode ser combinada com verificação de modelos para determinar as mudanças estruturais minimais sobre modelos de Kripke com base no resultado da verificação. As estruturas modais de Kripke (KMTS) são extensões das estruturas de Kripke com modalidades que permitem expressar informações incompletas explicitamente. Um KMTS pode ser interpretado como um conjunto de estruturas de Kripke, e a técnica de verificação de modelos pode ser utilizada para verificar se um KMTS atende à uma determinada especificação, devendo retornar os seguintes valores: verdadeiro quando todas as estruturas de Kripke representadas pelo KMTS satisfazem a especificação, falso quando nenhuma das estruturas de Kripke satisfaz a especificação, ou indefinido quando algumas das estruturas satisfazem e outras não. Uma das contribuições deste trabalho é a proposta de um verificador de modelos para KMTS considerando esta semântica utilizando CTL como linguagem de especificação de propriedades. A revisão de um KMTS ocorre quando a verificação de modelos resulta em falso ou indefinido. No caso de indefinido, o KMTS deve ser modificado para representar apenas os modelos de Kripke que satisfazem a propriedade requerida. Esta etapa da revisão é chamada de refinamento. Neste caso, de acordo com a revisão de modelos, devem-se aplicar mudanças estruturais minimais sobre o KMTS para obter os modelos resultantes do refinamento. Outra contribuição deste trabalho está em apresentar uma solução para este problema, através de algoritmos propostos com base em um grafo de testemunhas, definido nesta dissertação, que abstrai informações do grafo de um verificador de modelos baseado em jogos de forma a obter apenas os modelos gerados por mudanças minimais sobre o KMTS.