Istituzioni artificiali: specifica e verifica di sistemi di interazione aperti e distribuiti

Le istituzioni sono state proposte per progettare, analizzare e regolamentare sistemi multiagente aperti dove gli agenti sono sviluppati da molteplici organizzazioni. In tali sistemi, le istituzioni giocano due ruoli: i) definiscono un insieme di norme che rendono maggiormente predicibile il comportamento degli altri agenti e ii) descrivono l´ontologia del contesto di interazione.
Nei sistemi aperti è poco realistico aspettarsi che agenti autonomi rispettino sempre le norme. Pertanto, la ricerca sulle istituzioni si è maggiormente concentrata sullo sviluppo di linguaggi e strumenti per modellizzare e vigilare le interazioni tra agenti al fine di evitare la violazione delle norme. Nel fare ciò, le istituzioni aumentano l´efficienza delle transazioni elettroniche, ma sollevano il problema di come garantire che tali sistemi di regole non siano caratterizzati da norme contraddittorie e forniscano agli agenti i poteri istituzionali di cui necessitano per raggiungere i loro obiettivi. Ciò è particolarmente importante quando le istituzioni sono complesse ed è proibitivo prevedere tutte le possibili evoluzioni compatibili con esse.
Per queste ragioni, la verifica formale delle istituzioni dovrebbbe essere considerata come una fase importante durante il loro sviluppo, dal momento che può concorrere a aumentarne la correttezza. Questo progetto si propone di definire un formalismo per descrivere le istituzioni e di verificarne le proprietà mediante model checking.