I. INTRODUCTION

Many authors in logic and in Artificial Intelligence [5] developed epistemic logic and studied mathematical properties of it. Epistemic logic is theoretical and may be difficult to explain to students. This is the reason why in this article we are going to study a concrete example of multi-agent system. Let us take a line. We are going to put lamps and agents on this line as shown in the Figure 1. Now the question is "what do agents know about lamps and knowledge of other agents about lamps"? This system has been implemented as a pedagogical tool in order to illustrate any epistemic logic course. Indeed, students can easily understand some epistemic logic on concrete examples:

• Agent a sees the lamp p on, so he knows p; a • Agent a and agent b are looking at each other and there is the lamp p between them, so there is common knowledge that p is true. This kind of situations have already been considered in [8]. a

☼ p b

This approach can be compared to the approach in [2] for first order logic. In [2], you put objects like cube, pyramids and you can then write formulas in first order logic to check properties over those objects. Here the approach is similar: you put agents and lamps and then you can write formulas in epistemic logic to check whether properties over those agents and lamps are true.

Generally speaking many examples of epistemic situation mix time and space. The link between time and knowledge (perfect recall etc.) has been studied and you can find a survey in [3]. There exists also some work linking space and knowledge like in [10]: they provide a logic with a spatial modal operator dealing with topology and an epistemic modal operator. Here, our approach is different: we want to deal with a spatially grounded epistemic logic. We are not going to provide operators in the language to deal with space but only provide an epistemic operator for each agent in the language. The semantics will then directly rely on the geometrical properties of a line. We would like to describe a situation but directly by the graphical and natural representation of the system and not with a Kripke structure. We can formalize well known toy examples as Russian cards [13], Muddy children ( [4], [11], [3]) or the prisoner's test. For instance:

• The Muddy children. The spatial configuration is the following: two children are looking at each other. One knows the other's forehead is dirty. But one does not know he is dirty.

☼

a's forehead_dirty a b ☼ b's forehead_dirty

• The prisoner's test. There are three prisoners on a line. Each prisoner must guess the color of his head.

☼ pr 1 's head pr 1 pr 2 's head pr 2 ☼ pr 3 's head pr 3 Another motivation would be video surveillance. Propositions are objects we have to take care of. Agents are camera. We then can specify the video surveillance with epistemic logic formulas. Another possible application may be robots' space and knowledge reasoning because robots evolve in our spatial world. A last application could be video games. In many role playing games or strategy games, players or non-playing characters can have knowledge about the virtual world. The behaviours of a non-playing character can then be described by the game designer using a knowledge based programming language. For instance, the designer can specify that the guardian of the castle gets crazy if he knows that the door of the castle is open. A preliminary work about formalizing the video game Thief has been done in [7].

A piece of software is available on the Web Site http://www. irit.fr/~Francois.Schwarzentruber/agentsandlamps/. It provides a model-checker: you specify the graphical situation and a formula written using epistemic modal operators and/or public announcements operators. In this article:

• We are going to present the semantics of the geometric version of epistemic logic in section II; • We are going to deal with the model checking and satisfiability problems' complexities in section III; • In section IV, we will add public announcements to our language to model examples like Muddy children; • In section V, we are going to present the current implementation.

II. SEMANTICS

We are going to define a new logic based on the same language than the epistemic logic S5 n [5]. S5 n is the logic of frames where relations are equivalence relations. Here we are defining a logic where the semantics is based on a geometric point of view.

A. Language

Our logic is based on the same language as S5 n 's one. Let us recall the language of the epistemic logic S5 n [5].

Definition 1 (language): Let ATM be a countable set of atomic propositions. Let AGT be a countable set of agents. The language L AGT is defined by the following BNF:

ϕ ::= | p | ϕ ∧ ϕ | ¬ϕ | K a ψ

where p ∈ ATM and a ∈ AGT. As usual, ϕ ∨ ψ = def ¬(¬ϕ ∧ ¬ψ). Ka ψ = def ¬K a ¬ψ. Notice that we can only deal with knowledge (operator K a ) and states of lamps (proposition p is true means that the lamp called p is on) in the language. One may expect to deal also with position of lamps, position of agents or maybe spatial topologic operator like in [10] etc. This may be very interesting, especially in all applications cited in the introduction. For instance, we can not express a sentence like "the guardian knows that the beetle is near the old man." but we can say "The guardian knows that the beetle knows the old man's hat is red." (K guardian K beetle old_man_red) Here we have preferred to keep the language of classical epistemic logic for two reasons:

• a pedagogical tool for understanding epistemic logic should be simple and should have a simple syntax; • to focus on complexity results with the simple expressivity as S5 n .

B. Definitions

The semantics is not defined with a class of models but directly from what a concrete situation is. From this, we will obtain a spatially grounded epistemic logic. A world is situation where all agents have a location (position and direction where they look), all lamps (atomic propositions) have a location and a state (on or off). Formally:

Definition 2 (world): A world w is a tuple p AGT , d AGT , p ATM , π where:

• p AGT : AGT → R; • d AGT : AGT → {−1, +1}; • p ATM : ATM → R; 1 ☼ p 1 2 p 2 3 ☼ p 3 Fig. 1. Example of a world • π : ATM → {⊥, }.

The set of all worlds is noted W .

In a world p AGT , d AGT , p ATM , π , p AGT (a) denotes the position of agent a. d AGT (a) denotes the direction where the agent a looks: if d AGT (a) = +1, the agent a will look on the right and if d AGT (a) = −1, he will look on the left. p ATM (p) denotes the position of the lamp saying whether p is true or not. π(p) = iff the lamp "p" is on. π(p) = ⊥ means that the lamp "p" is off.

We have defined a world in the more close to the reality manner: that is to say using the real numbers. We could also consider locations of agents and lamps as a total preorder over ATM ∪ AGT. Considering a total preorder is discussed at the end of this section and total preorder is used in Section III.

Here we prefer to use the Definition 8 whose advantage is that it can be easily generalized to dimension n ≥ 2: you just have to replace R by R n and to adapt the notion of direction. In dimension 2 or more, total preorders can no longer be used.

We can also discuss the Definition 8 by the way propositions are treated. Here, a proposition p is associated to a point p ATM (p). This seems to be the simple way to define the semantics. But be aware that in some cases this is a limitation:

• Maybe a proposition p can be associated to a set of points.

For instance, if you are at home, you can know it rains either by looking towards the window of the left L or the window of the right R. Hence, here the proposition rain may be associated to the set of points {L, R}; • Maybe you want that a lamp is associated not to a proposition but more generally to a formula. For instance, when you know that the alarm system located on point P is on, you in fact know that either there is an oil problem or overheating. Hence, here the point is associated to the formula oil_problem ∨ overheating. Here we stay with the simple definition for two reasons:

• it is easier for a pedagogical tool to have a simple and clear semantics; • it is easier for us to begin study a simple case.

Definition 3 (cone):

Let us consider a world w = p AGT , d AGT , p ATM , π . We note cone(a) the set {p AGT (a

) + λ.d AGT (a) | λ ∈ R + }.

cone(a) denotes all the set of points the agent a sees.

Example 1:

The Figure 1 gives us an example of a world w. We have:

• p AGT (1) = 0; p AGT (2) = 2; p AGT (3) = 4; • d AGT (1) = +1; d AGT (2) = −1; d AGT (3) = −1; • p ATM (p 1 ) = 1; p ATM (p 2 ) = 3; p ATM (p 3 ) = 5; • π(p 1 ) = ; π(p 2 ) = ⊥; π(p 3 ) = ; • cone(1) = [0, +∞[; • cone(2) =] − ∞, 2]; • cone(3) =] − ∞, 4].

Now we are going to define the epistemic relation over worlds. wR a u means that agent a can not distinguish w from u. In other words, wR a u iff agent a sees the same things in w and u. Formally: Definition 4 (epistemic relation): Let a ∈ AGT. We define the relation R a over worlds: p AGT , d AGT , p ATM , π R a p AGT , d AGT , p ATM , π iff for all b ∈ AGT, for all p ∈ ATM ,

• if p AGT (b) ∈ cone(a) then p AGT (b) = p AGT (b) and d AGT (b) = d AGT (b); • if p AGT (b) ∈ cone(a) then p AGT (b) ∈ cone(a); • if p ATM (p) ∈ cone(a) then p ATM (p) = p ATM (p) and π(p) = π (p) • if p ATM (p) ∈ cone(a) then p ATM (p) ∈ cone(a).

Briefly, suppose that wR a u. If agent a see the agent b in the world w, then he will also see agent b in world u and agent b will have the same location (position and direction). If agent a does not see agent b in the world w, then he also does not see agent b in u. If agent a see the lamp p in the world w, then he will also see the lamp p in world u. The lamp will have the same position and state both in w and u. If agent a does not see the lamp p in w, then he will also not see the lamp p in u.

Until now, we have finally defined a model M = W, (R a ) a∈AGT , ν where ν maps each world w ∈ W to π w . From now, the truth conditions is standard:

Definition 5 (truth conditions): Let w ∈ W . We define w |= ϕ by induction:

• w |= ; • w |= p iff π(p) = • w |= ϕ ∧ ψ iff w |= ϕ and w |= ψ; • w |= ¬ϕ iff w |= ϕ; • w |= K a ψ iff

for all w , wR a w implies w |= ψ.

C. Comparison with epistemic logic

Now we are going to compare the epistemic logic S5 n and the set of validities we obtain with the truth conditions of Definition 12. First we give the definition of validities.

Definition 6 (set of validities): We denote the set of all validities by L ☼ 1D , that is to say,

L ☼ 1D = {ϕ ∈ L AGT | ∀w ∈ W, w |= ϕ}.

In "L ☼ 1D ", "1D" stands for "one dimension" (a line). Now, we can see that our set L ☼ 1D contains all validities of S5 n .

Proposition 1:

S5 n ⊆ L ☼ 1D .

Proof: We prove that for all a ∈ AGT, the relation R a is an equivalence relation. Hence, the model M is a model of the logic S5 n and satisfies validities of S5 n . We have to prove reflexivity, symmetry and transitivity. Let us just begin to prove transitivity. Suppose we have: The semantics of K a p in L ☼ 1D corresponds to the fact that the agent a sees the light p and the light p is on. More generally, K a ψ means that the agent a has the proof that ψ.

p AGT , d AGT , p ATM , π R a p AGT , d AGT , p ATM , π and p AGT , d AGT , p ATM , π R a p AGT , d AGT , p ATM , π . Let us prove that p AGT , d AGT , p ATM , π R a p AGT , d AGT , p ATM , π .

That is why we have those validities in L ☼ 1D : Proposition 2: Let p, q ∈ ATM .

|= L ☼ 1D K 1 (p ∨ q) → K 1 p ∨ K 1 q. |= L ☼ 1D K 1 (¬p ∨ ¬q) → K 1 ¬p ∨ K 1 ¬q. If p = q, |= L ☼ 1D K 1 (p ∨ ¬q) → K 1 p ∨ K 1 ¬q Proof: Let us prove |= L ☼ 1D K 1 (p ∨ q) → K 1 p ∨ K 1 q. Let w = p AGT , d AGT , p ATM , π be a world such that w |= K 1 (p ∨ q).

We are going to prove that either w |= K 1 p or w |= K 1 q. We have p ATM (p) ∈ cone(1) or p ATM (q) ∈ cone (1). Indeed, if we suppose the contrary, that is to say p ATM (p) ∈ cone(1) and p ATM (q) ∈ cone(1), there exists a world u = p AGT , d AGT , p ATM , π such that π (p) = ⊥ and π (q) = ⊥ and wR 1 u. Hence, w |= K 1 (p ∨ q). Contradiction. So p ATM (p) ∈ cone(1) or p ATM (q) ∈ cone(1). For instance, p ATM (p) ∈ cone (1). And for all u ∈ R 1 (w), π u (p) = . So w |= K 1 p. The other cases are treated in the same manner.

Informally, K 1 (p ∨ q) means that agent 1 has a proof that p ∨ q. In other words, either he sees p on, or he sees q on. Hence, either

K 1 p or K 1 q. Nevertheless, K 1 (ϕ∨ψ) → K 1 ϕ∨ K 1 ψ is not valid in L ☼ 1D .

Notice that there are crucial differences between S5 n and L ☼ 1D :

• S5 n is defined as the logic of a class of frames and has the property of uniform substitution. Now, here is a Proposition showing that we can have common knowledge only when

K 1 K 2 p ∧ K 2 K 1 p.

Proposition 3: We have:

|= L ☼ 1D K 1 K 2 p ∧ K 2 K 1 p → K 1 K 2 K 1 . . . K 2 . . . p where "K 1 K 2 K 1 . . . K 2 . . . " denotes any finite sequence of K 1 and K 2 .

Proof: Let w = p AGT , d AGT , p ATM , π be world such that w |= K 1 K 2 p ∧ K 2 K 1 p. We want to prove that w |= K 1 K 2 K 1 . . . K 2 . . . p. We are going to prove that:

• p AGT (2) ∈ cone(1);

(p) = ⊥. So w |= K 2 p. Hence w |= K 1 K 2 p. Contradiction.

Same proof for p AGT (1) ∈ cone(2). Now we can prove by induction on n that for n ∈ N, for all u ∈ (R 1 • R 2 ) n (w), we have:

• p AGT (2) ∈ cone(1); • p AGT (1) ∈ cone(2); • p ATM (p) ∈ cone(1); • p ATM (p) ∈ cone(2). • π(p) = . Hence w |= K 1 K 2 K 1 . . . K 2 . . . p. The validity K 1 K 2 p ∧ K 2 K 1 p → K 1 K 2 K 1 . . . K 2 . . . p expresses that if K 1 K 2 p ∧ K 2 K 1 p

then the state of the lamp p is the topic of a mutual social perception, studied in [8].

Corollary 1: If n ≥ 2 or card(ATM ) ≥ 2, S5 n L ☼ 1D . Proof: The formula K 1 (p∨q) → K 1 p∨K 1 q and K 1 K 2 p∧ K 2 K 1 p → K 1 K 2 K 1 p are in L ☼ 1D but are not valid in S5 n .

More surprising is the fact that common knowledge is not guaranteed by

K 1 K 2 ϕ ∧ K 2 K 1 ϕ for all ϕ. More precisely, K 1 K 2 ϕ ∧ K 2 K 1 ϕ → K 1 K 2 K 1 ϕ is not L ☼ 1D -valid for all ϕ.

Look at the model of the Figure 2: agent 1 = agent in blue. agent 2 = agent in red. Consider the world on the bottom on the right. Let us call it w. We have

w |= K 1 K 2 ¬K 2 p ∧ K 2 K 1 ¬K 2 p. But, we have w |= K 1 K 2 K 1 ¬K 2 p. Indeed there exists w such that wR 1 • R 2 • R 1 w such that w |= K 2 p.

Nevertheless, there are other formulas where it remains true. For instance, we have

|= L ☼ 1D K 1 K 2 K 3 p ∧ K 2 K 1 K 3 p → K 1 K 2 K 1 . . . K 2 . . . K 3 p. Question 1: What about K 1 K 2 ϕ ∧ K 2 K 1 ϕ → K 1 K 2 K 1 ϕ if ϕ do not contain agent 1 or 2? Do we have a characterisation or exhibit an interesting set of formulas ϕ such that K 1 K 2 ϕ ∧ K 2 K 1 ϕ → K 1 K 2 K 1 ϕ holds?

D. A compact representation

Last but not the least, you can remark that if we want to deal with model-checking, satisfiability problem and other algorithmic problems, we need a compact representation that an algorithm can manipulate. Worlds are difficult to manipulate: in particular, it is unadapted that R a (w) is infinite given a agent a and a world w. According to the Definition 8, the set W is infinite. Nevertheless, the semantics do not depend on positions of lamps and agents but only on how define the notion of description of a world w: it is simply a total preorder over all propositions and agents appearing in a formula, plus d AGT and π. Notice that we can do this because the space is a line. If our space were R n (n ≥ 2), the notion of total preorder would unfortunately not be suited anymore.

Definition 7 (description of a world):

A description of a world w is a tuple <, d AGT , π where:

• ≤ is a total preorder over AGT ∪ ATM ; • d AGT : AGT → {−1, +1}; • π : ATM → {⊥, }.

We can also define the epistemic relation between two description of a world w:

Definition 8 (epistemic relation):

Let a ∈ AGT. We define the epistemic relation R a on the set of descriptions of worlds by wR a v iff:

• if d AGT (a) = +1, -for all x ∈ AGT ∪ ATM , (x ≤ w a iff x ≤ v a); -for all x, y ∈ AGT ∪ ATM such that a ≤ w x and a ≤ w y, we have (x ≤ w y iff x ≤ v y); -for all x ∈ AGT, a ≤ w x implies d AGTw (x) = d AGTv (y); -for all x ∈ ATM , a ≤ w x implies π w (x) = π v (y). • if d AGT (a) = −1,

-for all x ∈ AGT ∪ ATM , (x ≥ w a iff x ≥ v a); -for all x, y ∈ AGT ∪ ATM such that a ≥ w x and a ≥ w y, we have (x ≥ w y iff x ≥ v y); -for all x ∈ AGT, a ≥ w x implies d AGTw (x) = d AGTv (y); -for all x ∈ ATM , a ≥ w x implies π w (x) = π v (y).

In the same way, we can define an epistemic model. We can define truth conditions of a formula ϕ in L AGT over the set of descriptions of worlds, using the epistemic relation. We can prove that we obtain the same validities.

Definition 9 (extracting description of world from a world):

Given a world w, we define the description of world d(w) by:

• for all x, y ∈ AGT ∪ ATM , x ≤ d(w) y iff p(x) ≤ R p(y) where p(x) stands for

p AGT (x) if x ∈ AGT or p ATM (x) if x ∈ ATM ; • d AGTw = d AGTd(w) ; • π w = π v . Proposition 4: For all w ∈ W , for all ϕ ∈ L AGT , w |= ϕ iff d(w) |= ϕ.

Proof: By induction on ϕ. In the case of one dimension, we simply rewrite mapping from ATM or AGT to real numbers into a total preorder over ATM ∪ AGT. In the case of two or more dimensions, it is an open problem how to represent a world in a compact way.

III. MODEL-CHECKING AND SATISFIABILITY PROBLEM

For definitions for complexity class and for more details about the problem QSAT (quantified boolean formulas satisfiability problem), the reader may refer to [9].

A. Definitions

Now we are going to recall the classical problem of modelchecking and satisfiability. The problem of model-checking consists on testing if a given formula ϕ is true in a given world w. Satisfiability problem consists to test if there exists a world w in which a given formula ϕ is true.

Definition 10 (model-checking of L ☼ 1D AGT,ATM ): Let AGT be a set of agents and ATM a set of atoms. We call model-checking of L ☼ 1D AGT,ATM problem the following problem:

• Input: a formula ϕ ∈ L AGT , a description of a world w where only atoms and agents occurring in ϕ are given; • Output: Yes iff we have w |= L ☼ 1D ϕ. No, otherwise. In the previous Definition, we give a description of a world w that is to say a total preorder over all agents and propositions occurring in ϕ where we say for each agent if he is look on the left or on the right and for each proposition if it is true or not. We do not care about propositions or agents not in the formula ϕ. The description of w is then finite. Definition 11 (L ☼ 1D AGT -satisfiability problem): Let AGT be a set of agents. We call L ☼ 1D AGT -satisfiability problem the following problem:

• Input: a formula ϕ ∈ L AGT ;

B. PSPACE-ness upper-bound of the two problems

In this subsection, we are going to give PSPACE-ness upper-bound of the model checking problem and also of the satisfiability problem. As you will see, the proof are directly given with algorithms using a polynomial amount of memory (Figures 3 and 4).

Proposition 5: Let AGT be any set of agents. The modelchecking of L ☼ 1D AGT problem is in PSPACE.

Proof: You can take a look at the recursive algorithm of Figure 3. We have to prove three points: terminaison, correctness and PSPACE-ness.

1) First let us prove terminaison by induction on ϕ. Let T (ϕ) be the property "for every world w, the call check(w, ϕ) terminates".

• check(w, ) and check(w, p) terminates. So T ( ) and T (p); • Let us prove that check(w, K a ψ) terminates. By induction, T (ψ) so every call check(u, ψ) terminates. So the call check(w, K a ψ) terminates and T (K a ψ); • Other cases are treated in the same manner.

2) Secondly, we have to prove correctness. Correctness corresponds to the property C(ϕ) defined by "for all world w, w |= ϕ iff check(w, ϕ) = ". We also prove C(ϕ) for all formula ϕ by induction. 3) Finally, we prove that check only requires a polynomial amount of memory. Just be careful at the line "for u ∈ R a (w) do ": although R a (w) may be of size exponential we do not compute it. Here we only enumerate here elements of R a (w) one by one. This can be done using only a linear amount of memory. This part is technical but I will nevertheless give some details how to implement a enumeration of elements of R a (w).

The block:

for u ∈ R a (w) do if check(u, ψ) = ⊥ then return ⊥; endIf endFor can be rewritten in a unreadable block using a linear amount of memory in (*):

u := f irst_permutation(w) while ¬is_last_permutation(u) do if u ∈ R a (w) if check(u, ψ) = ⊥ then return ⊥; endIf endIf u := next_permutation(u)

; endWhile where:

• assuming we have an order < over permutations of elements appearing in w, f irst_permutation(w) gives, using a linear amount of memory, the first permutation we can make with elements of w; For instance, if w = 0 ☼ p , f irst_permutation(w) can be 0 p ;

• next_permutation(u) is a function, using a linear amount of memory, giving the <-successor of u; For instance, we may have:

-next_permutation( 0 p ) = 0 ☼ p ; -next_permutation( 0 ☼ p ) = 0 ☼ p ; -next_permutation( 0 ☼ p ) = p 0 etc.

• is_last_permutation(u) = iff u has no <successor. Now, we can prove by induction on ϕ the following property for all ϕ, P(ϕ) defined as "for all world w, the call check(w, ϕ) needs O(|ϕ| × |w|) memory cells". Finally, P(ϕ) is true for all ϕ. In other words, the algorithm of Figure 3 only use a polynomial number of memory cells (we take in account (*) ).

☼ 1D AGT card(AGT) L ☼ 1D AGT − md L ☼ 1D AGT − sat 1 Σ 1 -hard, in Δ 2 -hard Σ 2 -complete n ∈ N, n ≥ 2 Σ n -hard, in ?? Σ n+1 -hard, in ?? ∞ PSPACE-complete PSPACE-complete card(AGT) S5 card(AGT) − sat 1 NP-complete n ≥ 2 PSPACE-complete ∞ PSPACE-complete Fig. 5.

Proposition 6: Let AGT be any set of agents. The L ☼ 1D AGTsatisfiability problem is in PSPACE.

Proof: You can read the algorithm of Figure 4. The algorithm consists in guessing non-deterministically a world w and then call the routine check of Figure 3 to check if ϕ is true in w. So, the problem is NPSPACE, hence from Savitch's theorem [12], it is PSPACE. Now we are going to investigate more in details complexities of the model checking and satisfiability problem depending on the size of AGT. The table of Figure 5 sums up all results we have. There is also the recall of complexity results about S5 n satisfiability problem as comparison.

C. When AGT is infinite: PSPACE-complete

We recall the complexity result about QBF formulas satisfiability problem:

Theorem 1: The QSAT-problem defined as following:

• Input: a formula ϕ = ∃ p 1 ∀ p 2 ∃ p 3 ∀ p 4 . . . Q n p n ψ where:

n is any integer; ψ is a boolean formula; -and

Q i = ∀ if i is even and Q i = ∃ if i is odd;

p j is a finite set of variables for each j.

• Output: Yes iff |= QBF ϕ. No, otherwise. is PSPACE-complete. Now the following Proposition gives a translation of a QBF-instance into a L ☼ 1D -model-checking instance or a L ☼ 1Dsatisfiability problem instance.

Proposition 7: Let ϕ = ∃ p 1 ∀ p 2 ∃ p 3 ∀ p 4 . . . Q n p n ψ be a formula of the logic QBF. We define f (ϕ) by induction:

• f (ψ) = ψ; • f (∀ p i ...Q n p n ψ) = K i−1 (put i → f (∃ p i+1 ...Q n p n ψ); • f (∃ p i ...Q n p n ψ) = Ki−1 (put i ∧ f (∀ p i+1 ...Q n p n ψ);

where:

• put a = i∈{a+1...2n} ¬K if a p i ∧ i∈{1...a} K if a p i ; • K if a p = q∈ p K if a q; • K if a q = K a q ∨ K a ¬q.

We have equivalence between:

• |= QBF ϕ; • put 1 ∧ f (∀ p 2 ∃ p 3 ∀ p 4 . . . Q n p n ψ) is L ☼ 1D AGT -satisfiable; • and w |= L ☼ 1D f (ϕ)

where w ∈ W 0 where W 0 is the set of all worlds where agent 0 is completely on the left looking to the left. (we note W 0 = " 0 . . . ").

Proof: We are going to note for all U ⊆ W , U |= ϕ iff for all u ∈ U , u |= ϕ. We are going to prove by induction

|= QBF ϕ iff W 0 |= L ☼ 1D f (ϕ).

We are going to note for all i ∈ N, for all valuation ν[ p 1 , . . . p i ],

W i (ν[ p 1 , . . . p i ]) def " 0 ☼ ν(p 1 ) 1 ☼ ν( p 2 ) 2 . . . ☼ ν( p i ) i ... .

The induction hypothesis is:ν[ p 1 , . . . p i−1 ] |= QBF Q i p i . . . Q n p n ψ iff W i−1 ( p 1 , . . . p i−1 ) |= L ☼ 1D f (Q i p i . . . Q n p n ψ)

.

The basis case correspond to i = n+1. It is the propositional case. We have:

ν[ p 1 , . . . p n ] |= QBF ψ iff W n ( p 1 , . . . p n ) |= L ☼ 1D ψ.

Now we can attack the induction case. Let us prove fori odd. ν[ p 1 , . . . p i−1 ] |= QBF Q i p i . . . Q n p n ψ means that there exists a valuation ν(p i ) such that ν[ p 1 , . . . p i ] |= QBF Q i+1 p i+1 . . . Q n p n ψ. By induction, it means that W i ( p 1 , . . . p i ) |= L ☼ 1D f (Q i p i . . . Q n p n ψ).

But for all w i−1 ∈ W i−1 ( p 1 , . . . p i−1 ) and for all w i ∈ W i ( p 1 , . . . p i ), we have:

• w i−1 R i−1 w i ; • w i |= put i .

Indeed, for all j > i, we have w |= ¬K if i p j because agent j does not see lamps p j in w i . On the contrary, for all j < i, we have w |= K if i p j because agent i do see lamps p j in w i (the valuation of lamps p j is the same in all worlds u ∈ R i (w i )). The technical proof of w i |= put i is left to the reader.

As f (∃ p i . . . Q n p n ψ) = Ki−1 (put i ∧ f (∀ p i+1 . . . Q n p n ψ), we have: W i−1 ( p 1 , . . . p i−1 ) |= L ☼ 1D f (∃ p i . . . Q n p n ψ).

We ensure that it is equivalent.

The case where i is even is similar.

Immediately from this translation, we deduce the lower bound for model-checking in L ☼ 1D .

Corollary 2: Let AGT an infinite enumerable set of agents. The model-checking problem of L ☼ 1D AGT is PSPACE-hard.

Proof: Reduction via Proposition 7 and Theorem 1 in order to the PSPACE-hardness and Proposition 6.

In the same way we have: Corollary 3: Let AGT an infinite enumerable set of agents. The satisfiability problem of L ☼ 1D AGT is PSPACE-hard.

D. When AGT is finite

We recall the complexity result about QBF formulas satisfiability problem but when the nesting of ∀ and ∃ is bounded by a fixed integer n.

Theorem 2: Let n be a integer. The QSAT n -problem defined as following:

• Input: a formula ϕ = ∃ p 1 ∀ p 2 ∃ p 3 ∀ p 4 . . . Q n p n ψ

where ψ is a boolean formula, and

Q i = ∀ if i is even and Q i = ∃ if i is odd; • Output: Yes iff |= QBF ϕ. No, otherwise. is Σ n -complete.

The Theorem 2 only differ from Theorem 1 by the fact that n is no more a input of the problem but is now fixed inside the problem. For each integer n, we have defined the QSAT nproblem. There is a enumerable number of problems.

In the same way, this precise complexity result of QBF combined with the translation of QBF to L ☼ 1D allows us to have complexity lower bounds of model-checking and satisfiability problem when the cardinality of the set AGT is finite and fixed.

Corollary 4: Let AGT a finite set of agents. The modelchecking problem of L ☼ 1D AGT is Σ card(AGT) P-hard.

Proof: Reduction via Proposition 7 and Theorem 2. Corollary 5: Let AGT a finite set of agents. The satisfiability problem of L ☼ 1D AGT is Σ card(AGT)+1 P-hard.

Proof: Reduction via Proposition 7 and Theorem 2.

E. When card(AGT) = 1

Unfortunately we do not have a precise complexity upperbound for those problems in the general case when card(AGT) is finite. Nevertheless, we have the exact complexity when card(AGT) = 1.

Proposition 8: The model-checking problem of L ☼ 1D {1} is in Δ 2 P.

Proof: The figure 6 gives us an Δ 2 P-algorithm (a Palgorithm with NP-oracles) for the model-checking problem of L ☼ 1D {1} . Given a world w, first we compute the V of propositions occurring in ϕ that the agent 1 sees and I the set of propositions the agent 1 does not see. Then we can replace each occurrence p of a proposition p from V function check1(w, ϕ)

V := set of variables that agent 1 sees in w; I := set of variables that agent 1 does not see in w; ψ := ψ in which we replace each p ∈ V by π w (p); ψ := ψ in which we replace each p ∈ I not in the scope of a K 1 by π w (p); while there exists K 1 χ subformula of ψ, where χ is a boolean formula do if oracle − sat(¬χ) then ψ := ψ in which we replace K 1 χ by ⊥; else ψ := ψ in which we replace K 1 χ by ; endIf endWhile return P CL({⊥, }) − sat(ψ); endFunction in ϕ by the corresponding valuation π w (p). Concerning a proposition p ∈ I, we only replace occurrences which are not in the scope of a K 1 . For instance, if p ∈ I, q ∈ V , and

π w (p) = , π w (q) = ⊥ p ∧ q ∨ K 1 (p ∨ q) is replaced by ∧ ⊥ ∨ K 1 (p ∨ ⊥).

Then we test satisfiability of boolean formulas ¬χ such that K 1 χ is a subformula of ψ and replace K 1 χ by ⊥ if ¬χ is satisfiable and by otherwise. At the end, we obtain a boolean formula ψ containing no variables. We test its satisfiability with P CL({⊥, }) − sat(ψ). Notice the while -loop is done in linear time because there are a linear number of subformulas in ψ.

Proposition 9: The satisfiability problem of L ☼ 1D {1} is Σ 2 P-complete.

Proof: The hardness comes from Corollary 5. The Figure 7 gives us an Σ 2 P-algorithm (a NP-algorithm with NP-oracles) for the satisfiability problem of L ☼ 1D {1} .

F. When AGT and ATM are both finite Proposition 10: Let ATM a finite set of agents and AGT = {1}. The satisfiability problem and model-checking of L ☼ 1D

{1} is in P. Proof: We adapt algorithms of the figure 6 and 7 in order to have an optimal polynomial algorithm. More precisely:

• You replace choose_world_with_symbols_in in Figure 7 by a loop over all worlds. You can notice that the set of all possible worlds is fixed, that is to say it does not depend on ϕ; • oracle − sat can now run in polynomial time because there is a fixed number of propositions. As done in [11] we can extend our framework with public announcements. This is essentially motivated by modelling examples like Muddy children. With public announcements, an agent will be able to learn something about the part of the actual world which he can not see. The technique is classical: we add an operator [ϕ!] and we define semantics as in S5 n .

A. Definitions

Our new language L ! AGT is defined by the following BNF:

ϕ ::= p | ϕ ∧ ϕ | ¬ϕ | K a ψ | [ϕ!]ϕ

where p ∈ ATM and a ∈ AGT.

From now, we do not only parameter |= with a world but also with the set of worlds.

Definition 12 (truth conditions): Let U a set of worlds (U ⊆ W ). Let w ∈ U . We define U, w |= ϕ by induction:

• U, w |= p iff π(p) = • U, w |= ϕ ∧ ψ iff U,

B. Example

Now we are going to study the Muddy children example. This example is also studied in [11]. You can also find this example in [4] and [3] with more than two children. The situation is the following: there are two children named 1 and 2. Their foreheads are dirty. They see each others. The situation is represented by the world w shown in Figure 8 in the top left. One child do not know if he is dirty or not but he knows the state of the forehead of the other one. We introduce two propositions: p stands for "1's forehead is dirty" and q stands for "1's forehead is dirty".

We have:

• W, w |= K 1 q ∧ K 2 p; • W, w |= ¬K 1 p ∧ ¬K 1 (¬p) ∧ ¬K 2 (¬q).

Then:

• the father says at least one of them are dirty; • the children answer that they do not know whether they are dirty of not. Formally, we also have:

W, w |= [ϕ 1 !][ϕ 2 !](K 1 p ∧ K 2 q)

where:

• ϕ 1 = p ∨ q; • ϕ 2 = (¬K 1 p ∨ ¬K 1 ¬p) ∧ (¬K 2 q ∨ ¬K 2 ¬q).

We verify that after having announced ϕ 1 , we only consider worlds in Figure 9. Then we only consider the initial world w drawn in 10.

C. Complexity

Because L ☼ 1D ! is a conservative extension of L ☼ 1D , we inherit from the lower bound results both for model-checking and satisfiability. In fact, we keep the PSPACE-ness upperbound with public announcements.

Proposition 11: The model-checking and satisfiability problem in L ☼ 1D ! is PSPACE-complete.

Proof: The Figure 11 gives an algorithm for modelchecking. As usual, w is a world, ϕ is a formula. The second argument C is a list of formulas and stands for the context: if C = [] (empty list), it corresponds to the whole set of worlds otherwise it is a list of announced formulas used to update the model. More precisely, let us define:

• W [] = W ; • W [ψ 1 :C ] = {w ∈ W C | W C , w |= ψ 1 }. We want: • mc(w, C, ϕ) returns true iff W C , w |= ϕ; • inupdatedM (w, C) returns true iff w ∈ W C .

We have to prove terminaison, correctness and complexity. Let us begin to prove terminaison. First of all, we are going to introduce an order ≺ over all possible inputs (C, ϕ) of the function mc! of Figure 11.

We define (C, ϕ) ≺ (D, ψ) by: More precisely:

-

|[]| = 0; -|[ψ 1 : C ]| = |ψ 1 | + |C |.

The order ≺ is well-founded and we can use it to prove terminaison by induction.

• Basic case: (∅, p) etc.

• Induction case: you just have to see that mc!(w, C, ϕ) will only call mc!(u, D, ψ) with (D, ψ) ≺ (C, ϕ). For instance, when mc!(w, C, ϕ) calls inupdatedM (u, C) which calls mc!(w, C , ψ), we have

|C | + |ψ| = |C| < |C| + |ϕ|.

Correction and the fact that the algorithm runs using a polynomial space can also be proved by induction using the order ≺.

The hardness comes from the fact that L ☼ 1D ! is a conservative extension of L ☼ 1D and the model checking of L ☼ 1D is PSPACE-hard (Corollary 2).

Concerning the satisfiability, we can make the same remark than in the proof of Proposition 6.

The upper-bound in special cases (AGT finite etc.) has not been studied yet.

From now, we are to discuss about the implementation and develop the example of the Muddy children. V. IMPLEMENTATION You can find an implementation on the Web site. You can put positions and directions of agents and positions and states of lamps on your own. Then you can write down a formula and check if your formula is true in the world you have drawn.

This program offers a concrete example to illustrate epistemic logic to students.

A. Description

The program is written in Scheme for the easy use of data structures and recursive programming. Haskell could also be a well-suited language especially for the lazy evaluation enabling us to write a program which seems to use a exponential amount of memory whereas it uses only a polynomial amount of memory. Here are the main Scheme functions:

• (mc world formula) computes if the formula formula is true in the world world; • (mc-with-context world context formula) computes of the formula formula is true in the world world but we restrict our check computations only on worlds satisfying the formula context; • (worldset-delete-not-satisfying worldset formula) removes from the set of world worldset all worlds which does not satisfy the formula formula. This function is used to deal with updated models; • (world-getpossibleworlds world agent) computes the set of all possible worlds for agent agent in world world. In order to be human readable, the implementation does not run in polynomial space but in exponential time. For instance the function (world-getpossibleworlds w a) computes really all worlds in R a (w).

B. Practising Muddy children

You can describe the current situation (world w on the top left in Figure 8 by ( (p #t) (1 <) (2 >) (q #t)). Notice that we are not going to construct the Kripke structure by hand. When you draw a Kripke model, you can easily mistakes all the more so the model is theoretical. Here we just enjoy specifying graphically the situation. The Kripke structure is then generated on-the-fly by the algorithm. You can test if W, w |= K 1 p ∧ K 2 q by calling (mc '( (p #t) (1 <) (2 >) (q #t)) ((1 knows p) and (2 knows q))).

The function returns #f meaning that we do not have W, w |= K 1 p ∧ K 2 q.

We ask the computer the different worlds the agent 1 imagine. To do this we write (world-getpossibleworlds '( (p #t) (1 <) (2 >) (q #t)) 1).

The system gives: (((p #t) (1 <) (2 >) (q #t)) ((p #f) (1 <) (2 >) (q #t))).

We can now test if the formula W, w |= [ϕ 1 !][ϕ 2 !](K 1 p ∧ K 2 q). You simply write (mc '( (p #t) (1 <) (2 >) (q #t)) (announce (p or q) (announce ((not (1 knows p)) and (not (2 knows q))) ((1 knows p) and (2 knows q)))))

The system answers #t.

VI. CONCLUSION

The epistemic logic S5 n is a general and theoretical framework for the representation of knowledge. In this paper, we have studied a spatially grounded epistemic logic. We have investigated two aspects of knowledge learning:

• With L ☼ 1D , we can reason about what agents know by learning only with their eyes (when they are located on a line space); • With L ☼ 1D ! we can reason about what agents know by looking at their environments and by listening to public announcements. Of course the case of the line is restrictive. The case of the plane or of the space may be more interesting. Nevertheless, this paper gives complexity results for model-checking and satisfiability problem for the case of the line. Even the line looks like easy, problems are already PSPACE-complete if the number of agents is not bounded. We conjecture that the complexity of this logic for dimension n ≥ 2 remains PSPACE-complete.

From now, there are two main perspectives: to adapt this logic to the case of two dimensions [1] and to study properly complexity of model checking and satisfiability with/without public announcements. Other perspectives are numerous:

• fill the Figure 5. The exact complexity classes of model checking and satisfiability L ☼ 1D AGT when AGT is finite are still open questions; • Study and implement the logic with agents and lamps in the plane [1] and compare it to the logic in the line.

Writing down the semantics is quite easy: you just have to replace R by R 2 in Definition 8 and tune the definition of directions and Definition 3. The main difficulty is to find a compact representation in order to deal with the model checking and satisfiability problem. In two dimensions it is no more possible to consider a total preorder on elements. Finding a good equivalent of Definition 7 satisfying Proposition 4 in the case of dimension 2 or more is still an open problem.

• Study the logic in the 3D-space and compare it to the one in the plane (I guess we obtain the same validities);

• Find an axiomatization of those logics in order to understand better how they work; • Study if it is possible to have a normal form (like for S5, where all formulas are equivalent to a formula of modal degree 1 [6]); • Extend with a common knowledge operator. Will the complexity of the satisfiability problem also increase and become EXPTIME-complete? • Extend with private communications between agents.