Indagini in Deep Inference

La tesi è uno studio di alcuni aspetti della nuova metodologia “deep inference”, abbinato ad una rivisitazione dei concetti classici di proof theory, con l'aggiunta di alcuni risultati originali orientati ad una maggior comprensione dell'argomento, nonché alle applicazioni pratiche. Nel primo capitolo vengono introdotti, seguendo un approccio di stampo formalista (con alcuni spunti personali), i concetti base della teoria della dimostrazione strutturale – cioè quella che usa strumenti combinatoriali (o “finitistici”) per studiare le proprietà delle dimostrazioni. Il secondo capitolo focalizza l'attenzione sulla logica classica proposizionale, prima introducendo il calcolo dei sequenti e dimostrando il Gentzen Hauptsatz, per passare poi al calcolo delle strutture (sistema SKS), dimostrando anche per esso un teorema di eliminazione del taglio, appositamente adattato dall'autore. Infine si discute e dimostra la proprietà di località per il sistema SKS. Un percorso analogo viene tracciato dal terzo ed ultimo capitolo, per quanto riguarda la logica lineare. Viene definito e motivato il calcolo dei sequenti lineari, e si discute del suo corrispettivo nel calcolo delle strutture. L'attenzione qui è rivolta maggiormente al problema di definire operatori non-commutativi, che mettono i sistemi in forte relazione con le algebre di processo.

Segmentazione e categorizzazione di oggetti mediante immagini depth e deep learning

Questo lavoro è iniziato con uno studio teorico delle principali tecniche di classificazione di immagini note in letteratura, con particolare attenzione ai più diffusi modelli di rappresentazione dell’immagine, quali il modello Bag of Visual Words, e ai principali strumenti di Apprendimento Automatico (Machine Learning). In seguito si è focalizzata l’attenzione sulla analisi di ciò che costituisce lo stato dell’arte per la classificazione delle immagini, ovvero il Deep Learning. Per sperimentare i vantaggi dell’insieme di metodologie di Image Classification, si è fatto uso di Torch7, un framework di calcolo numerico, utilizzabile mediante il linguaggio di scripting Lua, open source, con ampio supporto alle metodologie allo stato dell’arte di Deep Learning. Tramite Torch7 è stata implementata la vera e propria classificazione di immagini poiché questo framework, grazie anche al lavoro di analisi portato avanti da alcuni miei colleghi in precedenza, è risultato essere molto efficace nel categorizzare oggetti in immagini. Le immagini su cui si sono basati i test sperimentali, appartengono a un dataset creato ad hoc per il sistema di visione 3D con la finalità di sperimentare il sistema per individui ipovedenti e non vedenti; in esso sono presenti alcuni tra i principali ostacoli che un ipovedente può incontrare nella propria quotidianità. In particolare il dataset si compone di potenziali ostacoli relativi a una ipotetica situazione di utilizzo all’aperto. Dopo avere stabilito dunque che Torch7 fosse il supporto da usare per la classificazione, l’attenzione si è concentrata sulla possibilità di sfruttare la Visione Stereo per aumentare l’accuratezza della classificazione stessa. Infatti, le immagini appartenenti al dataset sopra citato sono state acquisite mediante una Stereo Camera con elaborazione su FPGA sviluppata dal gruppo di ricerca presso il quale è stato svolto questo lavoro. Ciò ha permesso di utilizzare informazioni di tipo 3D, quali il livello di depth (profondità) di ogni oggetto appartenente all’immagine, per segmentare, attraverso un algoritmo realizzato in C++, gli oggetti di interesse, escludendo il resto della scena. L’ultima fase del lavoro è stata quella di testare Torch7 sul dataset di immagini, preventivamente segmentate attraverso l’algoritmo di segmentazione appena delineato, al fine di eseguire il riconoscimento della tipologia di ostacolo individuato dal sistema.

Simulation of bistatic radar experiments with deep space missions

L’obiettivo del lavoro esposto nella seguente relazione di tesi ha riguardato lo studio e la simulazione di esperimenti di radar bistatico per missioni di esplorazione planeteria. In particolare, il lavoro si è concentrato sull’uso ed il miglioramento di un simulatore software già realizzato da un consorzio di aziende ed enti di ricerca nell’ambito di uno studio dell’Agenzia Spaziale Europea (European Space Agency – ESA) finanziato nel 2008, e svolto fra il 2009 e 2010. L’azienda spagnola GMV ha coordinato lo studio, al quale presero parte anche gruppi di ricerca dell’Università di Roma “Sapienza” e dell’Università di Bologna. Il lavoro svolto si è incentrato sulla determinazione della causa di alcune inconsistenze negli output relativi alla parte del simulatore, progettato in ambiente MATLAB, finalizzato alla stima delle caratteristiche della superficie di Titano, in particolare la costante dielettrica e la rugosità media della superficie, mediante un esperimento con radar bistatico in modalità downlink eseguito dalla sonda Cassini-Huygens in orbita intorno al Titano stesso. Esperimenti con radar bistatico per lo studio di corpi celesti sono presenti nella storia dell’esplorazione spaziale fin dagli anni ’60, anche se ogni volta le apparecchiature utilizzate e le fasi di missione, durante le quali questi esperimenti erano effettuati, non sono state mai appositamente progettate per lo scopo. Da qui la necessità di progettare un simulatore per studiare varie possibili modalità di esperimenti con radar bistatico in diversi tipi di missione. In una prima fase di approccio al simulatore, il lavoro si è incentrato sullo studio della documentazione in allegato al codice così da avere un’idea generale della sua struttura e funzionamento. È seguita poi una fase di studio dettagliato, determinando lo scopo di ogni linea di codice utilizzata, nonché la verifica in letteratura delle formule e dei modelli utilizzati per la determinazione di diversi parametri. In una seconda fase il lavoro ha previsto l’intervento diretto sul codice con una serie di indagini volte a determinarne la coerenza e l’attendibilità dei risultati. Ogni indagine ha previsto una diminuzione delle ipotesi semplificative imposte al modello utilizzato in modo tale da identificare con maggiore sicurezza la parte del codice responsabile dell’inesattezza degli output del simulatore. I risultati ottenuti hanno permesso la correzione di alcune parti del codice e la determinazione della principale fonte di errore sugli output, circoscrivendo l’oggetto di studio per future indagini mirate.

Ricerca di AGN oscurati nei Chandra Deep Fields

La forma spettrale dell’X-ray background richiede l’esistenza di un grande numero di AGN mediamente oscurati, oltre alla presenza di AGN fortemente oscurati, la cui densità di colonna supera il limite Compton (Nh>10^24 cm^(-2)). A causa della loro natura, questi oggetti risultano di difficile osservazione, per cui è necessario adottare un approccio multi-banda per riuscire a rivelarli. In questo lavoro di tesi abbiamo studiato 29 sorgenti osservate nel CDF-S e 10 nel CDF-N a 0.0710^23, spettro piatto, riga del ferro): a seguito di questa analisi sono state individuate 9 sorgenti che presentano indicazioni di forte oscuramento. Dallo studio del rapporto tra la luminosità X (2-10 keV) e quella MIR (12.3um) dedotta dal SED-fitting, si è ottenuta una conferma della possibile presenza di forte oscuramento nelle 9 sorgenti selezionate a seguito dell’analisi spettrale. Abbiamo inoltre confrontato il tasso di formazione stellare dedotto dalla banda X (0.5-8 keV) e da quella IR (8-1000um) per identificare le sorgenti nelle quali l’emissione da AGN risulta essere dominante. A seguito di questa analisi abbiamo identificato 9 sorgenti (le stesse di cui sopra) con indicazione di forte oscuramento; di queste, 3 mostrano chiare indicazioni della presenza di un AGN Compton Thick (Nh>10^24 cm^(-2), riga del ferro intensa, basso rapporto LX/MIR).

Modifiche al protocollo di trasporto LTP per migliorarne le prestazioni in presenza di perdite elevate

La presente tesi si pone come obiettivo quello di analizzare il protocollo LTP (in particolare in ION) e proporre dei miglioramenti utili al caso in cui siano presenti perdite elevate. Piu in dettaglio, una prima parte introduttiva motiva l'inefficacia del TCP/IP in ambito interplanetario e introduce l'architettura DTN Bundle Protocol (Cap.1). La tesi prosegue con la descrizione delle specifiche del protocollo LTP (Cap.2), in particolar modo evidenziando come un bundle venga incapsulato in un blocco LTP, come questo sia successivamente diviso in tanti segmenti LTP e come questi vengano successivamente inviati con il protocollo UDP o con un protocollo analogo. Viene quindi presentata un'approfondita analisi delle penalizzazioni dovute alle perdite dei segmenti LTP, sia di tipo dati che di segnalazione (Cap. 3). Quest'analisi permette di dimostrare la criticita degli effetti delle perdite, in particolare per quello che riguarda i segmenti LTP di segnalazione. Mentre in presenza di perdite basse tali effetti hanno in media un impatto minimo sul tempo di consegna di un blocco LTP (quindi del bundle in esso contenuto), in quanto avvengono raramente, in presenza di perdite elevate rappresentano un collo di bottiglia per il tempo di consegna di un blocco LTP. A tal proposito sono state proposte alcune modifiche che permettono di migliorare le prestazioni di LTP (Cap. 4) compatibilmente con le specifiche RFC in modo da garantire l'interoperabilita con le diverse implementazioni del protocollo. Successivamente nel Cap. 5 viene mostrato come sono state implementate le modifiche proposte in ION 3.4.1. Nel capitolo finale (Cap. 6) sono presenti i risultati numerici relativi ad alcuni test preliminari eseguiti confrontando la versione originale del protocollo con le versioni modificate contenenti i miglioramenti proposti. I test sono risultati molto positivi per elevate perdite, confermando cosi la validita dell'analisi e dei miglioramenti introdotti.

A deep learning-based approach for 3D people tracking

Questa tesi si occupa dell’estensione di un framework software finalizzato all'individuazione e al tracciamento di persone in una scena ripresa da telecamera stereoscopica. In primo luogo è rimossa la necessità di una calibrazione manuale offline del sistema sfruttando algoritmi che consentono di individuare, a partire da un fotogramma acquisito dalla camera, il piano su cui i soggetti tracciati si muovono. Inoltre, è introdotto un modulo software basato su deep learning con lo scopo di migliorare la precisione del tracciamento. Questo componente, che è in grado di individuare le teste presenti in un fotogramma, consente ridurre i dati analizzati al solo intorno della posizione effettiva di una persona, escludendo oggetti che l’algoritmo di tracciamento sarebbe portato a individuare come persone.

Bottom pressure time series study: the ANTARES deep sea observatory case

Questo elaborato riguarda l'analisi delle variazioni di pressione sul fondale del Mar Mediterraneo. Il primo obiettivo era quello di identificare la variabilità a basse frequenze della pressione sul fondo. I dati osservati sono stati raccolti presso l'osservatorio ANTARES che si trova 40 km al largo di Tolone e ricopre un'area di 180x180 m. Sono state analizzate tre serie temporali, L1, L3, L8, e da esse è stata ricostruita una serie temporale dall'1 gennaio 2009 al 31 dicembre 2013. Sono state applicate delle procedure di despiking, media su 30 minuti e gap-filling. Sono stati proposti due metodi di detiding, una media su tre giorni e il filtro di Doodson. Successivamente è stato eseguito un detrending. Un confronto tra l'analisi armonica e il filtro di Doodson mostra una similarità nei risultati. Per questa ragione, per continuare il lavoro, è stata utilizzata la serie a cui era stato tolto il trend e le maree tramite il filtro di Doodson. Togliere le maree ha reso possibile la rimozione dei segnali ad alta frequenza per potersi focalizzare sui segnali rimasti a bassa frequenza. Uno spettro sulla serie ha mostrato i segnali stagionali dominanti insieme alla cosiddetta Chandler wobble con una frequenza di 14 mesi.