Spatial Constraint Systems with Extrusion

Get Complete Project Material File(s) Now! »

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 chap-ter, thus the reader is referred to [DP02, Bly06, GHK+03, AJ94] for an in-depth introduction to these topics.
Definition 2.1.1 (Poset). Given a set of elements P and a binary relation v on P , we define a partially ordered set (P; v) where for all a; b; c 2 P we have;
i. a v a (reflexivity),
ii. a v b and b v a imply a = b (antisymmetry),
iii. if a v b and b v c then a v c (transitivity).
The inverse of the ordering relation is denoted by the symbol w. We write a < b if a v b but a 6= b and a 6vb when a v b is false (we define = and 6wdually). It might be the case that two elements are not related (i.e. a 6vb and b 6va), we denote this by writing a k b.
We use a graphical representation of posets called the Hasse diagram wherein elements of the poset are represented as circles. An element is related to another if there a line is drawn connecting its circle with another one above it (see Figure 2.1 as an example).
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.
Definition 2.1.2 (Directed/Filtered set). Given a poset (P; v), we say that D P is an upward directed set (resp. downward directed set) if for every a; b 2 D there exists c 2 D s.t. a v c and b v c (resp. c v a and c v b).
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 v b in P implies f(a) v f(b) in Q,
ii. order-reflecting if f(a) v f(b) in Q implies a v 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; v) and (Q; v) and two maps f : P ! Q and g : Q ! P , the pair (f; g) form a [monotone] Galois connection if for all a 2 P and b 2 Q we have;
f(a) v b iff a v g(b): Lattices
Before introducing lattices, it is necessary to define the concept of bounds.
Definition 2.1.5 (Bounds). An element c 2 P is said to be an upper bound (resp. lower bound) of subset S in poset (P; v) if for all a 2 S we have that a v c (resp.c v a).
We name the sets of all possible lower and upper bounds as Sl and Su respec-tively. They can be calculated as follows:
Sl = fc 2 P j (8a 2 S) a w cg (2.1.1)
Su = fc 2 P j (8a 2 S) a v cg (2.1.2)
We call the minimal element of Su the least upper bound (lub) of S and the maximal element of Sl the greatest lower bound (glb) of S. When they exist, these two elements are unique because v 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 t d and c u d to denote the lub and glb of the set fc; dg respectively.
We now continue with the definition of a lattice.
Definition 2.1.6 (Lattice). Let L = (P; v) be a poset where c t d and c u d exist for all c; d 2 P , then L is also called a Lattice.
A lattice L can also be seen as an algebraic structure with operations for cal-culating bounds, i.e. L = (P; v; t; u). We proceed to introduce special important types of lattices.
Definition 2.1.7 (Complete lattice). A lattice L is a Complete Lattice if S d F 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 F d 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; v; t; u; >; ?).
Example 2.1.2. Let us consider again Figure 2.1.
We calculate 2u = f3; 4; 5g and 1u = f3; 5g, therefore f1; 2gu = f3; 5g and 1 t 2 = 3 because 3 v 5. In the same way we can calculate 3 u 4 = 2. Let S be the set of all elements of the lattice, then FS = 5 = > and d 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, L0 = (P(S); ; \; [; S; 😉 is called the reverse powerset lattice of S.
Both L and L0 in Example 2.1.3 are complete lattices. Some important prop-erties of the join and meet operators need to be introduced.
Theorem 2.1.1. Let L be a lattice. For all a; b; c 2 L we have that:
— (a t b) t c = a t (b t c) and (a u b) u c = a u (b u c)
— a t b = b t a and a u b = b u a
— a t a = a and a u a = a
— a t (a u b) = a and a u (a t b) = a
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 2 L, we say that k is compact if for every subset S of L k v FS implies k v FT 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 L0 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 nS is finite).
Definition 2.1.9 (Algebraic lattice). A complete lattice L is said to be algebraic if for each c 2 L we have; c = f k 2 K(L) j k v c g:
Intuitively, an algebraic lattice is a lattice where each element can be approx-imated 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 2 L we have; a t (b u c) = (a t b) u (a t 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.
Definition 2.1.11 (Sub-lattice). Given P Q, a lattice M = (P; v; t; u) is a sub-lattice of lattice L = (Q; v; t; u) (written as M L) if for each c; d 2 P then c t d 2 P and c u d 2 P .
Theorem 2.1.2 (M3-N5 theorem). A lattice L is non-distributive if and only if M3 L or N5 L.
Proof. See [DP02].
Lastly, another significant type of lattice is that of a frame, also called a com-plete Heyting Algebra (cHa).
Definition 2.1.12 (Frame). A lattice L is a frame if it is complete and it satisfies the next equation:
l l c t S = fc t s j s 2 Sg (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; 0; 1) where:
i. (B; ^; _; 0; 1) is a distributive lattice,
ii. a ^ 1 = a and a _ 0 = a for all a 2 B,
iii. a ^ a0 = 0 and a _ a0 = 1 for all a 2 B.
Example 2.1.5. The powerset lattice of a set S of elements can form a boolean algebra where B = S, ^ = [, _ = \, 0 = Sn , 0 = ;, 1 = S. Moreover, the reverse power lattice of S forms the boolean algebra (S; \; [; Sn ; 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 L0, a set S 2 L and a map f : L ! L0 we say: F F
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 [KPPV12]. Following [BDPP95] we formalize constraint systems as complete algebraic lattices (an alternative syntactic charac-terization of cs, akin to Scott information systems, is given in [SRP91, PSSS93]).
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 v is meant to capture entailment of information: c v d, alternatively written d w c, means that the assertion d represents at least as much information as c. Thus we may think of c v d as saying that d entails c or that c can be derived from d. The least upper bound (lub) operator t represents join of information; c t d, the least element in the underlying lattice above c and d. Thus c t 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 [BDPP95]). A constraint system (cs) C is a complete algebraic lattice (Con; v). The elements of Con are called constraints. The symbols t, 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 [Vic96]. Next, we describe two typical concrete constraint systems. Example 2.2.1 (Herbrand Constraint System [BDPP95, SRP91]). The Herbrand cs captures syntactic equality between terms t; t0; : : : 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., fx = t; y = tg is a constraint. The relation c v d holds if the equalities in c follow from those in d: E.g., fx = yg v fx = t; y = tg. 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 fx; yg and constants fa; bg with a 6= 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 prim-itive propositions. A boolean (or truth) assignment over is a total map from to the set f0; 1g: 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 assign-ments ordered by . Thus constraints in Con are sets of assignments, v is , false is ;, true is A( ), the join operator t is \, and the meet operator u is [. A constraint c in B( ) is compact iff A( ) n c is a finite set.

Table of contents :

Abstract
Acknowledgments
Contents
1 Introduction
2 Background on Constraint Systems
2.1 Order Theory
Posets and Maps
Lattices
2.2 Constraint Systems
Spatial Constraint Systems
2.3 Summary
3 Spatial Constraint Systems with Extrusion
3.1 Extrusion as the right inverse of Space
3.2 Derived Notions and Applications
Heyting Implication
Lying Agents
Communicating Agents
Process Mobility
Outermost Extrusion
Spatial Safety
3.3 Limit Preservation
3.4 The Extrusion Problem
Local/Subjective Distribution
Global/Objective Distributed Extrusion
3.5 Properties of Space and Extrusion
Consistent and Contradicting Agents
Orders
3.6 Galois Connections
3.7 Summary
4 Opinions & Lies: A Bimodal Logic
4.1 Modal Logics
4.2 Kripke Spatial Constraint Systems
A modal language
4.3 A Logic of Belief and Utterance
Left-total left-unique Kripke Structures
The BUn logic
4.4 Summary
5 Knowledge in Terms of Global Space
5.1 Epistemic Logic
5.2 Knowledge Constraint System
5.3 Knowledge as Global Information
5.4 Summary
6 Algebraic view of LTL
6.1 Linear Temporal Logic
Future
Past
6.2 Constraint systems for LTL models
6.3 Constraint system semantics for LTL
6.4 Summary
7 Conclusions and Related Work
7.1 Related and Future Work
7.2 Correspondence between operators
Bibliography
Index

GET THE COMPLETE PROJECT