[INdAM-GNCS] Logica, Automi e Giochi per Sistemi Auto-adattivi

I moderni sistemi informatici sono sempre piu potenti e versatili e presentano diverse caratteristiche avanzate che ne rendono difficile lo sviluppo, come la presenza di una molteplicita di componenti che operano in modo concorrente, vincoli real-time, una distribuzione logica e fisica delle componenti. Inoltre, si trovano sempre piu spesso ad operare in scenari dinamici, dove il comportamento del sistema deve adattarsi ai cambiamenti dell'ambiente circostante e degli altri agenti che lo circondano. Infine, in molti casi sono chiamati ad eseguire compiti complessi con scarsa o nulla supervisione umana.

I costi e la complessita sempre piu alta di questo tipo di sistemi hanno reso da tempo inadeguate le tecniche classiche di validazione quali la simulazione e il testing e spingono verso un uso sistematico di metodi e strumenti formali di modellazione, verifica e sintesi in grado di garantire correttezza, affidabilita ed efficienza. Metodi formali basati su logica, automi e giochi sono stati utilizzati con profitto nella verifica e nella sintesi di diversi tipi di sistemi: dai circuiti digitali al software e dai sistemi a stati discreti a quelli ibridi continuo-discreti. Tuttavia, la maggior parte degli approcci esistenti sono stati sviluppati in un contesto di sistemi monolitici con una limitata possibilita di adattamento.

In questo progetto ci proponiamo di utilizzare gli strumenti della logica, della teoria degli automi e della teoria dei giochi per sviluppare un insieme di formalismi e algoritmi per risolvere problemi di soddisfacibilita, model checking e sintesi per sistemi auto-adattivi, ossia in grado di reagire ai cambiamenti dell'ambiente in maniera automatica. Il progetto mira a superare le limitazioni delle soluzioni esistenti guidati da due domini applicativi specifici. Il primo dominio applicativo è quello del planning; il secondo dominio applicativo è quello dell'autonomic computing.