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.
dezembro 20, 2019, 14:0
Publicação
Obra sujeita a Direitos de Autor
Orientação
