Certificates for Decision Problems in Temporal Logic using Context-Based Tableaux and Sequent Calculi

• DIRECTORES: Jorge Parra, Unai Díaz de Cerio y Montserrat Hermo
• UNIVERSIDAD: UPV/EHU

RESUMEN

En esta tesis se plantea la generación de certificados (evidencias que aseguren algo) en dos ámbitos: Satisfactibilidad Certificada y Model Checking Certificado. La satisfactibilidad certificada consiste en analizar si un conjunto de fórmulas puede ser cierto: en el caso en el que pueda serlo se provee un modelo (que hace cierto el conjunto) y en el caso contrario un certificado (demostrando que no existe ningún modelo que haga cierto el conjunto). Model Checking Certificado es un problema más concreto: teniendo un sistema representado con fórmula, se quiere comprobar que ese sistema cumple una propiedad. En el caso en el que la propiedad NO se cumpla, se provee una traza del sistema que no satisface la propiedad. En el caso contrario se provee un certificado que asegura que el sistema, en su totalidad, cumple la propiedad en cuestión. Esta tesis propone tres métodos (en tres lógicas) que marcan las bases para poderse asegurar que los sistemas se comportan según lo esperado (o, mejor dicho, según lo especificado).