1. Skip to Menu
  2. Skip to Content
  3. Skip to Footer

DEFESA DE DISSERTAÇÃO DE MESTRADO DO ALUNO MAURÍCIO DA SILVA PIRES

19/03/2020, quinta-feira, 14 horas, sala de videoconferência (310), prédio de salas de aulas do Instituto do Computação

Revisitando o Teorema de Courcelle

Resumo:

Grafos são estruturas matemáticas que possuem um alto potencial para modelar problemas do mundo real. Assim, estudos computacionais de problemas em grafos são um excelente ponto de partida na busca de soluções práticas a esses problemas. A Teoria da Complexidade Parametrizada apresenta um conjunto de ferramentas de projeto e análise de algoritmos que permite um estudo mais elaborado de problemas em grafos, visto que considera características das entradas ou dos problemas nas tarefas de projeto e análise. Um exemplo de parâmetro é a chamada treewidth, que é uma invariante do grafo que mensura sua semelhança com uma árvore.

O Teorema de Courcelle é um dos mais relevantes resultados parametrizados sobre estudos em grafos. O Teorema estabelece que problemas em grafos expressíveis em fórmulas de Lógica Monádica de Segunda Ordem de tipo 2 podem ser verificados em tempo FPT em instâncias com treewidth limitada por um valor k pré-estabelecido. Este resultado possui duas importantes facetas. A primeira refere-se à tarefa de classificação de problemas parametrizados na classe dos problemas tratáveis de acordo com a teoria. A segunda, muito pouco explorada na literatura, refere-se à implementação das etapas sugeridas em sua demonstração. Isso significa que a prova do Teorema de Courcelle envolve processos passíveis de mecanização, e, portanto, podem ser utilizados como um algoritmo para resolver problemas em grafos.

Neste trabalho é apresentada uma descrição algorítmica completa e explícita para as etapas envolvidas na prova da versão clássica do Teorema de Courcelle. O resultado obtido é um algoritmo baseado em autômatos que permite verificar propriedades em grafos por meio da técnica conhecida como model checking.

Abstract:

Graphs are mathematical structures with a high potential to model real-world problems. Thus, computational studies of graph problems are an excellent starting point in the search for practical solutions to these problems. The Parameterized Complexity Theory presents a set of algorithm design and analysis tools that allows a more elaborate study of problems in graphs since it considers characteristics off the inputs or problems in the design and analysis tasks. A parameter example is so-called treewidth, which is an invariant of the graph that measures its resemblance to a tree.

Courcelle's Theorem is one of the most relevant parameterized results in graph studies. This Theorem proves that graph problems expressed in formulas of type 2 Monadic Second-Order Logic are verifiable in FPT time in instances with treewidth limited by a pre-established k value. This result is twofold. The first refers to the task of classifying problems parameterized in the class of treatable problems according to the theory. The second, very little explored in the literature, refers to the implementation of the steps suggested in its demonstration. It means that the proof of Courcelle's Theorem involves processes that are mechanizable, and therefore used as an algorithm to solve graph problems.

This work presents a complete and explicit algorithmic description for all of the steps involved in the proof of the classic version of Courcelle's Theorem. The result obtained is an algorithm based on Tree-Automata that allows verifying properties in graphs through the technique known as model checking.

Banca examinadora:

Prof. Bruno Lopes Vieira, UFF - Presidente
Prof. Uéverton dos Santos Souza, UFF
Prof. Fábio Protti, UFF
Prof. Mario Roberto Folhadela Benevides, UFF
Prof. Edward Hermann Haeusler, PUC-Rio
Prof. Mateus de Oliveira Oliveira, Universitetet i Bergen

PESQUISA PELO SITE

MENU

Início Instituto Laboratórios Departamento
Pesquisa Pós-Graduação Graduação Fale Conosco

CONTATO

IC-Mapa

Av. Gal. Milton Tavares de Souza, s/nº
São Domingos - Niterói - RJ
CEP: 24210-346

IC-UFF-Telefone-icone Fale Conosco

 Como Chegar

CONECTE-SE

IC-Conecte-se-Facebook IC-Conecte-se-Twitter

LINKS

Faperj Lattes Finep SBC PROGRAD
CAPES CNPQ SIAPENET IDUFF NDC

 

Desenvolvido por pela equipe de Suporte Técnico do Instituto de Computação - suporte.ic.uff.br - Web Designer: Emanuel Machado