Sorrentino, Loredana
(2015)
On Games in Formal Verification.
[Tesi di dottorato]
| Item Type: |
Tesi di dottorato
|
| Resource language: |
English |
| Title: |
On Games in Formal Verification |
| Creators: |
| Creators | Email |
|---|
| Sorrentino, Loredana | loredana.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: |
| nome | email |
|---|
| Moscariello, Gioconda | gmoscari@unina.it |
|
| Tutor: |
| nome | email |
|---|
| Murano, Aniello | UNSPECIFIED |
|
| Date: |
31 March 2015 |
| Number of Pages: |
83 |
| Keywords: |
Formal verification, quantitative requirements |
| Settori scientifico-disciplinari del MIUR: |
Area 01 - Scienze matematiche e informatiche > INF/01 - Informatica |
[error in script]
[error in script]
| 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 |
Collection description
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 per month over past year
Actions (login required)
 |
View Item |
