Portal InstitucionalUFPEL

26/05/2018 - 31/07/2022

Ciências Exatas e da Terra - Ciência da Computação

Gramática de grafos pode ser utilizada como técnica de especificação para diferentes tipos de sistemas, especialmente em situações em que os estados são estruturas complexas que podem ser modeladas como grafos (possivelmente com uma parte de dados) e em que o comportamento envolve um grande quantidade de paralelismo e pode ser descrito por reações a estímulos que podem ser observados no estado do sistema. A verificação de propriedades de tais sistemas é uma tarefa difícil devido a diversos aspectos: em muitas situações os sistemas possuem um número infinito de estados; os estados são complexos e grandes; existe um número considerável de diferentes possibilidades de computações porque as aplicações de regras podem ocorrer em paralelo. Já existem diferentes abordagens para a verificação de gramática de grafos baseada em model-checking, mas nestes casos somente sistemas com espaço de estados finito podem ser analisados. Outras abordagens propõem super- e/ou sub- aproximar o espaço de estados, mas neste caso não é possível verificar propriedades arbitrárias do sistema. Neste projeto, propõe-se obter uma fundamentação teórica e a proposta de um método para a prova de teoremas de gramática de grafos. Este objetivo será alcançado pela tradução formal da linguagem gramática de grafos para a linguagem de entrada de um provador de teoremas, explorando também o uso do refinamento, o desenvolvimento de teorias de grafos e a definição de táticas de prova.