Dissertação

Model Checking with Distributed Temporal Logic EVALUATED

LTD (Lógica Temporal Distribuida) é uma lógica que nos permite estudar sistemas distribuidos quer de um ponto de vista global quer local no que toca a propriedades proposicionais, temporais e de sincronização. Nesta tese desenvolvemos um algoritmo de verificação de modelos baseado em autómatos de Büchi não-determinísiticos distribuidos, que retorna \textit{true} quando uma fórmula LTD é satisfeita por um sistema de transição distribuido, ou caso contrário retorna um caminho que falsifica essa mesma fórmula. Provámos ainda a sua correção e testámo-lo em alguns exemplos, onde mais uma vez verficámos que está correto.
Verficação de Modelos, autómato de Büchi, Sistemas Distribuidos, Lógica Temporal Distribuida

Dezembro 20, 2019, 14:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

Jaime Arsénio de Brito Ramos

Departamento de Matemática (DM)

Professor Auxiliar