An experimental and theoretical approach to correct for the scattered radiation in an X-ray computer tomography system for industrial applications

The main problem connected to cone beam computed tomography (CT) systems for industrial applications employing 450 kV X-ray tubes is the high amount of scattered radiation which is added to the primary radiation (signal). This stray radiation leads to a significant degradation of the image quality. A better understanding of the scattering and methods to reduce its effects are therefore necessary to improve the image quality. Several studies have been carried out in the medical field at lower energies, whereas studies in industrial CT, especially for energies up to 450 kV, are lacking. Moreover, the studies reported in literature do not consider the scattered radiation generated by the CT system structure and the walls of the X-ray room (environmental scatter). In order to investigate the scattering on CT projections a GEANT4-based Monte Carlo (MC) model was developed. The model, which has been validated against experimental data, has enabled the calculation of the scattering including the environmental scatter, the optimization of an anti-scatter grid suitable for the CT system, and the optimization of the hardware components of the CT system. The investigation of multiple scattering in the CT projections showed that its contribution is 2.3 times the one of primary radiation for certain objects. The results of the environmental scatter showed that it is the major component of the scattering for aluminum box objects of front size 70 x 70 mm2 and that it strongly depends on the thickness of the object and therefore on the projection. For that reason, its correction is one of the key factors for achieving high quality images. The anti-scatter grid optimized by means of the developed MC model was found to reduce the scatter-toprimary ratio in the reconstructed images by 20 %. The object and environmental scatter calculated by means of the simulation were used to improve the scatter correction algorithm which could be patented by Empa. The results showed that the cupping effect in the corrected image is strongly reduced. The developed CT simulation is a powerful tool to optimize the design of the CT system and to evaluate the contribution of the scattered radiation to the image. Besides, it has offered a basis for a new scatter correction approach by which it has been possible to achieve images with the same spatial resolution as state-of-the-art well collimated fan-beam CT with a gain in the reconstruction time of a factor 10. This result has a high economic impact in non-destructive testing and evaluation, and reverse engineering.

I rapporti di collaborazione tra vettori

L’elaborato ha ad oggetto l’analisi delle possibili forme di collaborazione tra vettori nei diversi settori del trasporto, con particolare attenzione all’ambito aeronautico e marittimo. Negli ultimi decenni l’incremento del livello di concorrenza tra i competitors su scala planetaria, a seguito della progressiva liberalizzazione e globalizzazione dei trasporti, ha indotto i vettori ad adottare nuove strategie commerciali dirette alla condivisione del rischio, alla riduzione dei costi di esercizio, all’espansione delle proprie reti e alla flessibilizzazione dei processi interni di adeguamento alle continue espansioni e contrazioni del mercato. Hanno, così, fatto la loro comparsa modelli contrattuali nuovi che differiscono per struttura, livello di integrazione delle parti coinvolte e grado di complessità dell’accordo. Nell’elaborato, pertanto, sono state attentamente esaminate le molteplici figure giuridiche generate dalla prassi commerciale, come gli accordi di codesharing, interlining, wet lease, dry lease, franchising, le grandi alleanze strategiche presenti sia in ambito aeronautico, sia in quello marittimo, le Conferences e i Consorzi. La ricerca, in particolare, è focalizzata, alla luce della prassi contrattuale e della normativa nazionale, comunitaria ed internazionale vigente, sui problemi di qualificazione giuridica di tali accordi e, conseguentemente, sulla disciplina di volta in volta ad essi applicabile, sul loro oggetto, regolamento contrattuale e contenuto. Si è proceduto poi ad uno studio comparativo-contrastivo delle differenze tra le varie forme di partnership e all’approfondimento delle questioni concernenti la tutela degli utenti dei servizi di trasporto, siano essi passeggeri o mittenti. Sono affrontati, infatti, con accurata indagine i profili di responsabilità dei vettori coinvolti, sulla base del quadro normativo di riferimento. Nel corso della ricerca si è data anche particolare attenzione all’analisi della compatibilità degli accordi tra vettori con la disciplina comunitaria della concorrenza, registrando una tendenza della Comunità a piegare l’interpretazione delle norme in materia alle superiori esigenze dell’economia, in considerazione delle peculiarità del mercato del trasporto.

Certificates for Incremental Type Checking

The central topic of this thesis is the study of algorithms for type checking, both from the programming language and from the proof-theoretic point of view. A type checking algorithm takes a program or a proof, represented as a syntactical object, and checks its validity with respect to a specification or a statement. It is a central piece of compilers and proof assistants. We postulate that since type checkers are at the interface between proof theory and program theory, their study can let these two fields mutually enrich each other. We argue by two main instances: first, starting from the problem of proof reuse, we develop an incremental type checker; secondly, starting from a type checking program, we evidence a novel correspondence between natural deduction and the sequent calculus.