Sorrentino, Loredana (2015) On Games in Formal Verification. [Tesi di dottorato]
Anteprima |
Testo
Sorrentino_Loredana.pdf Download (862kB) | Anteprima |
| Tipologia del documento: | Tesi di dottorato |
|---|---|
| Lingua: | English |
| Titolo: | On Games in Formal Verification |
| Autori: | Autore Email Sorrentino, Loredana loredana.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: | nome email Moscariello, Gioconda gmoscari@unina.it |
| Tutor: | nome email 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 |
