Project topics and materials
Get Complete Project Material File(s) Now! »
Introduction : Modal Logics
In this chapter we shall recall the notion of modal logic. Modal logics extend propositional logics with modal operators which can be used to represent different scenarios such as temporal and epistemic (depending on the interpretation we give to them). Modal logics are mainly used in computer science in the specification of programs, which is one of the main steps in the theory of formal verification. The notions introduced here will be relevant for this dissertation because the main results of this thesis have modal logics as elemental notions. Most of the material in this chapter is based on [BDRV01, BvBW06]. This chapter is organized as follows. First, we shall introduce the basics of modal logics. We shall start by defining how we can build formulae in modal logics (the language). Then we shall describe the way in which modal formulas are interpreted (the semantics). Finally, we shall define the notion of normality in modal logics. For more details or further references see [BDRV01, BvBW06, Gol03].
Modal Logics
In order to be able to deal with modal logics we would need to define how to build modal formulae and how to interpret them. In this section we shall give the basic definitions for modal languages that will help us to show how to interpret modal formulae.
Modal Logics
Modal Language
A modal language Ln(Φ) can be seen as the language that results by adding modalities m to the language formed by sets of primitive propositions and logical connectives such as or, and, negation and implication. Formally, a modal language can be defined as follows.
Definition 3.1.1 (Modal Language). Let Φ be a set of primitive proposi-tions. The modal language Ln(Φ) is given by the following grammar:
φ, , . . . := p | φ ^ | ¬φ | ⇤iφ
where p 2 Φ and i 2 {1, . . . , n}. We shall use the abbreviations φ _ for ¬(¬φ^¬ ), φ ) for ¬φ_ , φ , for (φ ) ) ^( ) φ), the constant false ↵ for p ^ ¬p, and the constant tt for ¬↵ .
Kripke Model
In Definition 3.1.1 we have formally defined the way in which modal for-mulae should be built. Now we shall introduce some basic definitions that will allow us to give semantics to modal formulae.
Kripke structures (KS) are a fundamental mathematical tool in logic and computer science. They can be seen as transition systems and they are used to give semantics to modal logics. A KS M provides a relational
structure with a set of states and one or more accessibility relations i M between them: s i M t can be seen as a transition, labelled with i, from s to t in M.
Definition 3.1.2 (Kripke Structures). An n-agent Kripke Structure (KS) M over a set of atomic propositions Φ is a tuple (S, ⇡, R1, . . . , Rn) where
• S is a nonempty set of states,
• ⇡ : S ! (Φ ! {0, 1}) is an interpretation associating with each state a truth assignment to the primitive propositions in Φ, and
• Ri is a binary relation on S.
Normal Modal Logics
A pointed KS is a pair (M, s) where M is a KS and s, called the actual world, is a state of M.
Finally, with the following definition we introduce how to give semantics to modal logics by using Kripke structures.
Definition 3.1.3. Let M = (S, ⇡, R1, . . . , Rn) be a Kripke structure and φ be a modal formula. Then we define the relation |= inductively, over M, φ and a given state s 2 S as follows:
(M, s) |= p iff ⇡M (s)(p) = 1
(M, s) |= φ ^ iff (M, s) |= φ and (M, s) |=
(M, s) |= ¬φ iff (M, s) |6= φ
(M, s) |= ⇤iφ iff (M, t) |= φ for all t, s.t. (s, t) 2 Ri
From now on we shall use the following notation.
Notation 3.1.1. Each Ri is referred to as the accessibility relation for agent i. We shall use i M to refer to the accessibility relation of agent i in M. We write s i M t to denote (s, t) 2 Ri. We use Ii(M, s) = {(M, t) | s i M t} to denote the pointed KS reachable from the pointed KS (M, s).
Recall that the interpretation function ⇡ tells us what primitive propositions are true at a given world: p holds at state s iff ⇡(s)(p) = 1. We shall use SM and ⇡M to denote the set of states and interpretation function of M.
Normal Modal Logics
We have already introduced how to build modal formulae and how to in-terpret them over Kripke structures. In this section we shall introduce the notion of normality in modal logics. We start by giving some basic defini-tions before we formally define normal modal logics.
Two important properties when dealing with modal logics are those of modus ponens and generalization. These two properties are the ones characterizing the type of modal logics we shall work with in this thesis. The modal logics satisfying modus ponens and generalization are called normal modal logics. The property of modus ponens can be formally defined as follows.
Definition 3.2.1 (Modus Ponens). We say that a set of formulas S is closed under modus ponens if whenever φ 2 S and φ ) 2 S then 2 S.
The notion of generalization can then be defined as follows.
Definition 3.2.2 (Generalization). We say that a given set of formulas S is closed under generalization if whenever φ 2 S then ⇤iφ 2 S, for all i 2 I, where I is the set of agents.
Normal Modal Logics
In modal logics one is interested in normal modal operators. We already know that modal logic formulae are those of propositional logic extended with modal operators. Roughly speaking, a modal logic operator m is called normal if and only if the following conditions are met :
1. The formula m(φ) is a theorem (i.e., true in all models for the under-lying modal language) whenever the formula φ is a theorem, and
2. the implication formula m(φ ) ) ) (m(φ) ) m( )) is a theorem.
Thus, as mentioned above, a normal modal logic is a modal logic in which the modalities satisfy the modus ponens and the generalization conditions. Formally, it can be defined as follows.
Definition 3.2.3 (Normal Modal Logics). Consider the modal language Ln(Φ) formed by the set of modal formulas Φ. We say that Ln(Φ) is a normal modal logic if it contains:
• all the tautologies from propositional logic,
• the implication formula m(φ ) ) ) (m(φ) ) m( )) for all modalities m 2 Ln(Φ) with φ, 2 Φ.
• and it is closed under modus ponens and generalization.
Table of contents :
Abstract
Résumé
Acknowledgments
Contents
List of Figures
1 Introduction
1.1 Introduction
1.1.1 The Extrusion Problem
1.1.2 Knowledge in Terms of Space
1.1.3 Distributed Spaces
I Constraint Systems and Modal Logics
2 Introduction: ConstraintSystems
2.1 Posets and Maps
2.1.1 Posets
2.1.2 Maps
2.2 Lattices
2.2.1 Lattices
2.2.2 Algebraic Lattice
2.2.3 Distributive lattices
2.3 Frames
2.3.1 Frames
2.3.2 Heyting algebras
2.4 Constraint Systems
2.5 Spatial Constraint Systems
2.6 Spatial Constraint Systems with Extrusion
3 Introduction: ModalLogics
3.1 Modal Logics
3.1.1 Modal Language
3.1.2 Kripke Model
3.2 Normal Modal Logics
3.2.1 Normal Modal Logics
II The Extrusion Problem
4 Introduction
4.1 Background: Spatial Constraint Systems
4.2 Constraint Frames and Normal Self-Maps
4.2.1 Normal Self-Maps
4.3 Extrusion Problem for Kripke Constraint Systems
4.3.1 KS and Kripke SCS
4.3.2 Complete Characterization of the Existence of Right Inverses
4.3.3 Deriving Greatest Right-Inverse
4.4 Deriving Normal Right-Inverses
4.4.1 Deriving Greatest Normal Right Inverse
4.4.2 Deriving Minimal Normal-Right Inverses
4.5 Applications
4.5.1 Right-Inverse Modalities
4.5.2 Normal Inverses Modalities
4.5.3 Inconsistency Invariance
4.5.4 Bisimilarity Invariance
4.5.5 Temporal Operators
4.6 Summary
III Knowledge in Terms of Space
5 Introduction
5.1 S4 Knowledge as Global Information
5.1.1 Knowledge Constraint System
5.1.2 Knowledge as Global Information
5.2 Summary
IV Distributed Information in Terms of Space
6 Introduction
6.1 Background
6.2 Spatial Constraint Systems
6.2.1 Extrusion and utterance
6.3 Distributed Spaces
6.3.1 Properties of Distributed Spaces
6.3.2 Views and Distributed Spaces
6.4 Summary
7 Conclusions andRelatedWork
7.1 Concluding Remarks
7.2 Related and Future Work
Bibliography
