By Damiano Macedonio
Università Ca’ Foscari di Venezia
January 2006
ABSTRACT
This Thesis studies logical characterisations of distributed systems for the purpose of de- scribing resources in heterogeneous environments. The focus is more on the structure and the distribution of resources than their behaviour. The research follows two complemen- tary strategies: a proof theoretical approach, not related to a particular formal model, and a model theoretical approach, deeply related to the choice of a formal model. The former consists in specialising a pure logical formalism to express properties in a distributed sys- tem; the latter consists in defining a new logic by considering a particular formalisation for distributed systems as a model, and by interpreting the logical constructs in such a model. To develop these two differing approaches, the Thesis is organised in two parts.
Part I introduces the ‘Logic’ from the basis by considering Basic Logic: a substruc- tural logic whose aim is to find a structure in the space of the logics. Classical, Intu- itionistic, and non-modal Linear logics are all obtained as extensions of Basic Logic in a uniform way. Basic Logic is taken as the fundament of a resource semantics, that is mod- ularly extended to Intuitionistic Linear Logic, Linear Logic and Bunched Implications Logic. This semantics, along with its extensions, is sound and complete, and provides a theorem of semantical cut-elimination.
By adding places, or locations, to a Modal Intuititionistic Logic we define a model that well describes distributed systems. The semantics provided for this modal logic is sound and complete, and can be further specialised to satisfy the finite model property, thus proving the decidability of the logic.
Part II introduces bigraphs, which are a graphical model of computation in which both locality and connectivity are prominent. Bigraphs are establishing themselves a truly general (meta)model of global systems, and appear to encompass several existing calculi and models. This part of the Thesis is devoted to the introduction of BiLog, a new con- textual and spatial logic based on bigraphs, that aims at achieving the same generality as a description language: as bigraphs specialise to particular models, we expect BiLog to specialise to powerful logics on these. In this sense we propose BiLog as a unifying lan- guage for the description of global resources, fortified by the positive preliminary results obtained by instantiating BiLog to well known spatial logics: Spatial Tree Logic, Spatial Graph Logic, Context Tree Logic, and a dynamic spatial logic for CCS. Another positive result in this direction has been obtained for semistructured data, by focusing on XML.