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

[img]
Anteprima
Testo
Sorrentino_Loredana.pdf

Download (862kB) | Anteprima
[error in script] [error in script]
Tipologia del documento: Tesi di dottorato
Lingua: English
Titolo: On Games in Formal Verification
Autori:
AutoreEmail
Sorrentino, Loredanaloredana.sorrentino@unina.it
Data: 31 Marzo 2015
Numero di pagine: 83
Istituzione: Università degli Studi di Napoli Federico II
Dipartimento: 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, Aniello[non definito]
Data: 31 Marzo 2015
Numero di pagine: 83
Parole chiave: Formal verification, quantitative requirements
Settori scientifico-disciplinari del MIUR: Area 01 - Scienze matematiche e informatiche > INF/01 - Informatica
Depositato il: 10 Apr 2015 11:55
Ultima modifica: 30 Set 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.

Downloads

Downloads per month over past year

Actions (login required)

Modifica documento Modifica documento