Specification, execution and verification of interaction protocols: an approach based on computational logic

Interaction protocols establish how different computational entities can interact with each other. The interaction can be finalized to the exchange of data, as in 'communication protocols', or can be oriented to achieve some result, as in 'application protocols'. Moreover, with the increasing complexity of modern distributed systems, protocols are used also to control such a complexity, and to ensure that the system as a whole evolves with certain features. However, the extensive use of protocols has raised some issues, from the language for specifying them to the several verification aspects. Computational Logic provides models, languages and tools that can be effectively adopted to address such issues: its declarative nature can be exploited for a protocol specification language, while its operational counterpart can be used to reason upon such specifications. In this thesis we propose a proof-theoretic framework, called SCIFF, together with its extensions. SCIFF is based on Abductive Logic Programming, and provides a formal specification language with a clear declarative semantics (based on abduction). The operational counterpart is given by a proof procedure, that allows to reason upon the specifications and to test the conformance of given interactions w.r.t. a defined protocol. Moreover, by suitably adapting the SCIFF Framework, we propose solutions for addressing (1) the protocol properties verification (g-SCIFF Framework), and (2) the a-priori conformance verification of peers w.r.t. the given protocol (AlLoWS Framework). We introduce also an agent based architecture, the SCIFF Agent Platform, where the same protocol specification can be used to program and to ease the implementation task of the interacting peers.

Excitonic properties of transition metal oxide perovskites and workflow automatization of GW schemes

The Many-Body-Perturbation Theory approach is among the most successful theoretical frameworks for the study of excited state properties. It allows to describe the excitonic interactions, which play a fundamental role in the optical response of insulators and semiconductors. The first part of the thesis focuses on the study of the quasiparticle, optical and excitonic properties of \textit{bulk} Transition Metal Oxide (TMO) perovskites using a G$_0$W$_0$+Bethe Salpeter Equation (BSE) approach. A representative set of 14 compounds has been selected, including 3d, 4d and 5d perovskites. An approximation of the BSE scheme, based on an analytic diagonal expression for the inverse dielectric function, is used to compute the exciton binding energies and is carefully bench-marked against the standard BSE results. In 2019 an important breakthrough has been achieved with the synthesis of ultrathin SrTiO3 films down to the monolayer limit. This allows us to explore how the quasiparticle and optical properties of SrTiO3 evolve from the bulk to the two-dimensional limit. The electronic structure is computed with G0W0 approach: we prove that the inclusion of the off-diagonal self-energy terms is required to avoid non-physical band dispersions. The excitonic properties are investigated beyond the optical limit at finite momenta. Lastly a study of the under pressure optical response of the topological nodal line semimetal ZrSiS is presented, in conjunction with the experimental results from the group of Prof. Dr. Kuntscher of the Augsburg University. The second part of the thesis discusses the implementation of a workflow to automate G$_0$W$_0$ and BSE calculations with the VASP software. The workflow adopts a convergence scheme based on an explicit basis-extrapolation approach [J. Klimeš \textit{et al.}, Phys. Rev.B 90, 075125 (2014)] which allows to reduce the number of intermediate calculations required to reach convergence and to explicit estimate the error associated to the basis-set truncation.