Dissertação

Model checking DTL - Automata theoretic and bounded approaches EVALUATED

Lógica temporal distribuída (LDT) é uma lógica que permite raciocinar sobre sistemas distribuídos do ponto de vista dos agentes locais e a sua semântica permite expressar com facilidade eventos de sincronização entre ditos agentes. Apesar disto poucos algoritmos para verificar LDT existem e, os que existem, foram introduzidos recentemente. Nesta tese fornecemos dois algoritmos para verificar LDT, o primeiro corresponde a uma abordagem fazendo uso de autómatos. O segundo algoritmo trata-se de um procedimento de bounded model checking, baseado nas construções pré-existentes para LTL (lógica temporal linear), que faz uso do problema de satisfação de fómulas boleanas para resolver o problema de verificação original.
verificação de modelos, lógica temporal distribuida, verificação com base em autómatos, verificação de modelos bounded, SAT based model checking

Outubro 23, 2020, 14:30

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

Francisco Miguel Alves Campos de Sousa Dionísio

Departamento de Matemática (DM)

Professor Auxiliar

ORIENTADOR

Jaime Arsénio de Brito Ramos

Departamento de Matemática (DM)

Professor Auxiliar