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

• DIRECTORS: Jorge Parra, Unai Díaz de Cerio and Montserrat Hermo
• UNIVERSITY: UPV/EHU

ABSTRACT

This thesis proposes the generation of certificates (evidences that ensure something) in two areas: Certified Satisfaction and Certified Model Checking. Certified satisfiability consists of analyzing whether a set of formulas can be true: in the case in which it can be true, a model is provided (which makes the set true) and in the opposite case, a certificate (demonstrating that there is no model that makes the set true).  Certified Model Checking is a more specific problem: having a system represented with a formula, you want to check that this system fulfills a property. In the case where the property is NOT satisfied, a trace of the system that does not satisfy the property is provided. Otherwise, a certificate is provided that ensures that the system, in its entirety, complies with the property in question. This thesis proposes three methods (in three logics) that mark the bases to be able to ensure that the systems behave as expected (or, rather, as specified).