• checking
• domain
• games
• language
• model
• parsing
• specific

Il model checking consiste in tecniche di verifica formale che consentono di controllare le proprietà comportamentali desiderate in un dato sistema, sulla base di un modello del sistema in questione, attraverso ispezioni sistematiche di tutti i suoi stati.
Nelle ultime due decadi queste tecniche si sono sviluppate notevolmente, soprattutto nell'ambito
della Computer Science, come metodo per verificare l'assenza di errori. Non è, tuttavia, difficile capire come la costruzione di modelli ad hoc e la verifica formale di proprietà desiderate, sia una tecnica utile in diversi campi del sapere.
Il lavoro di sperimentazione alla base di tale tesi tratta, appunto, la definizione di un linguaggio di modellazione da usare nell'ambito del game design per la verifica formale di proprietà di giochi. L'idea nasce da un precedente lavoro di sperimentazione, nel quale i modelli sono stati implementati con lo strumento di model checking PRISM. Il linguaggio di PRISM si è però dimostrato inadeguato per descrivere alcuni aspetti comuni ai giochi. Da questa riflessione è nata l'idea di definire un nuovo linguaggio di alto livello che renda più semplice e rapida la costruzione dei modelli, pur consentendo una successiva compilazione nel linguaggio di input di PRISM.