Michell Guzmán will defend his Ph.D thesis entitled "On the Expressiveness of Spatial Constraint Systems" on Tuesday September 26th at 3 p.m. in the Sophie Germain room at the Alan Turing building.
Abstract: Epistemic, mobile and spatial behaviour are commonplace in today’s distributed systems. The intrinsic epistemic nature of these systems arises from the interactions of the elements of which they are comprised. Most people are familiar with digital systems where users share their beliefs, opinions and even intentional lies (hoaxes). Models of such systems must take into account the interactions with others as well as the distributed quality presented by them. Spatial and mobile behaviour are exhibited by applications and data moving across possibly nested spaces defined by, for example, friend circles, groups, and shared folders. Thus a solid understanding of the notion of space and spatial mobility as well as the flow of epistemic information is relevant in many models of today’s distributed systems. In order to analyze knowledge, space, and mobility in distributed systems, we expand upon the mathematically simple and elegant theory of constraint systems (cs), used to represent information and information change in concurrent systems. In the formal declara- tive model known as concurrent constraint programming, constraint systems provide the basic domains and operations for the semantic foundations of this model. Spatial constraint systems (scs’s) are al- gebraic structures that extend cs’s for reasoning about basic spatial and epistemic behaviour such as belief and extrusion. Both, spatial and epistemic assertions, can be viewed as specific modalities. Other modalities can be used for assertions about time, knowledge and even the analysis of groups among other concepts used in the specification and verification of concurrent systems. In this thesis we study the expressiveness of spatial constraint systems in the broader perspective of modal and epistemic behaviour. We shall show that spatial constraint systems are sufficiently robust to capture inverse modalities and to derive new results for modal logics. We shall show that we can use scs’s to express a fundamental epistemic behaviour such as knowledge. Finally we shall give an algebraic characterization of the notion of distributed information by means of constructors over scs’s.