La notion de système de contraintes (cs -selon l'acronyme anglais) est un concept central aux formalismes de la théorie de la concurrence tels que les algèbres de processus pour la programmation concurrente par contraintes.

Les systèmes de contraintes sont souvent représentés par des treillis : ses éléments, appelées contraintes, représentent des informations partiales tandis que l'ordre du treillis correspond à des implications. Récemment, une notion appelée "système de contraintes spatiales à n-agents" a été développée pour représenter l'information dans la programmation concurrente par contraintes où les systèmes sont multi-agents et spatialement distribués. D'un point de vue informatique, un système de contraintes spatiales peut être utilisé pour spécifier l'information partiale contenue dans l'espace d'un certain agent (information locale). D'un point de vue épistémique, un cs spatial peut être utilisé pour représenter l'information qui est considérée vrai pour un certain agent (croyance). Les systèmes de contraintes spatiales, néanmoins, ne fournissent pas de mécanismes pour la spécification de la mobilité de l'information ou des processus d'un espace à un autre. La mobilité de l'information est un aspect fondamental des systèmes concurrents. Dans cette thèse nous avons développé la théorie des systèmes de contraintes spatiales avec des opérateurs pour spécifier le déplacement des informations et processus entre les espaces. Nous étudions les propriétés de cette nouvelle famille de systèmes de contraintes et nous illustrons ses applications. Du point de vue calculatoire, ces nouveaux opérateurs nous apportent de l'extrusion d'informations et/ou des processus, qui est un concept central dans les formalismes pour la communication mobile. Du point de vue épistémique, l'extrusion correspond à une notion que nous avons appelé énoni ciation ; une information qu'un agent souhaite communiquer à d'autres mais qui peut être inconsistante avec les croyances de l'agent même. Des énonciations peuvent donc être utilisées pour exprimer des notions épistémiques tels que les canulars ou les mensonges qui sont fréquemment utilisés dans les réseaux sociaux. Globalement, les systèmes de contraintes peuvent exprimer des notions épistémiques comme la croyance/énonciation et la connaissance en utilisant respectivement une paire de fonctions espace/extrusion qui représentent l'information locale, et un opérateur spatial dérivé qui représente l'information globale. Par ailleurs, nous montrons qu'en utilisant une construction précis de systèmes de contraintes, nous pouvons aussi représenter la notion du temps comme une imbrication des espaces qui représentent euxmême une séquence d'instances.

view a spatial constraint system can be used to specify partial information holding in a given agent's space (local information). From an epistemic point of view a spatial cs can be used to specify information that a given agent considers true (beliefs). Spatial constraint systems, however, do not provide a mechanism for specifying the mobility of information/processes from one space to another. Information mobility is a fundamental aspect of concurrent systems.

In this thesis we develop the theory of spatial constraint systems with operators to specify information and processes moving between spaces. We investigate the properties of this new family of constraint systems and illustrate their applications. From a computational point of view the new operators provide for process/information extrusion, a central concept in formalisms for mobile communication. From an epistemic point of view extrusion corresponds to what we shall call utterance; a piece of information that an agent communicates to others but that may be inconsistent with the agent's beliefs. Utterances can be used to express instances of epistemic notions such as hoaxes or intentional lies which are common place in social media.

iii On the whole, constraint systems can express the epistemic notions of belief /utterance and knowledge by means of respectively, a space/extrusion function pair that specifies local information and a derived spatial operator that specifies global information. We also show that, by using a specific construction of our constraint systems, we can encode the notion of time as an arbitrary nesting of spaces representing a sequence of instances. iv There is always a bittersweet taste when one writes acknowledgments. Just after starting a PhD, one sees its end in a very distant, fuzzy and dystopian way, when ending a PhD, one sees its beginning in a vivid, nostalgic and, as contrary as it may appear, utopian way. This is a testament that all these years dedicated to science can radically change your attitude, your perspective and your behaviors. Not only you learn how to write papers and research proposals, it is a social challenge that forces you to know yourself better, a mental test that teaches you how to get fortitude out of nothing.

And even if the world outside your lab minimizes this journey to either a list of publications or a two-page résumé de thèse when applying to a job out there in the jungle, none but you know its true cost. A bill that is passed with a total not in terms of time and money, but in terms (whether debited or credited) described in friendships, happiness, anxiety, obscurity, experiences, landscapes, family members, pictures, disappointments, expectations, and so on. All this whistle one is in this period of almost total quiescence in terms of finding a proper north. Nonetheless, as journeys are usually done with other travelers (at least during the time when their paths run in the same direction), this one was no exception and it is one's responsibility to mention these fellow adventurers. I would like to express here my gratitude to my mother Janeth, my father Yamil and my sister Faryde. These travelers, though far away, are still going in the same direction providing me with wisdom, love, and above all, unconditional support. I also wish to praise my soulmate Laura, a big part of my life and dreams and a big supporter of all my decisions. No less decisive, I want to acknowledge the importance of my supervisor Frank, the one responsible for this big opportunity and for passing onto me the secrets of science. I'm also indebted with Stefan and v Camilo for their supervision and big scientific advices. In these three years I made part of Comète, I couldn't ask for a better team and because of this I would like to thank Catuscia for her immense appreciation towards us, she makes every member of the team feel like he matters. Bibek, Michell, Luis, Yusuke, Marco, Ehab, Joris, Benjamin, Nico, Lili, and Kostas all were great teammates and colleagues. At the lab, I made the great acquaintance of Tomer Libal and his family, I wanna thank him for his friendship, chats and pizza evenings. I also thank professor Jean-Marc Steyaert with whom I chatted on the halls when staying late to work.

While I was living in France, I had the huge luck of meeting Guillaume Tirefort, one of those friends you don't cross paths with every day, I want to show my utmost appreciation for his friendship that I'm sure will last for many years more. I also wanna show my gratitude to the RPG group with its fun sessions and jokes; David, Alberto, Ben, Chiara, Enrico, Adam, Philippe, Nicolas, Spyros and Bethany. It is also vital that I acknowledge the friendship offered to me by Fereshteh Asgari, Vanessa Molina, Kaja Osiecka, Kamila Piotrowska, Fatima Jardali, Yu Chao and Mme. Traore; they are remarkable women I had the luck of meeting here and I will remember them for years to come. My longtime friend Francisco, who even with the time difference, had the time and disposition to always be there virtually and geek out. Though I didn't see them in the flesh, whenever I needed a laugh I could always count on Mat & Pat and JonTron.

All experiences in a journey do not necessarily come from people and, because I'm a great admirer of the 7th and 8th arts, I want to compile here a list of films and video-games that, during this three-year period, made an impact and/or gave comfort when solitude was the only option. Last but not remotely least, I would like to thank INRIA and the Government of France for completely funding my PhD. I will be forever indebted to the people of France. vii Chapter 1

Introduction

A sound, conscious, and thorough study about digital information is always a welcomed effort. In today's digital age, this intrinsic motivation is not freely granted by the apparent pervasiveness of the information revolution and its everincreasing scale. It is intrinsic because of the actual democratization of information, and freely granted due to the (virtually) zero cost now associated with its appropriation. Thus, it seems rather disparate that a work of scientific research attributes its motivation to a political/economical impetus based on people's epistemic relation with information and participation thereof. This I think, merits a philosophical introduction to an utterly scientific text.

The grasping of philosophical meanings is, more often than not, done by unearthing and analyzing ancient erudites. But with a phenomenon as modern as the information revolution, it is only fair to quote thinkers from our generation. And for this, I turn to a relatively niche film from 1995 called Ghost in the Shell, where our heroin Major Kusanagi is in a cat-and-mouse chase after an elusive hacker called The Puppet Master, purportedly capable of hacking even into human bodies. When they finally meet face-to-face and he is asked for the reasoning behind his actions, The Puppet Master utters the following snippet amid a long monologue:

"It can also be argued that DNA is nothing more than a program designed to preserve itself. Life has become more complex in the overwhelming sea of information. And life, 1 when organized into species, relies upon genes to be its memory system. So, man is an individual only because of his intangible memory... and memory cannot be defined, but it defines mankind. The advent of computers, and the subsequent accumulation of incalculable data has given rise to a new system of memory and thought parallel to your own. Humanity has underestimated the consequences of computerization."

Although subjective, it can be argued that in the context of the information revolution the individuality of man directly depends on his knowledge. However, in the above discourse one thing remains objective and undisputed and that is the underestimation of the information revolution. Even so, The Puppet Master (or the script writer for that matter) wisely avoids mentioning what the consequences of this revolution are. We need not venture much into the future, only six years laters when in 2001 the video game Metal Gear Solid 2: Sons of Liberty, known for its long and philosophical radio conversations between the main characters, dared to answer part of that question. In this 8th art [START_REF] Perchy | Can we finally agree on the 8th art? a technological approach[END_REF] opus we have our manly spy hero Solid Snake, trying to expose the existence of a secret state-of-the-art mobile bipedal nuclear tank. With the remote help of the geek, glass-wearing computer genius Otacon, they discuss at one point:

Otacon: When the photos are in, we'll put them online and blow this whole thing wide open on the Web. Snake: Don't you think that the authorities will just shut us down? Otacon: Probably. But it won't matter -there'll be mirror sites spawning within minutes after those images go up. We won't even have to ask; people will be grabbing the pictures. There's no way anyone can stop it. Information has a life of its own, and as long as it lasts, it'll keep existing -even if it has to change its form or location.

Snake: Life?

Otacon: Yeah -the desire of people to learn. The demand for data.

Snake: That's called idle curiosity in my book.

Otacon: Everyone's got some of that. And sometimes, it can pave the way for truth. That's what I believe.

Note that Otacon, apart from describing consequences of the information revolution, also ventures into moral judgements that are certainly outside the scope of any computer science text like this one. However, I (as author of this document) believe that this research thesis might provide men with mathematical and technological means for studying, and therefore gauging the consequences of this whole constant inertia of digital information (be it in its epistemic or doxastic direction). And what better motivation to do it than to stop people like The Puppet Master or to help scientists like Otacon.

Motivation

Epistemic, mobile and spatial behavior are common place in today's distributed systems. The intrinsic epistemic nature of these systems arises from social behavior. People are familiar with digital systems where users share their beliefs, opinions and even intentional lies (hoaxes). Also, systems modeling decision behavior must account for the partial dependance on the results of interacting with others within a social context. The courses of action stemming from some agent decision result not only from the rational analysis of a particular situation but also from the agent beliefs or information born from interactions with other participants involved in that situation. Appropriate performance in these social contexts requires the agent to form beliefs about the beliefs of others. Spatial and mobile behavior is exhibited by apps and data moving across (possibly nested) spaces defined by, for example, friend circles, groups, and shared folders. Thus we believe that a solid understanding of the notion of space and spatial mobility as well as the flow of epistemic information is relevant in any model of today's distributed systems.

Declarative formalisms of concurrency theory such as process calculi for concurrent constraint programming (ccp) [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] were designed to give explicit access to the concept of partial information and, as such, have close ties with logic [START_REF] Prakash Panangaden | A hyperdoctrinal view of concurrent constraint programming[END_REF][START_REF] Nax | A logical view of concurrent constraint programming[END_REF]. This makes them ideal for the incorporation of epis-temic and spatial concepts by expanding the logical connections to include multiagent modal logic [START_REF] Kripke | Semantical analysis of modal logic i normal modal propositional calculi[END_REF]. In fact, the sccp calculus [START_REF] Knight | Spatial and epistemic modalities in constraintbased process calculi[END_REF] extends ccp with the ability to define local computational spaces where agents can store epistemic information and run processes.

Problem: Spatial and Epistemic Mobility

Context

Despite being able to express meaningful epistemic and spatial phenomena such as belief, local and global information, the sccp calculus does not provide a mechanism to intentionally extrude information or processes from local spaces. Such a mechanism would allow sccp to express the transfer of epistemic information from one space into another.

The notion of constraint system (cs) is central to ccp and other declarative formalisms such as (concurrent) constraint logic programming (clp). All ccp calculi (including sccp) are parametric in a cs that specifies partial information upon which programs (processes) may act. A cs is often represented as a complete lattice (Con, ). The elements of Con, the constraints, represent partial information and we shall think of them as being assertions. The order , the join , the bottom true and the top false of the lattice correspond respectively to entailment, conjunction, the empty information and the join of all (possibly inconsistent) information.

Constraint systems provide the domains and operations upon which the semantic foundations of ccp calculi are built. As such, ccp operations and their logical counterparts typically have a corresponding elementary construct or operation on the elements of the constraint system. In particular, parallel composition and conjunction correspond to the join operation, and existential quantification and local variables correspond to a cylindrification operation on the set of constraints [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF].

Similarly, the notion of computational space and the epistemic notion of belief in sccp [START_REF] Knight | Spatial and epistemic modalities in constraintbased process calculi[END_REF] correspond to a family of functions [•] i : Con → Con on the elements of the constraint system Con. These functions are called space functions. From a computational point of view the assertion (constraint) [c] i specifies that c resides within the space of agent i. From an epistemic point of view, the assertion [c] i specifies that agent i considers c to be true (i.e. in the world of agent i assertion c is true). Both intuitions convey the idea of c being local (subjective) to agent i.

It is therefore natural to assume that a mechanism for extrusion in ccp ought to have a corresponding semantic concept in constraint systems. Furthermore, by incorporating extrusion directly in constraint systems, the concept may become available not only to sccp but also to other declarative constraint-based formalisms.

This Thesis: Algebraic Structures for Extrusion and Epistemic Reasoning

Our main goal is to investigate algebraic operations in constraint systems that help provide semantic foundations for extrusion and mobility of information. Systems where data moves across a given structure of information are now commonplace, and applications such as social networks, forums or any other that organizes its information in a defined hierarchy are among these systems. In practice, the nature of this information can be reviews, opinions, news, etc., which in turn belong to a certain entity, e.g. users, agents, applications. This relation of ownership can be conceptualized as space, and thus a clear understanding of information in spaces and its movement across them is pertinent to the study of these systems.

From a computational point of view, the new operations will allow us to specify mobile behavior as constraints. Consequently, this can help us model and analyze scenarios like process mobility and communicating agents and at the same time, detect potential offensive or intrusive behavior that may endanger the integrity or veracity of the information therein. Additionally, with a sound theory for mobility and multi-agent phenomena, we can enumerate important properties inherent to the systems and subsequently to all actors in them.

From a logical point of view, the operators will allow us to specify epistemic concepts such as opinions and intentional lies or even express properties regarding time. This way we can characterize well-stablished logical formalisms for epistemic behavior or time directives and reason about specifications made in them. As such, we are then able to describe the mobility of information as a concept inherent to a specific context like belief, knowledge, utterance, future or past. We believe that an algebraic characterization of all these concepts is a novel approach that will help analyse or prevent behavior that might be undesired in a specification.

Our Contributions

In this work we generalize the underlying theory of spatial constraint systems by adding extrusion functions to their structure. We show that spatial constraint systems provide for the specification of spatial mobility and epistemic concepts such as belief, utterance and lies. We shall also show that the spatial theory of sccp [START_REF] Knight | Spatial and epistemic modalities in constraintbased process calculi[END_REF], which captures belief, can also capture an epistemic notion of knowledge. This latter contribution is consistent with our goal of using algebraic spatial structures to capture epistemic behavior. Furthermore, we show that the concepts of future and past can be represented likewise by space and extrusion in order to express time properties.

Our main contributions can be summarized and structured as follows.

1. E xtrusion as the right inverse of space. We shall first introduce a family of functions ↑ i , called extrusion functions. Computationally, ↑ i can be used to intentionally extrude information from within a space [•] i . Epistemically, ↑ i can be used to express utterances by agent i. We shall put forward the notion of extrusion/utterance as the right inverse of space/belief. Under this interpretation we obtain

[c ↑ i e] i = [c] i e.
This equation illustrates the extrusion of e from the space of agent i and it is reminiscent of subjective mobility in the ambient calculus [START_REF] Cardelli | Mobile ambients[END_REF]. By building upon concepts of Heyting Algebra, we will illustrate meaningful spatial and epistemic behaviors. In particular, program mobility and intentional lies (hoaxes), i.e., utterance of statements by a given agent that are inconsistent with its beliefs.

T he Extrusion

Problem. We consider the following problem: Given a space function [•] i derive an extrusion (function) ↑ i for it. We will provide canonical constructions of extrusion for surjective space functions that satisfy limit conditions such as Scott-continuity. We shall also prove an impossibility result for the existence of join-preserving extrusion for surjective and Scottcontinuous space functions.

3. P roperties of Extrusion. We will also investigate distinctive properties of space and extrusion functions. We will show that space functions that admit extrusion are necessarily space consistent: [false] i = false. This corresponds to the Consistency Axiom of Epistemic (Doxastic) logic stating that no agent believes the false statement. We shall show that extrusion functions are order embeddings, and that injective spaces are order automorphisms (hence they preserve all limits). We shall also identify necessary and sufficient conditions under which space and extrusion form a Galois connection: namely a correspondence of the form

[c] i d ⇔ c ↑ i d.

4.

A logic of Belief and Utterance. As an application of the above-mentioned contributions we show how to derive extrusion for a previously-defined instance of spatial constraint systems, namely, Kripke spatial cs [START_REF] Knight | Spatial and epistemic modalities in constraintbased process calculi[END_REF].

We also derive the semantics for a logic of belief with reverse modalities by interpreting its formulae as elements in the Kripke spatial cs with extrusion. We can then show how to express instances of epistemic notions such as utterances and lies directly in the syntax of this logic. We conclude by showing that belief and utterance in this logic also form a Galois connection. Roughly speaking, this connection allows us to reduce the implication of belief from/to implication by utterance.

5. K nowledge in Terms of Global Space. We shall represent knowledge by using a derived spatial operation that expresses global information. The new representation is shown to obey the epistemic principles of the logic for knowledge S4. We also show a sound and complete spatial cs interpretation of S4 formulae. In previous work [START_REF] Knight | Spatial and epistemic modalities in constraintbased process calculi[END_REF] spatial constraint systems were required to satisfy additional properties in order to capture S4 knowledge. Namely, space functions had to be closure operators. Here we will show that S4 knowledge can be captured in spatial constraint systems without any further requirements.

6. E xpressing time properties. To apply our theory to different scenarios than those of epistemic interpretations, we take Linear Time Temporal Logic (LTL) [START_REF] Pnueli | The temporal logic of reactive and concurrent systems[END_REF] and characterize it using a special type of constraint system we call Time Constraint System. Here, we regard the future operator of LTL as the space function of the cs and proceed to derive two versions of the extrusion function. We show that one corresponds to the past operator of LTL and the other to a weak version which is regarded as a dual operator.

Publications

This manuscript is based on the following articles I have co-authored during my thesis:

-Michell Guzman, Stefan

Outline of this Work

After this introduction the document follows with Chapter 2 covering the necessary background on order theory to properly introduce constraint systems. This in turn allows to cover spatial constraint systems which are the main concept used in our theory of mobility in declarative programming. Chapter 3 defines extrusion functions as the main tool to represent mobility of information in a distributed system, it also introduces derived notions to increase the expressiveness of our paradigm. Moreover, the problem of deriving extrusion functions for pre-existing configurations of distributed systems is also considered, and in addition to this, different properties pertinent to the existence of extrusion functions in constraint systems are studied.

The rest of the thesis is dedicated to illustrate the use of our constraint systems for different scenarios where one can interpret mobility of information as a main contextual feature. After a brief background on modal logics, Chapter 4 introduces Kripke constraint systems which are central to modeling epistemic concepts in our structures. Subsequently, a logic of belief and utterance is specified and later characterized by a semantical interpretation using an extension to the Kripke constraint system. This extension is devised by identifying the proper structures to use for introducing extrusion functions as studied in the previous chapter. Chapter 5 provides a representation of knowledge in terms of a derived operator in the constraint systems that specifies global information. Later in the chapter, it is shown that this interpretation is complete with respect to the properties of S4 knowledge.

Finally, Chapter 6 is concerned with expressing time specification by using Time constraint systems. After defining this new type of constraint system, a fragment of Linear Temporal Logic is semantically characterized using its operators and furthermore, properties of the past and future operators of LTL are proved valid using the semantics. The thesis is brought to an end in Chapter 7 where concluding remarks and related work concerning the study and/or representation of epistemic and time concepts are given. Future work pertaining how all these related approaches can be encoded in our formalisms is also written out.

For convenience, we included an index table with the different notation symbols and definitions used throughout the document. Also, in Chapter 7 we provided a summary table of the relationship between constraint elements and operators and those from the different interpretation of space and extrusion.

Chapter 2

Background on Constraint Systems

In this chapter we cover constraint systems, the foundational work that we build upon in this thesis. A constraint system is an algebraic structure where its elements represent partial information. We provide some background on domain theory followed by the introduction of flat constraint systems. Afterwards, we define spatial constraint systems; an extension introducing the concepts of agent and space.

Order Theory

This section gives a general background on order theory and especially lattice theory. We describe in a terse manner the concepts used throughout this chapter, thus the reader is referred to [DP02, Bly06, GHK + 03, AJ94] for an in-depth introduction to these topics.

Posets and Maps

Definition 2.1.1 (Poset). Given a set of elements P and a binary relation on P , we define a partially ordered set (P, ) where for all a, b, c ∈ P we have; Example 2.1.1 (Powerset). Let S be any set. We construct a poset where the elements are all the subsets of S and the ordering relation is set inclusion, i.e.

(P(S), ⊆). Moreover, (P(S), ⊇) is also a poset.

A frequently used type of subset of elements in a poset is the directed set, its definition follows. Upward/downward directed sets are also referred to as just directed/filtered sets. We continue with some definitions for maps between posets.

Definition 2.1.3 (Maps). Let P and Q be posets. A map f :

P → Q is said to be: i. order-preserving (also called monotone) if a b in P implies f (a) f (b) in Q, ii. order-reflecting if f (a) f (b) in Q implies a b in P ,
iii. order-embedding if it is order-preserving and order-reflecting, iv. order-isomorphism if it is an order-embedding and surjective, v. self-map if P = Q.

Lastly, a particular correspondence in order theory between two maps on posets is that of a galois connection. Definition 2.1.4 (Galois connection). Given two posets (P, ) and (Q, ) and two maps f : P → Q and g : Q → P , the pair (f, g) form a [monotone] Galois connection if for all a ∈ P and b ∈ Q we have;

f (a) b iff a g(b).

Lattices

Before introducing lattices, it is necessary to define the concept of bounds.

Definition 2.1.5 (Bounds). An element c ∈ P is said to be an upper bound (resp. lower bound) of subset S in poset (P, ) if for all a ∈ S we have that a c (resp.

c a).

We name the sets of all possible lower and upper bounds as S l and S u respectively. They can be calculated as follows:

S l = {c ∈ P | (∀a ∈ S) a c}
(2.1.1)

S u = {c ∈ P | (∀a ∈ S) a c} (2.1.2)
We call the minimal element of S u the least upper bound (lub) of S and the maximal element of S l the greatest lower bound (glb) of S. When they exist, these two elements are unique because is antisymmetric (see Definition 2.1.1).

The least upper bound (lub) is also sometimes referred to as supremum or join and the greatest lower bound (glb) is also referred to as infimum or meet.

Notation 2.1.1. We shall write S and S to denote the join and the meet of the set S respectively. Alternatively, we write c d and c d to denote the lub and glb of the set {c, d} respectively.

We now continue with the definition of a lattice. Definition 2.1.6 (Lattice). Let L = (P, ) be a poset where c d and c d exist for all c, d ∈ P , then L is also called a Lattice.

A lattice L can also be seen as an algebraic structure with operations for calculating bounds, i.e. L = (P, , , ). We proceed to introduce special important types of lattices.

Definition 2.1.7 (Complete lattice). A lattice L is a Complete Lattice if S and S exist for every subset S of the elements of the L.

Remark 2.1.1. If a lattice L is complete, by definition there exist elements = S and ⊥ = S when S is the set of all elements or the empty set. These two elements are called top (or global supremum) and bottom (or global infimum) respectively. They are usually specified when denoting the lattice as an algebraic structure, i.e. L = (P, , , , , ⊥).

Example 2.1.2. Let us consider again Figure 2.1. We calculate 2 u = {3, 4, 5} and 1 u = {3, 5}, therefore {1, 2} u = {3, 5} and 1 2 = 3 because 3 5. In the same way we can calculate 3 4 = 2. Let S be the set of all elements of the lattice, then S = 5 = and S = 0 = ⊥ Example 2.1.3 (Powerset lattice). Let S be any set. We construct the powerset lattice of S as L = (P(S), ⊆, ∪, ∩, ∅, S). Moreover, L = (P(S), ⊇, ∩, ∪, S, ∅) is called the reverse powerset lattice of S.

Both L and L in Example 2.1.3 are complete lattices. Some important properties of the join and meet operators need to be introduced. We characterize the elements of a lattice that capture the notion of finiteness.

Definition 2.1.8 (Compact elements). Given a lattice L and an element k ∈ L, we say that k is compact if for every subset S of L k S implies k T for some finite T ⊆ S.

The set of compact elements of a lattice L is denoted by K(L).

Example 2.1.4. Let L be the powerset lattice of S, the set K(L) are all the finite subsets of S. Moreover, let L be a reverse power lattice of S, the set K(L) are all the co-finite subsets of S. Recall that a set P is cofinite if its complement is finite (i.e. P \S is finite).

Definition 2.1.9 (Algebraic lattice). A complete lattice L is said to be algebraic if for each c ∈ L we have;

c = { k ∈ K(L) | k c }.
Intuitively, an algebraic lattice is a lattice where each element can be approximated by the finite elements below it. It can easily be shown that lattices in Example 2.1.3 are algebraic. We continue with yet another important type of lattice.

Definition 2.1.10 (Distributive lattice). A lattice L is said to be distributive if for every a, b, c ∈ L we have;

a (b c) = (a b) (a c)
Checking distributivity can be cumbersome, specially when there is a significant number of elements in the lattice. We describe another way for verifying this property.

2.1.2 (M 3 -N 5 theorem). A lattice L is non-distributive if and only if M 3 L or N 5 L.
Proof. See [START_REF] Brian | Introduction to lattices and order[END_REF].

Lastly, another significant type of lattice is that of a frame, also called a complete Heyting Algebra (cHa).

Definition 2.1.12 (Frame). A lattice L is a frame if it is complete and it satisfies the next equation:

c S = {c s | s ∈ S} (2.1.3)
By definition, a frame is also a distributive lattice (Definition 2.1.10). We finish our exposition of lattices with a mathematical structure that serves as a semantic interpretation of boolean logics.

Definition 2.1.13 (Boolean algebra). A boolean algebra is a structure (B, ∧, ∨, , 0, 1) where: i. (B, ∧, ∨, 0, 1) is a distributive lattice, ii. a ∧ 1 = a and a ∨ 0 = a for all a ∈ B, iii. a ∧ a = 0 and a ∨ a = 1 for all a ∈ B.

Example 2.1.5. The powerset lattice of a set S of elements can form a boolean algebra where B = S, ∧ = ∪, ∨ = ∩, = S\•, 0 = ∅, 1 = S. Moreover, the reverse power lattice of S forms the boolean algebra (S, ∩, ∪, S\•, 0 = S, 1 = ∅).

An important property of maps with respect to the calculation of bounds is completeness. We formalize this concept as follows.

Definition 2.1.14. Given two lattices L and L , a set S ∈ L and a map f : L → L we say:

i. if f ( S) = f (S) then; a. f is [upward]-continuous (or Scott-continuous) if S is directed (see Def. 2.1.2), b. f is join-complete if S is any set. ii. if f ( S) = f (S) then; a. f is downward-continuous, b. f if meet-complete if S is any set.

Constraint Systems

We proceed to explain the notion of flat constraint system and the more recent notion of spatial constraint system [START_REF] Knight | Spatial and epistemic modalities in constraintbased process calculi[END_REF]. Following [START_REF] Boer | Nondeterminism and infinite computations in constraint programming[END_REF] we formalize constraint systems as complete algebraic lattices (an alternative syntactic characterization of cs, akin to Scott information systems, is given in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF][START_REF] Prakash Panangaden | A hyperdoctrinal view of concurrent constraint programming[END_REF]).

The elements of the lattice, the constraints, represent (partial) information. A constraint c can be viewed as an assertion (or a proposition). The lattice order is meant to capture entailment of information: c d, alternatively written d c, means that the assertion d represents at least as much information as c. Thus we may think of c d as saying that d entails c or that c can be derived from d. The least upper bound (lub) operator represents join of information; c d, the least element in the underlying lattice above c and d. Thus c d can be seen as an assertion stating that both c and d hold. The top element represents the lub of all, possibly inconsistent, information, hence it is referred to as false. The bottom element true represents the empty information. Definition 2.2.1 (Constraint Systems [START_REF] Boer | Nondeterminism and infinite computations in constraint programming[END_REF]). A constraint system (cs) C is a complete algebraic lattice (Con, ). The elements of Con are called constraints.

The symbols , true and false will be used to denote the least upper bound (lub) operation, the bottom, and the top element of C, respectively.

The lattice representation of information in constraint systems is reminiscent of the algebraic presentation of geometric logic [START_REF] Vickers | Topology via logic[END_REF]. Next, we describe two typical concrete constraint systems.

Example 2.2.1 (Herbrand Constraint System [START_REF] Boer | Nondeterminism and infinite computations in constraint programming[END_REF][START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]). The Herbrand cs captures syntactic equality between terms t, t , . . . built from a first-order alphabet L with variables x, y, . . ., function symbols, and equality =. The constraints are (equivalent classes of ) sets of equalities over the terms of L: E.g., {x = t, y = t} is a constraint. The relation c d holds if the equalities in c follow from those in d: E.g., {x = y} {x = t, y = t}. The constraint false is the set of all term equalities in L and true is (the equivalence class of ) the empty set. The compact elements are the (equivalence class of ) finite sets of equalities. The lub is the (equivalence class of ) set union. Figure 2.3 is the hasse diagram of a Herbrand cs with variables {x, y} and constants {a, b} with a = b.

In the above example constraints are represented as sets of equations and thus the join (lub) of constraints corresponds to the equivalence class of the union of their equations. We can also view a constraint c as a representation of a set of variable assignments [ABP + 11]. For instance a constraint x > 42 can be thought of as the set of assignments mapping x to a value greater than 42; i.e., the solutions to (or models of) x > 42. In this case the join of constraints naturally corresponds to the intersection of their assignments, false as the empty set of assignments, and true as the set of all assignments.

Example 2.2.2 (Boolean Constraint System [ABP + 11]). Let Φ be a set of primitive propositions. A boolean (or truth) assignment π over Φ is a total map from Φ to the set {0, 1}. We use A(Φ) to denote the set of all such boolean assignments. We can now define the boolean cs B(Φ) as (P(A(Φ)), ⊇): The powerset of assignments ordered by ⊇. Thus constraints in Con are sets of assignments, is ⊇, false is ∅, true is A(Φ), the join operator is ∩, and the meet operator is

∪. A constraint c in B(Φ) is compact iff A(Φ) \ c is a finite set.
Notice that logic propositions can be straightforwardly interpreted as constraints in B(Φ). Let L 0 (Φ) be the propositional language built from Φ by the grammar φ, ψ, . . .

:= p | φ ∧ ψ | ¬φ (2.2.1)
where p ∈ Φ. We shall use the classical abbreviations φ ∨ ψ for ¬(¬φ ∧ ¬ψ), φ ⇒ ψ for ¬φ ∨ ψ, F for p ∧ ¬p, and T for ¬F. A boolean assignment π satisfies φ iff π |= φ where |= is defined inductively as follows:

π |= p iff π(p) = 1, π |= φ ∧ ψ iff π |= φ
and π |= ψ, and π |= ¬φ iff π |= φ. We interpret each formula φ as the constraint Other typical examples include constraint system for streams (the Kahn cs), rational intervals, and first-order theories [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF].

B φ def = {π ∈ A(Φ) | π |= φ} in B(Φ). Clearly B φ B ψ holds iff ψ ⇒ φ is valid, i.

Spatial Constraint Systems

The authors of [START_REF] Knight | Spatial and epistemic modalities in constraintbased process calculi[END_REF] extended the notion of cs to account for distributed and multi-agent scenarios where agents have their own space for their local information and performing their computations.

Locality and Nested Spaces

Intuitively, each agent i has a space function [•] i from constraints to constraints. Recall that constraints can be viewed as assertions. We can then think of

[c] i (2.2.2)
as an assertion stating that c is a piece of information that resides within a space attributed to agent i. An alternative epistemic interpretation of [c] i is an assertion stating that agent i believes c or that c holds within the space of agent i (but it may or may not hold elsewhere). Both interpretations convey the idea that c is local to agent i.

Following the above intuition, the assertion

[[c] j ] i (2.2.3)
is a hierarchical spatial specification stating that c holds within the local space the agent i attributes to agent j. Nesting of spaces such as in [[. . . [c] im . . .] i 2 ] i 1 can be of any depth.

Parallel Spaces

We can think of a constraint of the form

[c] i [d] j (2.2.4)
as an assertion specifying that c and d hold within two parallel/neighboring spaces that belong to agents i and j, respectively. From a computational/ concurrency point of view, we think of as parallel composition. As mentioned before, from a logic point of view the join of information corresponds to conjunction.

We can combine the above parallel and hierarchical specifications to express more complex spatially distributed multi-agent systems. Consider for example

[a [b] i [c] j ] i [d] j
where agent i has a space within his own space, and agent j has two spaces one in parallel with the outer space of agent i, and other inside it.

An n-agent spatial constraint system (n-scs) is a cs parametric in n self-maps

[•] 1 , . . . , [•] n capturing the above intuitions. Definition 2.2.2 (Spatial Constraint System [KPPV12]
). An n-agent spatial con-

straint system (n-scs) C is a cs (Con, ) equipped with n self-maps [•] 1 , . . . , [•] n over its set of constraints Con such that for each function [•] i : Con → Con: S.1 [true] i = true, and S.2 [c d] i = [c] i [d] i for each c, d ∈ Con.
Henceforth, given an n-scs C, we refer to each [•] i as the space (or space function) of the agent i in C. We use

(Con, , [•] 1 , . . . , [•] n ) to denote the corresponding n-scs with space functions [•] 1 , . . . , [•] n .
We shall often omit components of an n-scs tuple when they are unnecessary or clear from the context. We shall simply write scs when n is unimportant.

We now give some intuition about the space properties. Property S.1 in Definition 2.2.2 requires space functions to be strict maps (i.e bottom preserving). Intuitively, it states that having an empty local space amounts to nothing. Property S.2 states that space functions preserve (finite) lubs and it allows us to join and distribute the local information of agent i.

Remark 2.2.2 (Monotone Spaces). Notice that S.2 implies that space function are order-preserving (or monotone

): i.e., if c d then [c] i [d] i . Intuitively, if
c can be derived from d then any agent i should be able to derive c from d within its own space.

Proof. Assume c d, thus d = c d. Then [d] i = [c d] i . Using S.2 we have [d] i = [c] i [d] i , hence [c] i [d] i .

Shared and Global Information

Some noteworthy derived spatial constructions are shared-spaces and globality.

Definition 2.2.3 (Global Information). Let C be an n-scs with space functions

[•] 1 , . . . , [•] n and G be a non-empty subset of {1, . . . , n}. Group-spaces [•] G and global information [[[•]]] G of G in C are defined as: [c] G def = i∈G [c] i and [[[c]]] G def = ∞ j=0 [c] j G (2.2.5)
where

[c] 0 G def = c and [c] k+1 G def = [[c] k G ] G . The constraint [c] G means that c holds in the spaces of agents in G. The constraint [[[c]]] G entails [[. . . [c] im . . .] i 2 ] i 1 for any i 1 , i 2 , . . . , i m ∈ G.
Thus it realizes the intuition that c holds globally wrt G: c holds in each nested space involving only the agents in G.

In particular if G is the set of all agents, [[[c]]] G means that c holds everywhere. From the epistemic point of view [[[c]]] G is related to the notion of common-knowledge of c [FHMV95].

Summary

We gave a terse introduction to lattices, the main stepping stone from order theory we are going to use throughout the thesis. We introduced various types of lattices, their properties, maps between them and proceeded to define constraint systems as complete algebraic lattices representing partial information. More indepth texts on these subjects are [START_REF] Brian | Introduction to lattices and order[END_REF][START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF].

Spatial constraint systems, an important structure from which our worked is based are also introduced here. The next chapter we introduce the concept of extrusion w.r.t. space in constraint systems, we again use maps between lattices as the mathematical concept to achieve this.

Chapter 3 Spatial Constraint Systems with Extrusion

We shall now introduce a new notion, that of spatial constraint systems with extrusion (scse) and use it to specify simple examples of mobile and epistemic behavior. We also investigate the problem of extending any given arbitrary spatial constraint system to a scse. We will then state some distinctive properties of space and extrusion as well as correspondences between these two concepts that will be used throughout the following chapters.

Extrusion as the right inverse of Space

In spatially distributed systems an agent can transfer information from its space to the outside. We shall refer to this kind of transmission as extrusion. The extruded information is posted outside, possibly addressed to some other agent. Our epistemic view of extrusion is what we shall call utterance. An agent may utter information which will then be available to others. The uttered information may be inconsistent with the agent's own beliefs, in particular it could be a lie.

Let us now extend spatial constraint systems with extrusion. First recall that given a function f : X → Y , we say that g : Y → X is a right inverse (or section) of f iff f (g(y)) = y for every y ∈ Y . Similarly, given g : Y → X we say that

f : X → Y is a left inverse (or retraction) of g iff f (g(y)) = y for every y ∈ Y.
We shall equip each agent i with an extrusion function ↑ i : Con → Con. Intuitively, within a space context [•] i , the assertion ↑ i c specifies that c must be posted outside of (or extruded from) agent i s space. This will be captured by requiring the extrusion property:

E.1: [ ↑ i c ] i = c. (3.1.1)
In other words, we view extrusion/utterance as the right inverse of space/belief (and thus space/belief as the left inverse of extrusion/utterance).

A spatial constraint systems with extrusion (scse) is an scs with right inverses for each one of its space functions. Definition 3.1.1 (Spatial Constraint System with Extrusion). An n-agent spa-

tial constraint system with extrusion (n-scse) C is an n-scs (Con, , [•] 1 , . . . , [•] n ) equipped with n self-maps ↑ 1 , . . . , ↑ n over Con such that ↑ i is a right inverse of [•] i . More precisely, each self-map ↑ i of C satisfies the following condition: E.1 [ ↑ i c ] i = c for every c ∈ Con.
Henceforward we shall refer to each ↑ i as the extrusion function of agent i in C. We use (Con, ,

[•] 1 , . . . , [•] n , ↑ 1 , . . . , ↑ n ) to denote the corresponding n-scs (Con, , [•] 1 , . . . , [•] n ) with extrusion functions ↑ 1 , . . . , ↑ n .
We shall study additional properties (i.e., axioms) for extrusion in Section 3.4. In the next chapter we show that E.1 already allows us to specify meaningful spatial and epistemic behavior.

Derived Notions and Applications

We now introduce some derived general constructs to illustrate the expressiveness of extrusion. First, we need a general notion of implication.

Heyting Implication

In Remark 2.2.1 (Section 2.2), we discussed an interpretation of implication that works for the Boolean cs. We can define a general form of implication by adapting the corresponding notion from Heyting Algebras [START_REF] Vickers | Topology via logic[END_REF] to constraint systems. The above construction corresponds to (intuitionistic) implication in lattices that are frames (see Definition 2.1.12) [START_REF] Vickers | Topology via logic[END_REF].

Intuitively, a

Remark 3.2.1. The Boolean constraint system (Example 2.2.2) is a frame since meets are unions and joins are intersections so the distributive requirement is satisfied. Furthermore, for cs's of the form (P(U ), ⊇), as e.g., B(Φ) , the operators → and ∼ are known to coincide with the constructions ⇒ and ¬ defined in Remark 2.2.1, since boolean implication and boolean negation are particular cases of Heyting implication and Heyting negation [START_REF] Vickers | Topology via logic[END_REF].

A typical example of a standard constraint system that is not a frame is Herbrand's. To see this consider the Herbrand constraint system in Figure 2 Another basic but important property of the Heyting implication is its direct link to the ordering relation of the constraint system, we formalize it in the next lemma.

Lemma 3.2.2. Suppose that (Con, ) is a frame. For every c, d we the following is true:

c → d = true iff c d Proof.
We Heyting implication can be used in combination with our spatial constructions to specify meaningful computational and social behavior.

Remark 3.2.2. For the applications examples in this chapter, we fix an scse

(Con, , [•] 1 , . . . , [•] n , ↑ 1 , . . . , ↑ n ).
Furthermore we assume (Con, ) is a frame.

Lying Agents

A lie is not necessarily a false statement but rather a statement that deviates from what its author actually knows, believes or holds to be true [START_REF] Van Ditmarsch | On the logic of lying. In Games, actions and social software[END_REF]. Instances of this concept can be realized in our setting by thinking of an (intentional) lie or hoax as the uttering/extrusion of a statement by an agent which is inconsistent with what he or she believes to be true. We can use the spatial axiom S.2 (Definition 2.2.2) followed by the extrusion axiom E.1 (Definition 3.1.1) to obtain the following derivation of [c] i d.

[c

↑ i d] i = [c] i [↑ i d] i (S.2) = [c] i d (E.1)
The transformation from Equation 3.2.3 to [c] i d with c d = false illustrates the extrusion of (the lie) d by agent i.

Communicating Agents

Let us now illustrate hoaxes and communication between agents via extrusion.

Recall that we think of [c] i

[d] j as an assertion saying that c and d hold within two parallel spaces that belong to agents i and j, respectively. Example 3.2.2 (Communication). Let us suppose that we have an agent j who would utter d if she thought ∼ c was true. This behavior of agent j can be specified as

[∼ c → ↑ j d] j .
(3.2.4) Furthermore, suppose that we have an agent i who considers c to be true and yet he wishes to communicate the opposite to agent j. The behavior of agent i can be expressed as

[c ↑ i [∼ c] j ] i . (3.2.5)
Notice that the constraint to be extruded from the space of agent i, i.e., [∼ c] j , can be viewed as a message ∼ c addressed to agent j.

The expected result, if i communicates his hoax ∼ c to j, is that d gets posted to the outermost position. The communication should take place if the agents' spaces are placed in parallel. In fact we put together Equations 3.2.4 and 3.2.5, we derive the expected result.

[∼ c → ↑ j d] j [c ↑ i [∼ c] j ] i = [∼ c → ↑ j d] j [c] i [↑ i [∼ c] j ] i (S.2 on [•] i ) = [∼ c → ↑ j d] j [c] i [ ∼ c] j (E.1 on [•] i ) = [∼ c ∼ c → ↑ j d] j [c] i (S.2 on [•] j ) = [∼ c ↑ j d] j [c] i (Lemma 3.2.1) = d [∼ c] j [c] i (E.1 on [•] j )

Process Mobility

From a declarative programming point of view the construct c → d can be seen as a program/computational process that produces d if the guard c holds true. We can then combine this construct with our extrusion to express meaningful mobile behavior of programs.

Example 3.2.3 (Mobility). Let us consider the following assertion:

[e ↑ i (c → [d] i )] i . ( 3
↑ i (c → [d] i )] i as follows: c [e ↑ i (c → [d] i )] i = c [e] i [↑ i (c → [d] i )] i (S.2) = c [e] i c → [d] i (E.1) = c [e] i [d] i (Lemma 3.2.1) = c [e d] i (S.
2)

The step corresponding to E.1 shows the extrusion of the process c → [d] i . For a more involved example of extrusion of implication processes consider

[e ↑ i [c → ↑ j [d] i ] j ] i (3.2.7)
Intuitively, the implication process c → ↑ j [d] i is sent from within the space of i to a parallel space that belongs to j. Then if c holds in that parallel space, [d] i is extruded from [•] j and thus d is placed in the space of i from where the implication process was sent.

In fact, after multiple applications of E.1, S.2 and Lemma 3.2.1 we obtain the following:

[e ↑ i [c → ↑ j [d] i ] j ] i [c] j [e d] i . (3.2.8)
(We use instead of = to omit some non essential information that would join

[e d] i .) Notice that c → ↑ j [d] i
above can be seen as an intrusive process wrt agent j since it reports to agent i if c holds in [•] j .

Outermost Extrusion

We now derive constructions that can be used to specify extrusion to the outermost position in arbitrary nested spaces. Definition 3.2.2 (Global Extrusion). Let C be an n-scse with extrusion functions ↑ 1 , . . . , ↑ n and G be a non-empty subset of {1, . . . , n}. Group-extrusion ↑ G and global extrusion ⇑ G of G in C are defined as:

↑ G c def = i∈G ↑ i c and ⇑ G c def = ∞ j=0 ↑ j G c (3.2.9) where ↑ 0 G c def = c and ↑ k+1 G c def = ↑ G ↑ k G c.
Recall the notion of shared space in Definition 2.2.3. The group extrusion ↑ G c extrudes c from any space or shared-space of the agents in G. In fact, for any G,

[↑ G c] G c and [↑ G c] j c for any j ∈ G.
Global extrusion ⇑ G c can pull c into the outermost position regardless of the nesting depth (of spaces involving the agents in G). One can verify that

[[. . . [⇑ G c . . .] im . . .] i 2 ] i 1 c for every i 1 , i 2 , . . . , i m ∈ G.

Spatial Safety

We conclude this section by combining all our previously derived constructions to specify the extrusion of d to the outermost position if c is present somewhere in a given constraint e with arbitrary nested spaces (e.g. e

= [[a] j ] i [[c] i ] j ).
If c represents an undesired event in e then d can be used as a witness of its presence.

Example 3.2.4 (Spatial Search). Suppose that G is the set of all agents. The assertion c → ⇑ G d specifies that d will be extruded to the outermost position if c holds. We can use the global space construction

[[[c → ⇑ G d]]] G in Definition 2.2.3 to specify that c → ⇑ G d is everywhere.
We can verify that for any spatial constraint e where c holds somewhere, i.e., for any e such that e [[. . . [c] im . . .] i 2 ] i 1 (3.2.10)

for some i 1 , i 2 , . . . , i m ∈ G, we have e [[[c → ⇑ G d]]] G d.
(3.2.11)

Limit Preservation

In the following sections we will often refer to preservation of some limits by space functions. Let C be an scs with constraints Con.

A space function [•] i of C preserves the supremum of a set S ⊆ Con iff [ S] i = {[c] i | c ∈ S}.
The preservation of the infimum of a set is defined analogously. Notice that S.2 and the associativity of imply that the space functions preserve the lub of any finite subset of Con. Recall (by Definition 2.1.14) that a space function that preserves the supremum/infimum of any arbitrary subset of Con is said to be join-complete/meet-complete. Also recall that a space function in C is continuous/downward continuous if it preserves the supremum/infimum of any directed set/filtered set.

The join-completeness of space functions trivially implies their (Scott) continuity, a central concept in domain theory. From S.2 and the fact that constraint systems are complete lattices, the reverse implication is also true: Space continuity implies space completeness.

Proposition 3.3.1. Let [•] i be a space function of an scs. If [•] i is continuous then [•] i is join-complete.
Proof. The above proposition follows from the fact that any function from a poset in which every non-empty finite supremum exists preserves arbitrary suprema if and only if it preserves both directed suprema and finite suprema [GHK + 03].

The Extrusion Problem

Given an scs a legitimate question is whether it can be extended to an scse. In this section we would like to identify conditions that guarantee the existence of extrusion functions ↑ 1 , . . . , ↑ n for spaces [•] 1 , . . . , [•] n of any given n-scs.

From set theory we know that there is an extrusion function (i.e., a right inverse)

↑ i for [•] i iff [•] i is surjective. Recall that the fiber of y ∈ Y , or pre-image of the singleton {y}, under f : X → Y is the set f -1 (y) = {x ∈ X | y = f (x)}.
Thus the extrusion ↑ i can be defined as a function, called choice function, that maps each element c to some element from the (non-empty because of surjectivity) fiber of c under [•] i . The existence of this choice function assumes, however, the Axiom of Choice.

Nevertheless, we are interested in an explicit construction for extrusion. This is possible for continuous space functions due to the following lemma stating that the fibers of space functions are directed sets. In fact, we can prove the lemma by showing something stronger: fibers are closed under finite joins. Proof. We prove that fibers are closed under finite joins. This trivially implies the lemma. Suppose a and b are in the fiber

[c] -1 i , that is [a] i = [b] i = c. We need to prove that a b ∈ [c] -1 i . Using S.2 we have [a b] i = [a] i [b] i = c c = c. Thus a b ∈ [c] -1 i .
The following theorem, an immediate consequence of Lemma 3.4.1 and space continuity, identifies a sufficient condition to construct an extrusion function for the space [•] i as the map that takes every c to the maximum of the fiber of c under

[•] i .
Theorem 3.4.1 (Max Extrusion). Let C be an scs and let [•] i be a surjective and continuous space function of C.

Then ↑ i : c → [c] -1 i is a right inverse of [•] i . Proof. It follows from Lemma 3.4.1 that [c] -1 i is a directed set, thus because of continuity of the space function [↑ i c] i = [ [c] -1 i ] i = {[d] i | d ∈ [c] -1 i } = {c} = c.
It follows from the above theorem that any scs can be extended to scse if its space functions are continuous and surjective.

Local/Subjective Distribution

Notice that unlike space functions, extrusion functions are not required to preserve bottoms or binary lubs, i.e., they are not required to distribute over finite joins. In fact, the construction ↑ i : c → [c] -1 i in Theorem 3.4.1 may result in ↑ i true = true for some scs's. To better illustrate this situation, consider the following example.

Example 3.4.1. Let Con = N ∪ {∞} and let be the standard linear-order over

N ∪ {∞}. Let [∞] 1 = ∞ and [n] 1 = n/
3 be a continuous and surjective space function. The tuple (Con, , [•] 1 ) is an scs with true = 0. We can apply Theorem 3.4.1 to obtain the extrusion function

↑ 1 : c → [c] -1 1 for c ∈ Con. Notice, however ↑ 1 0 = [0] -1 1 = {0, 1, 2} = 2 = 0.
From a spatial point of view, however, any extrusion function ↑ i distributes over finite joins if it is within a space [•] i ; and from the epistemic point of view

↑ i distributes
2. ↑ i (c d) ≈ i ↑ i c ↑ i d for each c, d ∈ Con.
Proof.

First we prove ↑ i true ≈ i true.

[↑ i true] i = true (E.1) [↑ i true] i = [true] i (S.1) ↑ i true ≈ i true We now prove ↑ i (c d) ≈ i ↑ i c ↑ i d. [↑ i (c d)] i = c d (E.1) [↑ i (c d)] i = [↑ i c] i [↑ i d] i (E.1) [↑ i (c d)] i = [↑ i c ↑ i d] i (S.2) ↑ i (c d) ≈ i ↑ i c ↑ i d
Because the above distribution equalities depend on an agent, they can be regarded in spatial terms as being local, or in epistemic terms as being subjective. We consider next the global/objective version of the these equalities.

Global/Objective Distributed Extrusion

The condition E.2: ↑ i true = true (i.e ↑ i is strict) is not an unreasonable requirement since extruding or uttering true amounts to nothing regardless of the space context or the agent. In spatial terms E.2 should hold everywhere (global ); in epistemic terms it should hold true regardless of the agent (objective). The same applies to the condition E.3: ↑ i (c d) = ↑ i c ↑ i d (for every c and d) since it is not unreasonable to assume that extruding two pieces of information from the same space has the same effect as extruding them joined together. Notice that extrusion functions satisfying E.2 and E.3 distribute over finite joins; i.e., they preserve the supremum of finite sets. For this reason we shall refer to those extrusion functions satisfying E.2 and E.3 as being (globally/objectively) distributed.

Definition 3.4.1 (Spatial cs with Distributed Extrusion). A spatial constraint system with distributed extrusion (scs-de) is an scse

(Con, , [•] 1 , . . . , [•] n , ↑ 1 , . . . , ↑ n ) such that E.2 ↑ i true = true, and E.3 ↑ i (c d) = ↑ i c ↑ i d for every c, d ∈ Con.
We are also interested in the problem of extending scs's with distributed extrusion functions. For any continuous (and surjective) space function [•] i , the condition E.2 can be easily satisfied by a slight modification to the construction in Theorem 3.4.1: Take ↑ i to be the function that maps c to true if c = true else it maps c to [c] -1 i . The condition E.3, however, can be too strong of a requirement: There are surjective space functions for which no inverse satisfies E.3 -even if we assume the axiom of choice or restrict our attention to continuous space functions. Theorem 3.4.2 states this impossibility result. We describe the proof of Theorem 3.4.2 because it brings some insights into our next result. Consider the set N ∪ {∞} partially ordered as in the complete algebraic lattice in Figure 3.2. Let f be the self-map given by the arrows in Figure 3.2. By examining this function, one can conclude that f is continuous and that it preserves finite joins (i.e., it satisfies S.1 and S.2). Hence the underlying lattice in Figure 3.2 is a one-agent spatial constraint system with f as space function.

Notice that the fiber of 10 under f is f -1 (10) = {4, 5, 6} and the fiber of any e ∈ N ∪ {∞} under f with e = 10 is a singleton set. This implies that there are exactly three different right inverse functions for f and they differ only on input 10. Name these functions g 4 , g 5 and g 6 where g n (10) = n. None of these functions satisfy E.3: We have 4 = g 4 (10) = g 4 (8 9) = g 4 (8) g 4 (9) = 5, then the symmetric case 5 = g 5 (10) = g 5 (7 8) = g 5 (7) g 5 (8) = 4, and finally 6 = g 6 (10) = g 6 (8 9) = g 6 (8) g 6 (9) = 5. This gives us a constructive witness f to the statement in Theorem 3.4.2.

Our strategy to prove Theorem 3.4.2 was to provide a space function with a fiber not closed under meets. In our particular construction the fiber of 10 under f is not closed under meets since {4, 5, 6} = 2. We can prevent the existence of this kind of fibers by requiring space functions to be meet-complete. We conclude this section by showing that meet-completeness for space functions is in fact a sufficient condition for the existence of distributed extrusion functions.

Theorem 3.4.3 (Min Extrusion). Let [•] i be any meet-complete and surjective space function of an scs. Then

↑ i : c → [c] -1 i satisfies [↑ i c] i = c (E.1), ↑ i true = true (E.2) and ↑ i (c d) = ↑ i c ↑ i d (E.3). Proof. Let us prove first [↑ i c] i = c. Since [•] i is meet-complete we deduce [↑ i c] i = [ [c] -1 i ] i = {[d] i | d ∈ [c] -1 i } = {c} = c.
We now prove ↑ i true = true. From S.1 true (c,d),(d,c) / ∈ .

∈ [true] -1 i thus [true] -1 i = true. Finally we need to prove ↑ i (c d) = ↑ i c ↑ i d. First we show ↑ i is monotone. Claim: Define ↑ i : c → [c] -1 i , if c d then ↑ i c ↑ i d.
-Assume that ↑ i d ↑ i c. We derive the following:

[↑ i d] i [↑ i c] i (Monotonicity of [•] i ) d c (E.1) d = c (From H.1) ↑ i d = ↑ i c (A contradiction with ↑ i d ↑ i c.) -Assume ↑ i c ↑ i d. Because [•] i is meet complete we have [↑ i c ↑ i d] i = [↑ i c] i [↑ i d] i
. Applying E.1 and using hypothesis H.1 we obtain

[↑ i c] i [↑ i d] i = c d = c, therefore ↑ i c ↑ i d ∈ [c] -1 i . (3.4.1)
From Equation 3.4.1 and the definition of

↑ i we conclude ↑ i c ↑ i c ↑ i d. But this contradicts ↑ i c ↑ i d ↑ i c which follows from the hypothesis ↑ i c ↑ i d.
This concludes the proof of the claim. We can now prove

↑ i (c d) = ↑ i c ↑ i d. Since c, d c d, from the monotonicity of ↑ i we have ↑ i c, ↑ i d ↑ i (c d), therefore ↑ i c ↑ i d ↑ i (c d)
. Furthermore applying S.2 and E.1 we obtain

[↑ i c ↑ i d] i = c d, thus ↑ i c ↑ i d ∈ [c d] -1 i . Since ↑ i (c d) = [c d] -1 i we derive ↑ i (c d) ↑ i c ↑ i d which concludes the proof.
Therefore any spatial cs whose space functions are meet-complete and surjective can be extended to an scse with distributed extrusion by defining ↑ i c as the map

c → [c] -1 i .
Remark 3.4.1. Notice that from Proposition 3.3.1, Theorem 3.4.1 and Theorem 3.4.3 are dual in the sense that whereas Theorem 3.4.1 requires space functions to be join-complete, Theorem 3.4.3 requires space functions to be meet-complete.

Properties of Space and Extrusion

In what follows we discuss some distinctive properties of space and extrusion. An immediate consequence of the definition of scse's is that their spatial and extrusion functions must be surjective and injective, respectively.

Corollary 3.5.1. Let [•] i and ↑ i be space and extrusion functions of an scse. Then

[•] i is surjective and ↑ i is injective.

Proof. Axiom E.1 implies that there exists y = ↑ i c for every c ∈ Con such that

[y] i = c. This proves surjectivity. Now, as a means of contradiction assume that

↑ i is not injective. Then there exists elements c = d such that ↑ i c = ↑ i d. But then [↑ i c] i = [↑ i d] i . Applying E.1 we obtain c = d, a contradiction.

Consistent and Contradicting Agents

The following property of spatial constraint systems with extrusion has a noteworthy epistemic interpretation. Notice that in scs's nothing prevented us from having [false] i = false. Intuitively, inconsistencies generated by an agent may be confined within its own space. In scs's with extrusion, however, the agents' ability to move information outside their spaces prevents inconsistency confinement. This has a pleasant correspondence with epistemic logic since [false] i = false reflects the principle, referred to as the Consistency Axiom in belief/doxastic logics, that no agent can possibly believe the false statement.

Property 3.5.1 (Space Consistency). Let [•] i be a space function of an scse. Then

[false] i = false.

Proof. We derive the following

[false] i = [false ↑ i false] i (false • = false) = [false] i [↑ i false] i (S.2) = [false] i false (E.1) = false (• false = false)
Nevertheless, for i = j we allow the following to occur in an scse: [c] i [d] j = false, even when c d = false. Thus we may have agents whose information is inconsistent with that of others. This reflects the distributive and epistemic nature of the agents as they may have different information about the same incident or have contradicting beliefs.

Orders

The next properties involve notions from order theory [START_REF] Brian | Introduction to lattices and order[END_REF]. They will allows us to infer properties of information from placing into a space or extruding it. For example, to infer c d from observing f (c) f (d) where f is either a space or a extrusion function. Recall Definition 2.1.3 and consider the next definition: Definition 3.5.1. Given (Con, ) a self-map f over Con is said to be orderautomorphism if it is a surjective order-embedding. Additionally, we say that f is strictly monotonic (or strict-order preserving) if c d implies f (c) f (d).

From E.3 it follows that globally distributed extrusion functions preserve (monotonicity). From the axioms S.2 and E.1 one can also show that they reflect . Thus, extrusion functions are order-embeddings:

Property 3.5.2 (Extrusion Embedding). Let ↑ i be a distributed extrusion function of an scse. Then ↑ i is an order-embedding.

Proof. Since ↑ i preserves binary joins (E.3) it follows that ↑ i is order-preserving.

To prove that ↑ i is order-reflecting suppose ↑ i c ↑ i d. Then, by monotonicity of the space functions (Remark 2.2.2) we obtain [↑ i c] i [↑ i d] i and using E.1 we conclude c d.

Analogous to inconsistency confinement, we could have [c] i = [d] i for some c and d such that c = d. As we already mentioned this could be interpreted as saying that agent i cannot distinguish c from d; i.e., c ≈ i d. For some meaningful constraint systems, space functions necessarily preserve distinctness, i.e., they are injective. In particular, Proposition 3.5.1 (Injective Spaces). Let [•] i be a space function of an scse

(Con, ). Then [•] i is injective if (1) Con is a finite set, or if (2) [•] i is strictly monotonic.
Proof. Suppose Con is a finite set. Then the injectivity of [•] i follows from the pigeon hole principle given surjectivity of the self-map [•] and the fact that Con is finite. Now suppose [•] i is strictly monotonic. Let c, d with c = d. We need to prove that [c] i = [d] i . We have two cases: (c,d),(d,c) / ∈ ). Then we have c c d, thus by using strict monotonicity and S.2 we obtain

-c d. Since [•] i is strictly monotonic then [c] i [d] i therefore [c] i = [d] i . -c d (i.e.,
[c] i [c] i [d] i . We conclude [c] i = [d] i .
Like extrusion functions, injective space functions of scse also preserve and reflect the order. Furthermore since they are surjective, we conclude the following.

Property 3.5.3 (Automorphic Spaces). Let [•] i be an injective space function of an scse. Then [•] i is an order automorphism.

Proof. An automorphism is defined as a bijective self-map that is also an orderembedding. As [•] i is a surjective function (Corollary 3.5.1), and by hypothesis it is injective, then it is also a bijection. Any space function is order-preserving since they preserve binary joins (Remark 2.2.2). It remains to prove that [•] i is order-reflecting.

Suppose [c] i

[d] i . Using S.2 and the hypothesis we obtain

[c] i [d] i = [c d] i = [d] i . From the injectivity of [•] i , c d = d, thus c d.
A noteworthy corollary of Property 3.5.3 is that injective space functions are Scott-continuous (in fact meet and joint-complete) since order automorphisms are known to preserve whatever infima and suprema may exist in the corresponding poset [START_REF] Kenneth | Partially ordered abelian groups with interpolation[END_REF].

Corollary 3.5.2 (Complete Spaces). Let [•] i be a space function of an scse (Con, ). If [•] i is an automorphism then [•] i is join-complete and also meet-complete.

Notice that from Proposition 3.5.1, Corollary 3.5.2, and Property 3.5.3 we conclude that any strictly monotonic space function of an scse is continuous. Any space function of an scse is surjective and it has a property that is stronger than monotonicity: Namely it preserves finite joins (Remark 2.2.2). One may then wonder if space functions from scse's are already continuous. A negative answer is given in the example below.

Example 3.5.1 (Lexical Order). Let Con = N × N ∪ {(∞, ∞)} and let be the obvious lexical order on Con. Notice (Con, ) is a complete algebraic lattice. The function and[(m, n)] 1 = (m -1, n) for every n, m ∈ N with m ≥ 2. Clearly [•] 1 satisfies S.1 and S.2. Furthermore [•] 1 is meet-complete and surjective, so Theorem 3.4.3 gives us a distributed extrusion function

[•] 1 is given by [(∞, ∞)] 1 = (∞, ∞), [(0, n)] 1 = (0, 0), [(1, n)] 1 = (0, n+1)
↑ 1 : (n, m) → [(n, m)] -1 i . Therefore (Con, , [•] 1 , ↑ 1 ) is an scs with distributed extrusion. Nevertheless [•] 1 is not continuous: Take the directed set S = {(0, n) | n ≥ 0}. We have [ S] 1 = [(1, 0)] 1 = (0, 1) = (0, 0) = {[(0, n)] 1 | n ≥ 0}.
The above example also shows an application of Theorem 3.4.3 to derive an extrusion function for a rather simple scs. Notice that we could not have applied Theorem 3.4.1 because the [•] 1 was shown not to be continuous. In the Application section we will derive extrusion functions for a meaningful and more involved scs using Theorem 3.4.1.

Galois Connections

We conclude this section by stating a pleasant correspondence between space and extrusion. In Example 3.5.1 we used Theorem 3.4.3 to derive extrusion. This theorem tells us that we can extend any spatial cs whose space functions are meetcomplete and surjective to an scse with distributed extrusion by defining ↑ i c as the map c → [c] -1 i . From order theory we know that with such a definition we obtain a (monotone) Galois connection between space and extrusion.

Let us remember Definition 2.1.4. Given (Con, ), we say that a pair (l, u) of monotone self-maps on Con is a Galois connection iff l(c) d ⇔ c u(d) for every c, d ∈ Con. In a Galois connection (l, u), l and u are called the lower and upper adjoint, respectively. The following property follows directly from the theory of adjoints [START_REF] Abramsky | Domain theory. Handbook of logic in computer science[END_REF].

Property 3.6.1 (Galois Connections). Let [•] i and ↑ i be the space and extrusion function for agent i in an scs with distributed extrusion (Con, ).

Then (↑ i , [•] i ) is a Galois connection if and only if ↑ i c = [c] -1 i for every c ∈ Con. Similarly, ([•] i , ↑ i ) is a Galois connection if and only if ↑ i c = [c] -1 i for every c ∈ Con.
Proof. Here we appeal to the theory of adjoints. We adapt proposition 3.1.10 from [START_REF] Abramsky | Domain theory. Handbook of logic in computer science[END_REF] to self-maps on Con: Given two monotonic self-maps l : Con → Con and u : Con → Con the following are equivalent:

1. ∀c ∈ Con : l(c) = u -1 (c) 2. ∀c ∈ Con : u(c) = l -1 (c) 3. ∀c, d ∈ Con : c u(d) iff l(c) d (i.e., (l, u) is a Galois connection).
The functions [•] i and ↑ i • are monotonic because they preserve binary joins (S.2, E.3). By taking

l = u -1 (c) = ↑ i = [c] -1 i we obtain (1). By taking u = l -1 (c) = ↑ i = [c] -1 i we obtain (2).
It follows from Property 3.6.1 that the pair (↑ 1 , [•] 1 ) in Example 3.5.1 is a Galois connection. The following is a simple example of a space and extrusion pair that can be shown not to be a Galois connection using Property 3.6.1.

Example 3.6.1. Let Con = N ∪ {∞} and let be the standard linear-order over

N ∪ {∞}. Let [∞] 1 = ∞ = ↑ 1 ∞, [0] 1 = 0 = ↑ 1 0 and [n] 1 = n/3 and ↑ 1 n = 3n -1 for any n ∈ N -{0}. The tuple (Con, , [•] 1 , ↑ 1 ) is an scs with distributed extrusion. But 2 = ↑ i 1 = [1] -1 i = 1
, hence from Property 3.6.1 we can conclude that (↑ i , [•] i ) is not a Galois connection. (One can also verify using Property 3.6.1 that the reversed pair ([•] i , ↑ i ) is not a Galois connection either.)

Recall that e e can be thought of as the entailment of e by e . A Galois connection of the form

[c] i d ⇔ c ↑ i d (3.6.1)
reduces entailment of space to the entailment by extrusion. We will see an application of this observation in the next section.

Summary

We considered the problem of deriving extrusion for space functions and we identified sufficient conditions of space functions to obtain explicit constructions for extrusion. Surjectivity of space functions is of course a necessary condition for the existence of the corresponding extrusion functions. If the space function is join-complete (or continuous), Theorem 3.4.1 gives us a construction that maps each constraint to the least upper bound of its pre-image (or fiber) under the space function. If the space function is meet-complete Theorem 3.4.3 gives us a dual construction that maps each constraint to the greatest lower bound of its pre-image under the space function.

In what follows from this thesis we use some of the above results to derive extrusion for some modal operators. For modal logics in general, the underlying constraint system we use is Kripke's (defined later in Definition 4.2.1) and thus space functions correspond to the box ( ) operator, the join correspond to conjunction, and meet correspond to disjunction (see Definition 4.2.2). If it exists, the extrusion operator would be a reverse modality, say -1 , such that -1 φ is logically equivalent to φ. Theorem 3.4.1 always applies since the space functions of any Kripke constraint system are join-complete (same argument from Remark 2.2.1). In fact the box operator always distributes over conjunction but not always over disjunction.

Nevertheless, there exist cases where space functions are also meet-complete. For example the box operator being interpreted as the next modality of temporal logic [START_REF] Pnueli | The temporal logic of reactive and concurrent systems[END_REF] since it distributes over both conjunction and disjunction. In this case we could apply both Theorem 3.4.1 and Theorem 3.4.3. Interestingly, we would obtain two different but well-known reverse modalities for the next operator. Theorem 3.4.1 would give us a strong-previous modality while Theorem 3.4.3 would give us a weak-previous modality . Notice that unlike Theorem 3.4.1, Theorem 3.4.3 guarantees that the derived extrusion preserves the bottom element true. In fact, the temporal formula T is logically equivalent to T while T is not (since p is false at time 0 for any p). This interpretation of space as a time operator will be expanded thoroughly in Chapter 6.

Finally, we presented distinctive properties of space and extrusion. Property 3.5.1 tells us a fundamental aspect of extrusion; unlike general spatial constraint systems, the space functions of scs with extrusion cannot confine inconsistencies. For example for Kripke constraint systems, where space functions correspond to the box ( ) operator if they admit extrusion then F must be equivalent to F. Proposition 3.5.1 identifies conditions under which spaces of scs with extrusion must preserve distinctiveness of information. The other properties state the preservation and reflection of the underlying order/entailment relation w.r.t space and extrusion. These properties allow us to infer entailment between some given information from the entailment when the information is placed in some agent's space or when it is extruded. Finally, the Galois connections between space and extrusion allow us to reduce the entailment of/by spatial information from entailment by/of extruded information. All the results presented in this chapter were published in [START_REF] Haar | An algebraic view of space/belief and extrusion/utterance for concurrency/epistemic logic[END_REF].

Chapter 4

Opinions & Lies: A Bimodal Logic

Modal Logics

In this section we present the basic concepts we use in this chapter from modal logics. See [START_REF] Blackburn | Modal Logic[END_REF] for a more thorough introduction to modal logic and their applications. We begin by defining what a modal language is. Definition 4.1.1 (Modal language). Let Φ be a set of primitive propositions. We denote by L n (Φ) the modal language made of formulas using the following syntax: Having defined a modal language, we can also define a semantic model to give meaning to the language. In other words, this enables us to represent a formula from the language in some abstract model.

M = (S, π, R 1 , . . . , R n ) (4.1.1)
where:

-S is a nonempty set of states, π : S → (Φ → {0, 1}) is an interpretation that associates with each state a truth assignment to the primitive propositions in Φ, and -R i is a binary relation on S.

Notation 4.1.2. The states of a KS are often referred to as worlds. Each R i is referred to as the accessibility or possibility relation for agent i: (s, t) ∈ R i is meant to capture that agent i considers world t possible given its information in world s. We use We can define a notion of semantic validity using a relation between the models and the formulas. We say that φ holds at (M, s) whenever (M, s) |= φ. Furthermore, φ is valid in M if φ holds in all states of M and φ is satisfied in M if there exists a state in M where φ holds.

s i -→ M t to denote (s, t) ∈ R i in the KS M . We use W i (M, s) = {t | s i -→ M t}
Definition 4.1.3 (Kripke semantics). We define the relation |= inductively as follows:

•

(M, s) |= p iff π M (s)(p) = 1 • (M, s) |= φ ∧ ψ iff (M, s) |= φ and (M, s) |= ψ • (M, s) |= ¬φ iff (M, s) |= φ • (M, s) |= i φ iff (M, t) |= φ for all t ∈ W i (M, s)
Theorem 4.1.1. The semantic validity of disjunction, implication and the dual modality are as follows:

• (M, s) |= φ ∨ ψ iff (M, s) |= φ or (M, s) |= ψ • (M, s) |= φ ⇒ ψ iff whenever (M, s) |= φ, (M, s) |= ψ holds • (M, s) |= i φ iff there exists t ∈ W i (M, s) such that (M, s) |= φ
Consider a class of Kripke structures M. We can expand the definition of validity and satisfiability accordingly; φ is valid in M if φ is valid in all KS of M and φ is satisfied in M if there exists a KS in M that satisfies φ.

In order to formally prove a statement, a logic can have an associated axiom system AX. This is a set of inference rules of the form "from φ infer ψ" and a set of axioms which are just formulas. A proof of a formula φ in AX is a sequence of formulas ending with the formula φ and each step is either an instance of an axiom or an application of an inference rule. We write AX φ if there exists such sequence for φ to say that φ is provable/true in AX.

Example 4.1.1 (Axiom System K n ). The axiom system K n is made up of two axioms and two inference rules:

A.1 All tautologies from propositional logic,

A.2 i (φ ⇒ ψ) ⇒ ( i φ ⇒ i ψ) for all i = 1 . . . n, R.1 From φ and φ ⇒ ψ infer ψ, R.2 From φ infer i φ for all i = 1 . . . n.
A.2 is usually called the distribution axiom, rule R.1 is modus ponens and R.2 is called the generalization or necessitation rule. A set of modal formulas Λ is called a normal modal logic if it contains the axioms system K n (or K when n is unimportant).

Finally, we formally state the link between the axiomatic and the semantic world. This correspondence is important in the sense that it ties what is valid (semantics) to what is true (axioms) in a logic. Definition 4.1.4 (Soundness and completeness). A logic Λ with axiom system AX is said to be sound wrt to semantic class M iff for every φ we have that AX φ implies M |= φ. Alternatively, a logic Λ with axiom system AX is complete wrt to semantic class M iff for every φ we have that M |= φ implies AX φ.

Kripke Spatial Constraint Systems

We now revisit a concrete spatial constraint system from [START_REF] Knight | Spatial and epistemic modalities in constraintbased process calculi[END_REF]. This constraint system will play a significant role in the rest of the document. We basically extend Example 2.2.2 by moving from Boolean assignments to KS. Other examples of spatial constraint system for epistemic reasoning are Aumann structures [START_REF] Knight | Spatial and epistemic modalities in constraintbased process calculi[END_REF].

Recall that in Example 2.2.2 constraints are sets of boolean assignments. This allowed us to interpret each propositional formula as a constraint; the set of assignments that are models of (or satisfy) the formula. Similarly, in the following example (spatial) constraints are sets of (pointed) KS models. A pointed KS is a pair (M, s) where M is a KS and s, called the actual world, is a state of M . This will allows us to interpret each modal formula as its set of pointed KS models; i.e., a spatial constraint. Definition 4.2.1 (Kripke scs [START_REF] Knight | Spatial and epistemic modalities in constraintbased process calculi[END_REF]). Let S n (Φ) be a non-empty set of nagent Kripke structures over Φ. Let ∆ be the set of all pointed Kripke structures (M, s) such that M ∈ S n (Φ). We define the Kripke n-scs for S n (Φ) as

K(S n (Φ)) = (Con, , [•] 1 , . . . , [•] n )
where Con = P(∆), and for every X, Y ∈ Con : X Y iff Y ⊆ X, and

[X] i = i(X) where i(X) def = {(M, s) ∈ ∆ | ∀t : s i -→ M t implies (M, t) ∈ X}
(4.2.1) for every agent i ∈ {1, . . . , n}.

The scs K(S n (Φ)) is a complete algebraic lattice given by a powerset ordered by ⊇. The is set intersection, the top element false is ∅, and bottom true is the set ∆ of all pointed Kripke structures (M, s) with

M ∈ S n (Φ). Similar to Example 2.2.2, a constraint c in K(S n (Φ)) is compact iff ∆ \ c is a finite set [KPPV12]. Proposition 4.2.1. Let K(S n (Φ)) = (Con, , [•] 1 , . . . , [•] n ) be a Kripke n-scs. Each [•] i is a space function.
Proof. We show that [•] i fulfills the axioms S.1 and S.2: For S.1:

[true] i by definition is [∆] i = {(M, s) ∈ ∆ | ∀t : s i -→ M t implies (M, t) ∈ ∆}. Nonetheless every (M, s) ∈ ∆ consequently [∆] i = ∆ and [true] i = true.
For S.2:

[c d] i = (M, s) ∈ ∆ | ∀t : s i -→ M t implies (M, t) ∈ c d = (M, s) ∈ ∆ | ∀t : s i -→ M t implies (M, t) ∈ c ∩ d = (M, s) ∈ ∆ | ∀t : s i -→ M t implies (M, t) ∈ c ∩ (M, s) ∈ ∆ | ∀t : s i -→ M t implies (M, t) ∈ d = [c] i ∩ [d] i = [c] i [d] i
Similarly to Remark 3.2.1, since in Kripke scs meets are unions and joins intersections then Kripke scs are also frames. Also, because Kripke scs are of the form (P(U ), ⊇) (see Example 2.1.1), the operators → and ∼ coincide with the constructions ⇒ and ¬ defined in Remark 2.2.1.

A modal language

Modal formulae can be interpreted as constraints in the scs K(S n (Φ)). This kind of interpretation will be frequently used in the rest of this thesis. Recall that the modal language L n (Φ) in Equation 4.1.1 is obtained by extending the grammar for the propositional language L 0 (Φ) in Equation 2.2.1 with modalities i φ in the standard way. Definition 4.1.3 gives us the semantics of modal logics using KS's. Therefore, as in Example 2.2.2 we can interpret each formula φ as constraints in Kripke constraint systems. Definition 4.2.2 (Kripke Constraint Interpretation). Let K(S n (Φ)) be a Kripke scs denoted by C. Given a modal formula φ in the language L n (Φ), its interpreta-tion in the Kripke scs C is the constraint C φ inductively defined as follows:

C p = {(M, s) ∈ ∆| π M (s)(p) = 1 } C φ ∧ ψ = C φ C ψ C ¬φ = ∆ \ C φ C i φ = [ C φ ] i
where ∆ is the set of all pointed Kripke structures (M, s) such that M ∈ S n (Φ).

Notation 4.2.1. Notice that the interpretation of i (φ),

C i (φ) , is equal to the constraint [ C φ ] i in K(S n (Φ)).
Often, by abuse of notation, we shall suppress the semantic symbols C from formulae-e.g., we write [φ] i for the constraint

[ C φ ] i .
Following our intended meaning of constraints, we think of [φ] i as stating that φ holds in the space of agent i, or as an epistemic assertion stating that agent i considers/believes φ to be true.

A Logic of Belief and Utterance

In Section 3.4 we discussed the problem of constructing extrusion functions for spatial constraint systems. In this section we want to derive explicit extrusion functions for a meaningful family of the Kripke scs (Definition 4.2.1) as an application of the results we obtained in Sections 3.4 and 3.5.

Recall that we can associate a modal language (Definition 4.1.1) to a Kripke scs by interpreting formulae as constraints, i.e., set of pointed Kripke structures. Under such association, i φ = [φ] i states that φ holds true in the space of i (Notation 4.2.1). Finding an extrusion ↑ i for each [•] i will also allow us to derive an inverse modality for i . We will use the derived modality to specify utterances and lies with a modal language.

Let us also recall the (n-agent) Kripke scs

K(S n (Φ)) = (Con, , [•] 1 , . . . , [•] n ) in Definition 4.2.
1. This scs is parametric in a set of (n-agents) Kripe structures S n (Φ) defined over a set of primitive propositions Φ. Its set of constraints is defined as Con = P(∆) where ∆ is the set of all pointed KS (M, s) such that

M ∈ S n (Φ),
is reversed set inclusion, the join operation is set intersection, the meet operation is set union, the top element false is ∅, and its bottom true is ∆. The space functions are given by :

[c] i def = {(M, s) ∈ ∆ | ∀t : if s i -→ M t then (M, t) ∈ c} (4.3.1)
for each i ∈ {1, . . . , n}.

We will thus endeavor to find suitable Kripke structures for scs such that extrusions for each space function can be constructed. The path we follow for this is: (1) we restrict KS to left-total accessibility and show this ensures space consistency, (2) KS are then further restricted to left-unique accessibility relations to guarantee surjectivity of space functions, (3) we show these to be also continuous and, finally (4) we apply theorem 3.4.1 to derive an extrusion for each space function over the restricted KS's.

Left-total left-unique Kripke Structures

Modal logics are typically interpreted over different classes of KS that are usually obtained by imposing conditions on their accessibility relations (see Section 5.1 for examples of this). We denote with M the class of KS whose accessibility relations are unrestricted, thus formulae should be interpreted as elements of the Kripke scs K(M n (Φ)) where M n (Φ) is the set of all n-agents KS's over Φ.

Notation 4.3.1. For notational convenience, we take the set Φ of primitive propositions and n to be fixed from now on and omit them from the notation. E.g., we write M instead of M n (Φ).

We say that a set S of KS's satisfies space consistency iff [false] i = false for every space function [•] i in K(S). It follows from Property 3.5.1 that space consistency is a necessary condition for the existence of extrusion functions.

Let us begin with K(M). We can verify that this scs does not satisfy space consistency. First recall from Notation 4.1.2 that W i (M, s) = {t | s i -→ M t} denote the worlds agent i considers possible from the world s of KS M . Take a pointed KS (M , s ) such that W i (M , s ) = ∅ . Notice that in K(M), false = ∅. From Equation 4.3.1 we conclude that (M , s ) ∈ [false] i thus violating space consistency. Property 3.5.1 then tells us that K(M) cannot be extended to an scs with extrusion.

Left-total KS's Let us consider more restricted sets of KS's. We already mentioned, in the preamble of Property 3.5.1, the connection between space consistency and the Consistency Axiom. The condition on KS associated with the Consistency Axiom is that of being left-total. An accessibility relation R i of agent i in a KS M is said to be left-total (or serial ) if for every s there exists t such that (s, t) ∈ R i (i.e., s i -→ M t). Let M lt be the set of those KS whose accessibility relations are all left-total. Notice that for every (M, s) with M ∈ M lt we have W i (M, s) = ∅. From this observation we can prove the following.

Proposition 4.3.1 (Left-total space-consistency). The set M lt satisfies space consistency.

Proof. Recall that in K(M lt ), false = ∅. [false] i = {(M, s) ∈ ∆ | ∀t if s i -→ M t then (M, t) ∈ false} = {(M, s) ∈ ∆ | ∀t if s i -→ M t then (M, t) ∈ ∅}.
Take an arbitrary (M, s) ∈ ∆. Since the accessibility relations in K(M lt ) are left-total, there exists t such that s

i -→ M t but (M, t) / ∈ ∅. Thus for every (M, s) ∈ ∆, (M, s) / ∈ [false] i , hence [false] i = ∅ = false.
We say that a set S of KS's satisfies surjectivity iff every space function in K(S) is surjective. The surjectivity of space functions is a necessary condition for the existence of extrusion (Corollary 3.5.1).

We can show that M lt does not satisfy surjectivity by taking M ∈ M lt , (M, s) and (M, s ) such that s = s and W i (M, s) = W i (M, s ). Let c ∈ P(∆) such that c = [d] i for some d ∈ P (∆). Since W i (M, s) = W i (M, s ), from Equation 4.3.1 we conclude that if (M, s) ∈ c then (M, s ) ∈ c. Thus, surjectivity is not satisfied by

[•] i since for every d ∈ P(∆), [d] i = {(M, s)}.
Thus K(M lt ) cannot be extended to an scs with extrusion.

Left-unique KS's A natural general condition to prevent counter-examples to

surjectivity as the one above is to restrict M lt to KS's whose accessibility relations are left-unique. More precisely, we say that an accessibility relation R i is a leftunique (or injective) iff for every t there is at most one s such that s i -→ M t. Let M ltu be the set of those KS whose accessibility relations are both left-total and left-unique. Notice that the left-unique condition guarantees that W i (M, s) ∩ W i (M, s ) = ∅ for any s = s and M ∈ M ltu . where ∆ is the set of pointed KS (M, s) such that M ∈ M ltu and s is a state of M. -Assume (H.5) (M, s) ∈ [↑ i c] i , we want to prove (M, s) ∈ c. Since the accessibility relations in K(M ltu ) are left-total, from H.5 we conclude that there exists t such that s i -→ M t and (M, t) ∈ ↑ i c. From (M, t) ∈ ↑ i c it follows that there exists s such that s i -→ M t and (M, s ) ∈ c. From the fact that the accessibility relations in K(M ltu ) are left-unique we conclude that s = s , and thus (M, s) ∈ c.

Proof. Let

↑ i c = {(M, t) ∈ ∆ | ∃s : s i -→ M t and (M, s) ∈ c}. (4.3.4) We need to prove ↑ i c = ↑ i c where ↑ i c = [c] -1 i = [c] -1 i . Recall the definition of [•] i : [c] i = {(M, s) ∈ ∆ | ∀t if s i -→ M t then (M, t) ∈ c}. -↑ i c ⊆ ↑ i c. Suppose that (H.1) (M, t) ∈ ↑ i c but (H.2) (M, t) / ∈ ↑ i c. From H.
d ∈ [c] -1 i such that (M, t) / ∈ d. Notice that [d] i = c since d ∈ [c] -1 i . But since (M, t) / ∈ d and s i -→ M t we conclude (M, s) / ∈ [d] i . This is a contradiction since we previously concluded [d] i = c and (M, s) ∈ c. -↑ i c ⊆ ↑ i c. We claim that (C.1) [↑ i c] i = c. From this claim we have ↑ i c ∈ [c] -1 i , therefore ↑ i c = [c] -1 i ⊆ ↑ i c
From the above we can now extend K(M ltu ) to the following scs with extrusion. Definition 4.3.1 (Kripke scs with extrusion). The n-agent scs with extrusion K ↑ (M ltu ) results from extending K(M ltu ) with an extrusion function ↑ i for each i ∈ {1, . . . , n} defined as in Equation 4.3.2.

It follows from Property 3.6.1 that in the derived scse, space and extrusion form a Galois connection.

Corollary 4.3.1. Let [•] i and ↑ i be the space and extrusion function of agent i in

K ↑ (M ltu ). The pair ([•] i , ↑ i ) is a Galois connection.
We shall apply this Galois connection in the following section.

The BU n logic

We shall now extend the modal language in Definition 4.1.1 with modalities to express utterances. The intended meaning and properties of the formulae in the extended language will be given from the scse K ↑ (M ltu ) we derived in the previous section (Definition 4.3.1). We shall refer to the resulting multi-modal logic as BU n .

For clarity we shall write B i instead of i . The language L BU n (Φ) is obtained by replacing i with B i in the grammar of Example 4.2.1 and extending it with modalities U i . Definition 4.3.2 (Modal language for utterance). Let L BU n (Φ) with n ≥ 1 be the language built from a set of primitive propositions Φ by the following syntax:

ϕ := p | ϕ ∧ ϕ | ¬ϕ | B i ϕ | U i ϕ where i ∈ {1 . . . n} and p ∈ Φ.
Before presenting the semantics of BU n , we give a dual spatial/epistemic intuition about its modal formulae. Let us consider s and t such that s i -→ M t. Recall from Notation 4.1.2 that t is a world that agent i considers possible in the world s (of a KS M ). In spatial terms we can think of t as being a local world for agent i wrt to the outside world s. If the belief modality B i ϕ holds true in outside world s it implies that ϕ must be true in the local world t.

The formulae in Equation 4.3.8 are consistency axioms. The first formula says that if agent i believes ϕ then it should not believe ¬ϕ. The other says that the extrusion of ϕ and ¬ϕ would generate an inconsistency.

Semantics We now give the semantics for BU n using the scse K ↑ (M ltu ) in Definition 4.3.1. Recall our definition of the negation constraint ∼ c (Definition 3.2.1) and that K ↑ (M ltu ) is also a frame (Remark 3.2.1).

Definition 4.3.3. Let K ↑ (M ltu ) = (Con, , [•] 1 , . . . , [•] n , ↑ 1 , . . . , ↑ n ) be the scse in Definition 4.3.1. Given ϕ in L BU n (Φ)
, its denotation K ↑ ϕ is inductively defined as follows:

K ↑ p = {(M, s) ∈ ∆| π M (s)(p) = 1} K ↑ ϕ ∧ ϕ = K ↑ ϕ K ↑ ϕ K ↑ ¬ϕ = ∼ K ↑ ϕ K ↑ B i ϕ = [ K ↑ ϕ ] i K ↑ U i ϕ = ↑ i K ↑ ϕ
where ∆ is the set of all pointed Kripke structures (M, s) such that M ∈ M ltu . We say that ϕ is valid in BU n iff K ↑ ϕ = true.

From the above semantics definition and the properties of scs with extrusion one can verify the expected behavior of utterance, opinion, and hoaxes in Equations 4.3.5, 4.3.6, 4.3.7 and 4.3.8. Proof. We show the validity of the various formulae using their semantics definition and the axioms of space and extrusion.

-

B i U i ϕ ⇔ ϕ is valid.
We need to prove K ↑ B i U i ϕ = K ↑ ϕ . We use the semantic definitions along with E.1 on the left side to obtain

K ↑ B i U i ϕ = [ K ↑ U i ϕ ] i = [ ↑ i K ↑ ϕ ] i = K ↑ ϕ -O i (ϕ) ⇔ B i ϕ ∧ ϕ is valid. We need to prove K ↑ B i (ϕ ∧ U i (ϕ)) = K ↑ B i ϕ ∧ ϕ .
We use the semantic definitions on the left side to obtain

K ↑ B i (ϕ∧U i (ϕ)) = [ K ↑ ϕ∧U i (ϕ) ] i = [ K ↑ ϕ K ↑ U i (ϕ) ] i . Using S.2 and E.1 we obtain [ K ↑ ϕ ] i [ K ↑ U i (ϕ) ] i = [ K ↑ ϕ ] i [ ↑ i K ↑ ϕ ] i = [ K ↑ ϕ ] i K ↑ ϕ = K ↑ B i ϕ K ↑ ϕ = K ↑ B i ϕ ∧ ϕ .
-

H i (ϕ) ⇔ B i ¬ϕ ∧ ϕ is valid. We need to prove K ↑ B i (¬ϕ ∧ U i (ϕ)) = K ↑ B i ¬ϕ ∧ ϕ .
We use the semantic definitions on the left side to obtain

K ↑ B i (¬ϕ ∧ U i (ϕ)) = [ K ↑ ¬ϕ ∧ U i (ϕ) ] i = [ K ↑ ¬ϕ K ↑ U i (ϕ) ] i . Using S.
2 and E.1 we obtain

[ K ↑ ¬ϕ ] i [ K ↑ U i (ϕ) ] i = [ K ↑ ¬ϕ ] i [ ↑ i K ↑ ϕ ] i = [ K ↑ ¬ϕ ] i K ↑ ϕ = K ↑ B i ¬ϕ K ↑ ϕ = K ↑ B i ¬ϕ ∧ ϕ . -B i ϕ ⇒ Bi ϕ is valid. It suffices to prove K ↑ Bi ϕ = K ↑ ¬B i ¬ϕ = ∼ K ↑ B i ¬ϕ =∼ [ K ↑ ¬ϕ ] i = ∼ [∼ K ↑ ϕ ] i K ↑ B i ϕ = [ K ↑ ϕ ] i . Notice that [ K ↑ ϕ ] i is defined as {(M, s) ∈ ∆ | ∀t if s i -→ M t then (M, t) ∈ K ↑ ϕ }. Similarly, ∼ [∼ K ↑ ϕ ] i is equivalent to the set {(M, s) ∈ ∆ | ∃t : s i -→ M t and (M, t) ∈ K ↑ ϕ }.
Using these equations we can verify that

[ K ↑ ϕ ] i ⊆ ∼ [∼ K ↑ ϕ ] i . There- fore ∼ [∼ K ↑ ϕ ] i [ K ↑ ϕ ] i as wanted.
-

U i ϕ ⇒ Ûi ϕ is valid. Analogous to the previous case. Notice that ϕ ⇒ ψ is valid in BU n iff K ↑ ψ K ↑ ϕ . It follows from Corollary 4.3.1 that in K ↑ (M ltu ) we have [c] i d iff c ↑ i (d).
We can then conclude the following property.

Corollary 4.3.2. ϕ ⇒ B i ψ is valid in BU n iff U i ϕ ⇒ ψ is valid in BU n .
Intuitively Corollary 4.3.2 says that belief and utterance form a Galois connection. We can therefore reduce the validity of the implication of a belief property to/from the implication by a utterance property.

We conclude this chapter by revisiting Example 3.2.2.

Example 4.3.1 (Hoax Communication). Let us consider the epistemic formulae

F = B j (¬p ⇒ U j (q)) and G = B i (p ∧ U i B j (¬p)).
The formula F specifies an agent j that would utter q if she believed that p was not true. The formula G specifies an agent i that believes p and yet he utters that j should believe the opposite, i.e., a lie ¬p by agent i. We can show that the combination of both specifications implies that q will be extruded, i.e., we will show that

(F ∧ G) ⇒ q
is valid in BU n . We obtain the following derivation using the properties of the space and extrusion functions:

K ↑ F ∧ G = [∼ K ↑ p → ↑ j K ↑ q ] j [K ↑ p ↑ i [∼ K ↑ p ] j ] i Def.4.3.3 = [∼ K ↑ p → ↑ j K ↑ q ] j [K ↑ p ] i [↑ i [∼ K ↑ p ] j ] i S.2 [•] i = [∼ K ↑ p → ↑ j K ↑ q ] j [K ↑ p ] i [ ∼ K ↑ p ] j E.1 [•] i = [∼ K ↑ p ∼ K ↑ p → ↑ j K ↑ q ] j [K ↑ p ] i S.2 [•] j = [∼ K ↑ p ↑ j K ↑ q ] j [K ↑ p ] i Lem.3.2.1 = K ↑ q [∼ K ↑ p ] j [K ↑ p ] i E.1 [•] j = K ↑ q ∩ [∼ K ↑ p ] j ∩ [K ↑ p ] i Def.4.2.1 ⊆ K ↑ q Thus every model of K ↑ F ∧ G is a model of K ↑ q .
We can conclude that (F ∧ G) ⇒ q is valid as wanted.

Summary

After introducing Kripke constraint systems, we devised a bimdodal logic of belief and utterance where we were able to define epistemic behaviors such as Chapter 5

Knowledge in Terms of Global Space

In the previous chapter we saw how spatial constraint systems can be used to represent epistemic concepts such as beliefs, lies and opinions. In this chapter we show that spatial constraint systems can also express the epistemic concept of knowledge using the notion of global information from Definition 2.2.3. We begin with an introduction to epistemic logic and the different axioms attributed to knowledge.

Epistemic Logic

When conceiving a modal logic, one can impose an interpretation on the modal operator for contextualizing its application. One usch important interpretation is that of knowledge wherein the logic takes the name of Epistemic Logic.

Similarly to what we did in Section 4.3, we now write the modal operator as K. Thus, K i φ can be read as "agent i knows φ" and nesting of modalities like K i K j φ is read as "agent i knows that agent j knows φ". An introductory text on the theory and application of epistemic logics is [START_REF] Fagin | Reasoning about knowledge[END_REF].

In epistemic logics, the axiom system K n (Example 4.1.1) has a more contextualized interpretation. Axiom A.2 is referred to as the Knowledge distribution axiom, intuitively speaking this means agents are perfect reasoners. Rule R.2 is called Knowledge generalization, meaning that universal truths are known by all the agents. if (s, t) ∈ R i and (s, u) imply (t, u) ∈ R i , and -serial if there exists s s.t.

(s, s ) ∈ R i .
Notice that S5 (i.e. Axioms A.1 -A.5 and by consequence A.7) requires the accessibility relation to be reflexive, transitive and symmetric. In other words, the axiom system S5 requires the accessibility relations to be equivalence relations.

Knowledge Constraint System

In [START_REF] Knight | Spatial and epistemic modalities in constraintbased process calculi[END_REF] the authors extended the notion of spatial constraint system to account for knowledge. In this chapter we shall refer to the extended notion in [START_REF] Knight | Spatial and epistemic modalities in constraintbased process calculi[END_REF] as S4 constraint systems since it is meant to capture the epistemic logic for knowledge S4. Roughly speaking, one may wish to use [c] i to represent not only some information c that agent i has but rather a fact that he knows. The domain theoretical nature of constraint systems allows for a rather simple and elegant characterization of knowledge by requiring space functions to be Kuratowski closure operators [START_REF] Charles | The algebra of topology[END_REF]: i.e., monotone, extensive and idempotent functions that preserve bottom and lubs. Definition 5.2.1 (Knowledge Constraint System [START_REF] Knight | Spatial and epistemic modalities in constraintbased process calculi[END_REF]). An n-agent S4 constraint system (n-s4cs) C is an n-scs whose space functions [•] 1 , . . . , [•] n are also closure operators. Thus, in addition to S.1 and S.2 in Definition 2.2.2, each [•] i also satisfies: (EP.1) [c] i c and (EP.2)

[[c] i ] i = [c] i .
Intuitively, in an n-s4cs, [c] i states that the agent i has knowledge of c in its store [•] i . The axiom EP.1 says that if agent i knows c then c must hold, hence

[c] i has at least as much information as c. The epistemic principle that an agent i is aware of its own knowledge (the agent knows what he knows) is realized by EP.2. Also the epistemic assumption that agents are idealized reasoners follows from the monotonicity of space functions

(Remark 2.2.2); for if c is a consequence of d (d c) then if d is known to agent i, so is c, [d] i [c] i .
Recall that modal logics are interpreted over families of Kripke structures obtained by restricting their accessibility relations. Also, M n (Φ) is used to denote the set of all Kripke structures over the set of primitive propositions Φ (Notation 4.3.1). We shall use M rt n (Φ) to denote the set of those n-agents Kripke structures, over the set of primitive propositions Φ, whose accessibility relations are reflexive and transitive. As in the previous chapter, for notational convenience, we take the set Φ of primitive propositions and n to be fixed from now on and omit them often from the notation. E.g., we write M rt instead of M rt n (Φ). Henceforth we use C rt to denote the Kripke constraint system K(M rt ) (Definition 4.2.1). In [START_REF] Knight | Spatial and epistemic modalities in constraintbased process calculi[END_REF] it was shown that C rt is in fact an S4 constraint system.

Proposition 5.2.1 ([KPPV12]). C rt is an s4cs.

Recall our interpretation of formulae of the modal language L n (Φ) (Definition 4.1.1) using Kripke spatial constraint systems (Definition 4.2.2). In particular the interpretation of the formula i (φ) in C rt , denoted C rt i (φ) , is the constraint [C rt φ ] i . Let us now recall the notion of validity in the modal logic S4 [START_REF] Hintikka | Knowledge and belief[END_REF].

Definition 5.2.2. Let φ be a modal formula from the modal language L n (Φ). The formula φ is said to be S4-valid iff for every (M, s) where M ∈ M rt (Φ) and s is a state of M, we have (M, s) |= φ. Notation 5.2.1. As stated at the beginning of this chapter, in the modal logic S4 the box modality i is often written as K i . The formula K i (φ) specifies that agent i knows φ.

The following proposition from [START_REF] Knight | Spatial and epistemic modalities in constraintbased process calculi[END_REF] is an immediate consequence of the above definition. It states the correctness wrt validity of the interpretation of S4 formulae in

C rt . Proposition 5.2.2 ([KPPV12]). C rt φ = true if and only if φ is S4-valid.

Knowledge as Global Information

Let C = (Con, , [•] 1 , . . . , [•] n ) be a spatial constraint system. From Definition 2.2.3 we obtain the following equation:

[[[c]]] {i} = c [c] i [[c] i ] i [[[c] i ] i ] i . . . = c [c] i [c] 2 i [c] 3 i . . . = ∞ j=0 [c] j i (5.3.1)
where

[e] 0 i def = e and [e] j+1 i def = [ [e] j i ] i . For simplicity we shall use [[[•]]] i as an abbreviation of [[[•]]] {i} .
Intuitively, [[[c]]] i says that c holds globally wrt i: c holds outside and in every nested space of agent i. We shall demonstrate that [[[c]]] i can also be used to represent the knowledge of c by agent i.

We will show that the global function

[[[c]]] i is
[[[[[c]]] i ]]] i = [[[c]]] i (EP.
2). Furthermore, we can combine knowledge with our belief interpretation of space functions: Clearly, [[[c]]] i

[c] i holds for any c. This reflects the epistemic principle that whatever is known is also believed [START_REF] Hintikka | Knowledge and belief[END_REF].

We now show that any spatial constraint system with continuous space functions One can show that C * is also a spatial constraint system. Furthermore it is an s4cs as stated next. -We want to prove that [

[[•]]] i satisfies S.2: [[[c d]]] i = [[[c]]] i [[[d]]] i . Since [•] i satisfies S.2 we can use [c d] i = [c] i [d] i to show by induction on j that [c d] j i = [c] j i
[d] j i for any j. We then obtain the following equation

[[[c d]]] i = ∞ j=0 [c d] j i = ∞ j=0 ([c] j i [d] j i ). (5.3.2) Clearly [[[c]]] i = ∞ j=0 [c] j i ∞ j=0 ([c] j i [d] j i ) ∞ j=0 [d] j i = [[[d]]] i . Therefore [[[c d]]] i [[[c]]] i [[[d]]] i . It remains to prove [[[c]]] i [[[d]]] i [[[c d]]] i . Notice that [[[c]]] i [[[d]]] i = ( ∞ j=0 [c] j i ) ( ∞ j=0 [d] j i ) is an upper bound of the set S = {[c] j i [d] j i | j ≥ 0}. Therefore [[[c]]] i [[[d]]] i S = ∞ j=0 ([c] j i [d] j i ) = [[[c d]]] i as wanted.
-We want to prove that

[[[•]]] i satisfies EP.1: [[[c]]] i c. Immediate consequence of Equation 5.3.1. -Finally we prove that [[[•]]] i satisfies EP.2: [[[[[[c]]] i ]]] i = [[[c]]] i . Since [[[•]]] i satisfies EP.1 we have [[[[[[c]]] i ]]] i [[[c]]] i . It remains to prove that [[[c]]] i [[[[[[c]]] i ]]] i . Let S = {[c] k i | k ≥ 0}. Notice that [[[c]]] i = S.
One can verify from the definition of [•] j i that for any j

[S] j i = {[[c] k i ] j i | k ≥ 0} = {[c] k+j i | k ≥ 0} ⊆ S
From the continuity of [•] i , one can show by induction on j the continuity of [•] j i for any j. It then follows that [ S] j i = [S] j i for any j. Since for any j, [S] j i ⊆ S we conclude that for every j, S [S] j i . Therefore S ∞ j=0 [S] j i . This concludes the proof since from Equation 5.

3.1 [[[c]]] i = S and [[[[[[c]]] i ]]] i = ∞ j=0 [ S] j i = ∞ j=0 [S] j i .
We shall now prove that S4 can also be captured using the global interpretation of space.

From now on C denotes the Kripke constraint system K(M) (Definition 4.2.1). Notice that unlike in C rt , constraints in C, and consequently also in C * , are sets of unrestricted (pointed) Kripke structures. Although C is not an S4 constraint system, from the above theorem, its induced scs C * is. Furthermore, just like C rt , we can give in C * a sound and complete compositional interpretation of formulae in S4.

We now define the compositional interpretation in our constraint system C * of modal formulae. Notice that C * is a powerset ordered by reversed set inclusion, hence it is a frame (Remark 3.2.1). Recall our definition of the negation constraint ∼ c for frames (Definition 3.2.1).

Definition 5.3.2. Let φ be a modal formula from the modal language L n (Φ). The interpretation of φ in C * is inductively defined as follows:

C * p = {(M, s) ∈ ∆| π M (s)(p) = 1 } C * φ ∧ ψ = C * φ C * ψ C * ¬φ = ∼ C * φ C * i φ = [[[ C * φ ]]] i
where ∆ is the set of all pointed Kripke structures (M, s) such that M ∈ M n (Φ).

Notice that i φ is interpreted in terms of the global operation. Since C * is a power-set ordered by reversed inclusion the lub is given by set intersection. Thus, from Equation 5.3.1

C * i φ = [[[ C * φ ]]] i = ω j=0 [C * φ ] j i = ω j=0 [C * φ ] j i (5.3.3)
In particular, notice that from Theorem 5.3.1 and Axiom EP.2 it follows that C * i φ = C * i ( i φ) as expected for an S4-knowledge modality; i.e., if agent i knows φ he knows that he knows it.

We conclude this chapter with the following theorem stating the correctness wrt validity of the interpretation of knowledge as as global operator. 5.3.3 we know that for every t such that s i -→ M * t we have (M * , t) ∈ C * ψ . We then conclude that for k = 0, 1, . . ., (M * , s k ) ∈ C * ψ . We use the induction hypothesis to conclude that (M, s k ) ∈ C * ψ for k = 0, 1, . . . as wanted.

Summary

In this chapter we created a variation of the Kripke constraint system where the space function is a closure operator that mimics S4 knowledge (i.e. the space function is extensive and idempotent). We then proceeded to encode S4 knowledge using a scs with the global information operator from Definition 2.2.3 restricted to one agent as the space function. We then proved the completeness of this constraint system with respect to S4 epistemic logic formulae. The work presented in this chapter is taken from [GHP + 16].

In the next chapter we will study how concepts of time such as future and past can be properly interpreted as space and extrusion in our constraint systems.

Chapter 6 Algebraic view of LTL

In this chapter we device a mechanism to specify time properties using spatial constraint systems with extrusion. For this, we take Linear Temporal Logic (LTL) and give its modalities a semantic interpretation in terms of space and extrusion. The idea is to encode the semantic model of LTL (sequences of states) [START_REF] Pnueli | The temporal logic of reactive and concurrent systems[END_REF] in the form of a constraint system. We then denote future as the space function and proceed to derive an extrusion, which in turn will denote past. Kripke semantics for temporal logics have been studied before [START_REF] Vladimir | Admissibility of logical inference rules[END_REF], thus it is theoretically possible to instead use our Kripke scs. Regardless, we shall take the direct approach of creating a new constraint system encoding the semantic model of LTL.

Linear Temporal Logic

Linear Temporal Logic (LTL) is a formalism initially conceived for specification of program properties, its main aim is to provide a logic for expressing timed behavior. A comprehensive guide for LTL can be found in [START_REF] Pnueli | The temporal logic of reactive and concurrent systems[END_REF], nonetheless we will introduce it in two parts accordingly to its expressivity regarding time behavior. We give intuitions on the modal operators. The formula ϕ (read as next ϕ) means "in the next instant, ϕ holds" and formula ϕ (read as always ϕ) is interpreted as "henceforth, ϕ is true". We define a dual of as ϕ def = ¬ ¬ϕ (read as eventually ϕ) meaning "ϕ will eventually be true". We proceed to describe a semantic model for LTL which is similar to that of Definition 4.1.2. Having defined the semantic model we are now able to formalize the semantic meaning of an L LTL formula. Similarly to the semantics of modal logics, we say ϕ holds in (M, s i ) whenever (M, s i ) |= ϕ. Validity and satisfiability in a model M is defined in the same manner as in modal logic. Definition 6.1.3 (LTL semantics). Consider a relation |= between states of LTL models and formulas from the set L LTL (Φ). We define it inductively as follows:

Future

• (M, s i ) |= p iff π M (s i )(p) = 1 • (M, s i ) |= ϕ ∧ ψ iff (M, s i ) |= ϕ and (M, s i ) |= ψ • (M, s i ) |= ¬ϕ iff (M, s i ) |= ϕ • (M, s i ) |= ϕ iff (M, s i+1 ) |= ϕ • (M, s i ) |= ϕ iff (M, s j ) |= ϕ for all j ≥ i • (M, s i ) |= ϕ iff there exists j ≥ i such that (M, s j ) |= ϕ

Past

Reasoning about properties in the past is also a desired feature. In order to obtain this, we redefine the LTL language by adding past operators. Definition 6.1.4 (LTL Language). Given a set Φ of atomic propositions, the language L LTL (Φ) is the set of modal formulas constructed with the following syntax:

ϕ, ψ := p | ϕ ∧ ψ | ¬ϕ | ϕ | ϕ | ϕ | ϕ
where p ∈ Φ. Logical operators ⇒, ⇔ and ∨ are defined in the standard way.

The intuition on the future operators (i.e. next, always and eventually) remain the same. The formula ϕ (read as previous ϕ) means "in the last instant, ϕ was true". Formula ϕ is interpreted as "ϕ has always been true" and finally, we also define a dual of as ϕ def = ¬ ¬ϕ (read as once ϕ) meaning "ϕ was once true".

Again, we use the model defined in 6.1.2 to complement the semantics of LTL by including the past operators. The semantics of future operators remain the same. Definition 6.1.5 (LTL-Semantics). We complement Definition 6.1.3 with the following:

• (M, s i ) |= ϕ iff i > 0 and (M, s i-1 ) |= ϕ • (M, s i ) |= ϕ iff (M, s j ) |= ϕ for all j ≤ i • (M, s i ) |= ϕ iff there exists j ≤ i such that (M, s j ) |= ϕ

Weak Past

Because state s 0 does not have a past, (M, s 0 ) |= ϕ is defined as false for all models M and all formulas ϕ. We can define a weaker version of the previous operator (written as ˜ ). Definition 6.1.6 (Weak past semantics). The weak past operator is semantically defined as follows:

• (M, s i ) |= ˜ ϕ iff i = 0 or (M, s i-1 ) |= ϕ
Using Definition 6.1.6 we can obtain the next theorem:

˜ ϕ ⇔ ¬ ¬ϕ
Moreover, (M, s 0 ) |= ˜ ϕ is equals to true for all models M and all formulas ϕ. This allows us to identify the first instant in time with the following definition:

first def = ˜ false

Constraint systems for LTL models

The semantic model of LTL (Definition 6.1.2) uses an infinite sequence of states to represent the timeline of a program execution [START_REF] Pnueli | The temporal logic of reactive and concurrent systems[END_REF]. We will encode this semantic structure in a constraint system following the same methodology used in our Krikpe scs (Definition 4.2.1). Definition 6.2.1 (Time scs). Let S(Φ) be a non-empty set of LTL models over Φ. Let ∆ be the set of all pairs (M, s i ) such that M ∈ S(Φ) and s i is a state of the sequence S M . We define the Time scs for S(Φ) as the following single agent scs:

T(S(Φ)) = (Con, , [•])
where Con = P(∆), c 1 c 2 iff c 2 ⊆ c 1 and for every c ∈ Con

[c] def = {(M, s i ) ∈ ∆ | (M, s i+1 ) ∈ c}.
Remark 6.2.1. Just as the Kripke scs, T(S(Φ)) is a complete algebraic lattice given by a powerset ordered by ⊇ where is the set intersection, the top element false is ∅ and bottom element true is ∆. Considering they are of the form (P(U ), ⊇) where meets are unions and joins intersections, we can also conclude that T(S(Φ)) is a frame and that the operators → and ∼ coincide with the constructions ⇒ and ¬ defined in Remark 2.2.1.

We nonetheless need to account for it being a spatial cs. As mentioned before, the weak past operator ˜ is the dual of the past operator . However, for the sake of completeness we also give cs semantics to the weak past operator. Definition 6.3.2. Let T ↑ (S(Φ)) be the scs-e in Definition 6.2.2. We augment the denotation T ↑ ϕ of formula ϕ from L LTL (Φ) to include the operator ˜ as follows:

T ↑ ˜ ϕ = ↑ T ↑ ϕ
Furthermore, using the extensional definitions in 6.2.1 and the semantics of Definition 6.3.1 we can verify the claim of the formula ˜ false capturing the initial states of the LTL models.

Proposition 6.3.1. if (M, s i ) ∈ T ↑ ˜ false then i = 0. Proof. T ↑ ˜ false = ↑ T ↑ false = ↑(∅) = {(M, s i ) ∈ ∆ | i = 0 or (M, s i ) ∈ ∅} = {(M, s i ) ∈ ∆ | i = 0}.

Summary

After introducing Linear Temporal Logic and following the same methodology of the last two chapters, we defined Time constraint systems as our main structures to encode time properties. We derived two extrusion operators using Theorems 3.4.1 and 3.4.3, which were then later shown to have the same intentional description as those of the normal and weak past operators of LTL. Moreover, we gave a semantic characterization of LTL formulae along with the definition of validity. Using this semantic interpretation we showed the relation between the normal and weak past operators and proved the ability of a specific LTL formula to capture the initial instant of time. Although the results here are complete, their publication is still a work in progress and will be done accordingly.

Chapter 7

Conclusions and Related Work

We finalize this document with concluding remarks and expand further on the problem of extrusion. We give some related approaches mainly at the conceptual level of the inverse of space and potential applicability of our results. We also discuss possible future research to enhance the epistemic expressivity of constraint systems and their relation to multi-agent interactive systems.

In this thesis we studied spatial constraint system (scs); complete lattices equipped with self-maps accounting for the concept of agent spaces. These maps are called space functions. We then proceeded to define spatial constraint systems with extrusion (scse); an extension of scs with a second set of self-maps called extrusion functions. We regard extrusion functions as the right inverse of space functions.

We formalized scse by building upon notions and concepts from order (domain) theory, epistemic (doxastic) theories, and the algebraic treatment of logic in [START_REF] Vickers | Topology via logic[END_REF][START_REF] Di Pierro | An algebraic perspective of constraint logic programming[END_REF]. Alternatively, we adapted the definition of implication in Heyting Algebras [START_REF] Vickers | Topology via logic[END_REF] to our constraint systems in order to have operators for negation and implication of elements. With these new concepts, we were able to model situations with concurrent and epistemic behaviors such as process mobility, communicating agents and hoaxes. Furthermore, we addressed the problem of constructing an extrusion function given a space function. This is an important aspect because building up the constraint system anew might not be an option; the user may wish to extend a previous scs with some fixed space functions. Supposing the axiom of choice, the sufficient and necessary condition for the existence of an extrusion function is surjectivity. Checking surjectivity on the space function might be expensive (depending on the number of elements of the cs), therefore we gave a necessary condition significantly easier to check (i.e. space consistency).

We also stated sufficient conditions for explicit constructions of an extrusion function given a space function. One of these explicit constructions allows the extrusion function to be distributive and strict (properties that space functions fulfill by definition). Finally, we also studied properties of space and extrusion such as space consistency, completeness, automorphisms and Galois connections.

As a first application of our results, we devised an epistemic logic of belief and utterance where the modality of utterance is the right inverse of the belief modality. We also defined common epistemic behaviors such as opinions and hoaxes, and then proceeded to characterize the logic by giving semantics for each operator and modality. The semantics were defined in terms of a Kripke scse and the two modalities were also demonstrated to form a Galois connection.

We also showed that Kripke spatial constraint system can represent S4 knowledge by using a global space construction. It was then proved that this representation fulfills the S4 axioms of knowledge -i.e., extensiveness and positive introspection. This encoding was also demonstrated to be sound and complete with respect to formulae of the S4 axiom system. Finally, we created Time constraint systems and used them to encode formulas of LTL. With this, we opened the possibility of expressing time behavior using algebraic expressions from scs with extrusion. A particular feature was the semantic definition of a normal and weak versions of the past operator that were shown to correspond to the explicit constructions of extrusion in the first half of this thesis.

All in all, we have argued that belief, knowledge and utterances correspond, respectively, to the spatial concepts of local space, global space, and extrusion. Alternatively, the concepts of future and past also correspond to space and extrusion, where different versions of the past may be definable. The Table 7.1 in the Appendix section gives a summary of the correspondence between lattice operators of spatial constraint systems, their instantiation in the Kripke constraint system, and their epistemic and time counterparts.

Related and Future Work

Our scse's can be used as constraint systems for concurrent constraint programming (ccp) calculi [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]. This way processes in these calculi would be able to express spatial mobility and epistemic/social behaviors. The issue of extending ccp calculi to provide for mobility and distributed information has been previously addressed in [DRV98, Rét98, GP00, BKJG02]. In [START_REF] Réty | Distributed concurrent constraint programming[END_REF][START_REF] Francisco Díaz | Pi+calculus: A calculus for concurrent processes with constraints[END_REF] processes can send constraints using communication channels much like in the π-calculus. Moreover, [GP00] extends ccp with primitives for process mobility within a hierarchically organized network described as a tree. Additionally, the authors of [START_REF] Brim | Modelling multi-agent systems as synchronous concurrent constraint processes[END_REF] create an extension to ccp where agents maintain a local store and communicate through a global store. In [START_REF] Olarte | The expressivity of universal timed ccp: undecidability of monadic fltl and closure operators for security[END_REF] temporal ccp process can transmit variables using existential and universal quantification. More recently, in [START_REF] Olarte | Dynamic spaces in concurrent constraint programming[END_REF] the authors added the notion of link mobility to spatial and linear ccp using a proof-theoretical approach. Furthermore, distributed versions of ccp in a network of nodes are studied in [START_REF] Bortolussi | A distributed and probabilistic concurrent constraint programming language[END_REF]. Our approach differs from these works in both conception, technical development, and applications. We view extrusion as an inverse of space and develop this concept using lattice theory and domain theory. None of the previously-mentioned works is concerned with applications for reasoning about epistemic behavior.

Another work that has influenced the design of scs's with extrusion is the ambient calculus [START_REF] Cardelli | Mobile ambients[END_REF]. Ambient provides for the specification of processes that can move in and out within their spatial hierarchy. It does not, however, address posting and querying epistemic information within a spatial distribution of processes. Our notion of extrusion is reminiscent of Ambient's notion of subjective mobility.

In future work we plan to investigate a domain-theoretical approach to Ambient concepts such as acid operations. Intuitively, an acid operation can cause space to be disolved, and thus we may be able to characterize it as a function ac i that "undoes" space, i.e., ac i

• [•] i = id.
The process calculi in [BJPV09, BM07, FRS01] provide for the use of assertions within π-like processes. They are not concerned with spatial distribution of information and knowledge. These frameworks are very generic and offer several reasoning techniques. Therefore, it would be interesting to see how the ideas here developed can be adapted to them.

Inverse modalities have been used in temporal, epistemic and Hennessy-Milner logic. For example, in [START_REF] Ryan | Counterfactuals and updates as inverse modalities[END_REF] the logical properties and consequences of introducing inverse modalities in a generic modal logic are thoroughly explained. Also in [START_REF] Phillips | A logic with reverse modalities for history-preserving bisimulations[END_REF] the authors put forward an extension of Hennessy-Milner logic with a reverse modality for expressing concurrent behavior. In future work we plan to develop an algebraic presentation of scse's by building upon the axiomatization of logics with reverse modalities given in [START_REF] Ryan | Counterfactuals and updates as inverse modalities[END_REF].

Epistemic logics have been widely applied to distributed systems; [START_REF] Fagin | Reasoning about knowledge[END_REF] gives a good summary of the subject. This work is all aimed at analyzing distributed protocols using epistemic logic as a reasoning tool. The work has been very influential in setting previous stages for the present work but it is not closely connected to the present proposal to put epistemic concepts into constraint systems and thus algebraic structures. Concerning time concepts, Kripke semantics for temporal logics have been studied before [START_REF] Vladimir | Admissibility of logical inference rules[END_REF]. Nonetheless, this thesis gives a direct algebraic characterization of the semantic models of LTL used in [START_REF] Pnueli | The temporal logic of reactive and concurrent systems[END_REF].

Social phenomena such as lies, utterance, opinions have been recently studied in epistemic (doxastic) logic [VDVESW12, VD14, SCH10]. We follow [START_REF] Van Ditmarsch | On the logic of lying. In Games, actions and social software[END_REF] and regard lies as utterances by an agent that are inconsistent with their beliefs. Apart from our domain-theoretical treatment of these epistemic concepts, a difference with [VDVESW12, VD14, SCH10] is that we developed utterance as an inverse modality (upper adjoint) of belief. As future work we would like to investigate how the dynamic-logic approach in [VDVESW12, SCH10, VD14] of the above-mentioned epistemic phenomena can be incorporated in our constraint systems.

The question of whether knowledge is definable in terms of belief has played an important role in epistemology. In [START_REF] Joseph Y Halpern | Defining knowledge in terms of belief: The modal logic perspective[END_REF] the authors studied this question in the framework of epistemic and doxastic logics. They proved that epistemic logic S5 cannot/can be explicitly/implicitly defined in terms of the belief logic KD45. Here we defined belief and knowledge in terms of space. The notion of knowledge we considered corresponds to the epistemic logic S4 while the notion of belief is KD [START_REF] Fagin | Reasoning about knowledge[END_REF]. We plan to address the question of whether S5 knowledge and KD45 belief can be defined in our spatial constraint systems.

An approach closely related to ours is the spatial logics for concurrency from [START_REF] Caires | A spatial logic for concurrency (part i)[END_REF][START_REF] Caires | A spatial logic for concurrency (part ii)[END_REF]. In this work they also take spatial location as the fundamental concept and develop modalities that reflect locality. Rather than using modal logic, they use the name quantifier that has been actively studied in the theory of freshness of names in programming languages. Their language is better adapted to the calculi for mobility where names play a fundamental role and the concept of freshness of a name is exploited to control the flow of information. In our framework, the epistemic concepts are manifested directly in the syntax and the semantics. It would be interesting to see how a name quantified scs would look and to study the relationship with the framework in [START_REF] Caires | A spatial logic for concurrency (part i)[END_REF][START_REF] Caires | A spatial logic for concurrency (part ii)[END_REF].

Concurrent systems may allow user/agents to join the network during computation. Therefore the number of agents can be unbounded. Other potential research direction for our work is therefore to generalize spatial constraint system (and thus scs with extrusion) by allowing an unbounded number of agents.

Quantitative reasoning is also another direction where constraint systems can increase their epistemic expressivity. Currently, there is a plethora of approaches to make probabilistic extensions to modal and epistemic logic [START_REF] Fagin | Reasoning about knowledge and probability[END_REF]. To the best of our knowledge no algebraic treatment of them exists. An attractive future endeavor would be an extension of our algebraic models that will allow us to add weights to agents beliefs and informations within the hierarchy of the system. The approach would be to generalize the notion of belief as a form of probabilistic measure on epistemic statements to express meaningful and ambiguous behavior commonly found in social scenarios. For instance, suppose that c represents a statement, the perception of which may change according to space, time or the individual -e.g., an inherently subjective statement about politics, religion, or sports. We may have, for example, that agent i initially believes that c holds with some probability p < 1. After interacting with other agents or moving across the hierarchy, agent i may end up convinced that c is true (or that it is false). We would also be able to express that agent i believes c more than agent j does and other similar statements related to social interaction. This quantitative modeling provides a more faithful representation of virtual social behavior in distributed networks, where information certainty changes parallel to its dissemination.

After introducing quantitative reasoning to our structures, a legitimate step would be to extend and/or characterize existing epistemic logics (such as the one in [START_REF] Baltag | Dynamic epistemic logics of diffusion and prediction in social networks[END_REF]) that are already able to express social behavior similar to the one mentioned above. All this whilst verifying a through correspondence to the concepts of validity and satisfiability from the logic. This in turn will allows us to reason about epistemic situations and verify their validity from an algebraic point of view, as well as see the properties and interaction of the epistemic operators. For example we could verify if the social phenomena 'group polarization' is present in a certain utterance of opinions in a multi-agent environment. Group polarization refers to the tendency of groups to hold more extreme beliefs than the initial individual beliefs of its members.

Correspondence between operators

Below is a table summarizing the correspondence between the lattice operators and those of the logical languages we have characterized in this thesis. The correspondence, although developed formally here, is meant to better reflect the direct relation of the concepts of space and extrusion to more particular interpretations. Résumé : Système de contraintes (cs -selon l'acronyme anglais) sont formalismes déclaratifs de la théorie de la concurrence tels que les algèbres de processus (p. ex. ccp). Les cs sont souvent représentés par des treillis : ses éléments, appelées contraintes, représentent des informations partiales tandis que l'ordre du treillis correspond à des implications. Récemment, une notion appelée "système de contraintes spatiales à n-agents" a été développée pour représenter l'information dans les systèmes multi-agents et spatialement distribués. Un cs spatial peut être utilisé pour spécifier l'information partiale contenue dans l'espace d'un certain agent (information locale), ou d'un point de vue épistémique, l'information qui est considérée vrai pour un certain agent (croyance). Les cs spatiales, néanmoins, ne fournissent pas de mécanismes pour la spécification de la mobilité de l'information ou des processus. Dans cette thèse nous avons développé la théorie des systèmes de contraintes spatiales avec des opérateurs pour spécifier le déplacement des informations et processus entre les espaces. Nous étudions les propriétés de cette nouvelle famille de cs et nous illustrons ses applications. Ces nouveaux opérateurs nous apportent de l'extrusion d'informations/processus, et du point de vue épistémique, l'extrusion correspond à ce que nous appelons énonciation ; une information qu'un agent souhaite communiquer à d'autres mais qui peut être inconsistante avec ses croyances. Des énonciations peuvent donc être utilisées pour exprimer des notions épistémiques tels que les canulars ou les mensonges.

Globalement, les cs peuvent exprimer la croyance/énonciation et la connaissance en utilisant respectivement une paire de fonctions espace/extrusion, et un opérateur spatial dérivé qui représente l'information globale. Par ailleurs, nous montrons qu'en utilisant un type précis de nos cs nous pouvons aussi représenter la notion du temps comme une séquence d'instances. Title: Opinions, Lies and Knowledge. An Algebraic Approach to Mobility of Information and Processes. Keywords: Constraint Systems, Mobility, Epistemic Logic, Lies, Concurrency Theory.

Abstract: Constraint systems (cs) are declarative formalisms from concurrency theory such as process calculi (e.g. ccp). Cs are often represented as lattices: their elements, called constraints, represent partial information and their order correspond to entailment. Recently a notion of n-agent spatial cs was introduced to represent information in spatially distributed multi-agent systems. A spatial cs can be used to specify partial information holding in a given agent's space (local information), or from an epistemic point of view, a piece of information the agent considers true (beliefs). Spatial cs however do not provide mechanisms for specifying the space mobility of information/processes.

In this thesis, we develop the theory of spatial cs with operators to specify information and processes moving between spaces. We investigate the properties of this new family of cs and illustrate their applications. The new operators provide for process/information extrusion, and from an epistemic point of view, said extrusion corresponds to what we shall called utterance; information that an agent communicates to others but that may be inconsistent with the agent's beliefs. Utterances can express epistemic notions such as hoaxes, opinions and lies.

On the whole, cs can express the epistemic notions of belief/utterance and knowledge by means of, respectively, a space/extrusion function pair and a derived spatial operator that specifies global information. We shall also see that, by using a specific construction of our constraint systems, we can encode the notion of time as an arbitrary nesting of spaces representing a sequence of instances.

  U.L.I.A. Among the Stars (2014) -The Boys are Back (2009)

  i. a a (reflexivity), ii. a b and b a imply a = b (antisymmetry), iii. if a b and b c then a c (transitivity).

Figure 2 . 1 -

 21 Figure 2.1 -Hasse diagram of a poset

  Definition 2.1.2 (Directed/Filtered set). Given a poset (P, ), we say that D ⊆ P is an upward directed set (resp. downward directed set) if for every a, b ∈ D there exists c ∈ D s.t. a c and b c (resp. c a and c b).

  Theorem 2.1.1. Let L be a lattice. For all a, b, c ∈ L we have that: -(a b) c = a (b c) and (a b) c = a (b c) a b = b a and a b = b a a a = a and a a = a a (a b) = a and a (a b) = a

Figure 2

 2 Figure 2.2 -The M 3 and N 5 lattices, both are non-distributive

Theorem

Figure 2

 2 Figure 2.3 -A Herbrand constraint system

  e., satisfied by every truth assignment. Remark 2.2.1 (Boolean Implication). Constraint systems of the form (P(U ) ⊇) as B(Φ) in Example 2.2.2, are standard examples of a Boolean algebra [GHK + 03]. Given the constraints c, d ∈ P(U ), the negation constraint ¬c and the implication constraint c ⇒ d in P(U ) are defined as U \ c and ¬c ∪ d, respectively.

  Heyting implication c → d in our settings corresponds to the weakest constraint one needs to join c with to derive d: The greatest lower bound {e | e c d}. Similarly, the negation of a constraint c, written ∼ c, can be seen as the weakest constraint inconsistent with c, i.e., the greatest lower bound {e | e c false} = c → false. Definition 3.2.1 (Heyting Implication and Negation). Let C be a constraint system (Con, ). Define c → d as: {e | e c d} (3.2.1) and ∼ c as c → false.

Figure 3

 3 Figure 3.1 -The Herbrand sub-lattice N 5

  first prove that c d whenever c → d = true. Suppose c → d = true, we join c to both sides to obtain c (c → d) = c. Using Modus-Ponens (Lemma 3.2.1) we get c d = c and conclude that c d. Finally we prove that if c d then c → d = true. Recall that c → d = S where S = {e | e c d}. Suppose c d then true ∈ S and c → d = S = true.

  Example 3.2.1 (Hoax). Suppose that c d = false. The assertion [c ↑ i d] i (3.2.3) specifies an agent i that believes c and wishes to utter/extrude d. Since c and d are inconsistent and agent i believes c we can regard d as a hoax or an intentional lie by agent i. It follows from Definition 3.2.1 that by taking d = ∼ c we obtain the weakest statement inconsistent with c. In other words ∼ c is the weakest/most general lie by agent i wrt his or her belief c.

  Lemma 3.4.1 (Directed Fibers). Let C be an scs and let [•] i be a surjective space function of C. The fiber of any constraint c of C under [•] i is a directed set.

  over finite joins as far as agent i can tell. The following proposition states this formally Let [•] i be the space function of agent i in an scse. We write c ≈ i d iff [c] i = [d] i . The equivalence relation ≈ i is sometimes referred to as the kernel of [•] i . Intuitively, c ≈ i d expresses the idea that c and d are equivalent to agent i. Proposition 3.4.1. Let C be an scse with constraints in Con, and let ↑ i be the extrusion function of the agent i in C. Then 1. ↑ i true ≈ i true, and

  Theorem 3.4.2 (Impossibility of Distributed Extrusion). There exists a surjective and continuous space function [•] i of an scs (Con, ) such that: For every right inverse g of [•] i there are c, d ∈ Con such that g(c d) = g(c) g(d).

Figure 3

 3 Figure 3.2 -A one-agent scs. Gray arrows depict a surjective and continuous space function over N ∪ {∞}.

  Remark 3.5.1. If [•] i is surjective, then for all a ∈ Con there exists c ∈ Con where a = [c] i for any i ∈ {1, . . . , n} in a n-scse. Now, this means there exist c ∈ Con and d ∈ Con s.t. [c] i = a = [d] j for all 1 ≤ i, j ≤ n. In an epistemic context, this property might seem unusual at first look and even hint to an equality of seemingly unrelated beliefs from different agents. However, beliefs c and d are indeed related and d = ↑ j [c] i is their actual relation.

  φ, ψ, . . . := p | φ ∧ ψ | ¬φ | i φ where p ∈ Φ and i ∈ {1, . . . , n}. Notation 4.1.1. Disjunction and implication are defined in the standard way; φ ∨ ψ def = ¬(¬φ ∧ ¬ψ) and φ ⇒ ψ def = ¬φ ∨ ψ. We also define a dual of the modality; i φ def = ¬ i ¬φ.

  Definition 4.1.2 (Kripke Structures). An n-agent Kripke structure (KS) M over a set of atomic propositions Φ is a tuple:

  to denote the worlds agent i considers possible from a state s of KS M . Alternatively, we writeW -1 i (M, s) = {t | t i -→ M s}to denote the worlds from which agent i considers state s possible. The interpretation function π tells us what primitive propositions are true at a given world: p holds at state s iff π(s)(p) = 1. We use π M to denote the interpretation π of the KS M .

  as wanted. It remains to prove Claim C.1: [↑ i c] i = c for every c ∈ P(M ltu ).-Assume (H.3) (M, s) ∈ c, we wish to prove (M, s)∈ [↑ i c] i .From the definition of [•] i , we need to show that (H.4) for any t if s i -→ M t then (M, t) ∈ c. From H.3, H.4 and Equation 4.3.4 we obtain (M, s) ∈ [↑ i c] i as we wished.

  Proposition 4.3.4. The formulae in Equations 4.3.5, 4.3.6, 4.3.7 and 4.3.8 are valid in BU n .

  The above gives a brief summary of the use in[START_REF] Knight | Spatial and epistemic modalities in constraintbased process calculi[END_REF] of Kuratowski closure operators [c] i to capture knowledge. In what follows we show an alternative interpretation of knowledge as the global construct [[[c]]] G in Definition 2.2.3.

  [•] 1 , . . . , [•] n induces an s4cs with space functions [[[•]]] 1 , . . . [[[•]]] n . Definition 5.3.1. Given an scs C = (Con, , [•] 1 , . . . , [•] n ), we use C * to denote the tuple (Con, , [[[•]]] 1 , . . . , [[[•]]] n ).

  Theorem 5.3.1. Let C = (Con, , [•] 1 , . . . , [•] n ) be a spatial constraint system. If [•] 1 , . . . , [•] n are continuous functions then C * is an n-agent s4cs. Proof. We need to show that each [[[•]]] i satisfies S.1, S.2, EP.1 and EP.2. -We want to prove that [[[•]]] i satisfies S.1: [[[true]]] i = true. Since [•] i satisfies S.1 we can use [true] i = true to show, by induction on j, that [true] j i = true for any j. Then from Equation 5.3.1 we conclude [[[true]]] i = {true} = true as wanted.

  Theorem 5.3.2. C * φ = true if and only if φ is S4-valid.Proof. Let ∆ be the set of all pointed Kripke structures (M, s) such that M ∈ M. Similarly, let ∆ rt be the set of all pointed Kripke structures (M, s) such that M ∈ M rt . Given M ∈ M, we use M * ∈ M rt to denote the Kripke structure that results from M by replacing its accessibility relations with their corresponding transitive and reflexive closure.From Definitions 4.2.1 and 5.3.1 we conclude that ∆ = true in C * and ∆ rt = true in C rt . From Definitions 4.2.1 and Proposition 5.2.2, it suffices to prove thatC * φ = ∆ if and only if C rt φ = ∆ rt(5.3.4) Property 5.3.4 is a corollary of the following two properties:For all (M, s) ∈ ∆ rt : (M, s) ∈ C rt φ iff (M, s) ∈ C * φ (5.3.5a) For all (M, s) ∈ ∆ : (M, s) ∈ C * φ iff (M * , s) ∈ C * φ (5.3.5b) Proof of 5.3.5a Let (M, s) ∈ ∆ rt .We proceed by induction on the size of φ. The base case φ = p is trivial. For the inductive step here we show the most interesting case: φ = i ψ (the other cases follow directly from the induction hypothesis and the compositionality of the interpretations).(⇒) Assume (M, s) ∈ C rt i ψ . From Equation5.3.3 we want to prove that (M, s)∈ ω j=0 [C * ψ ] j i . Take an arbitrary sequence s 1 , s 2 , . . . such that s = s 0 i -→ M s 1 i -→ M s 2 i -→ M . . . . From Definition 4.2.1 and Equation5.3.3 it suffices to show that (M, s k ) ∈ C * ψ for k = 0, 1, . . . . From the assumption and Definition 4.2.1 we know that for every t such that s i -→ M t we have (M, t) ∈ C rt ψ . From the assumption we also know that i -→ M is transitive and reflexive: We thus conclude that (M, s k ) ∈ C rt ψ for k = 0, 1, . . . . From the induction hypothesis, we derive (M, s k ) ∈ C * ψ for k = 0, 1, . . . as wanted.(⇐) Assume (M, s) ∈ C * φ . From Equation 5.3.3, (M, s) ∈ ω j=0 [C * ψ ] j i . Then (M, s) ∈ [C * ψ ] i . From Definition 4.2.1, for every t such that s i -→ M t we have (M, t) ∈ C * ψ . From the induction hypothesis, we can conclude that (M, t) ∈ C rt ψ for every t such that si -→ M t. This shows that (M, s) ∈ [C rt ψ ] i as wanted since [C rt ψ ] i = C rt φ .Proof of 5.3.5b Let (M, s) ∈ ∆. We proceed by induction on the size of φ. The base case φ = p is trivial. For the inductive step, we show the case φ = i ψ (as in the previous proof the other cases follow directly from the induction hypothesis and the compositionality of the interpretations).

(

  ⇒) Assume (M, s) ∈ C * φ . Take an arbitrary sequence s 1 , s 2 , . . . such thats = s 0 i -→ M * s 1 i -→ M * s 2 i -→ M * . . . . From Equation 5.3.3 it suffices to show that (M * , s k ) ∈ C * ψ for k = 0, 1, . . . . Notice that i -→ M * is the transitive and reflexive closure of i -→ M , thus we have s( i -→ M * ) * s k if and only if s i -→ M * s k . Consequently, let us then take an arbitrary t such that s i -→ M * t: It is sufficient to show that (M * , t) ∈ C * ψ . Since i -→ M * is the transitive and reflexive closure of i -→ M , there must exist s = t 0 i -→ M t 1 i -→ M t 2 i -→ M .. . such that t j = t for some j ≥ 0. From the assumption and Equation 5.3.3 we have (M, s)∈ ω j=0 [C * ψ ] j i . Thus for any t 1 , t 2 , . . . such that s = t 0 i -→ M t 1 i -→ M t 2 i -→ M . . . we have (M, t k ) ∈ C * ψ for k = 0, 1, . . . . We conclude that (M, t) ∈ C * ψ ,and thus from the induction hypothesis we obtain (M * , t) ∈ C * ψ as wanted. (⇐) Assume (M * , s) ∈ C * φ . Take an arbitrary sequence s 1 , s 2 , . . . such that s = s 0 i -→ M s 1 i -→ M s 2 i -→ M . . .. From Equation 5.3.3, it suffices to show that (M, s k ) ∈ C * ψ for k = 0, 1, . . . . Notice that s i -→ M * s k for k = 0, 1, . . . since i -→ M * is the transitive and reflexive closure of i -→ M . From the assumption and Equation

Definition 6 .

 6 1.1 (LTL Language). Given a set Φ of atomic propositions, the language L LTL (Φ) is the set of modal formulas constructed with the following syntax: ϕ, ψ, . . . := p | ϕ ∧ ψ | ¬ϕ | ϕ | ϕ where p ∈ Φ. Logical operators ⇒, ⇔ and ∨ are defined in the standard way.

Definition 6 .

 6 1.2 (LTL model). Given a set Φ of atomic propositions, a model M over Φ is a pair (S, π) where: -S = s 0 , s 1 , s 2 , . . . is a sequence of states, π : S → (Φ → {0, 1}) is an interpretation for every p ∈ Φ. Notation 6.1.1. The states of model M are considered instants in a timeline (denoted by S M ). Similar to Notation 4.1.2, we write L LTL when Φ is unimportant and use π M to stand for the interpretation π from model M .

Proposition 6 .

 6 2.1. Let T(S(Φ)) = (Con, , [•]) be a Time scs. The function [•] is a space function.

  Index(M, s), pointed Kripke structure, 48(Con, , [•] 1 , . . . , [•] n ), spatial constraint system, scs, 21 (Con, , [•] 1 , . . . , [•] n , ↑ 1 , . . . , ↑ n ),scse, scs with extrusion, 24 Con, set of constraints, 17 ∆, set of pointed Kripke structures, 48 ⇑ G , global extrusion, 30 Φ, set of primitive propositions, 19 ⇒, boolean implication, 19 [[[•]]] G , global information of G, 22 [[[•]]] i , global space of agent i, 65 ≈ i , kernel, equivalence for i, 34 B i , belief operator, 55 ⊥, bottom, 14 ∼, heyting negation, 25 ↑ i , extrusion function, 24 false, all (possibly inconsistent) information, 17 i -→ M , accessibility relation, 46 B(Φ), boolean constraint system, 19 B • , boolean interpretation, 19 T(S(•)), Time scs, 74 ↑(•), ↑(•), 76 [•], 74 T ↑ (S(•)), Time scs-e, 77 T ↑ • , 77 A(•), set of assignments, 19 C, (Con, ), constraint system, cs, 17 herbrand, 18 L LTL ( ), 73 L BU n (•), modal language for utterance, 55 L 0 (•), propositional language, 19 L n (•), modal language, 45 M rt , set of reflexive and transitive ks, 63 M lt , set of left-total ks, 52 M ltu , set of left-unique left-total ks, 52 M n (•),M set of all

  Haar, Salim Perchy, Camilo Rueda, and Frank D.

Valencia. Belief, knowledge, lies and other utterances in an algebra for space and extrusion. Accepted to the Journal of Logical and Algebraic Methods in Programming, JLAMP, 86, 2016. -Stefan Haar, Salim Perchy, Camilo Rueda, and Frank D. Valencia. An algebraic view of space/belief and extrusion/utterance for concurrency/epistemic logic. In Proceedings of the 17th ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming, PPDP 2015, pages 161-172, 2015. -Michell Guzman, Salim Perchy, Camilo Rueda, and Frank D. Valencia. Deriving inverse operators for modal logics. In Accepted to the 13th International Colloquium on Theoretical Aspects of Computing, ICTAC 2016, 2016. -Salim Perchy and Frank D. Valencia. Opinions and beliefs as constraint system operators. In Technical Communications of the 31st International Conference on Logic Programming, ICLP 2015, 2015.

  The proof of this claim is by contradiction: Suppose that H.1 c d but H.2 ↑ i c ↑ i d. Let us treat H.2 by cases. We use c d to mean that c is not related to d, i.e.,

  1, Equation 4.3.4, and the fact that accessibility relations in K(M ltu ) are left-unique, there exists a unique state, let us call it s in what follows, such that s M t and (M, s) ∈ c. From H.2 we know that there exists some

i -→

  in fact a Kuratowski closure operator and thus satisfies the epistemic axioms EP.1 and EP.2 above: It is easy to see that [[[c]]] i satisfies [[[c]]] i c (EP.1). Under certain natural assumption we shall see that it also satisfies [

  Opinions, Mensonges et Connaissance. Une Approche Algébrique à la Mobilité de l'Information et des Processus. Mots clés : Restrictions, Applications Mobiles, Logique Épistémique, Detection de Mensonges, Théorie de Treillis.

	Titre :	, , join, lub, supremum, 13	directed set, 12
		, , , , order, 11
		, 12	filtered set, 12
		, entailment, 17	frame, cHa, 16
		M 3 , N 5 , 16	galois connection, 13
		, top, 14
		true, empty information, 17	hasse diagram, 12
		U i , utterance operator, 55
		c d, (c, d), (d, c) / ∈ ., 37	KS, Kripke structures, 45
		f -1 , pre-image, fiber, 32	lattice, 14
		i(•), space function for Kripke	M 3 , N 5 , 16
		structures, 48 i -1 (.), extrusion for Kripke space	algebraic, 15 complete, 14
		functions, 53	distributive, 15
		K utterance, 57	powerset, P, 14 sub-lattice, , 15 map, 12 continuous, upward-continuous, Scott-continuous, 17 downward-complete, 17 join-complete, 17 meet-complete, 17 types, 12
		K(S n (•)), Kripke scs, 48	order-automorphism, 39
		boolean algebra, 16	poset, 11
		bounds, 13 properties, 14	from s, 46 ¬, boolean negation, 19 s4cs, knowledge constraint system, 63 scs-de, scs with distributed extrusion,
		compact (finite) elements, 15	π, π M , states interpretation, 46 35
			→, heyting implication, 25
			[•], space function, 21
			[•] k , nested space of depth k, 22
			, , meet, glb, infimum, 13
			96

Kripke structures, 51 O i ,H i , opinion/hoax operators, 56 P, powerset, 12 S n (•), set of Kripke structures, 48 W i (M, s), M worlds accessible by i i , knowledge modality, 61 C φ , Kripke scs interpretation of φ, 49 C * , transitive and reflexive closure scs of C, 65 C * , transitive and reflexive closure of kripke scs C, 66 C rt , reflexive and transitive Kripke scs, 63 K ↑ (M ltu ), kripke scs with extrusion, 54 K ↑ φ , denotation of φ in the logic of

Acknowledgments

Proposition 4.3.2 (Left-unique surjectivity). The set M ltu satisfies surjectivity.

Proof. It follows from Claim C.1 in the proof of Lemma 4.3.1.

We now have an scs M ltu whose space functions are surjective. As we pointed out earlier, the Axiom of Choice implies the existence of extrusion functions (right inverses). We want, however, constructive definitions like the ones given in Section 3.4 with Theorems 3.4.1 and 3.4.3.

We cannot apply Theorem 3.4.3 because the spatial functions of M ltu are not meet-complete. For a counter-example take (M, s) with W i (M, s) = {t, u}. Recall that the meet in K(M ltu ) is set union. One can verify that {(M, s)} =

Nevertheless, the space functions of any Kripke scs are continuous.

Proposition 4.3.3. The space functions of K(M) are continuous.

Proof. It suffices to show that space functions are join-complete (this implies continuity): i.e., that for every agent i and every set S ⊆ P(∆) we have

as wanted.

Therefore we can apply Theorem 3.4.1 and derive the following extrusion function for each [•] i in K(M ltu ) :

Furthermore, we can show that the construction in Equation 4.3.2 is equivalent to the intensional definition given below.

Lemma 4.3.1. (Extrusion for Kripke Spaces). Let ↑ i be defined as in Equation 4.3.2 over the Kripke scs K(M ltu ). Then Derived Specifications We expect the following formula to be valid:

(4.3.5)

The above equation can be seen as agent i uttering ϕ. We can also derive specifications for common social behaviors such as:

An opinion O i (ϕ) by agent i is the utterance of a statement ϕ that the agent believes true. Thus we expect the validity of the following:

(4.3.6)

A hoax or intentional lie H i (ϕ) by agent i is the utterance of a statement ϕ that the agent believes false: Thus

should be valid. We also define duals of belief and utterance as:

The formula Bi ϕ states that ϕ is consistent with agent i's beliefs. Similarly Ûi ϕ means ϕ is consistent with agent i's utterances. We expect the validity of the following formulae:

opinions and hoaxes. We then proceeded to identify the necessary condition for the Kripke cs to be able to derive extrusion functions using Theorem 3.4.1. Subsequently, we characterized formulae of the bimodal logic with semantics using the Kripke cs with extrusion. In this way we were able to provide a semantic represenation of the definition of opinions and hoaxes. The work exposed in this chapter is contained in [START_REF] Guzman | Deriving inverse operators for modal logics[END_REF][START_REF] Haar | An algebraic view of space/belief and extrusion/utterance for concurrency/epistemic logic[END_REF]. The following chapter explains how to represent a stricter epistemic behavior, that of knowledge.

Axiom Property of R

Table 5.1 -Axiom correspondence to possibility relation Nonetheless, this axiom system alone usually does not capture properties frequently imputed by philosopher to knowledge. We list some of these common properties of knowledge as axioms.

For all agents i = 1 . . . n:

Axiom A.3 captures the notion of knowledge, if agent i knows something then it is true . In other words, agents have factual knowledge, they cannot know something that is untrue. This might not be the normal case, specially if the modality is interpreted as belief instead of knowledge. In this case A.3 should be replaced with A.6, i.e. the agent's set of beliefs are always consistent. Subsequently, we could improve readability by writing the modality as B (e.g. A.6 ¬B i (false)).

Some important axioms systems are combinations of these properties. Axiom system K together with axiom A.3 or axiom A.6 are called T and D respectively. Axiom system T with axiom A.4 and also axiom A.5 are called S4 and S5 respectively. Adding axiom A.4 and A.5 to D is called axiom system KD45.

Semantically speaking, all axioms in an axiom system must be valid wrt a certain class of KS. The axiom system K is valid wrt the class of KS whose possibility relations are unrestricted (written as M). Table 5.1 shows the correspondence between axioms and the properties of the possibility relation.

Axiom A.7 φ ⇒ K i ¬K i ¬φ is a consequence of axioms A.3 and A.5. Going by Notation 4.1.2, for all s, t, u ∈ S we have that R i is; -reflexive if (s, s) ∈ R i , -transitive whenever (s, t) ∈ R i and (t, u) ∈ R i then (s, u) ∈ R i , euclidian Proof. We show that [•] fulfills axioms S.1 and S.2: For S.1:

For S.2:

Because surjectivity and completeness (as in Definition 2.1.14) are central properties of our extrusion operator we also verify their validity in Time scs. The space function is join-complete:

The space function is meet-complete: We need to prove

Considering there always exists a unique successor to any state s i (i.e. s i+1 ), we can then conclude

Having proved that the space function of T(S(Φ)) is surjective as well as meet and join-complete, we proceed to apply Theorems 3.4.3 and 3.4.1. We define the next extrusion functions:

As we also did in Section 4.3, we obtain the intensional definitions of the above extrusion functions. Lemma 6.2.1. Consider the spatial cs T(S(Φ)) and let ↑(c) = [c] -1 and ↑(c) =

[c] -1 , we then have:

We need to prove that (M,

This means (M, s i-1 ) ∈ c, i > 0 and that ∃d ∈

, and together with the fact that (M, s i-1 ) ∈ c we arrive to the contradiction (M, s i ) ∈ d.

-We proceed to prove that if (M,

inductively defined as follows:

where ∆ is the set of all pairs (M, s i ) such that M ∈ S(Φ). A formula ϕ of

Remark 6.3.1. While it is easy to see that, semantically speaking, the LTL modality is the right inverse of the modality, we cannot say the same about the and LTL modalities (see the equations after Definition 3.2.2).

Given the above mentioned semantics, and using the axioms and properties of spatial constraint systems with extrusion, one is now able to verify the validity of axioms from the L LTL language. Lemma 6.3.1. The LTL formula ˜ ϕ ⇔ ¬ ¬ϕ is valid.

Proof. We split the formula into ˜ ϕ ⇒ ¬ ¬ϕ and ¬ ¬ϕ ⇒ ˜ ϕ. According to the concept of validity in Definition 6.3.1 we need to prove that T ↑ ˜ ϕ ⇒ ¬ ¬ϕ = true and T ↑ ¬ ¬ϕ ⇒ ˜ ϕ = true which semantically is the same as proving ↑ T ↑ ϕ → ∼ ↑∼ T ↑ ϕ = true and ∼ ↑∼ T ↑ ϕ → ↑ T ↑ ϕ = true. By using Lemma 3.2.2 it is sufficient to show that ↑ T ↑ ϕ ∼ ↑∼ T ↑ ϕ and ∼ ↑∼ T ↑ ϕ ↑ T ↑ ϕ that subsequently is the same as proving ↑ T ↑ ϕ = ∼ ↑∼ T ↑ ϕ . To prove this final form, we use the intensional definitions in Lemma 6.2.1 and replace ∼ with set complement as dictated in Remark 2.2.1 as follows:

∼ ↑∼ T ↑ ϕ = ∆\{(M, s i ) | i > 0 and (M, s i-1 ) ∈ ∆\T ↑ ϕ } = ∆\{(M, s i ) | i > 0 and (M, s i-1 ) ∈ T ↑ ϕ } = {(M, s i ) | i = 0 or (M, s i-1 ) ∈ T ↑ ϕ } = ↑ T ↑ ϕ .

Spatial