Dissertação
DTL: Translation, SMT Verification, Separation and Interpolation EVALUATED
O objetivo desta dissertação é contribuir para uma melhor compreensão da Lógica Temporal Distribuída (DTL), nomeadamente ao investigar se possui algumas propriedades lógicas importantes. Começamos por apresentar uma tradução de fórmulas em DTL para fórmulas em lógica de primeira ordem (FOL) que preserva a consequência semântica, e de seguida recorremos a CVC4, um provador de teoremas e solucionador de satisfiability modulo theories (SMT), de forma a verificar a validade de fórmulas em DTL, capitalizando na tradução de DTL para FOL mencionada anteriormente. Também propomos uma extensão da propriedade da separação a DTL, e provamos que a lógica temporal distribuída cujas linguagens locais contêm os operadores Until e Since tem a nossa versão da propriedade da separação. Adaptamos ainda a propriedade da interpolação de Craig a DTL, e provamos que um fragmento desta lógica tem a propriedade referida.
janeiro 29, 2021, 9:30
Publicação
Obra sujeita a Direitos de Autor
Orientação
