RICERCA ITALIANA     

Programma di ricerca

Fondamenti Logici dei Sistemi Distribuiti e Codice Mobile

Università di riferimento

Università degli Studi di BOLOGNA - SCIENZE DELL'INFORMAZIONE - BOLOGNA(BO)

Responsabile dell'Unità di ricerca

Davide SANGIORGI

Descrizione

I contributi sono elencati dettagliatamente nel seguito. E' bene sottolineare che il piu' importante task dell'unita' e' quello relativo all'equivalenza comportamentale. In particolare, l'unita' sara' attiva sui seguenti argomenti relativi a questo task:
- tecniche coinduttive "up-to"
- equivalenze comportamentali tipizzate e ad alto livello
- relazioni tra proprieta' comportamentali e logiche spaziali

Equivalenze comportamentali.

Un obiettivo e' quello di sviluppare un linguaggio concorrente basato sulle tecniche delle relazioni logiche in formalismi con tipi (una tecnica molto utilizzata e ampiamente studiata per i linguaggi sequenziali di ordine superiore). Si tratta di un obiettivo ambizioso che potrebbe portare notevoli vantaggi. Infatti, anche se che queste relazioni logiche hanno un carattere intuizionista ed applicativo, esse non sono mai state utilizzate con successo in formalismi concorrenti nonostante le loro potenzialita'.

Un ulteriore obiettivo riguarda il raffinamento delle nozioni classiche di osservazioni e di azioni che possano essere adatte a formalismi per modellare processi mobili tipizzati. Un lavoro preliminare in questo settore e' stato portato avanti in [PiSa00] utilizzando pero' un sistema di tipi molto semplice e non completamente sviluppato.

Per quanto riguarda lo studio di meccanismi di inferenza per formalismi che modellano sistemi distribuiti con processi mobili, l'obiettivo e' quello di studiarli a fondo per raffinare la classificazione presentata in [LeSa03]. Inoltre si studieranno le implicazioni di questi meccanismi di inferenza sulle teorie comportamentali dei processi.

Un altro aspetto dell'effetto dei tipi sulle equivalenze che verra' affrontato riguarda l'utilizzo di informazione sui tipi negli algoritmi per la verifica automatica di proprieta', come quelli basati sulla minimizzazione o sul model checking, con l'obiettivo di aumentare la loro efficienza. Ad esempio la specifica di alcuni tipi puo' garantire che certe comunicazioni non sono preemptive. Si tratta di una proprieta' di confluenza parziale, che se verificata permette di analizzare dettagliatamente solo una parte del comportamento dei processi studiati.

Per quanto riguarda i linguaggi di comunicazione tra agenti, studieremo un estensione dell'architettura proposta in [Gas02] con meccanismi per trattare i fallimenti in modo da fornire primitive di comunicazione tolleranti ai guasti. Inoltre si studieranno diversi aspetti che riguardano le algebre degli attori, per poter studiare in modo piu' adeguato l'architettura presentata in [Gas02]. In particolare lo studio di diversi tipi di bisimulazione e di altre nozioni di equivalenza tra termini di attori e lo sviluppo di una logica per studiare le proprieta' dei programmi. Infine si studiera' un estensione dell'algebra per trattare fallimenti di tipo crash.

Un aspetto rilevante e comune a tutti gli argomenti indicati sopra e' lo sviluppo di tecniche di prova e algoritmi basati sulla coinduzione, in particolare sulle `bisimulation up-to'.

Tipi.

Contiamo di esportare le tecniche per tipi polimorfi su linguaggi sequenziali (soprattutto funzionali) su calcoli di processi mobili. Uno studio preliminare [PiSa00] mostra che il polimorfismo ha una forte conseguenza su aspetti comportamentali, ad esempio permette di trascurare dettagli implementativi dei server. Mancano ancora pero' principi parametrici per ragionare in questo scenario, che l'unita' conta di affrontare.

Intendiamo arricchire i tipi "capability-based" che esistono per versioni distribuite del pi-calcolo e dei vari calcoli di coordinazione (Linda-like) con meccanismi per supportare la declassificazione, cioe' la capacita' di declassificare temporaneamente alcune informazioni confidenziali o modificare dinamicamente domini di protezione. Questo potrebbe richiedere un uso maggiore del type checking dinamico.

Su questi argomenti di tipi, contiamo di collaborare con altre unita', specie Torino data la loro esperienza su tipi (particolarmente per quanto riguarda lo sviluppo dei tipi polimorfi).

Logiche per la specifica.

Espressivita' e decidibilita' delle logiche spaziali: Ci concentreremo sull'espressivita' delle logiche spaziali di base e cercheremo di identificare appropriate estensioni di alto livello. L'obiettivo finale e' sviluppare modalita' di alto livello, esprimibili nella logica di base, che aiutino a definire e provare proprieta' utilizzando tecniche di dimostrazione specializzate e possibilmente tool associati.

La semantica indotta dalle logiche spaziali e' intensionale e di conseguenza piu' fine di quella indotta dalla semantica operazionale standard. Cio' e' in evidente contrasto con la situazione per le logiche modali "classiche", per le quali esistono risultati che relazionano logiche ed equivalenze operazionali (tipicamente forme di bisimilarita'). Vogliamo indagare l'impatto dell'approccio intensionale sui problemi di decidibilita' per le logiche. Un'altra questione da affrontare riguarda l'impatto delle variazioni sulla semantica delle logiche su questioni di decidibilita' e intensionalita'. Aspiriamo a definire logiche spaziali che siano in accordo con la semantica operazionale, analogamente alle logiche modali classiche con la bisimilarita'.