On the Expressiveness of Spatial Constraint Systems
Sur l'expressivité des Systèmes de Contraintes Spatiales
Résumé
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 declarative 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 algebraic 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.
Les comportement épistémiques, mobiles et spatiaux sont omniprésent dans les systèmes distribués d’aujourd’hui. La nature
épistémique intrinsèque de ces types de systèmes, provient des interactions des éléments qui en font parties. La plupart des gens sont
familiarisés avec les systèmes numériques où les utilisateurs partagent leurs croyances, opinions et même des mensonges intentionnels (des canulars). Les modèles de ces systèmes doivent prendre en compte des interactions avec les autres ainsi que leurs qualité distribuée. Les comportements spatiaux et mobiles sont exposées par des applications et des données qui se déplaçant à travers des espaces (éventuellement imbriqués) définis par, par example, des cercles d’amis, des groupes et des dossiers communs. Nous croyons donc qu’une solide compréhension de la notion d’espace et mobilité spatial ainsi que le flux d’information épistémique est pertinente dans de nombreux modèles de systèmes distribués d’aujourd’hui.
Afin d’analyser la connaissance, l’espace et la mobilité dans les systèmes distribués, nous élargissons sur la théorie mathématique-
ment simple et élégante des systèmes de contraintes (sc), utilisée pour représenter l’information et le changement d’information dans
les systèmes concurrents. Dans le modèle déclaratif formel connu sous le nom de programmation concurrent par contraintes, les systèmes de contraintes fournissent les domaines de base et les opérations pour les fondements sémantiques de ce modèle. Les systèmes des contraintes spatiales (scs) sont des structures algébriques qui étendent les sc pour
le raisonnement sur les comportement spatiaux et épistémiques de base tels que la croyance et l’extrusion. Les affirmations spatiales
et épistémiques peuvent être considérées comme des modalités spécifiques. D’autres modalités peuvent être utilisées pour les assertions concernant le temps, les connaissances et même pour l’analyse des groupes parmi d’autres concepts utilisés dans la spécification et la vérification des systèmes concurrents.
Dans cette thèse nous étudions l’expressivité des systèmes de contraintes spatiales dans la perspective plus large du comportement modal et épistémique. Nous montrerons que les systèmes de contraintes spatiales sont suffisamment robustes pour capturer des
modalités inverses et pour obtenir de nouveaux résultats pour les logiques modales. Également, nous montrerons que nous pouvons
utiliser les scs pour exprimer un comportement épistémique fondamental comme connaissance. Enfin, nous allons donner une caractérisation algébrique de la notion de l’information distribuée au moyen de constructeurs sur scs.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...