Sorrentino, Loredana (2015) On Games in Formal Verification. [Tesi di dottorato]

[img]
Preview
Text
Sorrentino_Loredana.pdf

Download (862kB) | Preview
[error in script] [error in script]
Item Type: Tesi di dottorato
Lingua: English
Title: On Games in Formal Verification
Creators:
CreatorsEmail
Sorrentino, Loredanaloredana.sorrentino@unina.it
Date: 31 March 2015
Number of Pages: 83
Institution: Università degli Studi di Napoli Federico II
Department: Matematica e Applicazioni "Renato Caccioppoli"
Scuola di dottorato: Scienze matematiche e informatiche
Dottorato: Scienze computazionali e informatiche
Ciclo di dottorato: 27
Coordinatore del Corso di dottorato:
nomeemail
Moscariello, Giocondagmoscari@unina.it
Tutor:
nomeemail
Murano, AnielloUNSPECIFIED
Date: 31 March 2015
Number of Pages: 83
Uncontrolled Keywords: Formal verification, quantitative requirements
Settori scientifico-disciplinari del MIUR: Area 01 - Scienze matematiche e informatiche > INF/01 - Informatica
Date Deposited: 10 Apr 2015 11:55
Last Modified: 30 Sep 2015 16:49
URI: http://www.fedoa.unina.it/id/eprint/10355
DOI: 10.6092/UNINA/FEDOA/10355

Abstract

Nel Capitolo 1 facciamo uno studio generale del concetto di "prompt" applicato ai Parity Games. Tale studio permette di raggruppare diverse condizioni di parity, alcune introdotte da noi, altre già presenti in letteratura, sotto un unico framework. Inoltre, in questo capitolo, vengono descritte semplici riduzioni polinomiali da tutte queste condizioni a Buchi o Parity, che semplificano tutte le procedure conosciute finora. In particolare, le riduzioni che vengono descritte, abbassano la classe di complessità delle condizioni Cost e Bounded Cost Parity recentemente introdotte. Infatti, vengono forniti algoritmi che mostrano che, determinare il vincitore di tale giochi è in UPTime ∩ CoUPTime. Nel Capitolo 2 viene rivisitata l'implementazione dell'algoritmo ricorsivo di Zielonka introducendo diversi miglioramenti e facendo uso del linguaggio di programmazione Scala. Questa scelta è stata dimostrata essere vantaggiosa, riducendo il tempo di esecuzioni di due ordini di grandezza. Nel Capitolo 3, viene introdotto e studiato Graded Strategy Logic (GSL), un estensione di Strategy Logic (SL) con quantificatori di grado. In tale capitolo, oltre ad essere fornite sintassi e semantica di tale logica, vengono investigate alcune questioni riguardo il frammento vanilla di GSL. In particolare vengono riportati risultati positivi circa la determinatezza dei giochi turn-based ed il relativo problema del model checking, che è mostrato essere in Ptime.

Actions (login required)

View Item View Item