Certificates for Decision Problems in Temporal Logic using Context-Based Tableaux and Sequent Calculi
Alex Abuin Yepes
03/03/2023
- ZUZENDARIAK: Jorge Parra, Unai Díaz de Cerio eta Montserrat Hermo
- UNIBERTSITATEA: UPV/EHU
LABURPENA
Tesi honetan, ziurtagiriak sortzea planteatzen da (zerbait ziurtatzen duten ebidentziak), bi eremutan: Asebetetze Ziurtatua eta Model Checking Ziurtagiria. Asebetegarritasun ziurtatua, formula multzo bat egia izan daitekeen aztertzean datza: hala izan daitekeen kasuan, eredu bat ematen da (multzoa egia bihurtzen duena) eta, bestela, ziurtagiri bat (multzoa egia bihurtzen duen eredurik ez dagoela frogatuz). Model Checking Ziurtatua arazo zehatzagoa da: formularekin irudikatutako sistema bat izanda, sistema horrek propietate bat betetzen duela egiaztatu nahi da. Jabetza EZ bada betetzen, jabetza asetzen ez duen sistemaren traza ematen da. Bestela, sistemak bere osotasunean jabetza betetzen duela ziurtatzen duen ziurtagiri bat ematen da. Tesi honek hiru metodo proposatzen ditu (hiru logikatan), sistemek espero denaren arabera (edo, hobeto esanda, zehaztutakoaren arabera) jokatzen dutela ziurtatzeko oinarriak ezartzen dituztenak.