FenixEdu™

Dissertação

Model checking DTL - Automata theoretic and bounded approaches EVALUATED

Detalhes: 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.
Keywords: verificação de modelos, lógica temporal distribuida, verificação com base em autómatos, verificação de modelos bounded, SAT based model checking

Discussão: outubro 23, 2020, 14:30