Philippe Balbiani
email: philippe.balbiani@irit.fr

Franc ¸ois Schwarzentruber Olivier Gasquet
email: olivier.gasquet@irit.fr

Agents that look at one another

Keywords: Multiagent logics, spatial reasoning, axiomatization/completeness, decidability/complexity

Despite the fact that epistemic connectives are sometimes interpreted in concrete structures defined by means of runs and clock time functions, one of the things which strikes one when studying multiagent logics is how abstract their semantics are. Contrasting this fact is the fact that real agents like robots in everyday life and virtual characters in video games have strong links with their spatial environment. In this paper, we introduce multiagent logics which semantics can be defined by means of purely geometrical notions: possible states are defined by means of the positions in R n occupied by agents and the sections of R n seen by agents whereas accessibility relations are defined by means of the ability of agents to imagine possible states compatible with what they currently see.

Introduction

The field of Artificial Intelligence known as knowledge representation and reasoning is concerned with the problem of representing and reasoning about the knowledge of everyday entities called agents. In recent years, much activity in this field has centred on multiagent logics -modal languages whose atomic sentences range over sets and whose epistemic connectives represent operations involving those sets. In this respect, see [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF], or [START_REF] Fagin | Reasoning About Knowledge[END_REF] for an introduction, the most intensively studied epistemic connectives are modal operators of the form K a ("a knows that . . ."). Their semantics use two notions of Kripke models: possible state and accessibility relation. Possible states are states of affairs describing what is true whereas accessibility relations are indistinguishability relations between states of affairs characterizing the ability of agents to determine what states of affairs they can discriminate. And most find these traditional notions like possible state and accessibility relation intuitively transparent. Despite the fact that epistemic connectives are sometimes interpreted in more concrete structures defined by means of runs and clock time functions [START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF], one of the things which strikes one when studying multiagent logics is how abstract their semantics are.

Contrasting this fact is the fact that real agents like robots in everyday life and virtual characters in video games have strong links with their spatial environment: they occupy positions in it and they see sections of it. Moreover, the knowledge these agents have about their environment mostly depends on the positions they occupy and the sections they see: in the absence of message exchange, a knows that b sees c only if a sees b. These features imply the new opinion that geometrical notions like points and sets of points should be integrated into the semantics of multiagent logics. This tension between a traditional abstract semantics and a new spatial semantics disappears when one realizes that possible states and accessibility re-lations can be defined by means of purely geometrical notions: possible states can be defined by means of the positions in R n occupied by agents and the sections of R n seen by agents whereas accessibility relations can be defined by means of the ability of agents to imagine possible states compatible with what they currently see. In order to elaborate on this idea, we introduce an epistemic language where sentences like "a knows that b sees c" can be expressed.

The syntax of our language, in addition to the traditional epistemic connectives of the form K a ("a knows that . . .") considered in [START_REF] Fagin | Reasoning About Knowledge[END_REF][START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF], for example, will include atomic formulas of the form a⊲b ("a sees b"), the truth of which will depend on the position in R n occupied by agent b and the section of R n seen by agent a. In this setting, the above-mentioned sentence "a knows that b sees c only if a sees b" will be written K a b⊲c → a⊲b. Concerning the semantics of our language, in this first attempt at modelling what agents can see and what agents can know, we naturally work with certain simplifications. Firstly, we will require that agents know all the logical consequences of their knowledge. This is the so-called logical omniscience character of agents. For more on the various problems associated with it, see [START_REF] Sim | Epistemic logic and logical omniscience: a survey[END_REF][START_REF] Sim | Epistemic logic and logical omniscience: a unifying framework[END_REF]. Secondly, we will require that the visual capacity of agents satisfies the following conditions: agents can see through any agents that may be blocking their view; agents are never faulty, i.e. they always see what they are physically able to see; agents can see infinitely far from their positions; if a sees b then a is perfectly informed about what direction b is looking in.

The project of relating multiagent logics to space sprang from the fictional two-dimensional world of Flatland created by Edwin Abbott in 1884. The third author of the present article developed a logic for studying knowledge of agents along a line where sentences like "a knows that b knows that light λ is on" can be expressed [START_REF] Schwarzentruber | Knowledge about lights along a line[END_REF]. This logic turned out to have a P SP ACE-complete model checking problem and a P SP ACE-complete satisfiability problem. The original work was followed up then by further work in collaboration with the first two authors that resulted in an axiomatization of a logic for studying knowledge of agents along a line where sentences like "a knows that b sees c" can be expressed [START_REF] Balbiani | Epistemic reasoning in Lineland[END_REF]. In the present article, we generalize these multiagent logics to spaces of greater dimensions. Its section-by-section breakdown is as follows. Section 2 defines the syntax and the semantics of the multiagent logic we will be working with. In Section 3, we study its expressivity. Section 4 gives the axiomatization in dimension 1 of our multiagent logic. In Sections 5 and 6, we investigate the complexity of model checking problems and the complexity of satisfiability problems. Section 7 presents some variants. Some proofs can be found in the annex.

Syntax and semantics

In this section, we will mostly be concerned with the syntax and the semantics of our multiagent logic. First, we are going to investigate a Cartesian semantics where for some positive integer n, agents occupy positions in R n . Second, we are going to investigate an abstract semantics in dimension 1 where for some linear order T = (T, <) without endpoints, agents occupy positions in T .

Syntax

Let AGT be a countable set of agents (with typical members denoted a, b, etc). The set of all formulas (with typical members denoted φ, ψ, etc) is given by the rule

• φ ::= a⊲b | ⊥ | ¬φ | (φ ∨ ψ) | K a φ.
The intended meanings of a⊲b and K a φ are as follows:

• a⊲b: "a sees b", • K a φ: "a knows that φ".

EXAMPLE 2.1

The formula K a b⊲c can be read "a knows that b sees c".

In atomic sentences like a⊲b, we will always assume that a, b are distinct. This simplification is related to the fact that in Section 2.2, the section seen by an agent is assimilated to an open subset of R n not containing the position occupied by the agent. Let ⊲ be defined by

• a⊲b ::= ¬a⊲b.
Formulas like a⊲b and a⊲b are called literals. We adopt the standard definitions for the remaining Boolean connectives. As usual, for all agents a, we define the epistemic connective Ka as follows:

• Ka φ ::= ¬K a ¬φ.
The notion of a subformula is standard. It is usual to omit parentheses if this does not lead to any ambiguity. Considering an enumeration (a 1 , a 2 , . . .) of AGT , let k be a nonnegative integer. We use φ(a 1 , . . . , a k ) to denote the fact that φ is a formula whose agents form a sublist of a 1 , . . . , a k . In this case, we shall say that φ is a k-formula. A set Σ of formulas is k-maximal iff for all k-formulas φ, φ ∈ Σ, or ¬φ ∈ Σ.

Cartesian semantics

Let n be a positive integer. As we mentioned in the introduction, every agent occupies some position in the space and sees some section of the space. Hence, the notion of an n-scope will be of the utmost interest for us. An n-scope is a structure of the form (x, S) where x is an element of R n and S is a subset of R n . x and S are respectively called the position of the nscope (x, S) and the section of the n-scope (x, S). In a first attempt at modelling what agents can see and what agents can know, one must naturally work with certain simplifications. A natural semantics to look at would be one where the agents' scopes are cones of various angles, with the agents' positions at the basis of the cones. In a first setting, we will consider that agents' scopes are half spaces, with the agents' positions being at the frontier of the halfspaces. In this respect, we shall say that an n-scope (x, S) is simple iff

• S is an open half space, • x is on the frontier of S.
✉ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ❆ ❆ ❆ ❑ R 2 FIG. 1. A simple 2-scope.
We now provide a mechanism for interpreting our formulas in the Cartesian coordinate system R n . An n-world is a function u assigning to each agent a an n-scope u(a).

EXAMPLE 2.3

In the simple 2-world represented in Figure 2, the positions and the sections of three distinct agents are depicted.

✉ a ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ❆ ❆ ❆ ❑ ✉ b ❄ ✉ c ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ✁ ✁ ✁ ☛ R 2 FIG. 2. A simple 2-world.
Given an n-world u and agents a, b, we shall say that a sees b in u iff

• S u (a) contains x u (b).
Remark that in simple n-worlds, no agent can see itself.

✉ a ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ❆ ❆ ❆ ❑ ✉ b ❄ ✉ c ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ❆ ❆ ❆ ❑ R 2 FIG. 3. A simple 2-world.
Remark that ≡ n a is an equivalence relation on the set of all n-worlds. It will be used to interpret the epistemic connective K a . n-satisfaction is a 3-place relation |= n between a nonempty set W of n-worlds, an n-world u in W and a formula φ. It is inductively defined as follows:

• W, u |= n a⊲b iff a sees b in u, • W, u |= n ⊥, • W, u |= n ¬φ iff W, u |= n φ, • W, u |= n φ ∨ ψ iff W, u |= n φ, or W, u |= n ψ, • W, u |= n K a φ iff for all n-worlds v in W, if u ≡ n a v then W, v |= n φ.
As a result,

• W, u |= n a⊲b iff a does not see b in u,

• W, u |= n Ka φ iff there exists an n-world v in W such that u ≡ n a v and W, v |= n φ.

We shall say that a formula φ is valid (invalid) in a nonempty set W of n-worlds, in symbols Unless otherwise stated, we will always assume that all n-worlds are simple.

W val n φ (W inv n φ), iff for all n-worlds u in W, W, u |= n φ (W, u |= n φ). A

Abstract semantics in dimension 1

Let T = (T, <) be a linear order without endpoints. As we mentioned in the introduction, every agent occupies some position in the space and sees some section of the space. Hence, the notion of a T -scope will be of the utmost interest for us. A T -scope is a structure of the form (x, S) where x is an element of T and S is a subset of T . x and S are respectively called the position of the T -scope (x, S) and the section of the T -scope (x, S). We shall say that a T -scope (x, S) is simple iff S is an open semi-interval and x is on the frontier of S.

✉ b ✲ ✉ a ✛ ✉ c ✲ R FIG. 5. A simple R-world.
T -worlds u and v are said to be indiscernible for agent a, in symbols u ≡ T a v, iff x u (a) = x v (a), S u (a) = S v (a) and for all agents b, if a = b then one of the following conditions holds:

• a sees b in u, a sees b in v, x u (b) = x v (b) and S u (b) = S v (b),
• a does not see b in u and a does not see b in v.

EXAMPLE 2.10

The simple R-worlds considered in Figures 5 and6 are indiscernible for agent a.

✉ b ✲ ✉ a ✛ ✉ c ✛ R FIG. 6. A simple R-world.

Remark that ≡ T

a is an equivalence relation on the set of all T -worlds. It will be used to interpret the epistemic connective K a . T -satisfaction is a 3-place relation |= T between a nonempty set W of T -worlds, a T -world u in W and a formula φ. It is inductively defined as follows:

• W, u |= T a⊲b iff a sees b in u, • W, u |= T ⊥, • W, u |= T ¬φ iff W, u |= T φ, • W, u |= T φ ∨ ψ iff W, u |= T φ, or W, u |= T ψ, • W, u |= T K a φ iff for all T -worlds v in W, if u ≡ T a v then W, v |= T φ.
As a result,

• W, u |= T a⊲b iff a does not see b in u, • W, u |= T Ka φ iff there exists a T -world v in W such that u ≡ T a v and W, v |= T φ.
We shall say that a formula φ is valid (invalid) in a nonempty set W of T -worlds, in symbols

W val T φ (W inv T φ), iff for all T -worlds u in W, W, u |= T φ (W, u |= T φ). A
, u |= R K a b⊲a. If v is the simple R-world depicted in Figure 6 then W R s , v |= R a⊲c and W R s , v |= R Ka c⊲a.
Unless otherwise stated, we will always assume that all T -worlds are simple.

Expressivity

AGT being a countable set of agents, the fact that distinct agents occupy distinct positions imply that our multiagent logic forces its models to be infinite. In this section, we discuss some results concerning the expressive power of our multiagent logic.

In dimension 1

Let T = (T, <) be a linear order without endpoints. Our language cannot distinguish between the notion of satisfiability in W 1 s and the notion of satisfiability in W T s . In order to see why, let us consider an enumeration a 1 , a 2 , . . . of AGT . Given a nonnegative integer k, we shall say that a binary relation Z between W 1 s and W T s is a k-bisimulation between W 1 s and W T s iff for all simple 1-worlds u (1) and for all simple T -worlds u (T ) , if u (1) Z u (T ) then the following conditions are satisfied:

1. For all positive integers i, j ≤ k, if a i sees a j in u (1) then a i sees a j in u (T ) . 2. For all positive integers i, j ≤ k, if a i sees a j in u (T ) then a i sees a j in u (1) .

3. For all positive integers i ≤ k and for all simple 1-worlds v (1) , if u (1) ≡ 1 ai v (1) then there exists a simple T -world v (T ) such that u (T ) ≡ T ai v (T ) and v (1) Z v (T ) . 4. For all positive integers i ≤ k and for all simple T -worlds v (T ) , if u (T ) ≡ T ai v (T ) then there exists a simple 1-world v (1) such that u (1) ≡ 1 ai v (1) and v (1) Z v (T ) . Interestingly, LEMMA 3.1 Let φ(a 1 , . . . , a k ) be a formula. Let Z be a k-bisimulation between W 1 s and W T s . For all simple 1-worlds u (1) and for all simple T -worlds u (T ) , if u (1) Z u (T ) then W 1 s , u (1) |= 1 φ(a 1 , . . . , a k ) iff W T s , u (T ) |= T φ(a 1 , . . . , a k ). Given a nonnegative integer k, let Z k be the binary relation between W 1 s and W T s such that for all simple 1-worlds u (1) and for all simple T -worlds u (T ) , u (1) Z k u (T ) iff for all positive integers i, j ≤ k, a i sees a j in u (1) iff a i sees a j in u (T ) . Let Z ⋆ k be the restriction to W T s of the least equivalence relation on

W 1 s ∪ W T s containing Z k . EXAMPLE 3.2
The simple R-worlds considered in Figures 7, 8 and9 are in the binary relation Z ⋆ 3 . We have:

LEMMA 3.3 Z k is a k-bisimulation between W 1
s and W T s . Lemmas 3.1 and 3.3 establish the following PROPOSITION 3.4 Let φ be a formula. The following conditions are equivalent:

✉ a 1 ✲ ✉ a 2 ✲ ✉ a 3 ✛ ✉ a 4 ✲ ✉ a 5 ✲ R FIG. 7. A simple R-world. ✉ a 1 ✲ ✉ a 2 ✲ ✉ a 3 ✛ ✉ a 4 ✲ ✉ a 5 ✛ R FIG. 8. A simple R-world. ✉ a 3 ✲ ✉ a 2 ✛ ✉ a 1 ✛ ✉ a 4 ✛ ✉ a 5 ✛ R FIG. 9. A simple R-world. 1. W 1 s sat 1 φ. 2. W T s sat T φ.
PROOF. Let k be a nonnegative integer such that φ is a formula whose agents form a sublist of a 1 , . . . , a k .

1.⇒2. Suppose W 1 s sat 1 φ(a 1 , . . . , a k ). Hence, then there exists a simple 1-world u (1) such that W 1 s , u (1) |= 1 φ(a 1 , . . . , a k ). Since T is a linear order without endpoints, then there exists a simple T -world u (T ) such that the temporal relationships between a 1 , . . . , a k in u (1) are equal to the temporal relationships between a 1 , . . . , a k in u (T ) . Obviously, u (1) Z k u (T ) . Since W 1 s , u (1) |= 1 φ(a 1 , . . . , a k ), then by Lemmas 3.1 and 3.3, W T s , u (T ) |= T φ(a 1 , . . . , a k ). Thus, W T s sat T φ(a 1 , . . . , a k ).

2.⇒1

. Suppose W T s sat T φ(a 1 , . . . , a k ). Hence, then there exists a simple T -world u (T ) such that W T s , u (T ) |= T φ(a 1 , . . . , a k ). Since R is a linear order without endpoints, then there exists a simple 1-world u (1) such that the temporal relationships between a 1 , . . . , a k in u (1) are equal to the temporal relationships between a 1 , . . . , a k in u (T ) . Obviously, u (1)

Z k u (T ) . Since W T s , u (T ) |= T φ(a 1 , . . . , a k ), then by Lemmas 3.1 and 3.3, W 1 s , u (1) |= 1 φ(a 1 , . . . , a k ). Thus, W 1 s sat 1 φ(a 1 , . . . , a k ).
Proposition 3.4 has the following immediate consequence.

PROPOSITION 3.5

Let φ be a formula. The following conditions are equivalent:

1. W 1 s val 1 φ. 2. There exists a linear order T without endpoints such that W T s val T φ. 3. For all linear orders T without endpoints, W T s val T φ. PROOF. 2.⇒1. By Proposition 3.4.

1.⇒3. By Proposition 3.4.

3.⇒2. Obvious.

In dimensions n ≥ 2

Let n ≥ 2. Our language can distinguish between the notion of satisfiability in W 1 s and the notion of satisfiability in W n s . To illustrate the truth of this, let us consider the four following examples. As a first example, take the formula

• ((a⊲b ↔ b⊲a) ↔ (b⊲c ↔ c⊲b)) → (a⊲c ↔ c⊲a). ✉ a ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ❆ ❆ ❆ ❯ ✉ b ❄ ✉ c ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ✁ ✁ ✁ ☛ R 2 FIG. 10. A simple 2-world.

Its validity in W 1

s follows from the fact that if a and b look into the same direction iff b and c look into the same direction then a and c look into the same direction. Its falsifiability in W 2

s is illustrated by Figure 10 where a simple 2-world satisfying a⊲b ↔ b⊲a and b⊲c ↔ c⊲b -hence, satisfying (a⊲b ↔ b⊲a) ↔ (b⊲c ↔ c⊲b) -and falsifying a⊲c ↔ c⊲a is presented. As a second example, take the formula

• ¬(a⊲b ↔ a⊲c) ∨ ¬(b⊲c ↔ b⊲a).
Its validity in W 1 s follows from the fact that a is not betwen b and c, or b is not between c and a. Its falsifiability in W 2 s is illustrated by Figure 11 where a simple 2-world satisfying a⊲b ↔ a⊲c and b⊲c ↔ b⊲a is presented. As a third example, take the formula

✉ a ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ✟ ❆ ❆ ❆ ❯ ✉ b ✄ ✄ ✄ ✄ ✄ ✄ ✄ ✄ ✄ ✄ ✄ ✄ ❳ ❳ ③ ✉ c ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ✁ ✁ ✁ ☛ R 2 FIG. 11. A simple 2-world. • c⊲a ∧ c⊲b → Kc (((a⊲b ↔ b⊲a) ↔ (b⊲c ↔ c⊲b)) ∧ ¬(a⊲c ↔ c⊲a)).

Its falsifiability in W 1

s is illustrated by Figure 5 where a simple 1-world satisfying c⊲a ∧ c⊲b and falsifying Kc (((a⊲b

↔ b⊲a) ↔ (b⊲c ↔ c⊲b)) ∧ ¬(a⊲c ↔ c⊲a)) is presented. Its validity ✉ a ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ❈ ❈ ❈ ❈ ❈ ❈ ❖ ✉ b ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ✁ ✁ ✁ ☛ ✉ c ❄ R 2 FIG. 12. A simple 2-world.
in W 2 s follows from the fact that if c sees neither a nor b then c can imagine the simple 2world illustrated by Figure 12 where ((a⊲b ↔ b⊲a) ↔ (b⊲c ↔ c⊲b)) ∧ ¬(a⊲c ↔ c⊲a) holds. As a fourth example, take the formula

• c⊲a ∧ c⊲b → Kc ((a⊲b ↔ a⊲c) ∧ (b⊲c ↔ b⊲a)).

Its falsifiability in W 1

s is illustrated by Figure 5 where a simple 1-world satisfying c⊲a ∧ c⊲b and falsifying Kc ((a⊲b

↔ a⊲c) ∧ (b⊲c ↔ b⊲a)) is presented. Its validity in W 2 s follows ✉ a ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ✘ ❈ ❈ ❈ ❈ ❈ ❈ ❖ ✉ b ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ❍ ✁ ✁ ✁ ☛ ✉ c ❄ R 2 FIG. 13. A simple 2-world.
from the fact that if c sees neither a nor b then c can imagine the simple 2-world illustrated by Figure 13 where (a⊲b ↔ a⊲c) ∧ (b⊲c ↔ b⊲a) holds. Finally, for all we know, it is still open whether our language can distinguish between the notion of satisfiability in W n s and the notion of satisfiability in W n+1 s .

Axiomatization and completeness

In this section, our goal is to provide the axiomatization of our multiagent logic in dimension 1. Such an axiomatization will enable us to underline the most representative properties of sentences like "a knows that b sees c" when interpreted in R, or in linear orders without endpoints.

Axiomatization

Let G be a finite group of agents. A G-vector is a pair u = (pos u , sec u ) where

• pos u is a function assigning to each agent a ∈ G a positive integer pos u (a) ≤ Card(G),
• sec u is a function assigning to each agent a ∈ G an element sec u (a) ∈ {r, l}.

We will always assume that pos u is injective.

EXAMPLE 4.1 If G = {a 1 , a 2 , a 3 } then the pair u = (pos u , sec u ) defined by pos u (a 1 ) = 2, pos u (a 2 ) = 1, pos u (a 3 ) = 3, sec u (a 1 ) = l, sec u (a 2 ) = r and sec u (a 3 ) = l is a G-vector.
It corresponds to a situation where a 1 occupies the 2nd position and looks at its left, a 2 occupies the 1st position and looks at its right and a 3 occupies the 3rd position and looks at its left. Given a G-vector u and agents a, b ∈ G, a is said to be seeing b in u iff one of the following conditions holds:

• pos u (a) < pos u (b) and sec u (a) = r,

• pos u (b) < pos u (a) and sec u (a) = l.

Remark that in G-vectors, no agent can see itself. EXAMPLE 4.2 In the G-vector u considered in Example 4.1, a 1 sees a 2 , a 1 does not see a 3 , a 2 sees a 1 , a 2 sees a 3 , a 3 sees a 1 and a 3 sees a 2 .

We now associate to each G-vector u the conjunction χ u of the following literals based on G:

• for all distinct agents a, b ∈ G such that a sees b in u, the literal a⊲b,

• for all distinct agents a, b ∈ G such that a does not see b in u, the literal a⊲b.

EXAMPLE 4.3

The conjunction χ u associated to the

G-vector u considered in Example 4.1 is a 1 ⊲a 2 ∧ a 1 ⊲a 3 ∧ a 2 ⊲a 1 ∧ a 2 ⊲a 3 ∧ a 3 ⊲a 1 ∧ a 3 ⊲a 2 .
Let a ∈ G. We shall say that the G-vector v is a-compatible with the G-vector u, in symbols u ≡ G a v, iff for all b ∈ G, if a = b then one of the following conditions holds:

• a sees b in u, a sees b in v, pos u (b) = pos v (b) and sec u (b) = sec v (b), • a does not see b in u and a does not see b in v. EXAMPLE 4.4 The G-vector v = (pos v , sec v ) defined by pos v (a 1 ) = 2, pos v (a 2 ) = 1, pos v (a 3 ) = 3, sec v (a 1 ) = l, sec v (a 2 ) = r and sec v (a 3 ) = r is a 1 -compatible with the G-vector u consid- ered in Example 4.1.
Remark that ≡ G a is an equivalence relation on the set of all G-vectors. It will be used to provide one of the proper axioms of our multiagent logic. To continue, another technical lemma is necessary.

LEMMA 4.5

The following decision problem is decidable by a deterministic Turing machine in logarithmic space:

Input: a finite group G of agents, an agent a ∈ G and G-vectors u and v, Output: determine whether u ≡ G a v.

We shall say that a set L of formulas in our language is a logic iff L contains all propositional tautologies and L is closed under modus ponens (i.e. if φ ∈ L and φ → ψ ∈ L then ψ ∈ L). A logic L is said to be normal iff L contains all formulas of the form

K a (φ → ψ) → (K a φ → K a ψ) and L is closed under generalization (i.e. if φ ∈ L then K a φ ∈ L).
Let L min be the least normal logic in our language that contains the following formulas as proper axioms:

Ax 1 : ((a⊲b ↔ b⊲a) ↔ (b⊲c ↔ c⊲b)) → (a⊲c ↔ c⊲a), Ax 2 : ¬(a⊲b ↔ a⊲c) ∨ ¬(b⊲c ↔ b⊲a), Ax 3 : K a a⊲b ∨ K a a⊲b, Ax 4 : a⊲b → K a b⊲c ∨ K a b⊲c, Ax 5 : χ u → Ka χ v where G is a finite group of agents, a ∈ G is an agent and u and v are G-vectors such that u ≡ G a v, Ax 6 : K a φ → φ.
Let us remind that in atomic sentences like a⊲b, a, b are distinct. It follows that in dimension 1, a⊲b ↔ b⊲a and a⊲b ↔ a⊲c can be read as "a and b look into the same direction" and "a is between b and c". There are several points worth making about our proper axioms: Ax 1 says that if a and b look into the same direction iff b and c look into the same direction then a and c look into the same direction; Ax 2 says that a is not betwen b and c, or b is not between c and a; Ax 3 says that a knows whether it looks at b; Ax

Completeness

We show first that

PROPOSITION 4.6 Let φ be a formula. If φ is in L min then W 1 s val 1 φ. PROOF. It is readily seen that Ax 1 -Ax 6 are valid in W 1 s .
Slightly less trivial is the following PROPOSITION 4.7 Let φ be a formula. If for all linear orders T without endpoints, W T s val T φ then φ is in L min . Proposition 4.7 will be proved by a construction similar to the canonical model construction.

Let n be a positive integer. As usual, any L min -consistent set of formulas can be extended to an n-maximal L min -consistent set of formulas. LEMMA 4.8 If Σ is an L min -consistent set of formulas then there exists an n-maximal L min -consistent set ∆ of formulas such that Σ ⊆ ∆.

Let Z ⋆ be the set of all non-zero integers. We will interpret n-formulas in the linear order T = (T, ≺) defined as follows:

• T = Z ⋆ ∪ {(0, k): k ≤ n is a positive integer},
• for all α, β ∈ T , α ≺ β iff one of the following conditions hold:

α, β ∈ Z ⋆ and α < β, -α ∈ Z ⋆ , there exists a positive integer j ≤ n such that β = (0, j) and α < 0, there exists a positive integer i ≤ n such that α = (0, i), β ∈ Z ⋆ and 0 < β, there exists positive integers i, j ≤ n such that α = (0, i), β = (0, j) and i < j.

It follows immediately from the definition that FACT 4.9 T is a linear order without endpoints.

Let Σ be an n-maximal L min -consistent set of formulas. For all positive integers k ≤ n, k is said to be Σ-right iff k = 1, or k = 1 and (a 1 ⊲a k ↔ a k ⊲a 1 ) ∈ Σ and k is said to be Σ-left iff k = 1 and (a 1 ⊲a k ↔ a k ⊲a 1 ) ∈ Σ. The reader may easily verify that to be Σ-right and to be Σ-left are complementary properties of a positive integer k ≤ n. For all positive integers i, j ≤ n, we shall say that i Σ-precedes j iff i = j and one of the following conditions holds:

• i is Σ-right and a i ⊲a j ∈ Σ, • j is Σ-left and a j ⊲a i ∈ Σ, • i is Σ-left, j is Σ-right, a i ⊲a j ∈ Σ and a j ⊲a i ∈ Σ.
It is worth noting at this point the following FACT 4.10 Let i, j, k ≤ n be positive integers.

1. i does not Σ-precede i.

2. If i Σ-precedes j and j Σ-precedes k then i Σ-precedes k.

3. If i = j then i Σ-precedes j, or j Σ-precedes i.

As a result, there exists permutations π r Σ , π l Σ of the set of all positive integers k ≤ n such that for all positive integers i, j ≤ n,

• π r Σ (i) < π r Σ (j) iff i Σ-precedes j, • π l Σ (i) < π l Σ (j) iff j Σ-precedes i.
Obviously, for all positive integers k ≤ n, π r

Σ (k) + π l Σ (k) = n + 1.
We now wish to show that there exists a simple T -world u such that for all formulas φ(a

1 , . . . , a n ), if φ(a 1 , . . . , a n ) ∈ Σ then W T s , u |= T φ(a 1 , . . . , a n ). Let u r Σ , u l Σ be simple T -worlds such that for all positive integers k ≤ n, • x u r Σ (a k ) = (0, π r Σ (k)), • if k is Σ-right then S u r Σ (a k ) = ](0, π r Σ (k)), +∞[, • if k is Σ-left then S u r Σ (a k ) = ] -∞, (0, π r Σ (k))[, • x u l Σ (a k ) = (0, π l Σ (k)), • if k is Σ-right then S u l Σ (a k ) = ] -∞, (0, π l Σ (k))[, • if k is Σ-left then S u l Σ (a k ) = ](0, π l Σ (k)), +∞[. Remind that Z ⋆ n is the restriction to W T s of the least equivalence relation on W 1 s ∪ W T s containing Z n . It follows immediately from the definition that FACT 4.11 u r Σ Z ⋆ n u l Σ .
Not surprisingly, we have FACT 4.12 For all positive integers i, j ≤ n, if i = j then the following conditions are equivalent:

1. W T s , u r Σ |= T a i ⊲a j . 2. W T s , u l Σ |= T a i ⊲a j .
3. a i ⊲a j ∈ Σ.

For all positive integers i ≤ n, let ≡ T ai be the indiscernibility relation between T -worlds defined as in Section 2.3. The following fact is basic. FACT 4.13 Let ∆ be an n-maximal consistent set of formulas. For all positive integers i ≤ n, the following conditions are equivalent:

1. u r Σ ≡ T ai u r ∆ , or u r Σ ≡ T ai u l ∆ . 2. u l Σ ≡ T ai u r ∆ , or u l Σ ≡ T ai u l ∆ .
An important further result is FACT 4.14 Let ∆ be an n-maximal consistent set of formulas. For all positive integers i ≤ n, if

K ai Σ ⊆ ∆ then • u r Σ ≡ T ai u r ∆ , or u r Σ ≡ T ai u l ∆ , • u l Σ ≡ T ai u r ∆ , or u l Σ ≡ T ai u l ∆ .
With this established, the rest is easy.

FACT 4.15 Let ψ(a 1 , . . . , a n ) be a formula. The following conditions are equivalent:

1. W T s , u r Σ |= T ψ(a 1 , . . . , a n ). 2. W T s , u l Σ |= T ψ(a 1 , . . . , a n ). 3. ψ(a 1 , . . . , a n ) ∈ Σ.
The proof of Proposition 4.7 can now be done as follows.

PROOF OF PROPOSITION 4.7. Let n be a nonnegative integer such that φ is a formula whose agents form a sublist of a 1 , . . . , a n . Suppose φ(a 1 , . . . , a n ) is an L min -consistent formula. Hence, by Lemma 4.8, there exists an n-maximal L min -consistent set Σ of formulas such that φ(a 1 , . . . , a n ) ∈ Σ. Thus, by Fact 4.15, W T s , u Σ |= T φ(a 1 , . . . , a n ).

As a result, PROPOSITION 4.16 Let φ be a formula. The following conditions are equivalent:

1. φ is in L min . 2. W 1 s val 1 φ. 3.
There exists a linear order T without endpoints such that W T s val T φ. 4. For all linear orders T without endpoints, W T s val T φ.

PROOF. By Proposition 3.5, it suffices to prove that 1.⇒2. and 4.⇒1.

1.⇒2. By Proposition 4.6.

4.⇒1

. By Proposition 4.7.

In this section, for some positive integers k, we investigate the decidability and complexity of the model checking problem with respect to W k s : given a k-world u in W k s and a formula φ, determine whether W k s , u |= k φ. The results obtained are summarized as follows: P SP ACE-complete when k = 1 and P SP ACE-hard and in EXP SP ACE when k = 2. Let us remind that in the more traditional epistemic logics considered in [START_REF] Fagin | Reasoning About Knowledge[END_REF][START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF], for example, model checking problems are usually decidable in deterministic polynomial time.

In dimension 1

First, we prove the following LEMMA 5.1

The validity problem of quantified Boolean logic is reducible to the model checking problem with respect to W 1 s . As a result, PROPOSITION 5.2

The model checking problem with respect to W 1 s is P SP ACE-complete. PROOF. P SP ACE-hardness follows from Stockmeyer [START_REF] Stockmeyer | The polynomial-time hierarchy[END_REF] and Lemma 5.1. Membership in P SP ACE follows from Chandra et al. [START_REF] Chandra | Alternation[END_REF], Lemmas 3.1 and 3.3 and the fact that the following alternating algorithm (where without loss of generality, we assume that (u(a 1 ), . . . , u(a n )) is coded as a G-vector with G = {a 1 , . . . , a n }) decides in polynomial time the model checking problem with respect to W 1 s :

algorithm mc 1 ((u(a 1 ), . . . , u(a n )), φ(a 1 , . . . , a n )) begin case φ(a 1 , . . . , a n ) of begin a i ⊲a j : (•) if a i sees a j in (u(a 1 ), . . . , u(a n )) then succeed else fail ⊥: (•) fail ¬ψ(a 1 , . . . , a n ): (•) begin call mc 1 ((u(a 1 ), . . . , u(a n )), ψ(a 1 , . . . , a n )) if this call succeeds then fail else succeed end

ψ 1 (a 1 , . . . , a n ) ∨ ψ 2 (a 1 , . . . , a n ): (∃) begin choose i in {1, 2} call mc 1 ((u(a 1 ), . . . , u(a n )), ψ i (a 1 , . . . , a n )) if this call succeeds then succeed else fail end K ai ψ(a 1 , . . . , a n ): (∀) begin choose a G-vector (v(a 1 ), . . . , v(a n )) such that (u(a 1 ), . . . , u(a n )) ≡ G ai (v(a 1 ), . . . , v(a n )) call mc 1 ((v(a 1 ), . . . , v(a n )), ψ(a 1 , . . . , a n ))
if this call succeeds then succeed else fail end end end Its execution depends primarily on φ(a 1 , . . . , a n ), each case being existential, or universal. For example, the case ((u(a 1 ), . . . , u(a n )), ψ 1 (a 1 , . . . , a n ) ∨ ψ 2 (a 1 , . . . , a n )) is existential. It is an accepting case iff for some i ∈ {1, 2}, the case ((u(a 1 ), . . . , u(a n )), ψ i (a 1 , . . . , a n )) is accepting, thus corresponding to the fact that ψ 1 (a 1 , . . . , a n ) ∨ ψ 2 (a 1 , . . . , a n ) is true for (u(a 1 ), . . . , u(a n )) iff for some i ∈ {1, 2}, ψ i (a 1 , . . . , a n ) is true for (u(a 1 ), . . . , u(a n )). As well, the case ((u(a 1 ), . . . , u(a n )), K ai ψ(a 1 , . . . , a n )) is universal. It is an accepting case iff for every G-vector (v(a 1 ), . . . , v(a n )) such that (u(a 1 ), . . . , u(a n )) ≡ G ai (v(a 1 ), . . . , v(a n )), the case ((v(a 1 ), . . . , v(a n )), ψ(a 1 , . . . , a n )) is accepting, thus corresponding to the fact that K ai ψ(a 1 , . . . , a n ) is true for (u(a 1 ), . . . , u(a n )) iff for every G-vector (v(a 1 ), . . . , v(a n )) such that (u(a 1 ), . . . , u(a n )) ≡ G ai (v(a 1 ), . . . , v(a n )), ψ(a 1 , . . . , a n ) is true for (v(a 1 ), . . . , v(a n )). Cases labelled with (•) are both existential and universal. All in all, it is clear that mc 1 ((u(a 1 ), . . . , u(a n )), φ(a 1 , . . . , a n )) correctly solves the model checking problem with respect to W 1 s and that it can be implemented in a polynomial time-bounded alternating Turing machine. Hence, the model checking problem with respect to W 1 s is in P SP ACE.

In dimension 2

First, we prove the following LEMMA 5.3

The validity problem of quantified Boolean logic is reducible to the model checking problem with respect to W 2 s .

As a result, PROPOSITION 5.4 The model checking problem with respect to W 2 s is P SP ACE-hard and in EXP SP ACE.

PROOF. P SP ACE-hardness follows from Stockmeyer [START_REF] Stockmeyer | The polynomial-time hierarchy[END_REF] and Lemma 5.3. A general strategy for proving a decision problem to be in EXP SP ACE is to reduce it to a decision problem already known to be in EXP SP ACE. A suitable decision problem already known to be in EXP SP ACE is the validity problem of sentences in elementary algebra [START_REF] Ben-Or | The complexity of elementary algebra and geometry[END_REF]. The language of elementary algebra is a first-order language with equality. It consists of the constant symbols 0 and 1, the function symbols + and × of arity 2 and the relation symbol < of arity 2. Suppose that we are given a 2-world (u(a 1 ), . . . , u(a n )) in W 2 s and a formula φ(a 1 , . . . , a n ). We shall construct a sentence ϕ((u(a 1 ), . . . , u(a n )), φ(a 1 , . . . , a n )) in elementary algebra such that φ(a 1 , . . . , a n ) is true for (u(a 1 ), . . . , u(a

n )) in W 2 s iff ϕ((u(a 1 ), . . . , u(a n )), φ(a 1 , . . . , a n )) is valid. Choose distinct individual variables x α k , y α k
where k ≤ n is a positive integer and α is a nonnegative integer. For all positive integers k ≤ n, x 0 k , x 1 k , . . . and y 0 k , y 1 k , . . . will represent the abscissas and the ordinates of the positions in R 2 occupied by a k in such-and-such 2-world. Choose distinct individual variables z α k , t α k where k ≤ n is a positive integer and α is a nonnegative integer. For all positive integers k ≤ n, z 0 k , z 1 k , . . . and t 0 k , t 1 k , . . . will represent the coordinates of the endpoints in R 2 of the vectors located at the origin corresponding to the sections seen by a k in such-and-such 2-world. Without loss u(a n )), φ(a 1 , . . . , a n )) can be computed in logarithmic space. Moreover, the reader may easily verify that φ(a 1 , . . . , a n ) is true for (u(a 1 ), . . . , u(a n )) in W 2 s iff ϕ((u(a 1 ), . . . , u(a n )), φ(a 1 , . . . , a n )) is valid. Thus, the model checking problem with respect to W 2 s is reducible to the validity problem of sentences in elementary algebra.

Decidability and complexity of satisfiability problems

In this section, for some positive integers k, we investigate the decidability and complexity of the satisfiability problem with respect to W k s : given a formula φ, determine whether W k s sat k φ. The results obtained are summarized as follows: P SP ACE-complete when k = 1 and P SP ACE-hard and in EXP SP ACE when k = 2. Let us remind that in the more traditional epistemic logics considered in [START_REF] Fagin | Reasoning About Knowledge[END_REF][START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF], for example, satisfiability problems are usually decidable in nondeterministic polynomial time or in polynomial space, according as there exists only one agent or there exists at least two agents.

In dimension 1

First, we prove the following LEMMA 6.1

The validity problem of quantified Boolean logic is reducible to the satisfiability problem with respect to W 1 s .

As a result, PROPOSITION 6.2

The satisfiability problem with respect to W 1 s is P SP ACE-complete.

PROOF. P SP ACE-hardness follows from Stockmeyer [START_REF] Stockmeyer | The polynomial-time hierarchy[END_REF] and Lemma 6.1. Membership in P SP ACE follows from Savitch [START_REF] Savitch | Relationships between nondeterministic and deterministic tape complexities[END_REF], Proposition 3.4 and the fact that the following nondeterministic algorithm decides in polynomial space the satisfiability problem with respect to W 1 s :

algorithm sat 1 (φ(a 1 , . . . , a n )) begin choose a G-vector (u(a 1 ), . . . , u(a n )) call mc 1 P SP ACE ((u(a 1 ), . . . , u(a n )), φ(a 1 , . . . , a n )) if this call succeeds then succeed else fail end where mc 1 P SP ACE is a deterministic algorithm that decides in polynomial space the model checking problem with respect to W 1 s (by Proposition 5.2, we know that there exists such algorithms). It is clear that sat 1 correctly solves the satisfiability problem with respect to W 1 s and that it can be implemented in a polynomial space-bounded nondeterministic Turing machine. Hence, the satisfiability problem with respect to W 1 s is in P SP ACE.

In dimension 2

First, we prove the following LEMMA 6.3

The validity problem of quantified Boolean logic is reducible to the satisfiability problem with respect to W 2 s .

As a result, PROPOSITION 6.4

The satisfiability problem with respect to W 2 s is P SP ACE-hard and in EXP SP ACE.

PROOF. The proof is similar to the proof of Proposition 5.4. P SP ACE-hardness follows from Stockmeyer [START_REF] Stockmeyer | The polynomial-time hierarchy[END_REF] and Lemma 6.3. Membership in EXP SP ACE follows from Ben-Or et al. [START_REF] Ben-Or | The complexity of elementary algebra and geometry[END_REF] and the fact that the satisfiability problem with respect to W 2 s is reducible to the validity problem of sentences in elementary algebra. Suppose that we are given a formula φ(a 1 , . . . , a n ). We shall construct a sentence ϕ(φ(a 1 , . . . , a n )) in elementary algebra such that φ(a 1 , . . . , a n ) is satisfiable in W ) be the formulas in elementary algebra defined in the proof of Proposition 5.4. Let τ be the translation taking nonnegative integers and formulas to formulas in elementary algebra defined in the proof of Proposition 5.4. Let ϕ(φ(a 1 , . . . , a n )) be ∃x 0 1 ∃y 0 1 . . . ∃x 0 n ∃y 0 n ∃z 0 1 ∃t 0 1 . . . ∃z 0 n ∃t 0 n τ (0, φ(a 1 , . . . , a n )). Remark that ϕ(φ(a 1 , . . . , a n )) can be computed in logarithmic space. Moreover, the reader may easily verify that φ(a 1 , . . . , a n ) is satisfiable in W 2 s iff ϕ(φ(a 1 , . . . , a n )) is valid. Thus, the satisfiability problem with respect to W 2 s is reducible to the validity problem of sentences in elementary algebra.

Variants

In this section, we discuss several variants not captured by the syntax and the semantics considered in Sections 2-6. For most of them, the axiomatization/completeness issue and the decidability/complexity issue are still unsettled.

Group knowledge

There exists various notions of what may be called group knowledge. A well-known example of such a notion of knowledge for a group of agents is the following: C G φ ("φ is common knowledge in the group G"). The usual semantics definition of common knowledge runs as follows within the context of W n s :

W n s , u |= n C G φ iff for all n-worlds v in W n s , if u + {≡ n a : a ∈ G} v then W n s , v |= n φ, +
{≡ n a : a ∈ G} denoting the transitive closure of the union of the indiscernibility relations concerning agents in group G. In this respect, see [START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF] for details, the key valid principles of common knowledge are

• C G φ → {K a (φ ∧ C G φ): a ∈ G}, • C G (φ → {K a φ: a ∈ G}) → {K a (φ → C G φ): a ∈ G}.
However, W 1 s invalidates very specific formulas. For instance, choose distinct agents a 1 , a 2 , a 3 , b, c. The reader may easily verify that W 1 s inv 1 K {a1,a2,a3} b⊲c. Another interesting example of such a notion of knowledge for a group of agents is the following: D G φ ("φ is distributed knowledge in the group G"). The usual semantics definition of distributed knowledge runs as follows within the context of W n s :

W n s , u |= n D G φ iff for all n-worlds v in W n s , if u {≡ n a : a ∈ G} v then W n s , v |= n φ,
{≡ n a : a ∈ G} denoting the intersection of the indiscernibility relations concerning agents in group G. In this respect, see [START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF] for details, the key valid principle of distributed knowledge is

• D G φ → {K a φ: a ∈ G}.
Nevertheless, W 1 s validates formulas that are not valid in a more general setting. For example, choose a finite group G of agents. The reader may easily verify that for all formulas φ(G),

W 1 s val 1 D G φ(G) ↔ φ(G).

Announcements

We have considered in Sections 2-6 that the knowledge our agents have about their environment mostly depends on the positions they occupy and the sections they see. The truth is that knowledge is also affected by the messages our agents exchange. Following the intuition behind the logic of public announcements, see [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF] for an introduction, for all formulas ϕ, let us add modal operators of the form [ϕ] ("after announcement of ϕ, it holds that . . .") to our language. As usual, for all formulas ϕ, we define the modal operator ϕ as follows:

• ϕ φ ::= ¬[ϕ]¬φ.
Within the context of a nonempty set W n of n-worlds, W n |ϕ being the set of all n-worlds v in

W n such that W n , v |= n ϕ, n-satisfaction of [ϕ]φ is defined by • W n , u |= n [ϕ]φ iff if W n , u |= n ϕ then W n |ϕ , |= n φ. As a result, • W n , u |= n ϕ φ iff W n , u |= n ϕ and W n
|ϕ , |= n φ. See [START_REF] Schwarzentruber | Doing: Case Studies in Modal Logic[END_REF] for a study of this variant. This variant is interesting because it can be considered as a logic of public communications between agents that look at one another, formulas like [K a ϕ]φ and K a ϕ φ being read "if a knows that ϕ then after the announcement of ϕ by a, φ holds" and "a knows that ϕ and after the announcement of ϕ by a, φ holds".

Visual abilities

We have considered in Sections 2-6 that our agents had similar visual abilities. What happens if agents' sights vary? In Section 2.2, for all positive integers n, we have defined n-worlds as functions assigning n-scopes to agents. If the visual abilities of our agents are similar to those of a radar then the n-scopes assigned to agents can be classed as open n-discs of suchand-such diameter. We shall say that an n-scope (x, S) is circular iff S is an open n-disc and x is the center of S. verify that W 1 s val 1 a⊲b ∧ b⊲a → a⊲c ∨ b⊲c and W 1 c f al 1 a⊲b ∧ b⊲a → a⊲c ∨ b⊲c. Hence, our language can distinguish between the notion of satisfiability in W 1 s and the notion of satisfiability in W 1 c . We have considered in Sections 2-6 that the knowledge our agents have about their environment mostly depends on the positions they occupy and the sections they see. The truth is that knowledge is also affected by the amount of effort our agents put in. Following the intuition behind the logic of subset spaces, see [START_REF] Parikh | Topology and epistemic logic[END_REF] for an introduction, let us add modal operators of the form ✷ a ("whatever the effort a puts in, . . .") to our language. As usual, for all agents a, we define the modal operator ✸ a as follows:

• ✸ a φ ::= ¬✷ a ¬φ.

We shall say that agent a has sharpened its range of vision between n-scopes u and v iff the only difference between u and v lies in the fact that S u (a) S v (a). Within the context of W n c , n-satisfaction of ✷ a φ is defined by

• W n c , u |= n ✷ a φ iff for all n-worlds v in W n c
, if a has sharpened its range of vision between u and v then W n c , v |= n φ.

As a result,

• W n c , u |= n ✸ a φ iff there exists an n-world v in W n c such that a has sharpened its range of vision between u and v and W n c , v |= n φ.

We first observe that

W n c val n ✷ a φ → φ, W n c val n ✷ a φ → ✷ a ✷ a φ and W n c val n ✸ a φ ∧ ✸ a ψ → ✸ a (φ ∧ ✸ a ψ) ∨ ✸ a (✸ a φ ∧ ψ).
In other respects, for all ✷ • -free formulas φ, W n c val n ✷ a Ka φ → ✸ a K a φ. Let us consider an enumeration a 0 , a 1 , . . . of AGT . Consider a nonnegative integers i ≤ n. Let φ ⊲ i be the conjunction of the following literals:

• for all nonnegative integers j ≤ n, if i = j then a i ⊲a j .

Let φ ⊲ i be the conjunction of the following literals:

• for all nonnegative integers j ≤ n, if i = j then a i ⊲a j .

Let φ i be φ ⊲ i ∧ ✷ ai φ ⊲ i . φ i says that: for all nonnegative integers j ≤ n, if i = j then a i does not see a j ; whatever the effort a i puts in, for all nonnegative integers j ≤ n, if i = j then a i sees a j . As a result, φ i implies that for all nonnegative integers j, k ≤ n, if i = j and i = k then the distance between the positions of a i and a j and the distance between the positions of a i and a k are equal. Let φ be φ 0 ∧ . . . ∧ φ n . The reader may easily verify that W n c inv n φ and W n+1 c sat n+1 φ. Hence, our language can distinguish between the notion of satisfiability in W n c and the notion of satisfiability in W n+1 c .

Conclusion

This article considered a logic for studying knowledge of agents where sentences like "a knows that b sees c" can be expressed. We have studied its expressivity, axiomatized validity in W 1 s and investigated the complexity of the model checking and satisfiability problems in W 1 s and W 2 s . Much remains to be done. Firstly, there is the problem of the complete axiomatization of validity in W 2 s . Secondly, there is the question of the precise complexity of the model checking and satisfiability problems in W 2 s . Thirdly, there is the issue of the variants considered in Section 7. Of course, one could as well formulate these problems, questions and issues in dimensions n ≥ 3.

1. Let i, j ≤ k be positive integers such that a i sees a j in u (1) . Since u (1) Z k u (T ) , then a i sees a j in u (T ) .

2. Let i, j ≤ k be positive integers such that a i sees a j in u (T ) . Since u (1) Z k u (T ) , then a i sees a j in u (1) .

3. Let i ≤ k be a positive integer and v (1) be a simple 1-world such that u (1) ≡ 1 ai v (1) . Consider the set of all simple T -worlds v (T ) such that x u (T ) (a i ) = x v (T ) (a i ), S u (T ) (a i ) = S v (T ) (a i ) and for all positive integers j ≤ k, if a i sees a j in u (T ) then x u (T ) (a j ) = x v (T ) (a j ) and S u (T ) (a j ) = S v (T ) (a j ). Since T is a linear order without endpoints, then this set contains a simple T -world v (T ) such that, j 1 , . . . , j l being a list of all the positive integers j ≤ k such that a i does not see a j in u (T ) , the temporal relationships between a j1 , . . . , a j l in v (1) are equal to the temporal relationships between a j1 , . . . , a j l in v (T ) . Since u (1) Z k u (T ) , then u (T ) ≡ T ai v (T ) and v (1) Z k v (T ) .

4. Let i ≤ k be a positive integer and v (T ) be a simple T -world such that u (T ) ≡ T ai v (T ) . Consider the set of all simple 1-worlds v (1)

such that x u (1) (a i ) = x v (1) (a i ), S u (1) (a i ) = S v (1) (a i
) and for all positive integers j ≤ k, if a i sees a j in u (1)

then x u (1) (a j ) = x v (1) (a j ) and S u (1) (a j ) = S v (1) (a j ).
Since R is a linear order without endpoints, then this set contains a simple 1-world v (1) such that, j 1 , . . . , j l being a list of all the positive integers j ≤ k such that a i does not see a j in u (1) , the temporal relationships between a j1 , . . . , a j l in v (1) are equal to the temporal relationships between a j1 , . . . , a j l in v (T ) . Since u (1) Z k u (T ) , then u (1) ≡ 1 ai v (1) and v (1) Z k v (T ) .

PROOF OF LEMMA 4.5. Obvious.

PROOF OF LEMMA 4.8. The argument is similar to that given in Blackburn et al. [START_REF] Blackburn | Modal Logic[END_REF]Lemma 4.21], as the reader should check.

PROOF OF FACT 4.9. Obvious.

PROOF OF FACT 4.10. 1. Obvious.

2. Suppose i Σ-precedes j, j Σ-precedes k and i does not Σ-precede k. Since i Σ-precedes j, then i = j and

• (1) i is Σ-right and a i ⊲a j ∈ Σ, or (2) j is Σ-left and a j ⊲a i ∈ Σ, or (3) i is Σ-left, j is Σ-right, a i ⊲a j ∈ Σ and a j ⊲a i ∈ Σ.

Since j Σ-precedes k, then j = k and

• (4) j is Σ-right and a j ⊲a k ∈ Σ, or (5) k is Σ-left and a k ⊲a j ∈ Σ, or (6) j is Σ-left, k is Σ-right, a j ⊲a k ∈ Σ and a k ⊲a j ∈ Σ. Since i does not Σ-precede k, then i = k, or i = k and • (7) i is not Σ-right, or (8) a i ⊲a k ∈ Σ, • (9) k is not Σ-left, or (10) a k ⊲a i ∈ Σ, • (11) i is not Σ-left, or (12) k is not Σ-right, or (13) a i ⊲a k ∈ Σ, or (14) a k ⊲a i ∈ Σ.
Hence, we have to consider eighteen cases.

Case "( 1), ( 4) and i = k". Since (1), then i is Σ-right and a i ⊲a j ∈ Σ. Since (4), then j is Σ-right and a j ⊲a k ∈ Σ. Since i = k, then a j ⊲a i ∈ Σ. Since i = j, then (a i ⊲a j ↔ a j ⊲a i ) ∈ Σ (use axiom Ax 1 and the fact that i is Σ-right and j is Σ-right). Since a i ⊲a j ∈ Σ, then a j ⊲a i ∈ Σ: a contradiction.

Case "(1), ( 4), i = k, [START_REF] Chandra | Alternation[END_REF], or [START_REF] Chang | Model Theory[END_REF], [START_REF] Cook | The complexity of theorem-proving procedures[END_REF], or [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF] and [START_REF] Fagin | Reasoning About Knowledge[END_REF], or [START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF], or [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF], or ( 14)". Since (1), then i is Σ-right and a i ⊲a j ∈ Σ. Since (4), then j is Σ-right and a j ⊲a k ∈ Σ. Since [START_REF] Chandra | Alternation[END_REF], or (8), then i is not Σ-right, or a i ⊲a k ∈ Σ. Since i is Σ-right, then a i ⊲a k ∈ Σ. Since i = j, then (a i ⊲a j ↔ a j ⊲a i ) ∈ Σ (use axiom Ax 1 and the fact that i is Σ-right and j is Σ-right). Since a i ⊲a j ∈ Σ, then a j ⊲a i ∈ Σ. Since a i ⊲a j ∈ Σ and a j ⊲a k ∈ Σ, then a i ⊲a k ∈ Σ, or a j ⊲a i ∈ Σ (use axiom Ax 2 ). Since a j ⊲a i ∈ Σ, then a i ⊲a k ∈ Σ: a contradiction.

Case "(1), ( 5) and i = k". Since (1), then i is Σ-right. Since (5), then k is Σ-left. Since i = k, then i is Σ-left: a contradiction.

Case "(1), ( 5), i = k, [START_REF] Chandra | Alternation[END_REF], or ( 8), [START_REF] Cook | The complexity of theorem-proving procedures[END_REF], or [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF] and [START_REF] Fagin | Reasoning About Knowledge[END_REF], or [START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF], or [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF], or ( 14)". Since (1), then i is Σ-right and a i ⊲a j ∈ Σ. Since (5), then k is Σ-left and a k ⊲a j ∈ Σ. Since [START_REF] Chandra | Alternation[END_REF], or (8), then i is not Σ-right, or a i ⊲a k ∈ Σ. Since (9), or [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF]

, then k is not Σ-left, or a k ⊲a i ∈ Σ. Since i is Σ-right and k is Σ-left, then a i ⊲a k ∈ Σ and a k ⊲a i ∈ Σ. Since a i ⊲a j ∈ Σ and a k ⊲a j ∈ Σ, then a i ⊲a k ∈ Σ, or a k ⊲a i ∈ Σ (use axiom Ax 2 ). Since a i ⊲a k ∈ Σ, then a k ⊲a i ∈ Σ: a contradiction.
Case "(1), ( 6) and i = k". Since (1), then a i ⊲a j ∈ Σ. Since (6), then a k ⊲a j ∈ Σ. Since i = k, then a i ⊲a j ∈ Σ: a contradiction.

Case "( 1), ( 6), i = k, [START_REF] Chandra | Alternation[END_REF], or ( 8), [START_REF] Cook | The complexity of theorem-proving procedures[END_REF], or [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF] and [START_REF] Fagin | Reasoning About Knowledge[END_REF], or [START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF], or [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF], or ( 14)". Since (1), then i is Σ-right and a i ⊲a j ∈ Σ. Since (6), then j is Σ-left, k is Σ-right, a j ⊲a k ∈ Σ and a k ⊲a j ∈ Σ. Since [START_REF] Chandra | Alternation[END_REF], or (8), then i is not Σ-right, or a i ⊲a k ∈ Σ. Since i is Σ-right, then a i ⊲a k ∈ Σ. Since i = j, then (a i ⊲a j ↔ a j ⊲a i ) ∈ Σ (use axiom Ax 1 and the fact that i is Σ-right and j is Σ-left). Since a i ⊲a j ∈ Σ, then a j ⊲a i ∈ Σ. Since i = k, then (a i ⊲a k ↔ a k ⊲a i ) ∈ Σ (use axiom Ax 1 and the fact that i is Σ-right and k is Σ-right). Since a i ⊲a k ∈ Σ, then a k ⊲a i ∈ Σ. Since a i ⊲a j ∈ Σ, then a i ⊲a k ∈ Σ, or a k ⊲a j ∈ Σ (use axiom Ax 2 ). Since a i ⊲a k ∈ Σ, then a k ⊲a j ∈ Σ: a contradiction.

Case "( 2), ( 4) and i = k". Since (2), then j is Σ-left. Since (4), then j is Σ-right: a contradiction.

Case "( 2), ( 4), i = k, [START_REF] Chandra | Alternation[END_REF], or ( 8), [START_REF] Cook | The complexity of theorem-proving procedures[END_REF], or [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF] and [START_REF] Fagin | Reasoning About Knowledge[END_REF], or [START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF], or [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF], or ( 14)". Since (2), then j is Σ-left. Since (4), then j is Σ-right: a contradiction.

Case "( 2), ( 5) and i = k". Since (2), then j is Σ-left and a j ⊲a i ∈ Σ. Since (5), then k is Σ-left and a k ⊲a j ∈ Σ. Since i = k, then i is Σ-left and a i ⊲a j ∈ Σ. Since i = j, then (a i ⊲a j ↔ a j ⊲a i ) ∈ Σ (use axiom Ax 1 and the fact that i is Σ-left and j is Σ-left). Since a j ⊲a i ∈ Σ, then a i ⊲a j ∈ Σ: a contradiction.

Case "( 2), ( 5), i = k, [START_REF] Chandra | Alternation[END_REF], or ( 8), [START_REF] Cook | The complexity of theorem-proving procedures[END_REF], or [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF] and [START_REF] Fagin | Reasoning About Knowledge[END_REF], or [START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF], or [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF], or ( 14)". Since (2), then j is Σ-left and a j ⊲a i ∈ Σ. Since (5), then k is Σ-left and a k ⊲a j ∈ Σ. Since (9), or [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF],

then k is not Σ-left, or a k ⊲a i ∈ Σ. Since k is Σ-left, then a k ⊲a i ∈ Σ. Since j = k, then (a j ⊲a k ↔ a k ⊲a j ) ∈ Σ (use axiom Ax 1 and the fact that j is Σ-left and k is Σ-left). Since a k ⊲a j ∈ Σ, then a j ⊲a k ∈ Σ. Since a k ⊲a i ∈ Σ, then a j ⊲a i ∈ Σ, or a k ⊲a j ∈ Σ (use axiom Ax 2 ). Since a j ⊲a i ∈ Σ, then a k ⊲a j ∈ Σ: a contradiction.
Case "( 2), ( 6) and i = k". Since (2), then a j ⊲a i ∈ Σ. Since (6), then a j ⊲a k ∈ Σ. Since i = k, then a j ⊲a i ∈ Σ: a contradiction.

Case "( 2), ( 6), i = k, [START_REF] Chandra | Alternation[END_REF], or [START_REF] Chang | Model Theory[END_REF], [START_REF] Cook | The complexity of theorem-proving procedures[END_REF], or [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF] and [START_REF] Fagin | Reasoning About Knowledge[END_REF], or [START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF], or [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF], or ( 14)". Since (2), then j is Σ-left and a j ⊲a i ∈ Σ. Since (6), then j is Σ-left, k is Σ-right, a j ⊲a k ∈ Σ and a k ⊲a j ∈ Σ. Since [START_REF] Chandra | Alternation[END_REF], or (8), then i is not Σ-right, or a i ⊲a k ∈ Σ. Since [START_REF] Fagin | Reasoning About Knowledge[END_REF], or [START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF], or [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF], or ( 14), then i is not Σ-left, or k is not Σ-right, or a i ⊲a k ∈ Σ, or a k ⊲a i ∈ Σ. Suppose i is Σ-right. Since i is not Σ-right, or a i ⊲a k ∈ Σ, then a i ⊲a k ∈ Σ. Since i = k, then (a i ⊲a k ↔ a k ⊲a i ) ∈ Σ (use axiom Ax 1 and the fact that i is Σ-right and k is Σ-right). Since a i ⊲a k ∈ Σ, then a k ⊲a i ∈ Σ. Since a j ⊲a i ∈ Σ, then a j ⊲a k ∈ Σ, or a k ⊲a j ∈ Σ (use axiom Ax 2 ). Since a j ⊲a k ∈ Σ, then a k ⊲a j ∈ Σ: a contradiction. Suppose i is Σ-left. Since i = k, then (a i ⊲a k ↔ a k ⊲a i ) ∈ Σ (use axiom Ax 1 and the fact that i is Σ-left and

k is Σ-right). Since i is Σ-left, k is Σ-right and i is not Σ-left, or k is not Σ-right, or a i ⊲a k ∈ Σ, or a k ⊲a i ∈ Σ, then a i ⊲a k ∈ Σ, or a k ⊲a i ∈ Σ. Since (a i ⊲a k ↔ a k ⊲a i ) ∈ Σ, then a k ⊲a i ∈ Σ. Since a j ⊲a i ∈ Σ, then a j ⊲a k ∈ Σ, or a k ⊲a j ∈ Σ (use axiom Ax 2 )
. Since a j ⊲a k ∈ Σ, then a k ⊲a j ∈ Σ: a contradiction.

Case "( 3), ( 4) and i = k". Since (3), then a j ⊲a i ∈ Σ. Since (4), then a j ⊲a k ∈ Σ. Since i = k, then a j ⊲a i ∈ Σ: a contradiction.

Case "(3), ( 4), i = k, [START_REF] Chandra | Alternation[END_REF], or [START_REF] Chang | Model Theory[END_REF], [START_REF] Cook | The complexity of theorem-proving procedures[END_REF], or [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF] and [START_REF] Fagin | Reasoning About Knowledge[END_REF], or [START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF], or [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF], or ( 14)". Since (3), then i is Σ-left, j is Σ-right, a i ⊲a j ∈ Σ and a j ⊲a i ∈ Σ. Since (4), then j is Σ-right and a j ⊲a k ∈ Σ. Since [START_REF] Cook | The complexity of theorem-proving procedures[END_REF], or [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF], then k is not Σ-left, or a k ⊲a i ∈ Σ. Since [START_REF] Fagin | Reasoning About Knowledge[END_REF], or [START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF], or [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF], or [START_REF] Papadimitriou | Computational Complexity[END_REF], then i is not Σ-left, or k is not Σ-right, or a i ⊲a k ∈ Σ, or a k ⊲a i ∈ Σ. Suppose k is Σ-right. Since i is Σ-left and i is not Σ-left, or k is not Σ-right, or a i ⊲a k ∈ Σ, or a k ⊲a i ∈ Σ, then a i ⊲a k ∈ Σ, or a k ⊲a i ∈ Σ. Since i = k, then (a i ⊲a k ↔ a k ⊲a i ) ∈ Σ (use axiom Ax 1 and the fact that i is Σ-left and k is Σ-right). Since a i ⊲a k ∈ Σ, or a k ⊲a i ∈ Σ, then a i ⊲a k ∈ Σ. Since a j ⊲a k ∈ Σ, then a i ⊲a j ∈ Σ, or a j ⊲a i ∈ Σ (use axiom Ax 2 ). Since a i ⊲a j ∈ Σ, then a j ⊲a i ∈ Σ: a contradiction. Suppose k is Σ-left. Since k is not Σ-left, or a k ⊲a i ∈ Σ, then a k ⊲a i ∈ Σ. Since a j ⊲a i ∈ Σ, then a j ⊲a k ∈ Σ, or a k ⊲a j ∈ Σ (use axiom Ax 2 ). Since j = k, then (a j ⊲a k ↔ a k ⊲a j ) ∈ Σ (use axiom Ax 1 and the fact that j is Σ-right and k is Σ-left). Since a j ⊲a k ∈ Σ, or a k ⊲a j ∈ Σ, then a j ⊲a k ∈ Σ: a contradiction.

Case "(3), ( 5) and i = k". Since (3), then a i ⊲a j ∈ Σ. Since ( 5), then a k ⊲a j ∈ Σ. Since i = k, then a i ⊲a j ∈ Σ: a contradiction.

Case "( 3), ( 5), i = k, [START_REF] Chandra | Alternation[END_REF], or ( 8), [START_REF] Cook | The complexity of theorem-proving procedures[END_REF], or [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF] and [START_REF] Fagin | Reasoning About Knowledge[END_REF], or [START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF], or [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF], or ( 14)". Since (3), then i is Σ-left, j is Σ-right, a i ⊲a j ∈ Σ and a j ⊲a i ∈ Σ. Since (5), then k is Σ-left and a k ⊲a j ∈ Σ. Since (9), or [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF], then k is not Σ-left, or a k ⊲a i ∈ Σ. Since k is Σ-left, then a k ⊲a i ∈ Σ. Since i = k, then (a i ⊲a k ↔ a k ⊲a i ) ∈ Σ (use axiom Ax 1 and the fact that i is Σ-left and k is Σ-left). Since a k ⊲a i ∈ Σ, then a i ⊲a k ∈ Σ. Since j = k, then (a j ⊲a k ↔ a k ⊲a j ) ∈ Σ (use axiom Ax 1 and the fact that j is Σ-right and k is Σ-left). Since a k ⊲a j ∈ Σ, then a j ⊲a k ∈ Σ. Since a i ⊲a k ∈ Σ, then a i ⊲a j ∈ Σ, or a j ⊲a i ∈ Σ (use axiom Ax 2 ). Since a i ⊲a j ∈ Σ, then a j ⊲a i ∈ Σ: a contradiction.

Case "( 3), ( 6) and i = k". Since (3), then j is Σ-right. Since ( 6), then j is Σ-left: a contradiction.

Case "(3), ( 6), i = k, [START_REF] Chandra | Alternation[END_REF], or [START_REF] Chang | Model Theory[END_REF], [START_REF] Cook | The complexity of theorem-proving procedures[END_REF], or [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF] and [START_REF] Fagin | Reasoning About Knowledge[END_REF], or [START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF], or [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF], or ( 14)". Since (3), then j is Σ-right. Since (6), then j is Σ-left: a contradiction.

3. Suppose i = j, i does not Σ-precede j and j does not Σ-precede i. Since i = j and i does not Σ-precede j, then

• (1) i is not Σ-right, or (2) a i ⊲a j ∈ Σ, • (3)
j is not Σ-left, or (4) a j ⊲a i ∈ Σ, • (5) i is not Σ-left, or (6) j is not Σ-right, or (7) a i ⊲a j ∈ Σ, or (8) a j ⊲a i ∈ Σ.

Since i = j and j does not Σ-precede i, then

• (9) j is not Σ-right, or (10) a j ⊲a i ∈ Σ, • (11) i is not Σ-left, or (12) a i ⊲a j ∈ Σ, • (13)
j is not Σ-left, or (14) i is not Σ-right, or (15) a j ⊲a i ∈ Σ, or (16) a i ⊲a j ∈ Σ.

The 1st and 5th items imply conditions ( 2) and ( 12), i.e. a i ⊲a j ∈ Σ. The 2nd and 4th items imply conditions (4) and [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF], i.e. a j ⊲a i ∈ Σ. Thus, conditions ( 7), ( 8), ( 15) and ( 16) does not hold. Therefore, the 3rd and 6th items imply i is Σ-right and j is Σ-right, or i is Σ-left and j is Σ-left. Since i = j, then (a i ⊲a j ↔ a j ⊲a i ) ∈ Σ (use axiom Ax 1 and the fact that i is Σ-right and j is Σ-right, or i is Σ-left and j is Σ-left). Since a i ⊲a j ∈ Σ, then a j ⊲a i ∈ Σ: a contradiction.

PROOF OF FACT 4.11. It suffices to note that for all positive integers i, j ≤ n, a i sees a j in u r Σ iff a i sees a j in u l Σ .

PROOF OF FACT 4.12. By Fact 4.11, W T s , u r Σ |= T a i ⊲a j iff W T s , u l Σ |= T a i ⊲a j . Hence, it suffices to demonstrate that W T s , u r Σ |= T a i ⊲a j iff a i ⊲a j ∈ Σ. Suppose W T s , u r Σ |= T a i ⊲a j and a i ⊲a j ∈ Σ. Since W T s , u r Σ |= T a i ⊲a j , then a i sees a j in u r Σ . Hence, S u r Σ (a i ) contains x u r Σ (a j ). Thus, i is Σ-right and ](0, π r Σ (i)), +∞[ contains (0, π r Σ (j)), or i is Σ-left and ] -∞, (0, π r Σ (i))[ contains (0, π r Σ (j)). Therefore, we have to consider two cases.

Case "i is Σ-right and ](0, π r Σ (i)), +∞[ contains (0, π r Σ (j))". Since ](0, π r Σ (i)), +∞[ contains (0, π r Σ (j)), then (0, π r Σ (i)) ≺ (0, π r Σ (j)). Hence, π r Σ (i) < π r Σ (j). Thus, i Σ-precedes j and i = j. Since i Σ-precedes j, i is Σ-right and a i ⊲a j ∈ Σ, then j is Σ-left and a j ⊲a i ∈ Σ. Since i = j, then (a i ⊲a j ↔ a j ⊲a i ) ∈ Σ (use axiom Ax 1 and the fact that i is Σ-right and j is Σ-left). Since a i ⊲a j ∈ Σ, then a j ⊲a i ∈ Σ: a contradiction.

Case "i is Σ-left and ] -∞, (0, π r Σ (i))[ contains (0, π r Σ (j))". Since ] -∞, (0, π r Σ (i))[ con- tains (0, π r Σ (j)), then (0, π r Σ (j)) ≺ (0, π r Σ (i))
. Hence, π r Σ (j) < π r Σ (i). Thus, j Σ-precedes i and i = j. Since j Σ-precedes i, i is Σ-left and a i ⊲a j ∈ Σ, then j is Σ-right and a j ⊲a i ∈ Σ. Since i = j, then (a i ⊲a j ↔ a j ⊲a i ) ∈ Σ (use axiom Ax 1 and the fact that i is Σ-left and j is Σ-right). Since a i ⊲a j ∈ Σ, then a j ⊲a i ∈ Σ: a contradiction. Suppose a i ⊲a j ∈ Σ and W T s , u r Σ |= T a i ⊲a j . Since W T s , u r Σ |= T a i ⊲a j , then a i does not see a j in u r Σ . Hence, S u r Σ (a i ) does not contain x u r Σ (a j ). Thus, i is Σ-right and ](0, π r Σ (i)), +∞[ does not contain (0, π r Σ (j)), or i is Σ-left and ] -∞, (0, π r Σ (i))[ does not contain (0, π r Σ (j)). Therefore, we have to consider two cases.

Case "i is Σ-right and ](0, π r Σ (i)), +∞[ does not contain (0, π r Σ (j))". Since ](0, π r Σ (i)), +∞[ does not contain (0, π r Σ (j)), then (0, π r Σ (i)) ≺ (0, π r Σ (j)). Hence, π r Σ (i) < π r Σ (j). Thus, i does not Σ-precede j. Since i is Σ-right, then a i ⊲a j ∈ Σ: a contradiction.

Case "i is Σ-left and ]-∞, (0, π r Σ (i))[ does not contain (0, π r Σ (j))". Since ]-∞, (0, π r Σ (i))[ does not contain (0, π r Σ (j)), then (0, π r Σ (j)) ≺ (0, π r Σ (i)). Hence, π r Σ (j) < π r Σ (i). Thus, j does not Σ-precede i. Since i is Σ-left, then a i ⊲a j ∈ Σ: a contradiction. PROOF OF FACT 4.13. Obvious. PROOF OF FACT 4.14. Suppose K ai Σ ⊆ ∆. By Fact 4.13, it suffices to demonstrate that u r Σ ≡ T ai u r ∆ , or u r Σ ≡ T ai u l ∆ . Let j Σ 1 , . . . , j Σ l Σ being a list of all the positive integers j Σ ≤ n such that a i ⊲a j Σ ∈ Σ and j ∆ 1 , . . . , j ∆ l ∆ being a list of all the positive integers j ∆ ≤ n such that a i ⊲a j ∆ ∈ ∆. Since K ai Σ ⊆ ∆, then these two lists are equal (use axioms Ax 3 , Ax 4 and Ax 6 ). Obviously,

• if i is Σ-right and i is ∆-right, or i is Σ-left and i is ∆-left then u r Σ ≡ T ai u r ∆ and u l Σ ≡ T ai u l ∆ , • if i is Σ-right and i is ∆-left, or i is Σ-left and i is ∆-right then u r Σ ≡ T ai u l ∆ and u l Σ ≡ T ai u r ∆ . Hence, u r Σ ≡ T ai u r ∆ , or u r Σ ≡ T ai u l ∆ and u l Σ ≡ T ai u r ∆ , or u l Σ ≡ T ai u l ∆ .
PROOF OF FACT 4.15. By induction on ψ(a 1 , . . . , a k ). The argument is similar to that given in Blackburn et al. [START_REF] Blackburn | Modal Logic[END_REF]Lemma 4.21]. The case for a i ⊲a j follows from Fact 4.12. The cases for the Boolean connectives follow from the fact that Σ is an n-maximal L min -consistent set of formulas. It remains to deal with the epistemic connective K ai . By Lemmas 3.1 and 3.3 and Fact 4.11,

W T s , u r Σ |= T K ai ψ(a 1 , . . . , a n ) iff W T s , u l Σ |= T K ai ψ(a 1 , . . . , a n ). Hence, it suffices to demonstrate that W T s , u r Σ |= T K ai ψ(a 1 , . . . , a n ) iff K ai ψ(a 1 , . . . , a n ) ∈ Σ. Suppose W T s , u r Σ |= T K ai ψ(a 1 , . . . , a n ) and K ai ψ(a 1 , . . . , a n ) ∈ Σ. Since K ai ψ(a 1 , . . . , a n ) ∈ Σ, then K ai Σ ∪ {¬ψ(a 1 , . . . , a n )} is an L min -consistent
set of formulas. Hence, by Lemma 4.8, there exists an n-maximal L min -consistent set ∆ of formulas such that

K ai Σ ∪ {¬ψ(a 1 , . . . , a n )} ⊆ ∆. Thus, K ai Σ ⊆ ∆ and ¬ψ(a 1 , . . . , a n ) ∈ ∆. Since K ai Σ ⊆ ∆, then by Fact 4.14, u r Σ ≡ T ai u r ∆ , or u r Σ ≡ T ai u l ∆ . Since ¬ψ(a 1 , . . . , a n ) ∈ ∆, then by induction hypothesis, W T s , u r ∆ |= T ψ(a 1 , . . . , a n ) and W T s , u l ∆ |= T ψ(a 1 , . . . , a n ). Since u r Σ ≡ T ai u r ∆ , or u r Σ ≡ T ai u l ∆ , then W T s , u r Σ |= T K ai ψ(a 1 , . . . , a n ): a contradiction. Suppose K ai ψ(a 1 , . . . , a n ) ∈ Σ and W T s , u r Σ |= T K ai ψ(a 1 , . . . , a n ). Since W T s , u r Σ |= T K ai ψ(a 1 , . . . , a n ), then there exists a T -world v in W T s such that u r Σ ≡ T ai v and W T s , v |= T ψ(a 1 , . . . , a n ).
Without loss of generality, we can assume that for all positive integers k ≤

n, x v (a k ) ∈ {(0, l): l ≤ n is a positive integer}. Let G = {a 1 , . . . , a n } and u r Σ , v be the G-vectors associated to u r Σ , v in the obvious way. Obviously, W T s , u r Σ |= T χ u r Σ and W T s , v |= T χ v . Since W T s , u r Σ |= T χ u r Σ , then by Fact 4.12, χ u r Σ ∈ Σ. Since u r Σ ≡ T ai v, then u r Σ ≡ G ai v. Hence, χ u r Σ → Kai χ v is an instance of axiom Ax 5 . Since χ u r Σ ∈ Σ, then Kai χ v ∈ Σ. Since K ai ψ(a 1 , . . . , a n ) ∈ Σ, then Kai (ψ(a 1 , . . . , a n ) ∧ χ v ) ∈ Σ. Thus, K ai Σ ∪ {ψ(a 1 , . . . , a n ) ∧ χ v }
is an L min -consistent set of formulas. Hence, by Lemma 4.8, there exists an n-maximal L min -consistent set ∆ of formulas such that K ai Σ∪{ψ(a 1 , . . . , a n )∧χ v } ⊆ ∆. Thus, ψ(a 1 , . . . , a n ) ∈ ∆ and χ v ∈ ∆. Since ψ(a 1 , . . . , a n ) ∈ ∆, then by induction hypothesis, W T s , u r ∆ |= T ψ(a 1 , . . . , a n ). Since χ v ∈ ∆, then by Fact 4.12, • for all positive integers i, j ≤ n such that i < j, the literals a i ⊲a j and a i ⊲b j ,

W T s , u r ∆ |= T χ v . Since W T s , v |= T χ v , then u r ∆ Z n v. Since W T s , u r ∆ |= T ψ(
• the literal a i ⊲b i ,

• for all positive integers i, j ≤ n such that i > j, the literals a i ⊲a j and a i ⊲b j .

✉ a 1 ✛ ✉ b 1 ✉ a 2 ✛ ✉ b 2 . . . ✉ a n ✛ ✉ b n R FIG. 15. A simple R-world.
Obviously, ψ is true for a 1-world u in W 1 s iff u looks like the simple R-world depicted in Figure 15. Let u(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) be such a 1-world. Now, consider the sequence φ n+1 , φ n , . . . , φ 1 of formulas defined as follows:

• φ n+1 = θ(b 1 ⊲a 1 , . . . , b n ⊲a n ),
• for all positive integers k ≤ n, φ k = if σ k = ∃ then Ka k (ψ ∧φ k+1 ) else K a k (ψ → φ k+1 ).

Let φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) be φ 1 . Remark that u(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) and φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) can be computed in logarithmic space. Moreover, the reader may easily verify that σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n ), considered as a quantified Boolean expression, is valid in quantified Boolean logic iff φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )), considered as a formula, is true for u(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) in W 1 s . Thus, the validity problem of quantified Boolean logic is reducible to the model checking problem with respect to W 1 s .

PROOF OF LEMMA 5.3. The proof is similar to the proof of Lemma 5.1. Given a quantified Boolean expression σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n ) based on the propositional quantifiers σ 1 , . . . , σ n and the Boolean variables P 1 , . . . , P n , we wish to construct a 2-world u(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) and a formula φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) such that σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n ), considered as a quantified Boolean expression, is valid in quantified Boolean logic iff φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )), considered as a formula, is true for u(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) in W 2 s . Choose distinct agents a 1 , . . . , a n , a ′ 1 , . . . , a ′ n and b 1 , . . . , b n . Let G = {a 1 , . . . , a n , a ′ 1 , . . . , a ′ n } ∪ {b 1 , . . . , b n } and χ be the conjunction of the following literals based on G:

• for all positive integers i, j ≤ n such that i < j, the literals a i ⊲a j , a i ⊲a ′ j , a i ⊲b j , a ′ i ⊲a j , a ′ i ⊲a ′ j and a ′ i ⊲b j , • the literals a i ⊲a ′ i , a i ⊲b i , a ′ i ⊲a i and a ′ i ⊲b i , • for all positive integers i, j ≤ n such that i > j, the literals a i ⊲a j , a i ⊲a ′ j , a i ⊲b j , a ′ i ⊲a j , a ′ i ⊲a ′ j and a ′ i ⊲b j .

Obviously, χ is true for a 2-world u in W 2 s iff u looks like the simple R 2 -world depicted in Figure 16. Let u(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) be such a 2-world. Now, consider the sequence φ n+1 , φ n , . . . , φ 1 of formulas defined as follows:

• φ n+1 = θ(b 1 ⊲a 1 , . . . , b n ⊲a n ),
• for all positive integers k ≤ n, φ k = if σ k = ∃ then Ka k (χ ∧ φ k+1 ) else K a k (χ → φ k+1 ).

Let φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) be φ 1 . Remark that u(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) and φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) can be computed in logarithmic space. Moreover, the

✉ a 1 ❅ ❅ ■ ✉ a ′ 1 ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ ✠ ✉ b 1 ✉ a 2 ❅ ❅ ■ ✉ a ′ 2 ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ ✠ ✉ b 2 . . . ✉ a n ❅ ❅ ■ ✉ a ′ n ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ ✠ ✉ b n R 2 FIG. 16. A simple R 2 -world.
reader may easily verify that σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n ), considered as a quantified Boolean expression, is valid in quantified Boolean logic iff φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )), considered as a formula, is true for u(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) in W 2 s . Thus, the validity problem of quantified Boolean logic is reducible to the model checking problem with respect to W 2 s .

PROOF OF LEMMA 6.1. Given a quantified Boolean expression σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n ) based on the propositional quantifiers σ 1 , . . . , σ n and the Boolean variables P 1 , . . . , P n , we wish to construct a formula φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) such that σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n ), considered as a quantified Boolean expression, is valid in quantified Boolean logic iff φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )), considered as a formula, is satisfiable in W 1 s . Choose distinct agents a 1 , . . . , a n and b 1 , . . . , b n . Let G = {a 1 , . . . , a n } ∪ {b 1 , . . . , b n } and ψ be the conjunction of literals based on G defined in the proof of Lemma 5.1. Let φ n+1 , φ n , . . . , φ 1 be the sequence of formulas defined in the proof of Lemma 5.1. Let φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) be ψ ∧ φ 1 . Remark that φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) can be computed in logarithmic space. Moreover, the reader may easily verify that σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n ), considered as a quantified Boolean expression, is valid in quantified Boolean logic iff φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )), considered as a formula, is satisfiable in W 1 s . Hence, the validity problem of quantified Boolean logic is reducible to the satisfiability problem with respect to W 1 s .

PROOF OF LEMMA 6.3. The proof is similar to the proof of Lemma 6.1. Given a quantified Boolean expression σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n ) based on the propositional quantifiers σ 1 , . . . , σ n and the Boolean variables P 1 , . . . , P n , we wish to construct a formula φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) such that σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n ), considered as a quantified Boolean expression, is valid in quantified Boolean logic iff φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )), considered as a formula, is satisfiable in W 2 s . Choose distinct agents a 1 , . . . , a n , a ′ 1 , . . . , a ′ n and b 1 , . . . , b n . Let G = {a 1 , . . . , a n , a ′ 1 , . . . , a ′ n } ∪ {b 1 , . . . , b n } and χ be the conjunction of literals based on G defined in the proof of Lemma 5.3. Let φ n+1 , φ n , . . . , φ 1 be the sequence of formulas defined in the proof of Lemma 5.3. Let φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) be χ ∧ φ 1 . Remark that φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) can be computed in logarithmic space. Moreover, the reader may easily verify that σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n ), considered as a quantified Boolean expression, is valid in quantified Boolean logic iff φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )), considered as a formula, is satisfiable in W 2 s . Hence, the validity problem of quantified Boolean logic is reducible to the satisfiability problem with respect to W 2 s .

EXAMPLE 2. 2

 2 If one considers Figure 1 in dimension 2, a 2-scope is defined by the point and the open half plane located on the same side of the line through the point as indicated by the arrow.

  Given an n-world u and agents a, b, if u(a) = (x u (a), S u (a)) and u(b) = (x u (b), S u (b)) then x u (a) and x u (b) are respectively the positions in R n occupied by a and b in u and S u (a) and S u (b)are respectively the sections of R n seen by a and b in u. We will always assume that if a = b then x u (a) = x u (b): distinct agents occupy distinct positions. An n-world u is said to be simple iff for all agents a, the n-scope u(a) is simple.

EXAMPLE 2. 4

 4 In the simple 2-world considered in Figure 2, a sees b, a does not see c, b sees a, b sees c, c sees a and c does not see b. n-worlds u and v are said to be indiscernible for agent a, in symbols u ≡ n a v, iff x u (a) = x v (a), S u (a) = S v (a) and for all agents b, if a = b then one of the following conditions holds: • a sees b in u, a sees b in v, x u (b) = x v (b) and S u (b) = S v (b), • a does not see b in u and a does not see b in v. EXAMPLE 2.5 The simple 2-worlds considered in Figures 2 and 3 are indiscernible for agent a.

EXAMPLE 2. 7 FIG. 4 .

 74 FIG.4. A simple R-scope.

EXAMPLE 7. 1 2 FIG. 14 .

 1214 FIG.14. A circular 2-scope.

  EXAMPLE 2.6 If u is the simple 2-world depicted in Figure 2 then W 2 s , u |= 2 a⊲b and W 2 s , u |= 2 K a b⊲a. If v is the simple 2-world depicted in Figure 3 then W 2 s , v |= 2 a⊲c and W 2 s , v |= 2 Ka c⊲a.

formula φ is said to be satisfiable (falsifiable) in a nonempty set W of n-worlds, in symbols W sat n φ (W f al n φ), iff there exists an n-world u in W such that W, u |= n φ (W, u |= n φ). Let W n s be the set of all simple n-worlds.

  [START_REF] Ben-Or | The complexity of elementary algebra and geometry[END_REF] says that if a looks at b then a knows whether b looks at c; Ax 5 says that what is compatible with what a currently sees is also compatible with what a currently knows; Ax 6 says that what a knows is true. Note that we have no need, as proper axioms, of the traditional formulas of positive introspection (K a φ → K a K a φ) and negative introspection (¬K a φ → K a ¬K a φ). Seeing that these formulas are valid in W 1 s , the completeness result described below in Proposition 4.16 implies that they are derivable from the proper axioms.

  a 1 , . . . , a n ), then by Lemmas 3.1 and 3.3, W T s , v |= T ψ(a 1 , . . . , a n ): a contradiction. PROOF OF LEMMA 5.1. Given a quantified Boolean expression σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n ) based on the propositional quantifiers σ 1 , . . . , σ n and the Boolean variables P 1 , . . . , P n , we wish to construct a 1-world u(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) and a formula φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) such that σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n ), considered as a quantified Boolean expression, is valid in quantified Boolean logic iff φ(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )), considered as a formula, is true for u(σ 1 P 1 . . . σ n P n θ(P 1 , . . . , P n )) in W 1 s . Choose distinct agents a 1 , . . . , a n and b 1 , . . . , b n . Let G = {a 1 , . . . , a n } ∪ {b 1 , . . . , b n } and ψ be the conjunction of the following literals based on G:

New address of Franc ¸ois Schwarzentruber: IRISA, ENS Cachan -Antenne de Bretagne, Campus de Ker Lann, 35170 BRUZ, France.

Acknowledgements

We want to thank all our colleagues of the Institut de recherche en informatique de Toulouse who made several helpful comments for improving the correctness and the readability of this article. We are also grateful for the detailed comments referees made on a preliminary version of this paper.

of generality, let us assume that the 2-world (u(a 1 ), . . . , u(a n )) in W 2 s is given by means of rational numbers r x 0 1 , r y 0 1 , . . . , r x 0 n , r y 0 n , r z 0 1 , r t 0 1 , . . . , r z 0 n , r t 0 n corresponding to the abscissas and the ordinates of the positions in R 2 occupied by a 1 , . . . , a n and the coordinates of the endpoints in R 2 of the vectors located at the origin corresponding to the sections seen by a 1 , . . . , a n . Rational numbers being easily definable in the language of elementary algebra, there exists a formula ϕ u (x 0 1 , y 0 1 , . . . , x 0 n , y 0 n , z 0 1 , t 0 1 , . . . , z 0 n , t 0 n ) with free individual variables x 0 1 , y 0 1 , . . . , x 0 n , y 0 n , z 0 1 , t 0 1 , . . . , z 0 n , t 0 n in elementary algebra such that the following conditions are equivalent:

For all positive integers i, j ≤ n and for all nonnegative integers α, let sees(x α i , y α i , z α i , t α i , x α j , y α j ) be a formula with free individual variables x α i , y α i , z α i , t α i , x α j , y α j in elementary algebra such that the following conditions are equivalent:

• an agent occupying the position in R 2 defined by (v x α i , v y α i ) and seeing the section in R 2 defined by (v z α i , v t α i ) sees an agent occupying the position in R 2 defined by (v x α j , v y α j ). For all positive integers i ≤ n and for all nonnegative integers α, let equiv i (x α 1 , y

The translation τ taking nonnegative integers and formulas to formulas in elementary algebra is defined as follows: Let ϕ((u(a 1 ), . . . , u(a n )), φ(a 1 , . . . , a n )) be ∀x 0 1 ∀y 0 1 . . . ∀x 0 n ∀y 0 n ∀z 0 1 ∀t 0 1 . . . ∀z 0 n ∀t 0 n (ϕ u (x 0 1 , y 0 1 , . . . , x 0 n , y 0 n , z 0 1 , t 0 1 , . . . , z 0 n , t 0 n ) → τ (0, φ(a 1 , . . . , a n ))). Remark that ϕ((u(a 1 ), . . . ,


Vamsidhar Reddy Gaddam
email: vamsidhg@ifi.uio.no

Ragnar Langseth
email: ragnarla@ifi.uio.no

Hakon Kvale
email: haakonks@ifi.uio.no

Pierre Stensland

Vincent Gurdjos
email: pgurdjos@enseeiht.fr

Carsten Charvillat

Dag Griwodz

Pal Halvorsen Johansen

Håkon Kvale Stensland

Pierre Gurdjos

Vincent Charvillat
email: vincent.charvillat@enseeiht.fr

Carsten Griwodz

Dag Johansen

Pål Halvorsen

Be Your Own Cameraman: Real-Time Support for Zooming and Panning into Stored and Live Panoramic Video

Keywords: Experimentation, Performance demonstration, panorama video, zoom, panning, real-time

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

INTRODUCTION

Panoramic video is becoming increasingly more popular in various scenarios. In the context of arena sports like soccer, it provides opportunities for innovation in broadcasting and in the area of game analysis. For example, based on a camera array covering the whole field, virtual views can be supported by zooming and panning into a stitched panorama video, e.g., allowing individual users to interactively control his or her own virtual camera. This type of challenges has attracted researchers' attentions for more than a decade [START_REF] Sun | Region of interest extraction and virtual camera control based on panoramic video capturing[END_REF][START_REF] Wang | Automatic replay generation for soccer video broadcasting[END_REF][START_REF] Ariki | Automatic production system of soccer sports video by digital camera work based on situation recognition[END_REF][START_REF] Carr | Hybrid robotic/virtual pan-tilt-zom cameras for autonomous event recording[END_REF][START_REF] Mavlankar | Video streaming with interactive pan/tilt/zoom[END_REF][START_REF] Carr | Portable multi-megapixel camera with real-time recording and playback[END_REF][START_REF] Wieland | Remote camera control in a distributed multimedia system[END_REF], but often the zoom is made by simple cropping, or it does not scale. As can be seen in the literature, the challenges in providing such interactive experiences to a large audience span several fields, and one such challenge is to provide a real-time pannable and zoomable virtual camera to several thousands or even millions of users.

In this respect, we present an end-to-end real-time system to interactively zoom and pan into high-resolution panoramic videos. In contrast to many existing systems supporting zoom by cropping into a perspective panorama video, our system uses cylindrical panorama as an intermediate representation. Here, the perspective of the virtual view is corrected in real-time, and the result is a better and more natural zoom. The client has full freedom to pan, tilt and zoom into the panorama video using the system. The system supports (live switching between) several algorithms for pixel interpolation. Furthermore, our experimental results indicate that such zoomed virtual views can be generated far below the frame-rate threshold where an unoptimized GPU implementation generates a virtual view frame in about 10 ms. Thus, taking into account recent trends in device development, our approach should be able to scale to a large number of concurrent users in the near future to spectators and fans both within the stadium as well as outside. Inside the stadium, the Cisco connected stadium solution [4] already in use in more than 200 venues world-wide can be used to broadcast the panorama video to the spectators, and for users at home, there exist several scalable streaming solutions like segmented HTTP streaming [START_REF] Smoothhd | [END_REF][START_REF]HTTP Live Streaming[END_REF] or panorama video transfers in real-time [START_REF] Guntur | On tile assignment for region-of-interest video streaming in a wireless lan[END_REF].

In this demonstration, we present two versions of our system. The first is a demonstration which uses a recorded five 2K-camera panorama video from Alfheim stadium where the current prototype is installed. The second demonstration is a live, scaled down version 1 of the system with two 2K cameras zooming into live recorded video at the conference venue. The motivation is to provide a hands-on experience of such a system. The demo will allow users to interact with the virtual camera in both stored and live scenes.

SYSTEM OVERVIEW

The system presented in this demo is part of a larger system where the current prototype is running at Alfheim stadium in Tromsø. This system has been presented before [START_REF] Halvorsen | Bagadus: An integrated system for arena sports analytics -a soccer case study[END_REF][START_REF] Stensland | Bagadus: An integrated real-time system for soccer analytics[END_REF], but without the possibility to interactively zoom an pan into a high-resolution panorama.

System Setup

The relevant part of the system in this context is divided into a panorama generation part and a video delivery part, which supports our user-controlled interactive virtual cameras. A sketch of our system is given in figure 1. In this section, we describe these two parts.

Real-time Panorama Video Capture

To capture the entire soccer field, we use five Basler industry vision cameras [START_REF] Basler Aca | [END_REF], each of which delivers a maximum resolution of 2046 × 1086 pixels at 50 frames per second over 1 The live 2-camera setup is due to hardware constraints bringing equipment to the conference venue. The five camera version requires several recording machines and a processing machine. A live view from the camera setup at Alfheim stadium could be possible, but as we sometimes have bandwidth problems over the 19-hop Tromsø-Oslo link, we expect an even lower available bandwidth from Tromsø to Singapore. Gigabit Ethernet. We use an 8 mm lens [START_REF]Azure-0814m5m[END_REF] with virtually no image distortion, allowing us to bypass the lossy debarreling step of our previous real-time pipeline [START_REF] Tennøe | Efficient implementation and processing of a real-time panorama video pipeline[END_REF]. To maximize the panorama resolution, the cameras are rotated by 90°(see figure 2), giving a vertical field of view of 66°. Furthermore, the cameras are mounted in a circular pattern. This means that they are pitched, yawed and rolled to look directly through a point 5 cm in front of the lenses, in an attempt to reduce parallax effects. As a result of this, only minor adjustments are required before the images can be stitched together. The video capture system also determines the required exposure, which requires frequent changes due to quickly changing light conditions outdoors. In this respect, auto-exposure is performed on the center camera once every 4 seconds, and the camera reader module broadcasts the resulting exposure parameters to the other camera readers.

Figure 2: Mounted camera array

After the generation of the panorama video, it is encoded and compressed using x264. At the moment, with a focus on video quality, the system still demands a large network bandwidth to the full resolution panorama video. However, there are large potentials for trading of quality for lower bandwidth requirements (but an investigation of this is out of scope for this demonstration).

Live Panoramic Zoom and Panning

To deliver a virtual camera to clients, the panorama video is delivered to the client device. Currently, we use HTTP segment streaming (no quality adaption at the time of writing, but it can easily be added in the future). The segments of the panoramic videos are served by an Apache server along with a manifest file. The manifest file is used to inform the clients when the next file is ready for download. In case of live streaming, the viewer checks the manifest file periodically and downloads the next segment when ready. As soon as the panoramic video segment is transferred, it is decoded for processing by the multi-threaded client process. The downloading thread runs in the background without blocking either the display thread or the user input thread.

Using the cylindrical panorama as an intermediate representation, our system then generate an arbitrary virtual camera view from the position of the camera array. All the details of the pixel calculations are out of scope of this demonstration description (see [START_REF] Gaddam | Interactive zoom and panning from live panoramic video[END_REF]), but the main operation is to find the pixels of the virtual camera image from the cylindrical texture as shown in figure 3. A pin-hole camera model is used, and the a point projection from a 3D point to an image point is calculated using a 3D rotation matrix as a function of the rotation angles around the x, y and z axes. A particular pixel is then found by calculating the ray that passes from the camera center to the pixel. The intersection of this ray with the cylinder gives the exact position on the cylindrical texture. Finally, since there is sub-pixel accu-Figure 3: The intersection of the ray from the virtual view with the unit cylinder of the panorama image. racy of the intersection calculation, the used pixel value is calculated using interpolation of all the surrounding pixels.

The user has the full freedom to pan, tilt and zoom, being his or hers own camera-man2 . The virtual camera view is corrected to a perspective view very similar to that of a physical camera as shown in figure 4.

!"#$%&'$()#*+)%,')-)* .$'/0)#*()-1')* Figure 4: The virtual camera is generated from the region of interest marked in the panorama video. Note that it is not a simple crop from the bigger video.

System Performance

We have earlier shown that our system can generate panorama video in real-time using four 1K cameras [START_REF] Tennøe | Efficient implementation and processing of a real-time panorama video pipeline[END_REF]. Going for higher resolution, we have now distributed the capture and processing of five 2K cameras, and we are able to generate the panorama frames in 34.58 ms on an Intel i7 CPU. This is below our 25 fps threshold. The generated video can either be stored to disk or forwarded directly to connected client devices.

When presented to the user, the zooming and panning operations can be performed on both the sender and receiver side. In the current setup, we as explained above transmit the panorama video to the display device like a laptop. Here, the zoom and pan operations are executed where the perspective is corrected from the cylindrical panorama in realtime. We use the GPU on the client side, and each frame for virtual camera view with Full HD resolution (1920 × 1080) can be generated in about 10 milliseconds on a machine with an Intel i7-2600 CPU and an Nvidia GeForce GTX 460 GPU

Figure 1 :

 1 Figure 1: Demonstration setup

An example video using the known ball position, where the virtual camera-man is following the ball is shown here: http://www.youtube.com/watch?v=554RjEEtw3o -again, far below the target 25 fps requirement. This time is dependent of the output resolution, and going for a mobile phone resolution it can be further reduced by a millisecond or two, e.g., about 1.5 milliseconds for iPhone 4 and 5.

DEMONSTRATIONIn this demo, we present a system for real-time interactive zooming and panning of panorama video. The general setup is shown in figure1. We use two types of panorama input. We use stored panorama video captured in the Alfheim soccer stadium (the European League game between Tromsø IL and Tottenham Hotspurs)[START_REF] Pettersen | Soccer video and player position dataset[END_REF]. The video was recorded using five 2K industrial cameras, and processed and stitched in a distributed system. We also use a live system using 2 cameras on site to generate the panorama video. Both the stored-video and the live-video demos work in real-time, and the user interactions have a very low delay from command to visual response -thus, a user can be his or her own cameraman!

Acknowledgments

This work has been performed in the context of the iAD center for Research-based Innovation (project number 174867) funded by the Norwegian Research Council. Furthermore, the authors also acknowledge the support and hardware given by Hugo Kohmann and Roy Nordstrøm in Dolphin Interconnect Solutions.