=Paper=
{{Paper
|id=Vol-494/paper-22
|storemode=property
|title=Knowledge about Lights along a Line
|pdfUrl=https://ceur-ws.org/Vol-494/famaspaper4.pdf
|volume=Vol-494
|dblpUrl=https://dblp.org/rec/conf/mallow/Schwarzentruber09
}}
==Knowledge about Lights along a Line==
https://ceur-ws.org/Vol-494/famaspaper4.pdf
1
Knowledge about lights along a line
François S CHWARZENTRUBER
Abstract—In this article, we are going to talk about spatial sit- you put agents and lamps and then you can write formulas in
uations. Every agent (human, camera etc.) and every proposition epistemic logic to check whether properties over those agents
(lamp, object, etc.) are located in the space (here a line) and we and lamps are true.
express properties over a situation using standard epistemic logic
language possibly extended with public announcements. We study Generally speaking many examples of epistemic situation
links between validities of this geometrical version of epistemic mix time and space. The link between time and knowledge
logic and the standard one. We also investigate complexities of (perfect recall etc.) has been studied and you can find a
model checking and satisfiability. survey in [3]. There exists also some work linking space and
Keywords: Multi-agent system. Epistemic logic. Spatial rea- knowledge like in [10]: they provide a logic with a spatial
soning. Public announcements. Pedagogical tool. Complexity modal operator dealing with topology and an epistemic modal
theory. Polynomial hierarchy. operator. Here, our approach is different: we want to deal
with a spatially grounded epistemic logic. We are not going to
I. I NTRODUCTION provide operators in the language to deal with space but only
Many authors in logic and in Artificial Intelligence [5] provide an epistemic operator for each agent in the language.
developed epistemic logic and studied mathematical properties The semantics will then directly rely on the geometrical
of it. Epistemic logic is theoretical and may be difficult to properties of a line. We would like to describe a situation
explain to students. This is the reason why in this article we but directly by the graphical and natural representation of the
are going to study a concrete example of multi-agent system. system and not with a Kripke structure. We can formalize well
Let us take a line. We are going to put lamps and agents known toy examples as Russian cards [13], Muddy children
on this line as shown in the Figure 1. Now the question is ([4], [11], [3]) or the prisoner’s test. For instance:
“what do agents know about lamps and knowledge of other • The Muddy children. The spatial configuration
agents about lamps”? This system has been implemented as is the following: two children are looking at
a pedagogical tool in order to illustrate any epistemic logic each other. One knows the other’s forehead
course. Indeed, students can easily understand some epistemic is dirty. But one does not know he is
logic on concrete examples:
☼ ☼
☼ dirty. b
• Agent a sees the lamp p on, so he knows p; a’s forehead_dirty a b’s forehead_dirty
a p
• Agent a does not see the lamp p, so he does not know • The prisoner’s test. There are three prisoners on a
☼ line. Each prisoner must guess the color of his head.
whether p or ¬p;
pa ☼ ☼
• Agent a sees another agent b seeing the lamp p on, so pr1 ’s head pr1 pr2 ’s head pr2 pr3 ’s head pr3
☼ Another motivation would be video surveillance. Proposi-
agent a knows agent b knows p;
a b p tions are objects we have to take care of. Agents are camera.
• Agent a sees another agent b, and the lamp p, but agent We then can specify the video surveillance with epistemic
a sees that agent b is not looking in the direction of the logic formulas. Another possible application may be robots’
lamp p, so agent a knows agent b does not know whether space and knowledge reasoning because robots evolve in
our spatial world. A last application could be video games.
☼
p or ¬p; In many role playing games or strategy games, players or
a p b non-playing characters can have knowledge about the virtual
• Agent a and agent b are looking at each other and there is world. The behaviours of a non-playing character can then
the lamp p between them, so there is common knowledge be described by the game designer using a knowledge based
that p is true. This kind of situations have already been 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
considered in [8]. b
a p formalizing the video game Thief has been done in [7].
A piece of software is available on the Web Site http://www.
This approach can be compared to the approach in [2] for irit.fr/~Francois.Schwarzentruber/agentsandlamps/. It provides
first order logic. In [2], you put objects like cube, pyramids a model-checker: you specify the graphical situation and a
and you can then write formulas in first order logic to check formula written using epistemic modal operators and/or public
properties over those objects. Here the approach is similar: announcements operators. In this article:
2
• We are going to present the semantics of the geometric
version of epistemic logic in section II; ☼ ☼
p1 2 p2 3 p3
• We are going to deal with the model checking and 1
satisfiability problems’ complexities in section III;
• In section IV, we will add public announcements to our Fig. 1. Example of a world
language to model examples like Muddy children;
• In section V, we are going to present the current imple-
mentation. • π : ATM → {⊥, >}.
The set of all worlds is noted W .
II. S EMANTICS In a world hpAGT , dAGT , pATM , πi, pAGT (a) denotes the posi-
We are going to define a new logic based on the same tion of agent a. dAGT (a) denotes the direction where the agent
language than the epistemic logic S5n [5]. S5n is the logic of a looks: if dAGT (a) = +1, the agent a will look on the right and
frames where relations are equivalence relations. Here we are if dAGT (a) = −1, he will look on the left. pATM (p) denotes the
defining a logic where the semantics is based on a geometric position of the lamp saying whether p is true or not. π(p) = >
point of view. iff the lamp “p” is on. π(p) = ⊥ means that the lamp “p” is
off.
A. Language We have defined a world in the more close to the reality
manner: that is to say using the real numbers. We could also
Our logic is based on the same language as S5n ’s one. Let
consider locations of agents and lamps as a total preorder over
us recall the language of the epistemic logic S5n [5].
ATM ∪ AGT. Considering a total preorder is discussed at the
Definition 1 (language):
end of this section and total preorder is used in Section III.
Let ATM be a countable set of atomic propositions. Let AGT
Here we prefer to use the Definition 8 whose advantage is that
be a countable set of agents. The language LAGT is defined by
it can be easily generalized to dimension n ≥ 2: you just have
the following BNF:
to replace R by Rn and to adapt the notion of direction. In
dimension 2 or more, total preorders can no longer be used.
ϕ ::= > | p | ϕ ∧ ϕ | ¬ϕ | Ka ψ
We can also discuss the Definition 8 by the way propositions
where p ∈ ATM and a ∈ AGT. are treated. Here, a proposition p is associated to a point
As usual, ϕ ∨ ψ =def ¬(¬ϕ ∧ ¬ψ). K̂a ψ =def ¬Ka ¬ψ. pATM (p). This seems to be the simple way to define the
Notice that we can only deal with knowledge (operator semantics. But be aware that in some cases this is a limitation:
Ka ) and states of lamps (proposition p is true means that • Maybe a proposition p can be associated to a set of points.
the lamp called p is on) in the language. One may expect For instance, if you are at home, you can know it rains
to deal also with position of lamps, position of agents or either by looking towards the window of the left L or the
maybe spatial topologic operator like in [10] etc. This may window of the right R. Hence, here the proposition rain
be very interesting, especially in all applications cited in the may be associated to the set of points {L, R};
introduction. For instance, we can not express a sentence like • Maybe you want that a lamp is associated not to a
“the guardian knows that the beetle is near the old man.” but proposition but more generally to a formula. For instance,
we can say “The guardian knows that the beetle knows the when you know that the alarm system located on point P
old man’s hat is red.” (Kguardian Kbeetle old_man_red) Here is on, you in fact know that either there is an oil problem
we have preferred to keep the language of classical epistemic or overheating. Hence, here the point is associated to the
logic for two reasons: formula oil_problem ∨ overheating.
• a pedagogical tool for understanding epistemic logic Here we stay with the simple definition for two reasons:
should be simple and should have a simple syntax; • it is easier for a pedagogical tool to have a simple and
• to focus on complexity results with the simple expressiv-
clear semantics;
ity as S5n . • it is easier for us to begin study a simple case.
Definition 3 (cone):
B. Definitions Let us consider a world w = hpAGT , dAGT , pATM , πi. We note
The semantics is not defined with a class of models but cone(a) the set {pAGT (a) + λ.dAGT (a) | λ ∈ R+ }.
directly from what a concrete situation is. From this, we cone(a) denotes all the set of points the agent a sees.
will obtain a spatially grounded epistemic logic. A world
is situation where all agents have a location (position and Example 1: The Figure 1 gives us an example of a world
direction where they look), all lamps (atomic propositions) w. We have:
have a location and a state (on or off). Formally: • pAGT (1) = 0; pAGT (2) = 2; pAGT (3) = 4;
Definition 2 (world): • dAGT (1) = +1; dAGT (2) = −1; dAGT (3) = −1;
A world w is a tuple hpAGT , dAGT , pATM , πi where: • pATM (p1 ) = 1; pATM (p2 ) = 3; pATM (p3 ) = 5;
• pAGT : AGT → R; • π(p1 ) = >; π(p2 ) = ⊥; π(p3 ) = >;
• dAGT : AGT → {−1, +1}; • cone(1) = [0, +∞[;
• pATM : ATM → R; • cone(2) =] − ∞, 2];
3
• cone(3) =] − ∞, 4]. From now on, if pAGT (b) ∈ cone(a), then pAGT (b) = p0AGT (b)
and dAGT (b) = d0AGT (b). But, we have effectivelly, pAGT (b) =
Now we are going to define the epistemic relation over worlds. p0AGT (b) and cone(a) = cone0 (a). So p0AGT (b) ∈ cone0 (a). So
wRa u means that agent a can not distinguish w from u. In p0AGT (b) = p00AGT (b) and d0AGT (b) = d00AGT (b). Finally, pAGT (b) =
other words, wRa u iff agent a sees the same things in w and p00AGT (b) and dAGT (b) = d00AGT (b). The other cases are treated in
u. Formally: the same manner.
Definition 4 (epistemic relation): The semantics of Ka p in L☼1D corresponds to the fact
Let a ∈ AGT. We define the relation Ra over worlds: that the agent a sees the light p and the light p is on. More
hpAGT , dAGT , pATM , πiRa hp0AGT , d0AGT , p0ATM , π 0 i iff for all b ∈ generally, Ka ψ means that the agent a has the proof that ψ.
AGT, for all p ∈ ATM , That is why we have those validities in L☼1D :
• if pAGT (b) ∈ cone(a) then Proposition 2: Let p, q ∈ ATM .
pAGT (b) = p0AGT (b) and dAGT (b) = d0AGT (b); |=L☼1D K1 (p ∨ q) → K1 p ∨ K1 q.
0
• if pAGT (b) 6∈ cone(a) then pAGT (b) 6∈ cone(a);
|=L☼1D K1 (¬p ∨ ¬q) → K1 ¬p ∨ K1 ¬q.
• if pATM (p) ∈ cone(a) then
If p 6= q, |=L☼1D K1 (p ∨ ¬q) → K1 p ∨ K1 ¬q
pATM (p) = p0ATM (p) and π(p) = π 0 (p) Proof: Let us prove |=L☼1D K1 (p ∨ q) → K1 p ∨ K1 q.
0
• if pATM (p) 6∈ cone(a) then pATM (p) 6∈ cone(a).
Let w = hpAGT , dAGT , pATM , πi be a world such that w |=
K1 (p ∨ q). We are going to prove that either w |= K1 p or
Briefly, suppose that wRa u. If agent a see the agent b in the
w |= K1 q. We have pATM (p) ∈ cone(1) or pATM (q) ∈
world w, then he will also see agent b in world u and agent b
cone(1). Indeed, if we suppose the contrary, that is to say
will have the same location (position and direction). If agent
pATM (p) 6∈ cone(1) and pATM (q) 6∈ cone(1), there exists a
a does not see agent b in the world w, then he also does not
world u = hpAGT , dAGT , pATM , π 0 i such that π 0 (p) = ⊥ and
see agent b in u. If agent a see the lamp p in the world w,
π 0 (q) = ⊥ and wR1 u. Hence, w 6|= K1 (p ∨ q). Contradiction.
then he will also see the lamp p in world u. The lamp will
So pATM (p) ∈ cone(1) or pATM (q) ∈ cone(1). For instance,
have the same position and state both in w and u. If agent a
pATM (p) ∈ cone(1). And for all u ∈ R1 (w), πu (p) = >. So
does not see the lamp p in w, then he will also not see the
w |= K1 p. The other cases are treated in the same manner.
lamp p in u.
Informally, K1 (p ∨ q) means that agent 1 has a proof that
Until now, we have finally defined a model M =
p ∨ q. In other words, either he sees p on, or he sees q on.
hW, (Ra )a∈AGT , νi where ν maps each world w ∈ W to πw .
Hence, either K1 p or K1 q. Nevertheless, K1 (ϕ∨ψ) → K1 ϕ∨
From now, the truth conditions is standard:
K1 ψ is not valid in L☼1D .
Definition 5 (truth conditions):
Notice that there are crucial differences between S5n and
Let w ∈ W . We define w |= ϕ by induction:
L☼1D :
• w |= >;
• S5n is defined as the logic of a class of frames and has
• w |= p iff π(p) = >
the property of uniform substitution. If |=S5n ϕ[p], we
• w |= ϕ ∧ ψ iff w |= ϕ and w |= ψ;
have |=S5n ϕ[ψ/p] for every formula ψ ∈ LAGT ;
• w |= ¬ϕ iff w 6|= ϕ; ☼
• On the contrary (see Definition 12), L 1D is defined
0 0 0
• w |= Ka ψ iff for all w , wRa w implies w |= ψ.
as the set of formulas valid on one model: the model
M. As the definition of Ra (Definition 4) depends on
C. Comparison with epistemic logic worlds, and especially on valuations, it is not surprising
Now we are going to compare the epistemic logic S5n and that L☼1D does not have the property of uniform sub-
the set of validities we obtain with the truth conditions of stitution. A just one model semantics may seem a poor
Definition 12. First we give the definition of validities. pedagogical application. But, the model M is big (if AGT
Definition 6 (set of validities): and ATM are finite, the size of M is exponential in
We denote the set of all validities by L☼1D , that is to say, card(ATM ∪ AGT). In fact, you can imagine the model
L☼1D = {ϕ ∈ LAGT | ∀w ∈ W, w |= ϕ}. M to be a kind of canonical model. The model M is
In “L☼1D ”, “1D” stands for “one dimension” (a line). Now, made up with many connected components. For instance,
we can see that our set L☼1D contains all validities of S5n . Figure 2 and 8 show two connected components of the
Proposition 1: S5n ⊆ L☼1D . model M.
Proof: We prove that for all a ∈ AGT, the relation
Ra is an equivalence relation. Hence, the model M Now, here is a Proposition showing that we can have
is a model of the logic S5n and satisfies validities common knowledge only when K1 K2 p ∧ K2 K1 p.
of S5n . We have to prove reflexivity, symmetry and Proposition 3: We have:
transitivity. Let us just begin to prove transitivity. Suppose |=L☼1D K1 K2 p ∧ K2 K1 p → K1 K2 K1 . . . K2 . . . p where
we have: hpAGT , dAGT , pATM , πiRa hp0AGT , d0AGT , p0ATM , π 0 i “K1 K2 K1 . . . K2 . . . ” denotes any finite sequence of K1 and
and hp0AGT , d0AGT , p0ATM , π 0 iRa hp00AGT , d00AGT , p00ATM , π 00 i. Let us K2 .
prove that hpAGT , dAGT , pATM , πiRa hp00AGT , d00AGT , p00ATM , π 00 i. Proof: Let w = hpAGT , dAGT , pATM , πi be world such
First we have pAGT (a) ∈ cone(a). So pAGT (a) = p0AGT (a) = that w |= K1 K2 p ∧ K2 K1 p. We want to prove that w |=
pAGT (a) and dAGT (a) = d0AGT (a) = d00AGT (a). In other words,
00 K1 K2 K1 . . . K2 . . . p. We are going to prove that:
cone(a) = cone0 (a) = cone00 (a). • pAGT (2) ∈ cone(1);
4
• pAGT (1) ∈ cone(2);
• pATM (p) ∈ cone(1);
• pATM (p) ∈ cone(2).
Let us prove pATM (p) ∈ cone(1) by contradiction. Suppose
that pATM (p) 6∈ cone(1). Thus there exists a world w0 =
hp0AGT , d0AGT , p0ATM , π 0 i such that wR1 w0 and π 0 (p) = ⊥.
We have w0 6|= p so w0 6|= K2 p. So w 6|= K1 K2 p.
Contradiction.
Same proof for pATM (p) ∈ cone(2).
Let us prove that pAGT (2) ∈ cone(1) by contradiction.
Suppose that pAGT (2) 6∈ cone(1). Thus there exists a world
w0 = hp0AGT , d0AGT , p0ATM , π 0 i such that w R1 w0 and d0AGT (2)
is such that pATM (p) 6∈ cone0 (2). Thus, there exists a world
w00 = hp00AGT , d00AGT , p00ATM , π 00 i such that w0 R2 w00 and π 00 (p) =
⊥. So w0 6|= K2 p. Hence w 6|= K1 K2 p. Contradiction.
Same proof for pAGT (1) ∈ cone(2). Fig. 2. Some worlds of the model M
Now we can prove by induction on n that for n ∈ N, for
all u ∈ (R1 ◦ R2 )n (w), we have:
• pAGT (2) ∈ cone(1);
☼
• pAGT (1) ∈ cone(2); they are ordered on the line. For instance, a and
p
• pATM (p) ∈ cone(1);
• pATM (p) ∈ cone(2).
• π(p) = >.
Hence w |= K1 K2 K1 . . . K2 . . . p.
☼
a stands for the same world. We can
p
The validity K1 K2 p ∧ K2 K1 p → K1 K2 K1 . . . K2 . . . p
expresses that if K1 K2 p ∧ K2 K1 p then the state of the lamp define the notion of description of a world w: it is simply a
p is the topic of a mutual social perception, studied in [8]. total preorder over all propositions and agents appearing in a
formula, plus dAGT and π. Notice that we can do this because
Corollary 1: If n ≥ 2 or card(ATM ) ≥ 2, S5n ( L☼1D . the space is a line. If our space were Rn (n ≥ 2), the notion
Proof: The formula K1 (p∨q) → K1 p∨K1 q and K1 K2 p∧ of total preorder would unfortunately not be suited anymore.
K2 K1 p → K1 K2 K1 p are in L☼1D but are not valid in S5n .
More surprising is the fact that common knowledge is not Definition 7 (description of a world):
guaranteed by K1 K2 ϕ ∧ K2 K1 ϕ for all ϕ. More precisely, A description of a world w is a tuple h<, dAGT , πi where:
K1 K2 ϕ ∧ K2 K1 ϕ → K1 K2 K1 ϕ is not L☼1D -valid for all ϕ. • ≤ is a total preorder over AGT ∪ ATM ;
Look at the model of the Figure 2: agent 1 = agent in blue. • dAGT : AGT → {−1, +1};
agent 2 = agent in red. Consider the world on the bottom • π : ATM → {⊥, >}.
on the right. Let us call it w. We have w |= K1 K2 ¬K2 p ∧ We can also define the epistemic relation between two
K2 K1 ¬K2 p. But, we have w 6|= K1 K2 K1 ¬K2 p. Indeed there description of a world w:
exists w0 such that wR1 ◦ R2 ◦ R1 w0 such that w0 |= K2 p.
Nevertheless, there are other formulas where it remains true. Definition 8 (epistemic relation):
For instance, we have |=L☼1D K1 K2 K3 p ∧ K2 K1 K3 p → Let a ∈ AGT. We define the epistemic relation Ra on the set
K1 K2 K1 . . . K2 . . . K3 p. of descriptions of worlds by wRa v iff:
Question 1: What about K1 K2 ϕ ∧ K2 K1 ϕ → K1 K2 K1 ϕ • if dAGT (a) = +1,
if ϕ do not contain agent 1 or 2? Do we have a characterisation – for all x ∈ AGT ∪ ATM , (x ≤w a iff x ≤v a);
or exhibit an interesting set of formulas ϕ such that K1 K2 ϕ ∧ – for all x, y ∈ AGT ∪ ATM such that a ≤w x and
K2 K1 ϕ → K1 K2 K1 ϕ holds? a ≤w y, we have (x ≤w y iff x ≤v y);
– for all x ∈ AGT, a ≤w x implies dAGT w (x) =
D. A compact representation dAGT v (y);
Last but not the least, you can remark that if we want – for all x ∈ ATM , a ≤w x implies πw (x) = πv (y).
to deal with model-checking, satisfiability problem and other • if dAGT (a) = −1,
algorithmic problems, we need a compact representation that – for all x ∈ AGT ∪ ATM , (x ≥w a iff x ≥v a);
an algorithm can manipulate. Worlds are difficult to manip- – for all x, y ∈ AGT ∪ ATM such that a ≥w x and
ulate: in particular, it is unadapted that Ra (w) is infinite a ≥w y, we have (x ≥w y iff x ≥v y);
given a agent a and a world w. According to the Definition – for all x ∈ AGT, a ≥w x implies dAGT w (x) =
8, the set W is infinite. Nevertheless, the semantics do not dAGT v (y);
depend on positions of lamps and agents but only on how – for all x ∈ ATM , a ≥w x implies πw (x) = πv (y).
5
In the same way, we can define an epistemic model. We function check(w, ϕ)
can define truth conditions of a formula ϕ in LAGT over the match (ϕ)
>:
set of descriptions of worlds, using the epistemic relation. We
return >;
can prove that we obtain the same validities.
p ∈ ATM :
Definition 9 (extracting description of world from a world): return > if p is true in w;
return ⊥ if p is false in w;
Given a world w, we define the description of world ψ 1 ∧ ψ2 :
d(w) by: return check(w, ψ1 ) ∧ check(w, ψ2 );
¬ψ:
• for all x, y ∈ AGT ∪ ATM , x ≤d(w) y iff p(x) ≤R p(y)
return ¬check(w, ψ);
where p(x) stands for pAGT (x) if x ∈ AGT or pATM (x)
Ka ψ:
if x ∈ ATM ; for u ∈ Ra (w) do
• dAGTw = dAGTd(w) ; if check(u, ψ) = ⊥ then
• πw = πv . return ⊥;
Proposition 4: For all w ∈ W , for all ϕ ∈ LAGT , w |= ϕ endIf
endFor
iff d(w) |= ϕ. return >;
Proof: By induction on ϕ. endMatch
endFunction
In the case of one dimension, we simply rewrite mapping
from ATM or AGT to real numbers into a total preorder over Fig. 3. A PSPACE-algorithm for model-checking of L☼1D AGT
ATM ∪ AGT. In the case of two or more dimensions, it is an
open problem how to represent a world in a compact way.
B. PSPACE-ness upper-bound of the two problems
III. M ODEL - CHECKING AND SATISFIABILITY PROBLEM In this subsection, we are going to give PSPACE-ness
upper-bound of the model checking problem and also of the
For definitions for complexity class and for more details satisfiability problem. As you will see, the proof are directly
about the problem QSAT (quantified boolean formulas satisfi- given with algorithms using a polynomial amount of memory
ability problem), the reader may refer to [9]. (Figures 3 and 4).
Proposition 5: Let AGT be any set of agents. The model-
checking of L☼1D AGT problem is in PSPACE.
A. Definitions Proof:
Now we are going to recall the classical problem of model- You can take a look at the recursive algorithm of Figure 3.
checking and satisfiability. The problem of model-checking We have to prove three points: terminaison, correctness and
consists on testing if a given formula ϕ is true in a given PSPACE-ness.
world w. Satisfiability problem consists to test if there exists 1) First let us prove terminaison by induction on ϕ. Let
a world w in which a given formula ϕ is true. T (ϕ) be the property “for every world w, the call
check(w, ϕ) terminates”.
Definition 10 (model-checking of L☼1D AGT,ATM ): • check(w, >) and check(w, p) terminates. So T (>)
Let AGT be a set of agents and ATM a set of atoms. We and T (p);
call model-checking of L☼1D AGT,ATM problem the following • Let us prove that check(w, Ka ψ) terminates. By
problem: induction, T (ψ) so every call check(u, ψ) termi-
• Input: a formula ϕ ∈ LAGT , a description of a world w nates. So the call check(w, Ka ψ) terminates and
where only atoms and agents occurring in ϕ are given; T (Ka ψ);
• Other cases are treated in the same manner.
• Output: Yes iff we have w |=L☼1D ϕ. No, otherwise.
2) Secondly, we have to prove correctness. Correctness
In the previous Definition, we give a description of a world
corresponds to the property C(ϕ) defined by “for all
w that is to say a total preorder over all agents and propositions
world w, w |= ϕ iff check(w, ϕ) = >”. We also prove
occurring in ϕ where we say for each agent if he is look on
C(ϕ) for all formula ϕ by induction.
the left or on the right and for each proposition if it is true
3) Finally, we prove that check only requires a polyno-
or not. We do not care about propositions or agents not in the
mial amount of memory. Just be careful at the line
formula ϕ. The description of w is then finite.
“for u ∈ Ra (w) do ”: although Ra (w) may be of
size exponential we do not compute it. Here we only
Definition 11 (L☼1D AGT -satisfiability problem):
enumerate here elements of Ra (w) one by one. This
Let AGT be a set of agents. We call L☼1D AGT -satisfiability
can be done using only a linear amount of memory.
problem the following problem:
This part is technical but I will nevertheless give some
• Input: a formula ϕ ∈ LAGT ; details how to implement a enumeration of elements of
• Output: Yes iff there exists a world w such that w |=L☼1D Ra (w).
ϕ. No, otherwise. The block:
6
for u ∈ Ra (w) do function sat(ϕ)
if check(u, ψ) = ⊥ then w := choose_world_with_symbols_in(ϕ)
return ⊥; return check1(w, ϕ)
endIf endFunction
endFor
Fig. 4. A PSPACE-algorithm for satisfiability problem of L☼1D AGT
can be rewritten in a unreadable block using a linear
amount of memory in (*): card(AGT) L☼1D AGT − md L☼1D AGT − sat
1 Σ1 -hard, in Δ2 -hard Σ2 -complete
u := f irst_permutation(w) n ∈ N, n ≥ 2 Σn -hard, in ?? Σn+1 -hard, in ??
while ¬is_last_permutation(u) do ∞ PSPACE-complete PSPACE-complete
if u ∈ Ra (w)
if check(u, ψ) = ⊥ then card(AGT) S5card(AGT) − sat
return ⊥; 1 NP-complete
endIf n≥2 PSPACE-complete
endIf
∞ PSPACE-complete
u := next_permutation(u);
endWhile Fig. 5. Table of complexities
where:
• Now, we prove P(Ka ψ). By induction, every
• assuming we have an order < over permutations of
sub-call check(w, ψ) needs at most O(|ψ| × |w|)
elements appearing in w, f irst_permutation(w)
memory cells. Furthermore, we need O(|w|) for
gives, using a linear amount of memory, the first
f irst_permutation(w), is_last_permutation(u)
permutation we can make with elements of w; For
and next_permutation(u) and also to keep the
☼ local variable u in memory. So we need, O(|ψ| ×
instance, if w = 0 , f irst_permutation(w) |w|) + O(|w|) = O(|ϕ| × |w|).
p
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 (*) ).
can be 0 ;
p
Proposition 6: Let AGT be any set of agents. The L☼1D AGT -
• next_permutation(u) is a function, using a linear satisfiability problem is in PSPACE.
amount of memory, giving the <-successor of u; Proof: You can read the algorithm of Figure 4. The
For instance, we may have: 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
– next_permutation( 0 )= 0 ;
p p theorem [12], it is PSPACE.
Now we are going to investigate more in details com-
plexities of the model checking and satisfiability problem
☼ ☼
– next_permutation( 0 )= ; depending on the size of AGT. The table of Figure 5 sums
p 0 p
up all results we have. There is also the recall of complexity
results about S5n satisfiability problem as comparison.
☼
– next_permutation( )= 0 etc. C. When AGT is infinite: PSPACE-complete
0 p p
We recall the complexity result about QBF formulas satis-
• is_last_permutation(u) = > iff u has no <- fiability problem:
successor. Theorem 1: The QSAT-problem defined as following:
Now, we can prove by induction on ϕ the following • Input: a formula ϕ = ∃~ p1 ∀~
p2 ∃~
p3 ∀~
p4 . . . Qn p~n ψ where:
property for all ϕ, P(ϕ) defined as “for all world w, – n is any integer;
the call check(w, ϕ) needs O(|ϕ| × |w|) memory cells”. – ψ is a boolean formula;
• P(>) and P(p) are true; – and Qi = ∀ if i is even and Qi = ∃ if i is odd;
• Let us prove P(ψ1 ∧ψ2 ). The first call check(w, ϕ1 ) – p~j is a finite set of variables for each j.
needs O(|ϕ1 | × |w|) by hypothesis of induction. • Output: Yes iff |=QBF ϕ. No, otherwise.
Then we can release all the memory cells used for is PSPACE-complete.
the sub-call check(w, ϕ1 ) and we can treat the call
check(w, ϕ2 ). It needs O(|ϕ2 | × |w|). Hence, the Now the following Proposition gives a translation of a
sub-call check(w, ϕ1 ∧ ϕ2 ) needs max(O(|ϕ1 | × QBF-instance into a L☼1D -model-checking instance or a L☼1D -
|w|), O(|ϕ2 |×|w|)) = O(|ϕ|×|w|). So P(ψ1 ∧ψ2 ). satisfiability problem instance.
7
Proposition 7: Let ϕ = ∃~ p1 ∀~ p2 ∃~
p3 ∀~
p4 . . . Qn p~n ψ be a As f (∃~ pi . . . Qn p~n ψ) = K̂i−1 (puti ∧ f (∀~ pi+1 . . . Qn p~n ψ),
formula of the logic QBF. We define f (ϕ) by induction: we have:
• f (ψ) = ψ; Wi−1 (~ p1 , . . . p~i−1 ) |=L☼1D f (∃~
pi . . . Qn p~n ψ). We ensure
• f (∀~ pi ...Qn p~n ψ) = Ki−1 (puti → f (∃~ pi+1 ...Qn p~n ψ); that it is equivalent.
• f (∃~ pi ...Qn p~n ψ) = K̂i−1 (puti ∧ f (∀~ pi+1 ...Qn p~n ψ); The case where i is even is similar.
where:
V if
V Immediately from this translation, we deduce the lower
• puta = i∈{a+1...2n} ¬Ka p ~i ∧ i∈{1...a} Kaif p~i ; bound for model-checking in L☼1D .
if
V
• Ka p ~ = q∈~p Kaif q; Corollary 2: Let AGT an infinite enumerable set of agents.
The model-checking problem of L☼1D AGT is PSPACE-hard.
if
• Ka q = Ka q ∨ Ka ¬q.
We have equivalence between: Proof: Reduction via Proposition 7 and Theorem 1 in
• |=QBF ϕ; order to the PSPACE-hardness and Proposition 6.
• put1 ∧ f (∀~ p2 ∃~ p4 . . . Qn p~n ψ) is L☼1D AGT -satisfiable;
p3 ∀~ In the same way we have:
• and w |=L☼1D f (ϕ) where w ∈ W0 where W0 is the Corollary 3: Let AGT an infinite enumerable set of agents.
set of all worlds where agent 0 is completely on the left The satisfiability problem of L☼1D AGT is PSPACE-hard.
looking to the left. (we note W0 = “ 0 . . . ”). D. When AGT is finite
We recall the complexity result about QBF formulas satis-
fiability problem but when the nesting of ∀ and ∃ is bounded
Proof: We are going to note for all U ⊆ W , U |= ϕ iff by a fixed integer n.
for all u ∈ U , u |= ϕ. We are going to prove by induction Theorem 2: Let n be a integer. The QSATn -problem de-
|=QBF ϕ iff W0 |=L☼1D f (ϕ). We are going to note for all fined as following:
i ∈ N, for all valuation ν[~
p1 , . . . p~i ],
• Input: a formula ϕ = ∃~ p1 ∀~
p2 ∃~
p3 ∀~
p4 . . . Qn p~n ψ where ψ
Wi (ν[~
p1 , . . . p~i ]) is a boolean formula, and Qi = ∀ if i is even and Qi = ∃
if i is odd;
kdef • Output: Yes iff |=QBF ϕ. No, otherwise.
is Σn -complete.
☼ ☼ ☼ The Theorem 2 only differ from Theorem 1 by the fact that
“ 0 1 2 ... i ...00 . n is no more a input of the problem but is now fixed inside
~ν (p1 ) ν(~
p2 ) ν(~
pi )
the problem. For each integer n, we have defined the QSATn -
problem. There is a enumerable number of problems.
The induction hypothesis is:
In the same way, this precise complexity result of QBF
p1 , . . . p~i−1 ] |=QBF Qi p~i . . . Qn p~n ψ
ν[~ combined with the translation of QBF to L☼1D allows us
to have complexity lower bounds of model-checking and
iff
satisfiability problem when the cardinality of the set AGT is
p1 , . . . p~i−1 ) |=L☼1D f (Qi p~i . . . Qn p~n ψ)
Wi−1 (~ finite and fixed.
Corollary 4: Let AGT a finite set of agents. The model-
. checking problem of L☼1D AGT is Σcard(AGT) P-hard.
The basis case correspond to i = n+1. It is the propositional Proof: Reduction via Proposition 7 and Theorem 2.
case. We have: Corollary 5: Let AGT a finite set of agents. The satisfiabil-
ity problem of L☼1D AGT is Σcard(AGT)+1 P-hard.
p1 , . . . p~n ] |=QBF ψ iff Wn (~
ν[~ p1 , . . . p~n ) |=L☼1D ψ.
Proof: Reduction via Proposition 7 and Theorem 2.
Now we can attack the induction case. Let us prove
for i odd. ν[~ p1 , . . . p~i−1 ] |=QBF Qi p~i . . . Qn p~n ψ E. When card(AGT) = 1
means that there exists a valuation ν(pi ) such that Unfortunately we do not have a precise complexity upper-
ν[~p1 , . . . p~i ] |=QBF Qi+1 p~i+1 . . . Qn p~n ψ. By induction, bound for those problems in the general case when card(AGT)
it means that Wi (~ p1 , . . . p~i ) |=L☼1D f (Qi p~i . . . Qn p~n ψ). is finite. Nevertheless, we have the exact complexity when
But for all wi−1 ∈ Wi−1 (~ p1 , . . . p~i−1 ) and for all wi ∈ card(AGT) = 1.
Wi (~p1 , . . . p~i ), we have: Proposition 8: The model-checking problem of L☼1D {1} is
• wi−1 Ri−1 wi ; in Δ2 P.
if
• wi |= puti . Indeed, for all j > i, we have w |= ¬Ki p ~j Proof: The figure 6 gives us an Δ2 P-algorithm (a P-
because agent j does not see lamps p~j in wi . On the algorithm with NP-oracles) for the model-checking problem
contrary, for all j < i, we have w |= Kiif p~j because of L☼1D {1} . Given a world w, first we compute the V of
agent i do see lamps p~j in wi (the valuation of lamps propositions occurring in ϕ that the agent 1 sees and I
p~j is the same in all worlds u ∈ Ri (wi )). The technical the set of propositions the agent 1 does not see. Then we
proof of wi |= puti is left to the reader. can replace each occurrence p of a proposition p from V
8
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 K1 by πw (p);
while there exists K1 χ subformula of ψ, where χ is a Fig. 8. World for Muddy children
boolean formula do
if oracle − sat(¬χ) then
ψ := ψ in which we replace K1 χ by ⊥; IV. P UBLIC ANNOUNCEMENTS
else As done in [11] we can extend our framework with public
ψ := ψ in which we replace K1 χ by >; announcements. This is essentially motivated by modelling
endIf examples like Muddy children. With public announcements,
endWhile
return P CL({⊥, >}) − sat(ψ); an agent will be able to learn something about the part of the
endFunction actual world which he can not see. The technique is classical:
we add an operator [ϕ!] and we define semantics as in S5n .
Fig. 6. A Δ2 P -algorithm for model checking of L☼1D {1}
A. Definitions
function sat(ϕ)
w := choose_world_with_symbols_in(ϕ) Our new language L!AGT is defined by the following BNF:
return check1(w, ϕ)
endFunction ϕ ::= p | ϕ ∧ ϕ | ¬ϕ | Ka ψ | [ϕ!]ϕ
Fig. 7. Optimal Σ2 P-algorithm for satisfiability problem of L☼1D {1} where p ∈ ATM and a ∈ AGT.
From now, we do not only parameter |= with a world but
in ϕ by the corresponding valuation πw (p). Concerning a also with the set of worlds.
proposition p ∈ I, we only replace occurrences which are Definition 12 (truth conditions):
not in the scope of a K1 . For instance, if p ∈ I, q ∈ V , and Let U a set of worlds (U ⊆ W ). Let w ∈ U . We define
πw (p) = >, πw (q) = ⊥ p ∧ q ∨ K1 (p ∨ q) is replaced by U, w |= ϕ by induction:
> ∧ ⊥ ∨ K1 (p ∨ ⊥). Then we test satisfiability of boolean • U, w |= p iff π(p) = >
formulas ¬χ such that K1 χ is a subformula of ψ and replace • U, w |= ϕ ∧ ψ iff U, w |= ϕ and U, w |= ψ;
K1 χ by ⊥ if ¬χ is satisfiable and by > otherwise. At the end, • U, w |= ¬ϕ iff U, w 6|= ϕ;
we obtain a boolean formula ψ containing no variables. We 0 0 0
• U, w |= Ka ψ iff for all w ∈ U , wRa w implies U, w |=
test its satisfiability with P CL({⊥, >}) − sat(ψ). Notice the ψ;
while -loop is done in linear time because there are a linear • U, w |= [ϕ!]ψ iff U, w |= ϕ implies U ∩
number of subformulas in ψ. {w0 ∈ U | U, w0 |= ϕ}, w |= ψ.
Proposition 9: The satisfiability problem of L☼1D {1} is
The set of validities we obtain is noted L☼1D ! =
Σ2 P-complete.
{ϕ | W, w |= ϕ} where W is the set of all worlds defined
Proof:
Definition 8.
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} . B. Example
Now we are going to study the Muddy children example.
This example is also studied in [11]. You can also find this
F. When AGT and ATM are both finite example in [4] and [3] with more than two children. The
Proposition 10: Let ATM a finite set of agents and situation is the following: there are two children named 1
AGT = {1}. The satisfiability problem and model-checking and 2. Their foreheads are dirty. They see each others. The
of L☼1D {1} is in P. situation is represented by the world w shown in Figure 8
Proof: We adapt algorithms of the figure 6 and 7 in order in the top left. One child do not know if he is dirty or not
to have an optimal polynomial algorithm. More precisely: but he knows the state of the forehead of the other one. We
introduce two propositions: p stands for “1’s forehead is dirty”
• You replace choose_world_with_symbols_in in Figure
and q stands for “1’s forehead is dirty”.
7 by a loop over all worlds. You can notice that the set
We have:
of all possible worlds is fixed, that is to say it does not
depend on ϕ; • W, w |= K1 q ∧ K2 p;
• oracle − sat can now run in polynomial time because • W, w |= ¬K1 p ∧ ¬K1 (¬p) ∧ ¬K2 (¬q).
there is a fixed number of propositions. Then:
• the father says at least one of them are dirty;
9
function mc!(w, C, ϕ)
match (ϕ)
>:
return >;
p ∈ ATM :
return > if p is true in w;
Fig. 9. World for Muddy children after having announced ϕ1 return ⊥ if p is false in w;
ψ 1 ∧ ψ2 :
return mc!(w, C, ψ1 ) ∧ mc!(w, C, ψ2 );
¬ψ:
return ¬mc!(w, C, ψ);
Ka ψ:
for u ∈ Ra (w) do
if inupdatedM (u, C) and
Fig. 10. World for Muddy children after having announced ϕ1 and ϕ2 mc!(u, ψ) = ⊥ then
return ⊥;
endIf
•the children answer that they do not know whether they endFor
are dirty of not. return >;
Formally, we also have: [ψ1 !]ψ2 :
if mc!(w, C, ψ1 ) then
W, w |= [ϕ1 !][ϕ2 !](K1 p ∧ K2 q) return mc!(w, [ψ1 : C], ψ2 )
else
where: return >
• ϕ1 = p ∨ q; endIf
• ϕ2 = (¬K1 p ∨ ¬K1 ¬p) ∧ (¬K2 q ∨ ¬K2 ¬q).
endMatch
endFunction
We verify that after having announced ϕ1 , we only consider
worlds in Figure 9. Then we only consider the initial world w Fig. 11. Algorithm for model-checking in L☼1D !
drawn in 10.
C. Complexity • |ϕ|, |ψ| denotes the length (number of symbols) in ϕ, ψ;
Because L ☼1D !
is a conservative extension of L , we ☼1D • |C|, |D| denotes also the number of symbols in C, D.
inherit from the lower bound results both for model-checking More precisely:
and satisfiability. In fact, we keep the PSPACE-ness upper- – |[]| = 0;
bound with public announcements. – |[ψ1 : C 0 ]| = |ψ1 | + |C 0 |.
Proposition 11: The model-checking and satisfiability
The order ≺ is well-founded and we can use it to prove
problem in L☼1D ! is PSPACE-complete.
terminaison by induction.
Proof: The Figure 11 gives an algorithm for model-
checking. As usual, w is a world, ϕ is a formula. The second • Basic case: (∅, p) etc.
argument C is a list of formulas and stands for the context: if • Induction case: you just have to see that mc!(w, C, ϕ)
C = [] (empty list), it corresponds to the whole set of worlds will only call mc!(u, D, ψ) with (D, ψ) ≺ (C, ϕ). For
otherwise it is a list of announced formulas used to update the instance, when mc!(w, C, ϕ) calls inupdatedM (u, C)
model. More precisely, let us define: which calls mc!(w, C 0 , ψ), we have |C 0 | + |ψ| = |C| <
[] |C| + |ϕ|.
• W = W;
[ψ :C 0 ] 0 0
• W 1 = {w ∈ W C | W C , w |= ψ1 }.
Correction and the fact that the algorithm runs using a
We want: polynomial space can also be proved by induction using the
C
• mc(w, C, ϕ) returns true iff W , w |= ϕ; order ≺.
C
• inupdatedM (w, C) returns true iff w ∈ W .
The hardness comes from the fact that L☼1D ! is a conser-
We have to prove terminaison, correctness and complexity. vative extension of L☼1D and the model checking of L☼1D is
Let us begin to prove terminaison. First of all, we are going PSPACE-hard (Corollary 2).
to introduce an order ≺ over all possible inputs (C, ϕ) of the
Concerning the satisfiability, we can make the same remark
function mc! of Figure 11.
than in the proof of Proposition 6.
We define (C, ϕ) ≺ (D, ψ) by:
• |C| + |ϕ| < |D| + |ψ|;
The upper-bound in special cases (AGT finite etc.) has not
|C| + |ϕ| = |D| + |ψ| been studied yet.
• or
and |ϕ| < |ψ| From now, we are to discuss about the implementation and
where develop the example of the Muddy children.
10
function inpudatedM (w, C) The function returns #f meaning that we do not have
match (C) W, w |= K1 p ∧ K2 q.
[]: return >;
We ask the computer the different worlds the agent 1
[ψ : C 0 ]: mc!(w, C 0 , ψ);
endMatch imagine. To do this we write
endFunction (world-getpossibleworlds ’( (p #t) (1 <)
(2 >) (q #t)) 1).
Fig. 12. Algorithm for testing if a world w is in the updated model formulas
in C The system gives:
(((p #t) (1 <) (2 >) (q #t))
((p #f) (1 <) (2 >) (q #t))).
V. I MPLEMENTATION We can now test if the formula W, w |= [ϕ1 !][ϕ2 !](K1 p ∧
You can find an implementation on the Web site. You can K2 q). You simply write
put positions and directions of agents and positions and states (mc ’( (p #t) (1 <) (2 >) (q #t))
of lamps on your own. Then you can write down a formula (announce (p or q) (announce ((not (1
and check if your formula is true in the world you have drawn. knows p)) and (not (2 knows q))) ((1 knows
This program offers a concrete example to illustrate epis- p) and (2 knows q)))))
temic logic to students. The system answers #t.
VI. C ONCLUSION
A. Description
The program is written in Scheme for the easy use of data The epistemic logic S5n is a general and theoretical frame-
structures and recursive programming. Haskell could also be work for the representation of knowledge. In this paper, we
a well-suited language especially for the lazy evaluation en- have studied a spatially grounded epistemic logic. We have
abling us to write a program which seems to use a exponential investigated two aspects of knowledge learning:
☼
amount of memory whereas it uses only a polynomial amount • With L 1D , we can reason about what agents know by
of memory. Here are the main Scheme functions: learning only with their eyes (when they are located on
• (mc world formula) computes if the formula
a line space);
☼ !
• With L 1D we can reason about what agents know by
formula is true in the world world;
• (mc-with-context world context
looking at their environments and by listening to public
formula) computes of the formula formula is announcements.
true in the world world but we restrict our check Of course the case of the line is restrictive. The case of the
computations only on worlds satisfying the formula plane or of the space may be more interesting. Nevertheless,
context; this paper gives complexity results for model-checking and
• (worldset-delete-not-satisfying satisfiability problem for the case of the line. Even the line
worldset formula) removes from the set of looks like easy, problems are already PSPACE-complete if
world worldset all worlds which does not satisfy the the number of agents is not bounded. We conjecture that
formula formula. This function is used to deal with the complexity of this logic for dimension n ≥ 2 remains
updated models; PSPACE-complete.
• (world-getpossibleworlds world agent) From now, there are two main perspectives: to adapt this
computes the set of all possible worlds for agent agent logic to the case of two dimensions [1] and to study properly
in world world. complexity of model checking and satisfiability with/without
In order to be human readable, the implementation does public announcements. Other perspectives are numerous:
not run in polynomial space but in exponential time. For • fill the Figure 5. The exact complexity classes of model
instance the function (world-getpossibleworlds w checking and satisfiability L☼1D AGT when AGT is finite
a) computes really all worlds in Ra (w). 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.
B. Practising Muddy children Writing down the semantics is quite easy: you just have to
You can describe the current situation (world w on the top replace R by R2 in Definition 8 and tune the definition of
left in Figure 8 by ( (p #t) (1 <) (2 >) (q #t)). directions and Definition 3. The main difficulty is to find
Notice that we are not going to construct the Kripke structure a compact representation in order to deal with the model
by hand. When you draw a Kripke model, you can easily checking and satisfiability problem. In two dimensions
mistakes all the more so the model is theoretical. Here we it is no more possible to consider a total preorder on
just enjoy specifying graphically the situation. The Kripke elements. Finding a good equivalent of Definition 7
structure is then generated on-the-fly by the algorithm. You satisfying Proposition 4 in the case of dimension 2 or
can test if W, w |= K1 p ∧ K2 q by calling more is still an open problem.
(mc ’( (p #t) (1 <) (2 >) (q #t)) ((1 • Study the logic in the 3D-space and compare it to the
knows p) and (2 knows q))). one in the plane (I guess we obtain the same validities);
11
• Find an axiomatization of those logics in order to under-
stand 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.
R EFERENCES
[1] Edwin Abbott Abbott. Flatland. Basil Blackwell, 1884.
[2] Jon Barwise and John Etchemendy. Tarski’s World: Version 4.0 for
Macintosh (Center for the Study of Language and Information - Lecture
Notes). Center for the Study of Language and Information/SRI, 1993.
[3] Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi.
Reasoning About Knowledge. MIT Press, 1995.
[4] V. Goranko and M. Otto. Handbook of Modal Logic, chapter Model
Theory of Modal Logic, pages 255–325. Elsevier, 2006.
[5] Joseph Y. Halpern and Yoram Moses. A guide to completeness
and complexity for modal logics of knowledge and belief. Artificial
Intelligence, 54(3):319–379, 1992.
[6] G. E. Hughes and M. J. Cresswell. An Introduction to Modal Logic.
Methuen and Co., 1968.
[7] Ethan Kennerly, Andreas Witzel, and Jonathan A. Zvesper. Thief belief
(extended abstract). Presented at Logic and the Simulation of Interaction
and Reasoning 2 (LSIR2) Workshop at IJCAI-09, July 2009.
[8] E. Lorini, L. Tummolini, and A. Herzig. Establishing mutual beliefs
by joint attention: towards a formal model of public events. In Mon-
ica Bucciarelli Bruno G. Bara, Lawrence Barsalou, editor, Proceedings
of the XXVII Annual Conference of the Cognitive Science Society, pages
1325–1330. Lawrence Erlbaum, 2005.
[9] Christos H. Papadimitriou. Computational Complexity. Addison-Wesley,
1994.
[10] Rohit Parikh, Lawrence S. Moss, and Chris Steinsvold. Topology and
epistemic logic. In Handbook of Spatial Logics, pages 299–341. 2007.
[11] Jan Plaza. Logics of public communications. Synthese, 158(2):165–179,
2007.
[12] Walter J. Savitch. Relationships between nondeterministic and deter-
ministic tape complexities. J. Comput. Syst. Sci., 4(2):177–192, 1970.
[13] Hans P. van Ditmarsch, Wiebe van der Hoek, Ron van der Meyden, and
Ji Ruan. Model checking russian cards. Electr. Notes Theor. Comput.
Sci., 149(2):105–123, 2006.