On Games in Formal Verification

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.