Obiettivi del progetto

La diffusione capillare di Internet e World Wide Web ha creato un forte interesse per applicazioni e servizi informatici che ne sfruttino appieno le potenzialità. A questo scopo si richiede alle moderne applicazioni di essere aperte verso gruppi di utenti e componenti software ignoti a priori ed in continuo cambiamento, richiedendo al nuovo software requisiti di adattabilità, scalabilità e sicurezza senza precedenti. Per soddisfare tali requisiti sono stati utilizzati con successo sistemi multiagente, in cui gli agenti sono dotati di autonomia e capacità di ragionamento. Tali agenti, capaci di interagire con altro software o utenti umani per perseguire i propri obiettivi, vengono utilizzati in molti campi portando, per esempio, alla realizzazione di applicazioni mediche, industriali, di telecomunicazioni ed intrattenimento.
Il comportamento dei sistemi multiagente è difficile da prevedere e controllare soprattutto al crescere della complessità delle interazioni. Infatti il comportamento di questi sistemi non è controllato centralmente, ma "emerge" dall'interazione dei loro componenti, che si prevede sempre più "intelligente" e trasparente agli utenti, e coinvolgerà forme di negoziazione, competizione e cooperazione.
Sono pertanto desiderabili sia meccanismi di modellazione e specifica, che permettano di vincolare almeno parzialmente struttura e comportamento globale del sistema (ad esempio restringendo le possibili interazioni senza irrigidire troppo i protocolli) sia strumenti di verifica automatica o semi-automatica dei comportamenti emergenti di sistemi multiagente.

Il progetto si pone quindi i seguenti obbiettivi:

• Individuare e sviluppare formalismi logici atti a modellare e specificare il comportamento di agenti, le loro modalità di interazione intelligente ed i comportamenti globali dei sistemi multiagente.
• Definire linguaggi di specifica eseguibili, ottenuti considerando frammenti computazionali delle logiche studiate nel punto precedente.
• Sviluppare tecniche per la verifica di proprietà di sistemi multiagente.

Una scelta naturale è di perseguire questi obiettivi mediante l'uso di logiche non classiche, ad es. epistemiche e temporali, e della logica computazionale. Le logiche temporali sono uno standard nell'analisi dei sistemi distribuiti e con le logiche epistemiche hanno un ruolo rilevante nella modellazione dei sistemi ad agenti (vedasi ad es. il modello BDI). La logica computazionale porta a specifiche eseguibili, semplificando così i compiti di realizzazione e verifica. In particolare, nell'ambito del progetto, verranno utilizzate estensioni della programmazione logica mediante abduzione e ragionamento non-monotono - atti a modellare la conoscenza incompleta che gli agenti hanno sul mondo e l'evoluzione dinamica del sistema - nonché estensioni modali e temporali per modellare il ragionamento su azioni e la dinamica degli stati mentali degli agenti.
Per la verifica automatica, verranno considerate principalmente tecniche di model checking, con l’obiettivo di adattare le tecniche e gli strumenti sviluppati per la verifica di sistemi software distribuiti alla verifica di proprietà di sistemi multiagente.
Verranno compiute sperimentazioni in diversi ambiti applicativi.