Dissertação

Deciding Distributed Temporal Logic EVALUATED

O propósito desta dissertação é implementar um sistema de tableaux para Lógica Temporal Distribuída (DTL) e um algoritmo para a verificação de invariantes globais em sistemas especificados usando esta versão da DTL. O sistema de tableaux e o algoritmo implementados já tinham sido propostos em [2], mas não havia uma implementação dos mesmos. A falta de um programa que implementasse este algoritmo e automaticamente verificasse os invariantes globais destes sistemas foi a motivação principal deste trabalho. Como tal, incluímos todas as definições necessárias para entender esta versão da DTL e o sistema de tableaux utilizado. Iremos também apresentar todos os resultados e teoremas necessários para compreender o algoritmo implementado e como este funciona. O algoritmo implementado e aqui descrito é utilizado para a verificação de invariantes globais: com um conjunto Gama de fórmulas DTL e uma fórmula global $\delta$, verificamos se a fórmula é consequência semântica de Gama e se não for, apresentamos um contraexemplo: uma estrutura de interpretação que satisfaz Gama, mas não delta. Com isto em mente, apresentamos alguns tópicos desta dissertação: - a descrição da DTL e de um sistema de tableaux para esta lógica, assim como vários resultados importantes sobre este sistema; - a descrição do procedimento para verificação de invariantes globais; - a descrição da implementação do sistema de tableaux e do algoritmo para a verificação de invariantes globais.
Lógica Temporal Distribuída, sistema de tableaux, invariantes.

Dezembro 16, 2015, 10:30

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

Maria Paula Antunes Abrantes Gouveia

Departamento de Matemática (DM)

Professor Auxiliar