-In this article, we are going to talk about spatial situations. Every agent (human, camera etc.) and every proposition (lamp, object, etc.) are located in the space (here a line) and we express properties over a situation using standard epistemic logic language possibly extended with public announcements. We study links between validities of this geometrical version of epistemic logic and the standard one. We also investigate complexities of model checking and satisfiability.
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 does not see the lamp p, so he does not know ☼ p whether p or ¬p; ☼p
a • Agent a sees another agent b seeing the lamp p on, so agent a knows agent b knows p; a b • Agent a sees another agent b, and the lamp p, but agent a sees that agent b is not looking in the direction of the lamp p, so agent a knows agent b does not know whether ☼ p p or ¬p; ☼ p a b • 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]. b
This approach can be compared to the approach in [2] for ifrst 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.
☼ pr1’s head pr1 pr2’s head pr2
☼ pr3’s head pr3
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.
We are going to define a new logic based on the same language than the epistemic logic S5n [5]. S5n 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.
Our logic is based on the same language as S5n’s one. Let us recall the language of the epistemic logic S5n [5].
Definition 1 (language): Let ATM be a countable set of atomic propositions. Let AGT be a countable set of agents. The language LAGT is defined by the following BNF:
ϕ ::= > | p | ϕ ∧ ϕ | ¬ϕ | Kaψ where p ∈ ATM and a ∈ AGT.
As usual, ϕ ∨ ψ =def ¬(¬ϕ ∧ ¬ψ). Kˆaψ =def ¬Ka¬ψ.
Notice that we can only deal with knowledge (operator Ka) 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.” (KguardianKbeetleold_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 S5n.
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 hpAGT, dAGT, pATM , πi where: • pAGT : AGT → R; • dAGT : AGT → {−1, +1}; • pATM : ATM → R; 1
• π : ATM → {⊥, >}.
The set of all worlds is noted W .
In a world hpAGT, dAGT, pATM , πi, pAGT(a) denotes the position of agent a. dAGT(a) denotes the direction where the agent a looks: if dAGT(a) = +1, the agent a will look on the right and if dAGT(a) = −1, he will look on the left. pATM (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 Rn 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 pATM (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 = hpAGT, dAGT, pATM , πi. We note
cone(a) the set {pAGT(a) + λ.dAGT(a) | λ ∈ R+}.
cone(a) denotes all the set of points the agent a sees.
• pAGT(
Now we are going to define the epistemic relation over worlds. wRau means that agent a can not distinguish w from u. In other words, wRau iff agent a sees the same things in w and u. Formally:
Definition 4 (epistemic relation): Let a ∈ AGT. We define the relation Ra over worlds: hpAGT, dAGT, pATM , πiRahp0AGT, d0AGT, p0ATM , π0i iff for all b ∈ AGT, for all p ∈ ATM , • if pAGT(b) ∈ cone(a) then
pAGT(b) = p0AGT(b) and dAGT(b) = d0AGT(b); • if pAGT(b) 6∈ cone(a) then p0AGT(b) 6∈ cone(a); • if pATM (p) ∈ cone(a) then
pATM (p) = p0ATM (p) and π(p) = π0(p) • if pATM (p) 6∈ cone(a) then p0ATM (p) 6∈ cone(a).
Briefly, suppose that wRau. 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 = hW, (Ra)a∈AGT, νi 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 6|= ϕ; • w |= Kaψ iff for all w0, wRaw0 implies w0 |= ψ.
Now we are going to compare the epistemic logic S5n 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 = {ϕ ∈ LAGT | ∀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 S5n.
Proposition 1: S5n ⊆ L☼1D .
Proof: We prove that for all a ∈ AGT, the relation Ra is an equivalence relation. Hence, the model M is a model of the logic S5n and satisfies validities of S5n. We have to prove reflexivity, symmetry and transitivity. Let us just begin to prove transitivity. Suppose we have: hpAGT, dAGT, pATM , πiRahp0AGT, d0AGT, p0ATM , π0i and hp0AGT, d0AGT, p0ATM , π0iRahp0A0GT, d0A0GT, p0A0TM , π00i. Let us prove that hpAGT, dAGT, pATM , πiRahp0A0GT, d0A0GT, p0A0TM , π00i.
First we have pAGT(a) ∈ cone(a). So pAGT(a) = p0AGT(a) = p0A0GT(a) and dAGT(a) = d0AGT(a) = d0A0GT(a). In other words, cone(a) = cone0(a) = cone00(a).
From now on, if pAGT(b) ∈ cone(a), then pAGT(b) = p0AGT(b) and dAGT(b) = d0AGT(b). But, we have effectivelly, pAGT(b) = p0AGT(b) and cone(a) = cone0(a). So p0AGT(b) ∈ cone0(a). So p0AGT(b) = p0A0GT(b) and d0AGT(b) = d0A0GT(b). Finally, pAGT(b) = p0A0GT(b) and dAGT(b) = d0A0GT(b). The other cases are treated in the same manner.
The semantics of Kap in L☼1D corresponds to the fact that the agent a sees the light p and the light p is on. More generally, Kaψ means that the agent a has the proof that ψ. That is why we have those validities in L☼1D :
Proposition 2: Let p, q ∈ ATM . |=L☼1D K1(p ∨ q) → K1p ∨ K1q. |=L☼1D K1(¬p ∨ ¬q) → K1¬p ∨ K1¬q.
If p 6= q, |=L☼1D K1(p ∨ ¬q) → K1p ∨ K1¬q
Proof: Let us prove |=L☼1D K1(p ∨ q) → K1p ∨ K1q.
Let w = hpAGT, dAGT, pATM , πi be a world such that w |=
K1(p ∨ q). We are going to prove that either w |= K1p or
w |= K1q. We have pATM (p) ∈ cone(
Informally, K1(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 K1p or K1q. Nevertheless, K1(ϕ∨ψ) → K1ϕ∨ K1ψ is not valid in L☼1D .
Notice that there are crucial differences between S5n and L☼1D : • S5n is defined as the logic of a class of frames and has the property of uniform substitution. If |=S5n ϕ[p], we have |=S5n ϕ[ψ/p] for every formula ψ ∈ LAGT; • On the contrary (see Definition 12), L☼1D is defined as the set of formulas valid on one model: the model M. As the definition of Ra (Definition 4) depends on worlds, and especially on valuations, it is not surprising that L☼1D does not have the property of uniform substitution. A just one model semantics may seem a poor pedagogical application. But, the model M is big (if AGT and ATM are finite, the size of M is exponential in card(ATM ∪ AGT). In fact, you can imagine the model M to be a kind of canonical model. The model M is made up with many connected components. For instance, Figure 2 and 8 show two connected components of the model M.
Now, here is a Proposition showing that we can have common knowledge only when K1K2p ∧ K2K1p.
Proposition 3: We have: |=L☼1D K1K2p ∧ K2K1p → K1K2K1 . . . K2 . . . p where “K1K2K1 . . . K2 . . . ” denotes any finite sequence of K1 and K2.
Proof: Let w = hpAGT, dAGT, pATM , πi be world such
that w |= K1K2p ∧ K2K1p. We want to prove that w |=
K1K2K1 . . . K2 . . . p. We are going to prove that:
• pAGT(
Let us prove pATM (p) ∈ cone(
We have w0 6|= p so w0 6|= K2p. So w 6|= K1K2p. Contradiction.
Same proof for pATM (p) ∈ cone(
Let us prove that pAGT(
Same proof for pAGT(
Now we can prove by induction on n that for n ∈ N, for
all u ∈ (R1 ◦ R2)n(w), we have:
• pAGT(
• π(p) = >.
Hence w |= K1K2K1 . . . K2 . . . p.
The validity K1K2p ∧ K2K1p → K1K2K1 . . . K2 . . . p expresses that if K1K2p ∧ K2K1p 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, S5n ( L☼1D .
Proof: The formula K1(p∨q) → K1p∨K1q and K1K2p∧ K2K1p → K1K2K1p are in L☼1D but are not valid in S5n.
More surprising is the fact that common knowledge is not guaranteed by K1K2ϕ ∧ K2K1ϕ for all ϕ. More precisely, K1K2ϕ ∧ K2K1ϕ → K1K2K1ϕ 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 |= K1K2¬K2p ∧ K2K1¬K2p. But, we have w 6|= K1K2K1¬K2p. Indeed there exists w0 such that wR1 ◦ R2 ◦ R1w0 such that w0 |= K2p.
Nevertheless, there are other formulas where it remains true. For instance, we have |=L☼1D K1K2K3p ∧ K2K1K3p → K1K2K1 . . . K2 . . . K3p.
Question 1: What about K1K2ϕ ∧ K2K1ϕ → K1K2K1ϕ if ϕ do not contain agent 1 or 2? Do we have a characterisation or exhibit an interesting set of formulas ϕ such that K1K2ϕ ∧ K2K1ϕ → K1K2K1ϕ holds?
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 Ra(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 they are ordered on the line. For instance, ☼ p a and ☼ p a
stands for the same world. We can 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 dAGT and π. Notice that we can do this because the space is a line. If our space were Rn (n ≥ 2), the notion of total preorder would unfortunately not be suited anymore.
A description of a world w is a tuple h<, dAGT, πi where: • ≤ is a total preorder over AGT ∪ ATM ; • dAGT : AGT → {−1, +1}; • π : ATM → {⊥, >}.
We can also define the epistemic relation between two description of a world w:
Let a ∈ AGT. We define the epistemic relation Ra on the set of descriptions of worlds by wRav iff: • if dAGT(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 dAGTw(x) = dAGTv(y); – for all x ∈ ATM , a ≤w x implies πw(x) = πv(y). • if dAGT(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 dAGTw(x) = dAGTv(y); – for all x ∈ ATM , a ≥w x implies πw(x) = πv(y). function check(w, ϕ) match (ϕ) >: ¬ψ: Kaψ:
return >; p ∈ ATM : return > if p is true in w; return ⊥ if p is false in w; ψ1 ∧ ψ2: return check(w, ψ1) ∧ check(w, ψ2); return ¬check(w, ψ); • for all x, y ∈ AGT ∪ ATM , x ≤d(w) y iff p(x) ≤R p(y) where p(x) stands for pAGT(x) if x ∈ AGT or pATM (x) if x ∈ ATM ;
Proposition 4: For all w ∈ W , for all ϕ ∈ LAGT, 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].
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 ϕ ∈ LAGT, 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 ϕ ∈ LAGT; • Output: Yes iff there exists a world w such that w |=L☼1D ϕ. No, otherwise. endMatch endFunction Fig. 3. A PSPACE-algorithm for model-checking of L☼1D 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, Kaψ) terminates. By induction, T (ψ) so every call check(u, ψ) terminates. So the call check(w, Kaψ) terminates and T (Kaψ); • 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 ∈ Ra(w) do ”: although Ra(w) may be of size exponential we do not compute it. Here we only enumerate here elements of Ra(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 Ra(w).
The block: 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 ∈ Ra(w) if check(u, ψ) = ⊥ then
return ⊥; endIf u := next_permutation(u); endWhile
endIf 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 – next_permutation( 0 p ) = ☼ ) = p 0 0 ☼ ; p ☼ ; p – next_permutation( 0 ☼ ) = p p 0 etc. • is_last_permutation(u) =
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”. • P(>) and P(p) are true; • Let us prove P(ψ1∧ψ2). The first call check(w, ϕ1) needs O(|ϕ1| × | |
w ) by hypothesis of induction.
Then we can release all the memory cells used for the sub-call check(w, ϕ1) and we can treat the call check(w, ϕ2). It needs O(|ϕ2| × |w|). Hence, the sub-call check(w, ϕ1 ∧ ϕ2) needs max(O(|ϕ1| × |w|), O(|ϕ2|×|w|)) = O(|ϕ|×|w|). So P(ψ1 ∧ψ2). function sat(ϕ) w := choose_world_with_symbols_in(ϕ) return check1(w, ϕ) endFunction • Now, we prove P(Kaψ). By induction, every sub-call check(w, ψ) needs at most O(|ψ| × | | w ) memory cells. Furthermore, we need O(|w|) for f irst_permutation(w), is_last_permutation(u) and next_permutation(u) and also to keep the local variable u in memory. So we need, O(|ψ| × |w|) + O(|w|) = O(|ϕ| × |w|).
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 (*) ).
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 S5n satisfiability problem as comparison. C. When AGT is infinite: PSPACE-complete
We recall the complexity result about QBF formulas satis> iff u has no <- fiability problem:
Theorem 1: The QSAT-problem defined as following: • Input: a formula ϕ = ∃p~1∀p~2∃p~3∀p~4 . . . Qnp~nψ where: – n is any integer; – ψ is a boolean formula; – and Qi = ∀ if i is even and Qi = ∃ 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☼1D satisfiability problem instance.
Proposition 7: Let ϕ = ∃p~1∀p~2∃p~3∀p~4 . . . Qnp~nψ be a formula of the logic QBF. We define f (ϕ) by induction: • f (ψ) = ψ; •• ff ((∃∀pp~~ii......QQnnpp~~nnψψ)) == KKˆii−−11((ppuuttii ∧→ff(∀(∃p~p~i+i+11.....Q.Qnnp~p~nnψψ);); where: •• pKuaitfp~a == VVi∈{a+1...2n} ¬Kaifp~i ∧ Vi∈{1...a} Kaifp~i; q∈p~ Kaifq; • Kaifq = Kaq ∨ Ka¬q.
We have equivalence between: • |=QBF ϕ; • put1 ∧ f (∀p~2∃p~3∀p~4 . . . Qnp~nψ) is L☼1D AGT-satisfiable; • and w |=L☼1D f (ϕ) where w ∈ W0 where W0 is the set of all worlds where agent 0 is completely on the left looking to the left. (we note W0 = “ 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 W0 |=L☼1D f (ϕ). We are going to note for all i ∈ N, for all valuation ν[p~1, . . . p~i],
Wi(ν[p~1, . . . p~i]) k def “ 0
☼ ~ν(p1) 1
☼ ν(p~2) 2 . . . ν(☼p~i)
Wi−1(p~1, . . . p~i−1) |=L☼1D f (Qip~i . . . Qnp~nψ) .
The basis case correspond to i = n+1. It is the propositional case. We have:
ν[p~1, . . . p~n] |=QBF ψ iff Wn(p~1, . . . p~n) |=L☼1D ψ.
Now we can attack the induction case. Let us prove for i odd. ν[p~1, . . . p~i−1] |=QBF Qip~i . . . Qnp~nψ means that there exists a valuation ν(pi) such that ν[p~1, . . . p~i] |=QBF Qi+1p~i+1 . . . Qnp~nψ. By induction, it means that Wi(p~1, . . . p~i) |=L☼1D f (Qip~i . . . Qnp~nψ).
But for all wi−1 ∈ Wi−1(p~1, . . . p~i−1) and for all wi ∈ Wi(p~1, . . . p~i), we have: • wi−1Ri−1wi; • wi |= puti. Indeed, for all j > i, we have w |= ¬Kiifp~j because agent j does not see lamps p~j in wi. On the contrary, for all j < i, we have w |= Kiifp~j because agent i do see lamps p~j in wi (the valuation of lamps p~j is the same in all worlds u ∈ Ri(wi)). The technical proof of wi |= puti is left to the reader.
As f (∃p~i . . . Qnp~nψ) = Kˆi−1(puti ∧ f (∀p~i+1 . . . Qnp~nψ), we have:
Wi−1(p~1, . . . p~i−1) |=L☼1D f (∃p~i . . . Qnp~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.
We recall the complexity result about QBF formulas satisifability problem but when the nesting of ∀ and ∃ is bounded by a fixed integer n.
Theorem 2: Let n be a integer. The QSATn-problem deifned as following: • Input: a formula ϕ = ∃p~1∀p~2∃p~3∀p~4 . . . Qnp~nψ where ψ is a boolean formula, and Qi = ∀ if i is even and Qi = ∃ 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 ifnite 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)+1P-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 Δ2P.
Proof: The figure 6 gives us an Δ2P-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 endIf endWhile return P CL({⊥, >}) − sat(ψ); endFunction Fig. 6. A Δ2P -algorithm for model checking of L☼1D {1} Fig. 7. Optimal Σ2P-algorithm for satisfiability problem of L☼1D {1} where p ∈ ATM and a ∈ AGT.
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 S5n.
Our new language L!AGT is defined by the following BNF: ϕ ::= p | ϕ ∧ ϕ | ¬ϕ | Kaψ | [ϕ!]ϕ in ϕ by the corresponding valuation πw(p). Concerning a proposition p ∈ I, we only replace occurrences which are not in the scope of a K1. For instance, if p ∈ I, q ∈ V , and πw(p) = >, πw(q) = ⊥ p ∧ q ∨ K1(p ∨ q) is replaced by > ∧ ⊥ ∨ K1(p ∨ ⊥). Then we test satisfiability of boolean formulas ¬χ such that K1χ is a subformula of ψ and replace K1χ 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 Σ2P-complete.
Proof:
The hardness comes from Corollary 5. The Figure 7 gives us an Σ2P-algorithm (a NP-algorithm with NP-oracles) for the satisfiability problem of L☼1D {1}.
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.
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, w |= ϕ and U, w |= ψ; • U, w |= ¬ϕ iff U, w 6|= ϕ; • U, w |= Kaψ iff for all w0 ∈ U , wRaw0 implies U, w0 |= ψ; • U, w |= [ϕ!]ψ iff U, w |= ϕ implies U ∩ {w0 ∈ U | U, w0 |= ϕ}, w |= ψ.
The set of validities we obtain is noted L☼1D ! = {ϕ | W, w |= ϕ} where W is the set of all worlds defined Definition 8.
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 |= K1q ∧ K2p; • W, w |= ¬K1p ∧ ¬K1(¬p) ∧ ¬K2(¬q).
Then: • the father says at least one of them are dirty; Fig. 9. World for Muddy children after having announced ϕ1
• 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: • |C| + |ϕ| < |D| + |ψ|; • or where |C| + |ϕ| = |D| + |ψ| and |ϕ| < |ψ| function mc!(w, C, ϕ) match (ϕ) >: and return >; p ∈ ATM : return > if p is true in w; return ⊥ if p is false in w; ψ1 ∧ ψ2:
return mc!(w, C, ψ1) ∧ mc!(w, C, ψ2); ¬ψ: Kaψ: return ¬mc!(w, C, ψ); for u ∈ Ra(w) do if inupdatedM (u, C) mc!(u, ψ) = ⊥ then
return ⊥; endIf endFor return >; [ψ1!]ψ2: if mc!(w, C, ψ1) then
return mc!(w, [ψ1 : C], ψ2) else endIf
return >
• 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, C0, ψ), we have |C0| + |ψ| = |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. function inpudatedM (w, C) match (C) []: return >; [ψ : C0]: mc!(w, C0, ψ); endMatch endFunction Fig. 12. Algorithm for testing if a world w is in the updated model formulas in C
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.
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 Ra(w).
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 |= K1p ∧ K2q 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 |= K1p ∧ K2q.
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!](K1p ∧ K2q). 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.
The epistemic logic S5n 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 R2 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. Acknowledgements.
I thank Philippe Balbiani, Olivier Gasquet, Andreas Herzig, Emiliano Lorini and the reviewers for their different helpful remarks.