options
search icon
email icon
EU
rrss gif icons
twitter icon
linkedin icon youtube icon
shape

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.

close overlay