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.
Recentemente, alcuni dei partecipanti al progetto hanno proposto un metodo per la costruzione di logiche modali/temporali applicabili a sistemi concorrenti e parametrizzate in base alle etichette sulle strutture delle computazioni; ciò ha permesso di derivare uniformemente sistemi del primo ordine classici o intuizionistici, a seconda del grado di nondeterminismo coinvolto. Si è quindi iniziato un lavoro esplorativo per estendere questa costruzione per ottenere logiche adeguate alle problematiche dell'analisi di sistemi distribuiti, dove la possibilità di inconsistenza potrebbe sostituire il nondeterminismo; ciò ha fornito dei primi indizi promettenti. L'attività di ricerca verterà quindi sull'identificazione delle strutture astratte caratterizzanti i modelli di sistemi distribuiti, tramite cui svolgere almeno lo studio delle tre tipologie di sistemi considerati come casi di studio ; ciò porterà ad ottenere una garanzia logica a fondamento delle soluzioni algoritmiche e probabilistiche tipicamente usate in questi ambiti. Ci si aspetta quindi sia di derivare un quadro di riferimento uniforme per questo ambito di problemi, sia di ottenere risultati specifici per i tre casi di studio.
In particolare l'approccio logico alla base del progetto di ricerca, che sfrutta la presenza di una struttura di semi-reticolo caratterizzante lo spazio delle computazioni [BGKL17], analogamente a quanto richiesto per i CRDT basati sullo stato, può quindi essere adattato facilmente alla loro modellazione, mentre può fornire una base logica e non puramente operazionale alla caratterizzazione di CRDT basati su operazioni.
Analogamente a quanto avviene per i CRDT, la ricerca sui bitcoin è tradizionalmente basata, nell'approccio di Nakamoto, su garanzie di eventual consistency, cioè di potere completare una computazione in modo che tutti i nodi siano in accordo sulla composizione attuale della blockchain [GKL15]. Ciò ha messo in luce alcune insufficienze connesse alla garanzia di eventual consistency, e ha portato a proporre una nozione di strong consistency, in cui ogni stato stabile è sicuro, cioè tutte le transazioni riportate nella blockchain sono legali, con alta probabilità [DSW16]. Un approccio logico basato su considerazioni completamente diverse dalle nostre (su logica lineare) è stato proposto per caratterizzare gli algoritmi per le blockchain, in modo da poter ragionare su una singola rappresentazione, in termini di alberi di prova, dell'intero stato del sistema [Mer17].
L'estensione di un approccio logico in modo da incorporare nella stessa struttura aspetti di evoluzione della computazione e aspetti di comunicazione può permettere di esprimere proprietà dello stato in modo direttamente logico, eventualmente incorporando valori riconducibili ad aspetti probabilistici, dando uno strumento formale più potente rispetto alla caratterizzazione puramente probabilistica. Si potrebbe in questo senso tracciare un'analogia con il passaggio nei modelli concorrenti dal CCS al pi-calcolo, che incorpora una nozione di comunicazione nella struttura della computazione [Mil99].
[BGLK17] P.Bottoni, D.Gorla, A.Labella, S.Kasangian: A doctrinal approach to modal/temporal Heyting logic and non-determinism in processes, Mathem. Str. in Comp. Sci., 1-25. doi:10.1017/S0960129517000019.
[BLK12] P.Bottoni, A.Labella, S.Kasangian: Spatial and temporal aspects in visual interaction. J. Vis. Lang. Comput. 23(2): 91-102 (2012)
[DSW16] C.Decker, J.Seidel, R.Wattenhofer: Bitcoin meets strong consistency. In Proc. ICDCN '16. ACM, Article 13, DOI:https://doi.org/10.1145/2833312.2833321
[Mer17] L.G.Meredith, Linear Types Can Change the Blockchain, arXiv:1506.01001
[Mil99] R.Milner. Communicating and Mobile Systems: The pi-calculus. Cambridge, UK: Cambridge Univ. Press 1999