Ricerc@Sapienza

Tipicamente, l'analisi dei sistemi concorrenti mira ad analizzare i conflitti fra le possibili evoluzioni individuali, mentre per i sistemi distribuiti l'enfasi è sulle possibili inconsistenze tra le informazioni disponibili a ogni singolo agente. In entrambi i casi, il ricorso a meccanismi ad hoc, logici o algoritmici, rende difficile la generalizzazione dei risultati raggiunti per una certa classe di problemi ad altre situazioni. Al contrario, gli approcci categoriali alla definizione di logiche partono da proprietà algebriche delle strutture formali delle computazioni per derivare, in modo canonico, strutture logiche applicabili uniformemente a tutti i modelli che condividono quel tipo di proprietà. Ciò ha trovato ampio utilizzo nei sistemi concorrenti; recentemente, si è iniziata l'applicazione anche ai sistemi distribuiti, i cui aspetti spaziali e topologici rendono più difficile identificare strutture algebriche maneggevoli. Lo studio dei sistemi distribuiti acquisisce oggi nuove dimensioni, soprattutto in tre ambiti che forniranno anche i casi di studio su cui verificare la ricerca.

1. La garanzia di eventual consistency e strong consistency sul raggiungimento di stati comuni per CRDTs

2. La diffusione delle tecnologie blockchain, dove la legittimità di informazioni disponibili dipende da un insieme qualificato di altri nodi.

3. La diffusione della Secure Multiparty Computation, in cui ciascun nodo realizza una parte diversa di una computazione, senza accedere a informazioni non rilevanti al suo compito.

L'attività di ricerca mira a estendere, attraverso logiche adeguate all'analisi di sistemi distribuiti, la recente proposta di un metodo per la costruzione di logiche modali/temporali per sistemi concorrenti, da cui derivare uniformemente sistemi (intuizionistici) del primo ordine, in base alle proprietà dei morfismi derivabili sulle strutture delle computazioni.