ETD

Archivio digitale delle tesi discusse presso l'Università di Pisa

Tesi etd-01192015-204228


Tipo di tesi
Tesi di laurea magistrale
Autore
SESTINI, DARIO
URN
etd-01192015-204228
Titolo
Verifica di proprieta' di modelli di giochi con tecniche di model checking probabilistico
Dipartimento
FILOLOGIA, LETTERATURA E LINGUISTICA
Corso di studi
INFORMATICA UMANISTICA
Relatori
relatore Dott. Milazzo, Paolo
Parole chiave
  • model
  • checking
  • modelli
  • games
  • board
  • game
  • design
Data inizio appello
09/02/2015
Consultabilità
Completa
Riassunto
Il gioco e l'attività di giocare sono insite nell'essere umano il quale nel corso dei secoli ha messo alla prova le sue capacità in sfide di ogni sorta. Nei primi due capitoli di questo elaborato si fornisce un quadro teorico e introduttivo al mondo del gioco, analizzando alcuni contributi provenienti sia dall'area umanistica in generale, sia dal cerchio un po' più ristretto dei Games Studies i quali recentemente stanno vivendo un momento di felice espansione. Si propone una definizione di gioco partendo dalle definizioni che altri studiosi del fenomeno hanno fornito in passato per poi passare all'analisi del gioco inteso come artefatto, oggetto immaginario o tangibile in grado di far vivere ai giocatori esperienze più o meno significative. Soffermandoci in particolare sui giochi da tavolo, oggetto specifico dell'elaborato, si fa un elenco di alcune delle proprietà che un gioco possiede o dovrebbe possedere al fine di poter offrire un ai giocatori un'esperienza di un certo tipo. La progettazione degli artefatti ludici, che prende il nome di game design, sarà affrontata a partire da alcuni concetti chiave che ne stanno alla base.
Nel terzo capitolo si affronta in modo più approfondito la modellazione di un gioco e l'analogia che esiste tra questo e i sistemi transizionali, per poi fornire un esempio di studio di un modello di gioco implementato attraverso la piattaforma software PRISM. Grazie a questo strumento è infatti possibile verificare se un modello soddisfa o meno determinate proprietà sfruttando tecniche di model checking probabilistico e statistico. In questo capitolo si offre inoltre una breve panoramica sul model checking stesso, mettendo in luce alcune delle problematiche legate ai metodi formali di verifica e i risultati che ad oggi si è riusciti a ottenere in questo campo. Infine l'ultimo capitolo contiene tre casi di studio con i quali si intende esplorare una metodologia con la quale, attraverso l'analisi delle proprietà di un gioco, si possa rendere più efficace la progettazione di artefatti ludici di qualsiasi genere. In particolare nei casi di studio verranno mostrati alcuni test effettuati su modelli di gioco da noi creati, allo scopo di verificare formalmente alcune delle proprietà viste nei capitoli precedenti.
File