Nome do Projeto
Prova de Teoremas para Gramática de Grafos
Ênfase
PESQUISA
Data inicial - Data final
26/05/2018 - 31/07/2022
Unidade de Origem
Coordenador Atual
Área CNPq
Ciências Exatas e da Terra - Ciência da Computação
Resumo
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.

Objetivo Geral

O projeto tem por objetivo geral explorar o uso da técnica de prova de teoremas para o formalismo gramática de grafos. Como objetivos específicos propõe-se definir formalmente a tradução de gramática de grafos para a linguagem de entrada de um provador de teoremas, codificar extensões deste formalismo considerando atributos e condições negativas de aplicação, investigar como a especificação de teorias, o uso do refinamento e a definição de táticas de prova podem ser utilizados para o estabelecimento de uma estratégia que possa ser aplicada para analisar sistemas (possivelmente com estados infinitos) especificados com gramática de grafos.

Equipe do Projeto

NomeCH SemanalData inicialData final
BRAZ ARAUJO DA SILVA JUNIOR1201/08/201731/03/2018
BRAZ ARAUJO DA SILVA JUNIOR1201/08/201531/07/2016
JOÃO VÍTOR CHAGAS POSSOBOM VAZ1201/08/201831/07/2019
JOÃO VÍTOR CHAGAS POSSOBOM VAZ1201/04/201831/07/2018
LUCIANA FOSS1026/05/201831/07/2022
NATÁLIA TORALLES DARLEY1201/08/201431/07/2015
NÍCOLAS OREQUES DE ARAUJO1201/08/201631/07/2017

Página gerada em 30/11/2021 19:01:17 (consulta levou 0.176799s)