Coordinatore scientifico

Prof. Alberto Martelli
Dipartimento di Informatica - Università degli Studi di Torino

Obiettivi del progetto

I servizi forniti in molti domini applicativi sempre più possono essere descritti e realizzati come espressione di un insieme di agenti cooperanti. Rispetto all'approccio più tradizionale della programmazione a componenti, il paradigma ad agenti esplicita aspetti sociali, connessi alla caratteristica degli agenti di essere autonomi e proattivi: le componenti comunicano e si coordinano in maniera dinamica, utilizzando linguaggi ad alto livello, per perseguire scopi comuni (o propri). Tra gli aspetti sociali è particolarmente importante definire "regole comportamentali", espresse mediante protocolli di comunicazione (interazione), finalizzate a controllare l'organizzazione del sistema. I protocolli di comunicazione possono essere utilizzati per regolare l'interazione fra gli agenti specificando un insieme di conversazioni accettabili, ossia sequenze di operazioni (in particolare scambi di messaggi) che si possono svolgere fra agenti diversi. Con la rapida espansione di internet, gli agenti si trovano sempre più ad operare in ambienti fortemente dinamici. Diventa quindi essenziale che gli agenti soddisfino proprietà che ne garantiscano l'interoperabilità, come ad esempio che un agente sia conforme a un protocollo di interazione, che un agente stia rispettando i suoi vincoli sociali o che un protocollo ottenuto per composizione conservi le proprietà dei protocolli che lo compongono. Per dimostrare se un protocollo garantisce o meno determinate proprietà è necessario specificarlo in un linguaggio formale. Infatti l'utilizzo di linguaggi formali di specifica consente di sviluppare tecniche di verifica formale di proprietà.
L'obiettivo di questo progetto è quello di sviluppare strumenti e tecniche per la specifica e la verifica di proprietà riguardanti l'interazione fra agenti in un sistema multiagente. Più precisamente i principali obiettivi del progetto sono i seguenti:

  • Definizione di formalismi per la specifica e la verifica di protocolli di interazione
    Verranno analizzate le principali proprietà dei protocolli di interazione che si intendono verificare, e verranno individuati i formalismi più adeguati per esprimere queste proprietà. I formalismi utilizzati per specificare protocolli di comunicazione e per descriverne le proprietà saranno prevalentemente basati sulla logica (temporale e computazionale), ma si prenderanno in considerazione anche formalismi a vincoli, linguaggi formali ed automi.
  • Verifica automatica delle proprietà
    Verranno messe a punto tecniche di verifica per i formalismi sviluppati nel punto precedente. In particolare, per le logiche temporali, saranno sviluppate tecniche di model checking. In altri casi, si applicheranno tecniche basate su procedure di dimostrazione e si indagheranno tecniche basate su risoluzione estesa. Verranno anche sviluppate tecniche di prototipazione rapida per la validazione di protocolli di interazione.
  • Linguaggi di modellazione e loro traduzione nei linguaggi formali definiti nel progetto
    Per lo sviluppo dei sistemi multiagente sono stati proposti numerosi linguaggi di modellazione. Questi linguaggi mancano di semantica formale e quindi non sono utilizzabili direttamente per la dimostrazione automatica di proprietà delle componenti del sistema. Un obiettivo è quello di analizzare i linguaggi di modellazione più diffusi, in particolare formalismi grafici, e di definire tecniche di traduzione nei formalismi sviluppati nel progetto.

I linguaggi, le tecniche e gli strumenti sviluppati verranno valutati in diversi ambiti applicativi, fra cui principalmente: linee guida cliniche, servizi web, commercio elettronico e sicurezza, presentazioni multimediali.