Voir, savoir, faire : une étude de cas en logique modale

Voir, savoir, faire : une étude de cas en logique modale

 Comparisons between our approach and the literature 

Classical epistemic logic VS Lineland/Flatland

 In the classical epistemic modal logic S5n, wRav stands for w and v are indistinguishable for the agent a. The epistemic logic S5n has been combined with temporal modal operator [HV88]. In such temporal epistemic modal logic, the properties of total recall (no forgetting) and no learning are modeled as a constraint of the epistemic relation and the temporal relation. Kripke worlds are abstract: they are valuations. On the contrary, in our approach, we would like to describe a situation directly by the graphical and natural representation of the system (position and direction of agents) and not with a Kripke structure. In fact, we also have one canonical Kripke structure made up of those graphical Kripke worlds that embed some geometrical informations: the position of agents and the direction where they look. (see Denition 14 and Denition 27) In the same way, the epistemic relation of an agent a is built-in and relies on geometry concepts: as depicted in Figure 3.5 two Kripke worlds are indistinguishable for agent a i agent a sees the same thing in both worlds. Other built-in logics in the literature There are other logics in the literature where the semantics is built-in, that is to say where Kripke’s worlds are not abstract valuations and where the epistemic relations take into account the structure of those Kripke’s worlds. In [FHMV95] (Chapter 3), the author consider global states (you can think of them as possible worlds). A state is a tuple (se, s1, . . . , sn) where se is the state of the environment and si is the state of agent i for all agent i. Global states s = (se, s1, . . . , sn) and s 0 = (s 0 e , s0 1 , . . . , s0 n ) are then said to be indistinguishable to agent i if agent i has the same state in both s and s 0 , i.e., if si = s 0 i . In other worlds, the epistemic relation is not arbitrary but directly built-in from the denition of states. In [Jag09], the author develops a logic for rule-based agents. It is not the epistemic relation which is built-in but the belief change. A state s denes the belief of the agent: agent believes ϕ i ϕ ∈ V (s). Then the relation of belief change works as follows: T is a transition relation on states and sT u means the agent in state s can gain some belief and be in state t. This relation T is built-in with respect to a set of rules. In particular the relation T must satisfy the following statement: if a rule λ1 . . . λn → λ matches with the belief of the agent in state s then there must exist a state u such that sT u and V (u) = V (s) ∪ {λ}. 3.4.2 Spatial logic VS Lineland/Flatland 63 a b c obstacle a b c obstacle d d Figure 3.5: Two Kripke worlds that are undistisguishagle for agent a In the same manner, in our approach, we provide a logic in which wRau, that is to say, world u is possible for agent a in u, i agent a sees the same thing both in w and u.

Spatial logic VS Lineland/Flatland

 In the same way, in the next two chapters, we develop epistemic modal logic based on geometry. Our approach will be rather dierent concerning the syntax. In S4, RCC − 8, we have spatial operators like  = in the neighborhood, EC = are externally connected, etc. whereas in the next two chapters the syntax relies on the standard epistemic modal logic and will provide the classical knowledge operator Kaϕ meaning agent a knows that ϕ. This is motivated because we want to focus on epistemic reasoning. Concerning the semantics, our approach is quite similar to the logic seen in this chapter. Indeed, in Chapter 4 and 5, we have also decided to encode the geometrical structure in the model. Nevertheless, our approach is also dierent. In logics seen in this chapter, the domains in the semantics are geometrical entities: • in S4 points x of a topo-model are points of the topological space; • in the geometry seen in Subsection 3.2.1.2, the domain is the union of points and lines of the geometrical space; • in RCC − 8, the domain is the set of regions of the space, etc. Our approach rely on a Kripke model where a possible world is dened as the values of positions for all agents of the system. The epistemic relation will be dened directly from the possible worlds in term of what agents see. 3.4.3 Topological epistemic logic VS Lineland/Flatland In the topological epistemic logic presented in [MP92], [PMS07] and [Hei06], the authors provide an epistemic modal logic based on the accuracy of the observation. Concerning the semantics, models are topo-models M = (E, τ, V ). The language made up of two operators  (and its dual ♦) and K interpreted as follows, for all x ∈ E, U ∈ τ such that x ∈ U: • M,(x, U) |= ϕ i M,(x, V ) |= ϕ for all V ∈ τ such that x ∈ V ⊆ U; • M,(x, U) |= ♦ϕ i there exists V ∈ τ such that x ∈ V ⊆ U and M,(x, V ) |= ϕ; • M,(x, U) |= Kϕ i M,(y, U) |= ϕ for all y ∈ U. In (x, U), x ∈ E represents the real world but the accuracy/precision of the observation is such that the agent only knows that the real world is in U ∈ τ . The reading of the modal operators are: • M,(x, U) |= ♦ϕ: it is possible to have a better precision of the observation, that is to say, to have V ⊆ U instead of U such that ϕ is true. In other worlds, the agent can make an eort to improve her precision such that ϕ is true. • M,(x, U) |= Kϕ: the agent knows that ϕ is true, that is to say, according to the current precision of the observation represented by U, ϕ is true in all possible worlds y ∈ U. There are crucial dierences between their approach and ours: • For them, the geometry is used to represent the state of knowledge. For us, the geometry is devoted to give a position and a direction to agents. In this sense, their logic is abstract like S5n. • In their logic, there is only one agent. Chapter 4 is devoted to the case where agents are points and are located on the line. In Chapter 5, agents are located on the plan