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.
Lógica temporal distribuída, CVC4, propriedade da separação, interpolação de Craig

Janeiro 29, 2021, 9:30

Documentos da dissertação ainda não disponíveis publicamente

Orientação

ORIENTADOR

João Filipe Quintas dos Santos Rasga

Departamento de Matemática (DM)

Professor Associado

ORIENTADOR

Jaime Arsénio de Brito Ramos

Departamento de Matemática (DM)

Professor Auxiliar