Philippe Balbiani
email: philippe.balbiani@irit.fr

David Fernández-Duque

Emiliano Lorini
email: emiliano.lorini@irit.fr

A Logical Theory of Belief Dynamics for Resource-Bounded Agents

Keywords: Epistemic logic, cognitive agents, resource-bounded reasoning

The paper presents a new logic for reasoning about the formation of beliefs through perception or through inference in non-omniscient resource-bounded agents. The logic distinguishes the concept of explicit belief from the concept of background knowledge. This distinction is reflected in its formal semantics and axiomatics: (i) we use a non-standard semantics putting together a neighbourhood semantics for explicit beliefs and relational semantics for background knowledge, and (ii) we have specific axioms in the logic highlighting the relationship between the two concepts. Mental operations of perceptive type and inferential type, having effects on epistemic states of agents, are primitives in the object language of the logic. At the semantic level, they are modelled as special kinds of model-update operations, in the style of dynamic epistemic logic (DEL). Results about axiomatization, decidability and complexity for the logic are given in the paper.

INTRODUCTION

Most of existing logical theories of epistemic attitudes developed in the area of epistemic logic assume that agents are omniscient, in the sense that: (i) their beliefs are closed under conjuction or under known implication, i.e., if ϕ is believed and ψ is believed then ϕ ∧ ψ is believed and if ϕ is believed and ϕ → ψ is believed then ψ is believed; (ii) their explicit beliefs are closed under logical consequence (alias valid implication), i.e., if ϕ is believed and ϕ logically implies ψ, i.e., ϕ → ψ is valid, then ψ is believed as well; (iii) they believe valid sentences or tautologies; (iv) they have introspection over their beliefs, i.e., if ϕ is believed then it is believed that ϕ is believed.

As pointed out by [START_REF] Hintikka | Impossible possible worlds vindicated[END_REF][START_REF] Levesque | A logic of implicit and explicit belief[END_REF], relaxing the assumption of logical omniscience allows for a resource-bounded agent who might fail to draw any connection between ϕ and its logical consequence ψ and, consequently, to believe any valid sentence and who might need time to infer and form new beliefs from her existing knowledge and beliefs.

The aim of this paper is to propose a new logic which helps in clarifying how a non-omniscient resource-bounded agent can form new beliefs either through perception or through inference from her existing knowledge and beliefs. More precisely, the aim of the paper is to introduce a dynamic logic, called DLEK (Dynamic Logic of Explicit Beliefs and Knowledge) in which programs are mental operations, either of perceptive type or of inferential type, having effects on epistemic states of resourced-bounded agents. This is not the first attempt to build a logic of epistemic attitudes for non-omniscient agents. Logics of awareness have been studied in the recent years (see, e.g., [START_REF] Van Ditmarsch | Semantics for knowledge and change of awareness[END_REF][START_REF] Halpern | Reasoning about knowledge of unawareness[END_REF][START_REF] Grossi | Twelve Angry Men: A study on the fine-grain of announcements[END_REF][START_REF] Ågotnes | A logic for reasoning about knowledge of unawareness[END_REF]) starting from the seminal work of Fagin & Halpern [START_REF] Fagin | Belief, awareness, and limited reasoning[END_REF]. These logics distinguish between explicit beliefs that are under the focus of attention and implicit beliefs, namely, potential beliefs that are derivable from what an agent explictly believes. However, the crucial difference between DLEK and existing logics of awareness is that the former provides a constructive theory of explicit beliefs, as it accounts for the perceptive and inferential steps leading from an agent's knowledge and beliefs to new beliefs. A notable exception is [START_REF] Velázquez-Quesada | Explicit and implicit knowledge in neighbourhood models[END_REF], although our conceptual framework is different (see Section 2) and, unlike the present paper, the author does not provide any axiomatization or decidability result for his logic of reasoning steps, as he only provides a semantics. Moreover, [START_REF] Velázquez-Quesada | Explicit and implicit knowledge in neighbourhood models[END_REF] does not distinguish the concept of explicit belief and the concept of background knowledge, which is the fundamental distinction of our logic DLEK.

DLEK is the first logical theory of the relationship between explicit beliefs and background knowledge, both from a static and from a dynamic perspective. This is reflected in its formal semantics and axiomatics: (i) we use a nonstandard semantics putting together a neighbourhood semantics for explicit beliefs and relational semantics for background knowledge, and (ii) we have specific axioms in the logic highlighting the relationship between the two concepts.

Our constructive approach to explicit beliefs also distin-guishes DLEK from existing logics of time-bounded reasoning which represent reasoning as a process that requires time (see, e.g., [START_REF] Alechina | A complete and decidable logic for resource-bounded agents[END_REF][START_REF] Grant | A logic for characterizing multiple bounded agents[END_REF]). Specifically, existing logics of time-bounded reasoning account for the formation of new beliefs due to the time-consuming application of inference rules to the beliefs that are under the focus of attention. However, differently from DLEK, they do not include mental operations of perceptive type and inferential type as primitives in the object language of the logic. As we will show in the paper, the advantage of having mental operations in the object language of DLEK is that we can use it to reason about the consequences of a sequence of perceptive and inferential steps on the epistemic states of agents.

The paper is organized as follows. In Section 2 we present the conceptual foundation of our logic DLEK, namely the general view about dynamics of beliefs in resource-bounded agents which underlies our formal theory. The general idea is that new beliefs can be formed either by perception or by inferring them from existing beliefs in working memory and by retrieving information from background knowledge in long-term memory. Section 3 presents the syntax and the semantics of DLEK. We will show that in DLEK perceptive and inferential steps are modelled as special kinds of modelupdate operations, in the style of dynamic epistemic logic (DEL) [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF]. In Section 4 we present an example illustrating the expressive power of the logic. Section 5 is devoted to present an axiomatics. Finally, Section 6 presents complexity results for the satisfiability problem of the static fragment of DLEK, called LEK as well as a decidability result for the satisfiability problem of DLEK.

CONCEPTUAL FRAMEWORK

The cognitive architecture underlying the logic DLEK (Dynamic Logic of Explicit Beliefs and Knowledge) is represented in Figure 1. It clarifies the processing of information in human agents and human-like artificial agents. In accordance with existing psychological theories and computational models of memory and attention [START_REF] Baddeley | Working memory[END_REF][START_REF] Cowan | An embedded process model of working memory[END_REF][START_REF] Young | The Soar cognitive architecture and human working memory[END_REF][START_REF] Lovett | Modeling working memory in a unified architecture: An ACT-R perspective[END_REF], we assume that an agent has two kinds of information in her mind, those available in long-term memory (LTM) and those directly accessible in working memory (WM).

Long-term memory

The information available in long-term memory, generally called background knowledge, includes both knowledge of specific events in the past and conceptual or causal knowledge representing the agent's unproblematic interpretation of reality. 1 For example, an agent may have background conceptual knowledge about how restaurants are organized or background causal knowledge about the relation between smoke and fire. In particular, she may know that restaurants have waiters, chairs and tables or that if smoke comes out from a window of a certain house, then there is fire inside the house.

Working memory retains information in an accessible state suitable for carrying out any kind of reasoning or decision task. In particular, following [START_REF] Kahneman | Variants of uncertainty[END_REF], we assume that the information available in an agent's working memory includes all explicit beliefs of the agent that occupy her consciousness and draw on her limited capacity of attention.2 Some explicit beliefs are formed via perception. Formation of explicit beliefs via perception just consists of adding a new belief to the set of beliefs that are under the focus of the agent's attention. For example, an agent may look outside the window, see that it is raining outside, and thereby start believing that it is raining outside.

An agent can also use her explicit beliefs as premises of an inference which leads to the formation of a new belief. In some cases, formation of explicit beliefs via inference requires the retrieval of information from long-term memory. For example, suppose that an agent sees that smoke comes out from the window of a certain house and, as a result, she starts to explicitly believe this. The agent retrieves from her background knowledge stored in her long-term memory the information that if smoke comes out from a window of a certain house, then it means that there is fire inside the house. The agent can use this information together with the belief that smoke comes out from the window available in her working memory, to infer that there is fire inside the house and to form the corresponding belief.

Information can also be lost from working memory through forgetting: an agent may explicitly believe something but not believe it anymore at a later point. Information can also be removed from working memory and stored in long-term memory to make it available for a later moment. Storage of information in long-term memory might be necessary, given the limited capabilities of working memory.

In the next section we present the syntax and the semantics of the logic DLEK which makes precise all concepts informally discussed in this section.

LOGICAL FRAMEWORK

DLEK is a logic which consists of a static component and a dynamic one. The static component, called LEK, is a logic of explicit beliefs and background knowledge. The dynamic component extends the static one with dynamic operators capturing the consequences of the agents' mental operations on their explicit beliefs.

Syntax

Assume a countable set of atomic propositions Atm = {p, q, . . .} and a finite set of agents Agt = {1, . . . , n}. The set of groups (or coalitions) is defined to be 2 Agt * = 2 Agt \{∅}. Elements of 2 Agt * are denoted by J, J ′ , . . . We denote with Prop the set of all Boolean formulas built out of the set of atomic propositions Atm.

The language of DLEK, denoted by LDLEK, is defined by the following grammar in Backus-Naur Form:

α ::= ⊢(ϕ,ψ) | ∩(ϕ,ψ) | +ϕ | -ϕ ϕ, ψ ::= p | ¬ϕ | ϕ ∧ ψ | Biϕ | Kiϕ | [α]ϕ
where p ranges over Atm and i ranges over Agt.

The other Boolean constructions ⊤, ⊥, ∨, → and ↔ are defined from p, ¬ and ∧ in the standard way.

The language of LEK, the fragment of DLEK without dynamic operators, is denoted by LLEK and defined by the following grammar in Backus-Naur Form:

ϕ, ψ ::= p | ¬ϕ | ϕ ∧ ψ | Biϕ | Kiϕ
where p ranges over Atm and i ranges over Agt. The other Boolean constructions ⊤, ⊥, ∨, → and ↔ are defined from p, ¬ and ∧ in the standard way. In what follows, we explain the meaning of the operators of our logic.

The formula Biϕ is read "the agent i explicitly believes that ϕ is true" or, more shortly, "the agent i believes that ϕ is true". As explained in Section 2, explicit beliefs are accessible in working memory and are the basic elements of the agents' reasoning process.

The modal operator Ki captures the notion of background knowledge discussed in Section 2. It represents the information that agent i can use and that is available in long term memory to infer new explicit beliefs. Some pieces of background knowledge are either conceptual or causal and represent the agent's unproblematic interpretation of reality.

Differently from explicit beliefs, background knowledge is assumed to satisfy 'omniscience' principles like closure under conjuction and known implication, closure under logical consequence and introspection. Specifically, as we will show below, Ki is nothing but the well-known S5 operator for knowledge widely used in computer science [START_REF] Fagin | Reasoning about knowledge[END_REF]. The fact that the operator Ki satisfies 'omniscience' principles is justified by the assumption that the information that an agent possesses in background defines a deductively closed knowledge base.

The formula [α]ψ has to be read "ψ holds, after the mental operation (or mental action) α is publicly performed by all agents". We distinguish four types of mental operations α which allow us to capture some of the dynamic properties of explicit beliefs and background knowledge informally described in Section 2 above: +ϕ, -ϕ, ⊢(ϕ,ψ) and ∩(ϕ,ψ).

+ϕ and -ϕ correspond, respectively, to the mental operations of forming an explicit belief via perception and forgetting an explicit belief represented in Figure 1.

⊢(ϕ,ψ) and ∩(ϕ,ψ) characterize two basic operations of forming explicit beliefs via inference. Specifically, ⊢(ϕ,ψ) is the mental operation which consists in inferring ψ from ϕ in case ϕ is believed and, according to an agent's background knowledge, ψ is a logical consequence of ϕ. In other words, by performing this mental operation, an agent tries to retrieve from her background knowledge in long-term memory the information that ϕ implies ψ and, if she succeeds, she starts to believe ψ. ∩(ϕ,ψ) is the mental operation which consists in closing the explicit belief that ϕ and the explicit belief that ψ under conjunction. In other words, ∩(ϕ,ψ) characterizes the mental operation of deducing ϕ ∧ ψ from the explicit belief that ϕ and the explicit belief that ψ.

In this paper we assume that, differently from explicit beliefs, background knowledge is irrevocable in the sense of being stable over time [START_REF] Baltag | A qualitative theory of dynamic interactive belief revision[END_REF]. In the conclusion, we will offer some insights on how to make background knowledge dynamic by including in our logic the operation of storing information in long-term memory, represented in Figure 1.

Semantics

The main notion in semantics is given by the following definition of LEK model which provides the basic components for the interpretation of the static logic LEK:

Definition 1 (LEK model). A LEK model is a tuple M = (W, N, R1, . . . , Rn, V ) where:
• W is a set of worlds or situations;

• for every i ∈ Agt, Ri ⊆ W × W is an equivalence relation on W ; • N : Agt ×W -→ 2 2 W is a neighbourhood function such that for all i ∈ Agt, w, v ∈ W and X ⊆ W : (C1) if X ∈ N (i, w) then X ⊆ Ri(w), (C2) if wRiv then N (i, w) = N (i, v); • V : W -→ 2 Atm is a valuation function.
For every i ∈ Agt and w ∈ W , Ri(w) = {v ∈ W : wRiv} identifies the set of situations that agent i considers possible at world w. In cognitive terms, Ri(w) can be conceived as the set of all situations that agent i can retrieve from her long-term memory and reason about them. More generally, Ri(w) is called agent i's epistemic state at w. The reason why Ri is an equivalence relation is that it is used to model a form of omniscient background knowledge instead of omniscient background belief. The latter could be modelled by replacing the equivalence relations Ri by serial, transitive and Euclidean relations commonly used in doxastic logic to model a notion of belief.

For every i ∈ Agt and every w ∈ W , N (i, w) defines the set of all facts that agent i explicitly believes at world w, a fact being identified with a set of worlds. More precisely, if A ∈ N (i, w) then, at world w, agent i has the fact A under the focus of her attention and believes it. N (i, w) is called agent i's explicit belief set at world w.

Constraint (C1) just means that an agent can have explicit in her mind only facts which are compatible with her current epistemic state. According to Constraint (C2), if world v is compatible with agent i's epistemic state at world w, then agent i should have the same explicit beliefs at w and v.

Truth conditions of DLEK formulas are inductively defined as follows.

Definition 2 (Truth conditions). Let M = (W, N, R1, . . . , Rn, V ) be a LEK model. Then:

M, w |= p ⇐⇒ p ∈ V (w) M, w |= ¬ϕ ⇐⇒ M, w |= ϕ M, w |= ϕ ∧ ψ ⇐⇒ M, w |= ϕ and M, w |= ψ M, w |= Biϕ ⇐⇒ ||ϕ|| M i,w ∈ N (i, w) M, w |= Kiϕ ⇐⇒ M, v |= ϕ for all v ∈ Ri(w) M, w |= [α]ϕ ⇐⇒ M α , w |= ϕ where ||ϕ|| M i,w = {v ∈ W : M, v |= ϕ} ∩ Ri(w)
and M α = (W, N α , R1, . . . , Rn, V ) such that, for all i ∈ Agt and w ∈ W :

N +ψ (i, w) = N (i, w) ∪ {||ψ|| M i,w } N -ψ (i, w) = N (i, w) \ {||ψ|| M i,w } N ⊢(ψ,χ) (i, w) =      N (i, w) ∪ {||χ|| M i,w } if M, w |= Biψ∧ Ki(ψ → χ) N (i, w) otherwise N ∩(ψ,χ) (i, w) =      N (i, w) ∪ {||ψ ∧ χ|| M i,w } if M, w |= Biψ∧ Biχ N (i, w) otherwise
Note that in the mono-agent case, thanks to Constraint (C1), we can assume, in a given model M = (W, N, R1, V ), that R1 is the universal relation on W . According to the previous truth conditions, an agent i explicitly believes ϕ at world w if and only if, at world w, agent i has the fact corresponding to the formula ϕ (i.e., ||ϕ|| M i,w ) included in her explicit belief set. Moreover, an agent has background knowledge that ϕ is true if and only if ϕ is true in all situations that are included in the agent's epistemic state. Mental operations of the form α are formalized as model update operations that expand or contract the agents' explicit belief sets. In particular, the mental operation +ψ consists in perceiving ψ and adding it to the explicit belief set, while the mental operation -ψ consists in forgetting ψ and removing it from the explicit belief set. The mental operation ⊢(ψ,χ) consists in adding the explicit belief χ to an agent's explicit belief set if the agent believes ψ and has background knowledge that ψ implies χ. The mental operation ∩(ψ,χ) consists in adding the explicit belief ψ ∧ χ to an agent's explicit belief set if the agent explicitly believes both ψ and χ.

We write |=DLEK ϕ to denote that ϕ is valid, i.e., ϕ is true at every world w of every LEK-model M . In the next section we show some interesting validities of the logic DLEK.

Some validities

The following four validities capture the basic properties of the four mental operations ⊢(ϕ,ψ), ∩(ϕ,ψ), +ϕ and -ϕ semantically defined above. Let ϕ, ψ ∈ Prop. Then:

|=DLEK (Ki(ϕ → ψ) ∧ Biϕ) → [⊢(ϕ,ψ)]Biψ (1) |=DLEK (Biϕ ∧ Biψ) → [∩(ϕ,ψ)]Bi(ϕ ∧ ψ) (2) |=DLEK [+ϕ]Biϕ (3) |=DLEK [-ϕ]¬Biϕ (4)
For instance, according to the first validity, if ϕ and ψ are propositional formulas, agent i explicitly believes ϕ and has background knowledge that ϕ implies ψ then, as a consequence of the mental operation ⊢ (ϕ,ψ), she will start to believe ψ. According to the third validity, if ϕ is a propositional formula then, as a consequence of perceiving that ϕ is true, agent i starts to explicitly believe that ϕ is true.

The reason why we need to impose that ϕ and ψ are propositional formulas is that there are DLEK-formulas such as the Moore-like formula p∧¬Bip for which the previous four principles do not hold. For instance, the following formula is not valid:

[+(p ∧ ¬Bip)]Bi(p ∧ ¬Bip)
It is worth noting that in the logic DLEK we can 'simulate' in a dynamic way the rule of necessitation. Indeed:

|=DLEKϕ implies |=DLEK [+⊤]Biϕ (5)
We can also dynamically 'simulate' Axiom K for the explicit belief operator, in the case of propositional formulas. Let ϕ, ψ ∈ Prop. Then, we have the following validity:

|=DLEK(Biϕ ∧ Bi(ϕ → ψ)) → [∩(ϕ,ϕ → ψ)][⊢(ϕ ∧ ψ,ψ)]Biψ (6)

EXAMPLE

In this section we are going to illustrate our logic DLEK with the help of a concrete example. We are interested in describing the dynamics of explicit beliefs in a multi-agent scenario.

The scenario goes as follows. There are two robotic assistants, say robot A (Anne) and robot B (Bob), who have to take care of a person. The two robots are resource-bounded in the sense that they have background knowledge and (nonomniscient) explicit beliefs and form new explicit beliefs by means of the mental operations highlighted in Figure 1 in Section 2. The person communicates with the robots via a coloured electric light which can be either red or green. The communication code is the following one: (i) if the electric light is red (atom r) then it means that the person needs help (atom h), and (ii) if the electric is green (atom g) then it means that the person is having a rest and wants not to be bothered (atom b). We assume that: H1. robot A has full knowledge about the communication code as she knows that r implies h and that g implies b,

H2. robot B has only partial knowledge about the communication code as he knows that r implies h but he does not know that g implies b, and H3. robot A and robot B have common knowledge that they share a part of the communication code, namely that each of them knows that r implies h.

Thus, let us suppose that Agt = {A, B} and Atm = {r, g, h, b}. We represent the initial situation by the minimal LEK model satisfying the previous hypothesis H1, H2 and H3 and which only excludes the impossible situations in which the electric light is both red and green and the person needs help and takes a rest at the same time. This model is the tuple MR = (W, N, RA, RB, V ) (where MR stands for 'model of the robots') such that:

• W = {w1, w2, w3, w4, w5, w6, w7, w8, w9};

• N (i, w) = ∅ for all i ∈ Agt and for all w ∈ W ;

• the quotient set of W by RA is {{w1, w2, w3, w4, w5}, {w6, w7}, {w8, w9}};

• the quotient set of W by RB is {{w1, w2, w3, w4, w5, w6, w7}, {w8, w9}};

• V (w1) = {r, h} V (w2) = {h} V (w3) = {g, b} V (w4) = {b} V (w5) = ∅ V (w6) = {g} V (w7) = {g, h} V (w8) = {r} V (w9) = {r, b}.
The fact that N (i, w) = ∅ for all i ∈ Agt and for all w ∈ W just means that in the initial situation the robots do not have any explicit belief in their short-term memories.

Let us assume that w1 is the actual situation in which the electric light is red and the person needs help.

The first thing to observe is that in the actual situation the hypothesis H1 and H2 are both satisfied. Indeed, as for H1, we have:

MR, w1 |= KA(r → h) ∧ KA(g → b).
As for H2, we have:

MR, w1 |= KB(r → h) ∧ ¬KB(g → b).
In order to specify hypothesis H3, let EKJ ϕ be an abbreviation of i∈J Kiϕ, standing for "every agent in J has background knowledge that ϕ". Then, let us define EK k J ϕ by induction for every natural number k ∈ N:

EK 0 J ϕ def = ϕ
and for all k ≥ 1:

EK k J ϕ def = EKJ (EK k-1 J ϕ).
For every natural number n ∈ N, let MK n J ϕ be an abbreviation of 1≤k≤n EK k J ϕ. MK n J ϕ expresses J's background mutual knowledge that ϕ up to n iterations, i.e., everyone in J has background knowledge that ϕ, everyone in J has background knowledge that everyone in J has background knowledge that ϕ, and so on until level n. We omit the full definitions of the universal explicit belief operator EBJ (with EBJ ϕ standing for "every agent in J explicitly believes that ϕ") and of the mutual explicit belief operator MB n J (with MB n J ϕ standing for "the agents in J have mutual explicit belief that ϕ up to n iterations") since they can be defined exactly in the same way as the universal knowledge and mutual knowledge operators, starting from the individual explicit knowledge operators.

The previous hypothesis H3 holds in the initial situation since, for every n ∈ N, we have:

MR, w1 |= MK n {A,B} EK {A,B} (r → h).
Let us suppose that the person switches on the red light in order to signal to the two robots that she needs help. This event is represented by the mental operation +r which leads from model MR to the updated model MR +r = (W, N +r , RA, RB, V ) such that:

N +r (A, w1) = {{w1}}, N +r (A, w2) = {{w1}}, N +r (A, w3) = {{w1}}, N +r (A, w4) = {{w1}}, N +r (A, w5) = {{w1}}, N +r (A, w6) = ∅, N +r (A, w7) = ∅, N +r (A, w8) = {{w8, w9}}, N +r (A, w9) = {{w8, w9}}, N +r (B, w1) = {{w1}}, N +r (B, w2) = {{w1}}, N +r (B, w3) = {{w1}}, N +r (B, w4) = {{w1}}, N +r (B, w5) = {{w1}}, N +r (B, w6) = {{w1}}, N +r (B, w7) = {{w1}}, N +r (B, w8) = {{w8, w9}}, N +r (B, w9) = {{w8, w9}}.
It is easy to check that in the new situation, after the mental operation +r has been executed, the two robots explicitly believe that the light is red. That is: MR +r , w1 |= EB {A,B} r.

However, the mental operation is not sufficient to guarantee that the robots believe that the person needs helps. Indeed, we have:

MR +r , w1 |= ¬BAh ∧ ¬BBh.
It is by trying to infer that the person needs help from the fact that she switched on the red light, represented by ⊢(r,h), that the robots can form this explicit belief. The mental operation ⊢(r,h) leads from model MR +r to the updated model (MR +r ) ⊢(r,h) = (W, (N +r ) ⊢(r,h) , RA, RB, V ) such that:

(N +r ) ⊢(r,h) (A, w1) = {{w1}, {w1, w2}},

(N +r ) ⊢(r,h) (A, w2) = {{w1}, {w1, w2}}, (N +r ) ⊢(r,h) (A, w3) = {{w1}, {w1, w2}}, (N +r ) ⊢(r,h) (A, w4) = {{w1}, {w1, w2}}, (N +r ) ⊢(r,h) (A, w5) = {{w1}, {w1, w2}}, (N +r ) ⊢(r,h) (A, w6) = {∅}, (N +r ) ⊢(r,h) (A, w7) = {∅}, (N +r ) ⊢(r,h) (A, w8) = {{w8, w9}}, (N +r ) ⊢(r,h) (A, w9) = {{w8, w9}}, (N +r ) ⊢(r,h) (B, w1) = {{w1}, {w1, w2, w7}}, (N +r ) ⊢(r,h) (B, w2) = {{w1}, {w1, w2, w7}}, (N +r ) ⊢(r,h) (B, w3) = {{w1}, {w1, w2, w7}}, (N +r ) ⊢(r,h) (B, w4) = {{w1}, {w1, w2, w7}}, (N +r ) ⊢(r,h) (B, w5) = {{w1}, {w1, w2, w7}}, (N +r ) ⊢(r,h) (B, w6) = {{w1}, {w1, w2, w7}}, (N +r ) ⊢(r,h) (B, w7) = {{w1}, {w1, w2, w7}}, (N +r ) ⊢(r,h) (B, w8) = {{w8, w9}}, (N +r ) ⊢(r,h) (B, w9) = {{w8, w9}}.
It is easy to check that in the new situation, after the mental operation ⊢ (r,h) has been executed, the two robots explicitly believe that the person needs help. That is:

(MR +r ) ⊢(r,h) , w1 |= EB {A,B} h.

To sum up, we have the following which holds:

MR, w1 |= [+r]EB {A,B} r ∧ [+r](¬BAh ∧ ¬BBh)∧ [+r][⊢(r,h)]EB {A,B} h.
It is worth noting that the sequence of the two mental operations +r and ⊢(r,h) is not sufficient for the robots to acquire the explicit common belief that the person needs help. Indeed, it is to check that the following holds:

(MR +r ) ⊢(r,h) , w1 |= ¬BABBh ∧ ¬BBBAh.
In order to obtain such explicit common belief, the two robots need to perform the two additional mental operations ⊢(h,BAh) and ⊢(h,BBh) (i.e., trying to infer that robot A/robot B explicitly believes that h from the fact that h holds), no matter the order in which they are executed. Indeed, for every n ∈ N, we have:

MR, w1 |= [+r][⊢(r,h)][⊢(r,BAh)][⊢(r,BBh)]MB n {A,B} h, MR, w1 |= [+r][⊢(r,h)][⊢(r,BBh)][⊢(r,BAh)]MB n
{A,B} h. It is just routine to check that the mental operations +g and ⊢(g,b) are also sufficient for robot A to start to believe b explicitly after performing them, but they are not sufficient for robot B since he does not have background knowledge that g implies b. In formal terms, we have:

MR, w1 |= [+g][⊢(g,b)]BAb, MR, w1 |= [+g][⊢(g,b)]¬BBb.

AXIOMATIZATION

Let us now present sound and complete axiomatizations for the logic LEK and its dynamic extension DLEK. Definition 3. We define LEK to be the extension of classical propositional logic given by the following rules and axioms:

(Kiϕ ∧ Ki(ϕ → ψ)) → Kiψ (K K i ) Kiϕ → ϕ (T K i ) Kiϕ → KiKiϕ (4 K i ) ¬Kiϕ → Ki¬Kiϕ (5 K i ) (Biϕ ∧ Ki(ϕ ↔ ψ)) → Biψ (Mix1 K i ,B i ) Biϕ → KiBiϕ (Mix2 K i ,B i ) ϕ Kiϕ (Nec K i )
The axiomatics of the logic DLEK includes all principles of the logic LEK plus a set of reduction axioms and the rule of replacement of equivalents. Definition 4. We define DLEK to be the extension of LEK generated by the following axioms:

[α]p ↔p (Redp) [α]¬ϕ ↔¬[α]ϕ (Red¬) [α](ϕ ∧ ψ) ↔([α]ϕ ∧ [α]ψ) (Red∧) [α]Kiϕ ↔Ki[α]ϕ (Red K i ) [+ϕ]Biψ ↔(Bi[+ϕ]ψ ∨ Ki([+ϕ]ψ ↔ ϕ)) (Red B i ,+ ) [-ϕ]Biψ ↔(Bi[-ϕ]ψ ∨ ¬Ki([-ϕ]ψ ↔ ϕ)) (Red B i ,-) [⊢(ϕ,ψ)]Biχ ↔ Bi[⊢(ϕ,ψ)]χ∨ (Biϕ ∧ Ki(ϕ → ψ))∧ Ki([⊢(ϕ,ψ)]χ ↔ ψ) (Red B i ,⊢ ) [∩(ϕ,ψ)]Biχ ↔ Bi[∩(ϕ,ψ)]χ∨ (Biϕ ∧ Biψ)∧ Ki([∩(ϕ,ψ)]χ ↔ (ϕ ∧ ψ)) (Red B i ,∩ )
and the following rule of inference:

ψ1 ↔ ψ2 ϕ ↔ ϕ[ψ1/ψ2] (RRE)
We write DLEK ⊢ ϕ to denote the fact that ϕ is a theorem of DLEK.

It is straightforward to check that all axioms are valid and all rules preserve validity in the class of DLEK-models, from which the following is an immediate consequence: Lemma 1. The logics LEK and DLEK are sound for the class of LEK-models.

Our goal now is to prove that LEK is strongly complete for its intended semantics. We will achieve this by a fairly standard canonical-model argument, although the neighborhood structure will require some care. where:

• Wc is the set of all maximal consistent subsets of LLEK.

• wRciv if and only if, for all formulas ϕ and all agents i, Kiϕ ∈ w if and only if Kiϕ ∈ v.

• In order to define Nc, for w ∈ W and ϕ ∈ LLEK, first define

Aϕ(i, w) = {v ∈ Ri(w) : ϕ ∈ v}.
Then, define Nc by letting Nc(i, w) = {Aϕ(i, w) : Biϕ ∈ w}.

• Finally, we define the valuation Vc by w ∈ Vc(p) if and only if p ∈ w.

The following is standard and we omit the proof:

Lemma 2. The structure Mc defined above is a LLEK-model. Moreover, if w ∈ Wc and ϕ ∈ LLEK, then 1. Kiϕ ∈ w if and only if, for every v such that wRciv, ϕ ∈ v, and 2. if wRciv and Biϕ ∈ w, then Biϕ ∈ v.

We also need to prove that Mc has a somewhat less familiar property. This will be used later in the truth lemma, for the case of Bi. Lemma 3. For every w ∈ Wc and Biϕ, Biψ ∈ LLEK, if Biϕ ∈ w but Biψ ∈ w, it follows that there is v ∈ Rci(w) such that either ϕ ∈ v but ¬ψ ∈ v, or ¬ϕ ∈ v but ψ ∈ v.

Proof. Let w ∈ Wc and ϕ, ψ be such that Biϕ ∈ w, Biψ ∈ w. Towards a contradiction, assume that for every v ∈ Rci(w), either ϕ, ψ ∈ v or ¬ϕ, ¬ψ ∈ v; then, it follows from Lemma 2 that Ki(ϕ ↔ ψ) ∈ w, so that by Axiom (Mix1 K i ,B i ), Biψ ∈ w, contrary to our assumption.

With this, we may state and prove our version of the Truth Lemma: Proof. The proof proceeds by a standard induction on the construction of ϕ. All cases are routine except ϕ = Biψ.

First assume that Biψ ∈ w. Then, A ψ (i, w) ∈ Nc(i, w). But,

A ψ (i, w) = {v ∈ Ri(w) : ψ ∈ v} IH = ψ ∩ Ri(w). Thus, Mc, w |= Biψ.
Now, suppose Biψ ∈ w, so that ¬Biψ ∈ w. We must check that ψ ∩ Rci(w) ∈ N (i, w). Choose an arbitrary set A ∈ N (i, w); by definition, A = A θ (i, w) for some θ with Biθ ∈ w. By Lemma 3, there is some v ∈ Ri(w) such that ψ, ¬θ ∈ v or ¬ψ, θ ∈ v; in the first case, this shows using the induction hypothesis that v ∈ ( ψ ∩ Ri(w)) \ A θ (i, w), while in the second we obtain v ∈ A θ (i, w)\( ψ ∩Ri(w)). In either case we obtain A θ (i, w) = ψ ∩ Ri(w), and since A = A θ (i, w) was an arbitrary element of N (i, w), we conclude that ψ ∩ Ri(w) ∈ N (i, w) and thus Mc, w |= Biψ.

We are now ready to prove that the static LEK is strongly complete.

Theorem 1. LEK is strongly complete for the class of LEK models.

Proof. Any consistent set of formulas Φ may be extended to a maximal consistent set of formulas w * ∈ Wc, and Mc, w * |= Φ by Lemma 4.

The strong completeness of DLEK follows from this result, in view of the fact that the reduction axioms may be used to find, for any DLEK formula, a provably equivalent LEK formula.

Lemma 5. If ϕ is any formula of LDLEK, there is a formula ϕ in LLEK such that DLEK ⊢ ϕ ↔ ϕ.

Proof. This follows by a routine induction on ϕ using the reduction axioms and the rule of replacement of equivalents (RRE) from Definition 4.

As a corollary, we get the following: Theorem 2. DLEK is strongly complete for the class of LEK models.

Proof. If Γ is a consistent set of LDLEK formulas, then Γ = { ϕ : ϕ ∈ Γ} is a consistent set of LLEK formulas (since DLEK is an extension of LEK), and hence by Theorem 1, there is a model M with a world w such that M, w |= Γ. But, since DLEK is sound and for each ϕ ∈ Γ, DLEK ⊢ ϕ ↔ ϕ, it follows that M, w |= Γ.

Thus our logics are strongly complete, but the construction we have given will in general produce infinite models. In the next section, we are going move from axiomatics to complexity of the satisfiability problem.

COMPLEXITY

In this section we will study the computability of the satisfiability problem of LEK: given a formula ϕ, determine whether ϕ is satisfiable. We will also provide a decidability result of the satisfiability problem of DLEK. We first consider the single-agent case and move then to the multi-agent case. Below, card(A) denotes the cardinality of the set A. For all j ∈ B+ , let Aj ∈ N be such that Aj = {v ∈ W : M, v |= χj}. Such Aj exists because M, w |= Bχj. For all j ∈ B+ and for all k ∈ B-, let u j,k ∈ W be such that M, u j,k |= χj ↔ χ k . Such u j,k exists because M, w |= Bχj and M, w |= Bχ k . Let M ′ = (W ′ , N ′ , V ′ ) be the model defined as follows:

Mono-agent case

• W ′ = {w} ∪ {vi : i ∈ K} ∪ {u j,k : j ∈ B+ & k ∈ B-}, • N ′ = {Aj ∩ W ′ : j ∈ B+ }, • for all p ∈ V AR, V ′ (p) = V (p) ∩ W ′ .
Obviously, card(W ′ ) and card(N ′ ) are polynomial in the size of ϕ. Let Φ be the closure under single negations of the set of all ϕ's subformulas. Proof. Membership in NP follows from Lemma 6. NPhardness follows from the NP-hardness of classical propositional logic.

Multi-agent case

Our study of the computability in the multi-agent case will be based on the modal tableaux approach developed by Halpern and Moses [START_REF] Halpern | A guide to completeness and complexity for modal logics of knowledge and belief[END_REF]. Assume card(Agt) ≥ 2. For all formulas ϕ, let SF (ϕ) be the closure under single negations of the set of all subformulas of ϕ.

Modal tableaux.

A set T of formulas is said to be fully expanded if for all formulas ϕ, if ϕ ∈ T then for all formulas ψ, if ψ ∈ SF (ϕ) then either ψ ∈ T , or ¬ψ ∈ T , SF (ϕ) denoting the closure under single negations of the set of all ϕ's subformulas. A propositional tableau is a set T of formulas such that the following conditions holds: (i) for all formulas ϕ, if ¬¬ϕ ∈ T then ϕ ∈ T ; (ii) for all formulas ϕ, ψ, if ¬(ϕ ∨ ψ) ∈ T then ¬ϕ ∈ T and ¬ψ ∈ T ; (iii) for all formulas ϕ, ψ, if ϕ ∨ ψ ∈ T then either ϕ ∈ T , or ψ ∈ T . A propositional tableau T is said to be blatantly consistent iff for all formulas ϕ, either ϕ ∈ T , or ¬ϕ ∈ T .

A modal tableau is a structure of the form T = (W, R, L) where W is a nonempty set of states (with typical members denoted w, v, etc), R is a function associating a binary relation Ri on W to each i ∈ Agt and L is a function assigning to each w ∈ W a blatantly consistent and fully expanded propositional tableau L(w) such that for all w ∈ W , the following conditions holds: (i) for all formulas ϕ, if ¬Kiϕ ∈ L(w) then there exists v ∈ Ri(w) such that ¬ϕ ∈ L(v); (ii) for all formulas ϕ, if Biϕ ∈ L(w) then for all formulas ψ, if ¬Biψ ∈ L(w) then there exists v ∈ Ri(w) such that either ϕ ∈ L(v) and ¬ψ ∈ L(v), or ¬ϕ ∈ L(v) and ψ ∈ L(v); (iii) for all formulas ϕ, if

Kiϕ ∈ L(w) then for all v ∈ (Ri ∪ R -1 i ) ⋆ (w), ϕ ∈ L(v) and Kiϕ ∈ L(v); (iv) for all formulas ϕ, if Biϕ ∈ L(w) then for all v ∈ (Ri ∪ R -1 i ) ⋆ (w), Biϕ ∈ L(v). For all formulas ϕ, let L -1 (ϕ) = {w : w ∈ W & ϕ ∈ L(w)}. We shall say that a modal tableau T = (W, R, L) is a modal tableau for a formula ϕ if L -1 (ϕ) = ∅.
From models to modal tableaux.

Given a model M = (W, R, N, V ), let T ′ = (W ′ , R ′ , L ′ ) be defined as follows: W ′ = W , R ′ i = Ri for each i ∈ Agt, L ′ is the function assigning to each w ∈ W ′ the propositional tableau L ′ (w) = {ϕ : M, w |= ϕ}. The proof that T ′ is a modal tableau is easy. As a result, Proposition 1. Let ϕ be a formula. If ϕ is satisfiable then there exists a modal tableau for ϕ.

From modal tableaux to models.

Given a modal tableau T = (W, R, L), let

M ′ = (W ′ , R ′ , N ′ , V ′ )
be defined as follows:

W ′ = W , R ′ i = (Ri ∪ R -1 i ) ⋆ for each i ∈ Agt, N ′ i (w) = {(Ri ∪ R -1 i ) ⋆ (w) ∩ L -1 (
ϕ) : Biϕ ∈ L(w)} for each w ∈ W and for each i ∈ Agt, V ′ is the function assigning to each p ∈ Atm the subset V ′ (p) = {w : w ∈ W & p ∈ L(w)} of W ′ . The proof that T ′ is a model is easy. Moreover, one can prove by induction on ϕ that for all w ∈ W , ϕ ∈ L(s) iff M ′ , s |= ϕ. As a result, Proposition 2. Let ϕ be a formula. If there exists a modal tableau for ϕ then ϕ is satisfiable.

Membership in PSPACE.

By Propositions 1 and 2, satisfiability is reducible to the following decision problem (MT): given a formula ϕ, determine whether there exists a modal tableau for ϕ. Based on the tools and techniques developed in ordinary epistemic logics by Halpern and Moses [START_REF] Halpern | A guide to completeness and complexity for modal logics of knowledge and belief[END_REF], one can design an algorithm that tries to construct a modal tableau for a given formula ϕ. The main properties of such algorithm are:

• For all given formulas ϕ, the above algorithm terminates and runs in polynomial space,

• for all given formulas ϕ, the algorithm returns "there is a modal tableau for ϕ" iff there is a modal tableau for ϕ.

Proposition 3. There is an algorithm for deciding satisfiability that runs in polynomial space.

As a result, Theorem 4. If card (Agt) ≥ 2 then satisfiability problem of LEK is PSPACE-complete.

Proof. Membership in PSPACE follows from the above discussion. PSPACE-hardness follows from the PSPACEhardness of multi-agent epistemic logic.

The reduction axioms and the rule of replacement of equivalents in Definition 4 may then be used to give a decision procedure for the satisfiability of DLEK; however, due to exponential blow-up in the size of formulas, this algorithm would no longer remain in PSPACE without modification. Thus we will state only the following: Corollary 1. The satisfiability problem of DLEK is decidable.

Proof. Immediate from the decidability of LEK and the fact that, given a formula ϕ of LDLEK, the formula ϕ is clearly computable from ϕ. However, we do not believe that such a procedure would be optimal, and indeed conjecture that DLEK is in PSPACE. We leave the computation of its precise complexity for future work.

CONCLUSION

Let's take stock. In the paper we have introduced DLEK, a logical theory of belief dynamics for resource-bounded agents inspired by existing psychological theories of human memory. We have provided decidability and complexity results for DLEK as well as for its static fragment LEK.

Directions of future research are manifold. On the conceptual level, we plan to complete the conceptual framework described in Section 2 by extending the family of mental operations with operations of storage of information in longterm memory. We believe that these kinds of operations can be modelled as special kinds of epistemic actions in the DEL sense. Specifically, a storage operation modifies an agent's background knowledge by restricting the epistemic relation Ri to worlds in which the information ϕ to be stored is true, under the condition that this information is already available in the agent's working memory and explicitly believed by the agent.

On the technical level, as emphasized in Section 6, we plan to obtain a result about complexity of the satisfiability problem of DLEK. In particular, we plan to prove that this problem is PSPACE-complete by appropriately adapting to our framework the technique proposed by Lutz [START_REF] Lutz | Complexity and Succinctness of Public Announcement Logic[END_REF] for studying complexity of the satisfiability problem of public announcement logic (PAL). We also plan to refine our approach by relaxing the assumption that mental operations are performed by all agents and that this is a public fact. To this aim, we will have to introduce a notion of action model in this sense of [START_REF] Baltag | Logics for Epistemic Programs[END_REF] which allows us to model a private form of mental operation (i.e., an operation which occurs in the mind of a specific agent without the other agents being aware of this).

Figure 1 :

 1 Figure 1: Cognitive view of the relationship between background knowledge and explicit beliefs

Definition 5 (

 5 canonical LEK model). We define the canonical LEK model Mc = (Wc, Nc, Rc1 . . . , Rcn, Vc)

Lemma 4 .

 4 For every ϕ ∈ LLEK and every w ∈ Wc, ϕ ∈ w if and only if Mc, w |= ϕ.

Firstly, assume

  card(Agt) = 1. Let ϕ be a satisfiable formula. Let M = (W, N, V ) be a model and w ∈ W be such that M, w |= ϕ. Let Kψ1, . . . , Kψm and Bχ1, . . . , Bχn be lists of the set of all subformulas of ϕ of the form Kψ and Bχ.Let K = {i : 1 ≤ i ≤ m & M, w |= Kψi}, B+ = {j : 1 ≤ j ≤ n & M, w |= Bχj} and B-= {k : 1 ≤ k ≤ n & M, w |= Bχ k }.For all i ∈ K, let vi ∈ W be such that M, vi |= ψi. Such vi exists because M, w |= Kψi.

Lemma 6 .Theorem 3 .

 63 Let ϕ be a formula. If ϕ ∈ Φ then for all s ∈ W ′ , M, s |= ϕ iff M ′ , s |= ϕ.Proof. By induction on ϕ. We only consider the cases ϕ = Bχ. Suppose M, s |= Bχ and M ′ , s |= Bχ. Let j ∈ B+ be such that Bχ = Bχj. Hence,Aj = {t ∈ W : M, t |= χ}. By induction hypothesis, Aj ∩ W ′ = {t ∈ W ′ : M ′ , t |= χ}. Thus, M ′ , s |= Bχ: a contradiction. Suppose M ′ , s |= Bχ and M, s |= Bχ. Let j ∈ B+ be such that Aj ∩ W ′ = {t ∈ W ′ : M ′ , t |= χ}. By induction hypothesis, Aj ∩ W ′ = {t ∈ W ′ : M, t |= χ}. Let k ∈ Bbe such that Bχ = Bχ k . Remember that Aj = {t ∈ W : M, t |= χj}. Moreover, u j,k ∈ W ′ is such that M, u j,k |= χj and M, u j,k |= χ k , or M, u j,k |= χj and M, u j,k |= χ k .In the former case, u j,k ∈ Aj ∩ W ′ . Hence, M, u j,k |= χ: a contradiction. In the latter case, u j,k ∈ Aj ∩ W ′ . Thus, M, u j,k |= χj: a contradiction. If card (Agt) = 1 then satisfiability problem of LEK is NP-complete.

In the Soar architecture[START_REF] Laird | The Soar Cognitive Architecture[END_REF] these two kinds of background are called, respectively, episodic memory and semantic memory.

2 Some psychologists (e.g.,[START_REF] Cowan | An embedded process model of working memory[END_REF]) distinguish focus of attention from working memory, as they assume that there might be information activated in working memory which is not under the focus of the agent's attention. For simplicity, we here assume that focus of attention and working memory are coextensive.


Matthieu Arzel
email: matthieu.arzel@enst-bretagne.fr

Cyril Lahuec

Michel Jezequel

Fabrice Seguin

Michel J Éz Équel

Analogue decoding of duo-binary codes

INTRODUCTION

In telecommunication receivers many tasks which were performed by analogue circuits are now mostly being performed by digital ones. However, powerful error correcting techniques such as turbo decoding use continuous values which suggests that analogue circuits have yet to offer many advantages for such a type of integrated function. The first analogue solutions for this particular application were proposed by European laboratories [START_REF] Hagenauer | Der analoge Decoder[END_REF][START_REF] Moerz | An analog 0.25µm BiCMOS tailbiting MAP decoder[END_REF][START_REF] Lustenberger | An analog VLSI decoding technique for digital codes[END_REF] and were implemented using either BiC-MOS or CMOS processes. These works have not only proved the validity of the concepts but have also shown significant gains in terms of speed, power consumption and silicon area over digital solutions [START_REF] Moerz | An analog 0.25µm BiCMOS tailbiting MAP decoder[END_REF][START_REF] Lustenberger | An analog VLSI decoding technique for digital codes[END_REF][START_REF] Winstead | CMOS analog MAP decoder for (8,4) hamming code[END_REF]. However, none of the decoders presented in [START_REF] Moerz | An analog 0.25µm BiCMOS tailbiting MAP decoder[END_REF][START_REF] Lustenberger | An analog VLSI decoding technique for digital codes[END_REF][START_REF] Winstead | CMOS analog MAP decoder for (8,4) hamming code[END_REF] were developed for an industrial application, only simple short codes were used. A first design for an industrial standard -the Universal Mobile Telecommunication System (UMTS) -is presented in [START_REF] Amat | A full CMOS analog turbo decoder for UMTS coding schemes[END_REF]. This paper points out the fact that it is now crucial to apply the analogue technique to other standards to certify the industrial viability of analogue decoding. This is what this work aims to do. This article highlights the principles and results of the analogue decoding simulations of the duobinary codes that were chosen for the recent standard Digital Video Broadcasting -Return Channel via Satellite (DVB-RCS) of the European Telecommunications Standard Institute (ETSI) [START_REF]Interaction channel for satellite distribution systems[END_REF]. In the first section, the principles of duo-binary convolutional codes are outlined. The BiCMOS design of an analogue decoder and simulation results are then presented. Finally, the design of a complete analogue DVB-RCS turbo decoder is raised.

PRINCIPLES AND ADVANTAGES OF DUO-BINARY CONVOLUTIONAL CODES

The DVB-RCS standard has adopted a duo-binary Convolutional Recursive Systematic Circular turbo code. This type of code does not treat bits individually but in couples. The elementary DVB-RCS convolutional encoder (Fig. 1) produces two parity bits for each duo-binary input symbol. A trellis section of this code is illustrated in Fig. 2. Compared to a trellis section of a binary code, the number of branches is doubled but the length is halved since a section treats a two-bit symbol rather than a one-bit symbol. Such a code has major advantages compared to its binary counterparts. Berrou et al. [START_REF] Berrou | The advantages of non-binary turbo-codes[END_REF] showed that the convergence of m-ary turbo codes is better but the gain is less noticeable for m > 2. Their minimal distances and their asymptotic gains are larger. They are also less sensitive to puncturing. These advantages make duo-binary turbo codes key candidates for many other telecommunications standards.

DESIGN OF AN ANALOGUE DECODER IN A BICMOS TECHNOLOGY

A convolutional circular binary code can be decoded with the Maximum A Posteriori (MAP) algorithm [START_REF] Anderson | Tailbiting MAP decoders[END_REF]. It uses only two mathematical operators (addition and multiplication) and two functions (logarithm and exponential). The last two are necessary for converting loglikelihood ratios (LLR) to probabilities and vice-versa. If X is a binary random variable and x its outcome, the LLR of X, L(X), is defined by:

L(X) = ln P X (x = 1) P X (x = 0) (1)
The exponential and the natural logarithm functions are readily available from a bipolar junction transistor (BJT) working in the forward active region. The collector current I C depends on the base-emitter voltage V BE :

I C ≈ I S e V BE V T (2)
where I S is the saturation current and V T is the thermal voltage. When diode connected, the BJT produces

Β Α Dec Γ Extr PSfrag replacements L " X i 1 " L " X i 2 " L " Y i " L " W i " L X i eIN α i+1 α i β i+1 β i d i 1 d i 2 L(X i eOU T )
Figure 3: Analogue circular MAP decoder. Each section is made up of modules defined by the MAP algorithm. There are as many sections as symbols to decode.

a voltage V which depends on the current I flowing through it:

V ≈ V T ln I I S (3)
Associating a current with a probability and a voltage with an LLR, it is thus possible by using transistors and diodes to convert LLRs to probabilities, equation [START_REF] Moerz | An analog 0.25µm BiCMOS tailbiting MAP decoder[END_REF], and probabilities to LLRs, equation [START_REF] Lustenberger | An analog VLSI decoding technique for digital codes[END_REF], respectively. This is a clear advantage of analogue decoders over digital decoders since currents, representing the probabilities, can be easily added and multiplied. Thus, the MAP algorithm can be implemented using a BJT-based analogue network [START_REF] Moerz | An analog 0.25µm BiCMOS tailbiting MAP decoder[END_REF]. The frame is decoded by letting this network converge to a stable state. The on-chip network is the direct mapping of the MAP algorithm. It is divided into as many sections as duo-binary symbols to be decoded (see Fig. 3).

Each section is built from four modules: a Γ module to compute the branch metrics, an A module for the forward metrics, a B module for the backward metrics and a Dec module to decide on the value of the duo-binary symbol. There are two sets of inputs to the section. The first set is the data produced by the channel, L(X i 1 ) L(X i 2 ) L(Y i ) L(W i ), which are associated with the i th symbol X i 1 X i 2 and its parity bits Y i and W i . The second set of inputs is composed of the forward and backward metrics α i and β i+1 produced by the adjacent trellis sections. The outputs are the metrics α i+1 and β i , fed to the adjacent sections, and the decisions d i 1 d i 2 for the transmitted symbol X i 1 X i 2 . A fifth module is required if the MAP decoder is part of a turbo decoder: the Extr module. This module computes the extrinsic information L(X i eOU T ) which is then used by the Γ module of the second MAP decoder as the input L(X i eIN ). All the modules are connected in a voltage mode. Each module, except the Dec one, is divided into a computing BJT-based core and two MOS interface circuits. The BJT-based core is an analogue multiplier: the well-known Gilbert cell [START_REF] Moerz | An analog 0.25µm BiCMOS tailbiting MAP decoder[END_REF]. Designed for two differential inputs, this cell is adapted for treating binary symbols. However, it can be extended to m-ary symbols. The complexity of the extended structures grows geometrically with m. The A module is taken as an example to illustrate this growth in Fig. 4. Considering the duo-binary trellis section shown in Fig. 2, there are eight possible states per section. Let α i (s) be the forward metric associated with a state s of the i th section. Let γ i (s , s) be the metric of the branch between a state s of the i th section and a state s of the (i + 1) th section of the trellis. Applying the MAP algorithm to a trellis of length k, the eight forward metrics of each section i between 0 and k -1 are computed using:

V α 0,1 i-1 V α 0,7 i-1 V γ 0,1 i V γ 0,7 i V α 0,7 i V α 0,1 i
α i+1 (s) = 7 s =0 α i (s )γ i (s , s) (4)
For a duo-binary convolutional code of rate 2/3 with eight states (only one parity bit is produced per each quaternary symbol) the branch metrics can take eight values (16 for a code of rate 1/2 as illustrated in Fig. 2). The A module requires the design of an extended Gilbert structure with 8-ary inputs (Fig. 4). The bipolar transistors produce the product of probabilities, supplied by the LLR-voltages, and return the results as currents. Consequently, if the multiplication core requires only 6 transistors in the binary case, it uses 72 transistors in the 8-ary case.

RESULTS AND COMPARISONS

Running behavioural simulations using Simulink validated an analogue MAP architecture for decoding frames of 24 duo-binary symbols. The encoding uses the DVB-RCS elementary convolutional code. The modelled decoder was then designed for a 0.25µm Philips SiGe process. Electrical simulations proved its ability to correct errors: frames altered by a gaussian noise were successfully decoded as predicted by behavioural simulations. Fig. 5 shows that the circuit's state converges to a solution and finally distinguishes the probabilities associated with the four possible values of a received duo-binary symbol. The lower the voltage, the higher the probability of the corresponding value. In this case, the hard decision at the channel output (not illustrated) is 10, which is an error, whereas the analogue decoder converges to the correct value 00.

The decoding capability was tested using several frames altered by a gaussian noise with different signal to noise ratios. The outputs were corrected and sampled after a minimal time of 80ns. This figure gives an estimated decoding speed of 600Mbit/s. Since the circuit is a direct mapping of the MAP trellis, the power consumption must be considered with respect to the length of the coding frame and the number of states of the code. The criterion to consider is the power per information bit and code state. From simulations, the proposed decoder consumes 1.4mW per information bit and code state. This result compares well with what was obtained with the decoder described in [START_REF] Moerz | An analog 0.25µm BiCMOS tailbiting MAP decoder[END_REF] which consumes 1.2mW per information bit and code state. This decoder treats frames of 16 binary symbols, among which eight are information bits (rate 1/2) coded on two states. The circuit presented in this paper decodes frames of 24 duo-binary information symbols coded on eight states, representing 72 bits. Fig. The lower the voltage, the higher the probability. As can be seen, at the beginning, it is not possible to distinguish which is the correct symbol since symbol 00 and 10 have the same probability.

shows that the complexity of the modules grows geometrically with the number of states, that is four times more than in [START_REF] Moerz | An analog 0.25µm BiCMOS tailbiting MAP decoder[END_REF]. It also shows that the complexity grows geometrically with the number of bits per symbol, that is twice as many as in [START_REF] Moerz | An analog 0.25µm BiCMOS tailbiting MAP decoder[END_REF]. However, the power consumptions per information bit and code state are similar. There are two reasons for this result. First, the bias current of the extended Gilbert cells does not grow proportionally to their size. Next, the duo-binary decoder needs only one parity bit per two information bits whereas the decoder in [START_REF] Moerz | An analog 0.25µm BiCMOS tailbiting MAP decoder[END_REF] uses one parity bit per information bit. As the decoder's need for power depends on the number of bits treated (whether they are: parity or information bits), implementing a code with a minimal rate reduces the power consumption per information bit. These results can also be compared to those obtained by the eight-state analogue turbo decoder presented in [START_REF] Amat | A full CMOS analog turbo decoder for UMTS coding schemes[END_REF] which is designed for a CMOS process. [START_REF] Amat | A full CMOS analog turbo decoder for UMTS coding schemes[END_REF] uses MOS transistors biased in the subthreshold region resulting in a low power consumption (21µW per information bit and state) at the expense of data throughput (only 2Mbit/s).

TOWARDS A TURBO DECODER FOR THE DVB-RCS STANDARD

A turbo decoder can be designed by reusing the described elementary MAP decoder in order to decode the smallest frame of the DVB-RCS standard (48 symbols). This complete turbo decoder was simulated using a high-level model. Fig. 6 shows that the analogue decoding has a gain of 0.1dB, for a bit error rate of 10 -4 , compared to an optimal digital version. The digital equivalent circuit uses floating point number representation and runs for 15 iterations, which provides maximum iterative performance. The analogue model performs better because it benefits from continuous time: there is no iteration but a permanent sharing of extrinsic information. The ability of the analogue decoder to use "soft" time enhances its error correcting performance.

CONCLUSION

An analogue MAP decoder for the DVB-RCS standard has been designed by extending the basic concepts of BiCMOS analogue decoding. As this standard is based on a duo-binary 8-state convolutional code, the extended Gilbert cells reach a complexity that had not yet been studied for a an analogue decoder. The decoding of 24 duo-binary symbols frames was simulated at a transistor level. It provides a sufficient accuracy to enable error correction. Moreover, the power consumption per information bit and per state is 1.4mW per information bit and state, which is similar to that of a reference circuit [START_REF] Moerz | An analog 0.25µm BiCMOS tailbiting MAP decoder[END_REF]. The decoding speed is estimated at 600Mbit/s.

The DVB-RCS decoder is a turbo decoder which was simulated at a behavioural level for the smallest frame length of the standard. The analogue decoding outperforms its digital counterpart by 0.1dB at a BER of 10 -4 . This decoder benefits from the continuous exchange of extrinsic information for better convergence.

Figure 1 : 8 -

 18 Figure 1: 8-state duo-binary encoder for DVB-RCS standard. Depending on the code rate, each two-bit symbol X 1 X 2 is associated with either one or two redundant bits, Y and W.

Figure 2 :

 2 Figure 2: Trellis associated with the encoder of Fig. 1. The branches are labelled with the encoded symbol X 1 X 2 Y W . Y and W are transmitted for a coding rate of 1/2 whereas only Y is used for a coding rate of 2/3 .

Figure 4 :

 4 Figure 4: Extended Gilbert cell to compute the state metrics. The differential input voltages represent the LLRs.

4

 4

Figure 5 :

 5 Figure5: Correction of an error. The four voltages represent the four log-probabilities associated with the quaternary symbol. The lower the voltage, the higher the probability. As can be seen, at the beginning, it is not possible to distinguish which is the correct symbol since symbol 00 and 10 have the same probability.

Figure 6 :

 6 Figure 6: Bit and frame error rate curves for DVB-RCS frames of 48 duo-binary symbols. Optimal analogue and digital turbo decodings are compared on a channel with an additive white gaussian noise (AWGN).


Daniela Schmidt
email: daniela.schmidt@acad.pucrs.br

Cassia Trojahn
email: cassia.trojahn@irit.fr

Renata Vieira
email: renata.vieira@pucrs.br

Mouna Kamel
email: mouna.kamel@irit.fr

Validating Top-level and Domain Ontology Alignments using WordNet

Keywords:

Matching domain and top-level ontologies is an important task but

still an open problem in the ontology matching field, particularly due to their different levels of abstraction. Beyond that, validating candidate alignments is crucial before exploiting them within ontology construction and integration processes involving such kinds of ontologies. This paper concerns the automatic validation of candidate alignments between top and domain ontologies, exploiting WordNet background knowledge. We apply our approach for validating alignments generated by a set of matching tools and discuss the results against manual validation. Our experiments are based on one domain ontology and three well-known top-level ontologies.

Introduction

According to their "level of generality", ontologies can be classified in different categories [START_REF] Guarino | Formal Ontology in Information Systems[END_REF]]. Top-level ontologies describe very general concepts (e.g., space, time, object, etc.), which are independent of a particular domain, and are usually equipped with a rich axiomatic layer; domain ontologies describe the entities related to a domain (e.g., biology or aeronautic). While the rich semantics and formalization of top-level ontologies are important requirements for ontology building [START_REF] Mika | Foundations for Service Ontologies: Aligning OWL-S to Dolce[END_REF], they act as well as semantic bridges supporting very broad semantic interoperability between domain ontologies [START_REF] Mascardi | Automatic Ontology Matching via Upper Ontologies: A Systematic Evaluation[END_REF]. For grounding domain concepts, one is required to find relationships with concepts from a top-level ontology, i.e., to match them.

There have been many proposals to the matching task in the literature [START_REF] Euzenat | Ontology Matching[END_REF], which exploit in different ways the knowledge encoded within each ontology when identifying correspondences between their features or structures. However, most efforts have been particularly dedicated to domain ontologies and the problem of matching domain and top-level ontologies has been addressed to a lesser extent. Matching domain and top-level ontologies poses different challenges, in particular due to their different levels of abstraction. This is a complex task, even manually, that requires to deeply identify the semantic context of concepts. It involves going beyond the frontiers of the knowledge encoded in the ontologies and, in particular, the identification of subsumption relations. The latter is in fact largely neglect by most matchers. Beyond that, the validation of alignments is a crucial step before exploiting them within ontology building and integration processes. While manual validation is a time-consuming task requiring expert judges, automatic ones generally rely on gold standards, which are not always available or may suffer of imperfections or low coverage. Exploiting background knowledge can be an alternative. However, knowledge on top level ontologies is highly specialized and requires resources covering different levels of abstraction. This paper concerns the automatic validation of candidate alignments between top-level and domain ontologies, relying on background knowledge from WordNet [START_REF] Miller | WordNet: A Lexical Database for English[END_REF]] and on the notion of context, which has been exploited in different ways in ontology matching [START_REF] Maedche | Measuring Similarity between Ontologies[END_REF][START_REF] Wang | Lily Results on SEALS Platform for OAEI 2011[END_REF][START_REF] Schadd | Coupling of Wordnet Entries for Ontology Mapping Using Virtual Documents[END_REF][START_REF] Djeddi | A Novel Approach Using Context-Based Measure for Matching Large Scale Ontologies[END_REF]. Contexts are constructed from all available information about an ontology entity, including entity naming (ID), annotation properties (labels and comments) and information on the neighbors of entities (super and sub-concepts). They are used for disambiguating the senses that better express the meaning of ontology entities, before looking for relations between these senses in WordNet in order to validate or not a correspondence between those entities. Although our approach can be applied for validating any kind of alignment (i.e., domain ontology alignments), it is particularly suitable for validating alignments which are rich in subsumption relations, what is typically the case when matching domain and top-level ontologies, since it takes advantage of the network of conceptual-semantic and lexical relations in WordNet (in particular, hypernym relations). Furthermore, although this approach can be seen as a matching approach itself, our motivation here is to automatically validate alignments in the lack of gold standards. We apply our approach for validating alignments generated by a set of matching tools (see more details in [START_REF] Schmidt | Analysing Top-level and Domain Ontology Alignments from Matching Systems[END_REF]) and discuss the results against a manual validation. Our experiments are based on three well-known top-level ontologies (DOLCE, GFO, and SUMO) and one domain ontology from one of the most used data set in the Ontology Alignment Evaluation Initiative (OAEI) campaigns (the Conference data set). The rest of the paper is organised as follows. §2 introduces WordNet structure, top-level ontologies and ontology matching. §3 describes the validation approach. §4 presents the experiments. §5 discusses related work and, finally, §6 concludes the paper.

Background

WordNet

WordNet [START_REF] Miller | WordNet: A Lexical Database for English[END_REF]] is a general-purpose large lexical database of English. Nouns, verbs, adjectives and adverbs are grouped into sets of cognitive synonyms (synsets), each expressing a distinct concept. Synsets are interlinked by means of conceptual-semantic and lexical relations. A synset denotes a concept or a sense of a group of terms. Word-Net also provides textual descriptions of the concepts (gloss) containing definitions and examples. For instance, for the concept "Poster", one of the associated WordNet synsets (SID-06793426-N) groups the synonyms "poster, posting, placard, notice, bill, card", together with a gloss "a sign posted in a public place as an advertisement; a poster advertised the coming attractions".

Top-level ontologies

A top-level ontology is a high-level and domain independent ontology. The concepts expressed are intended to be basic and universal to ensure generality and expressivity for a wide range of domains. It is often characterized as representing common sense concepts and concerns concepts which are meta, generic, abstract and philosophical. There are two approaches for the use of top-level ontologies. The top-down approach uses the ontology as a foundation for deriving concepts in the domain ontology, taking advantage of the knowledge and experience already expressed in the top-level ontology. In a bottom-up approach, one usually matches a new or existing domain ontology to a top-level ontology. This paper concerns bottom-up approaches. Several top-level ontologies have been proposed in the literature. The reader can refer to [START_REF] Mascardi | A Comparison of Upper Ontologies[END_REF]] for a review of them. Here, we briefly introduce some well-known and largely used top-level ontologies which are used further in our experiments:

• DOLCE [START_REF] Gangemi | Sweetening Ontologies with DOLCE[END_REF]

Ontology matching

The process of finding correspondences between ontology entities is known as ontology matching. It takes as input two ontologies o s (source) and o t (target) and an (possibly empty) alignment A to be completed, and determines as output an alignment A ′ , i.e., a set of correspondences. Here, we borrow the definition of correspondence from [START_REF] Euzenat | Ontology Matching[END_REF]:

Definition 1 (Correspondence) A correspondence can be defined as <e s ,e t ,r,n>, such that: e s and e t are entities (e.g., concepts, properties, instances) of o s and o t , respectively; r is a relation holding between two entities e s and e t , (for instance, equivalence, subsumption, disjointness, overlapping); and n is a confidence measure number in the [0;1] range. The confidence assigns a degree of trust on the correspondence from the matcher.

Different matching approaches have emerged from the literature [START_REF] Kalfoglou | Ontology mapping: the state of the art[END_REF]Schorlemmer 2003, Euzenat and[START_REF] Euzenat | Ontology Matching[END_REF]. While terminological methods lexically compare strings (tokens or n-grams) used in naming entities (or in the labels and comments of entities), semantic methods utilize model-theoretic semantics to determine whether or not a correspondence exists between 2 entities. Approaches may consider the internal ontological structure, such as the range of their properties, their cardinality, and their transitivity and/or symmetry features, or alternatively the external ontological structure, such as the position of the 2 entities within the ontological hierarchy. The instances of concepts can also be compared using statistical, probabilistic and linguistic approaches. Moreover, ontology matching systems rely on several approaches.

Validation approach

Our validation approach is based on the intuition that a correspondence c from an alignment A, expressing a relation r (in particular, equivalence or sumbumption) between the entities e d and e t of a domain ontology o d and a top-level ontology o t , respectively, may exist as a semantic relation in WordNet (synonymy or hypernymy). Given e d and e t concepts in the ontologies, we have first to retrieve the most appropriated WordNet synsets and then check if there exists a relation r between such synsets. Our approach thus is based on two main steps : (i) synset disambiguation and (ii) synset relation identification.

Synset disambiguation. In order to select the synset that better expresses the meaning behind the ontology concept, we adopt the notion of context. A context is constructed from all information available about an ontology entity, including entity naming (ID), annotation properties (usually labels and comments) and information on the neighbors (super and sub-concepts). Given Sup e and Sub e , the sets of terms denoting the superconcepts and sub-concepts of the entity e, and Ann e the set of terms from its annotations, a naive strategy for building a context (ctx) considers these sets as a bag of words. In a preprocessing phase, the annotations are tokenized and stop words and special characters are removed. Hence, the context ctx e of an entity e is a bag of words from the pre-processed sets Sup e , Sub e and Ann e , including e itself (i.e., its ID) :

ctx e = {e, w | w ∈ Sup e ∪ w ∈ Sub e ∪ w ∈ Ann e }
We take ctx e for retrieving the closer WordNet synset with respect to the meaning of e. For that, we overlap ctx e with the context of each retrieved synset e i when looking for e in WordNet, and select the set with higher intersection. We compute the number of words occurring in both sets, based on the exact match between words. Given Terms e i the set of terms in a synset e i and Gloss e i the corresponding set of terms from the gloss (i.e, textual description containing definitions and examples) associated to the synset, the context ctx synset e i of the synset e i is defined as follows:

ctx synset e i = {e, w | w ∈ Terms e i ∪ w ∈ Gloss e i }
The overlap between ctx e and ctx synset Example. Given <Presentation Con f erence ,Event GFO >, one correspondence to be validated (taken from the ontologies used in our experiments) and the sets:

• Sup Presentation = {conference, document, contribution, invited, talk} (from the original set {Conference document, Conference contribution, Invited talk}); • Sub Presentation = / 0 (the domain concept has no sub-concepts); • Ann Presentation = / 0 (the domain concept has no annotations); • Sup Event = {individual, concrete, processual, structure, occurrent} (from the original set {individual, concrete, processual structure, occurrent}); • Sub Event = / 0 (the domain concept has no sub-concepts); • Ann Event = {event, processual, structure, process} (from the annotation "Events are processual structures comprising a process ...");

The following contexts can be constructed:

• ctx presentation = {presentation, conference, document, contribution, invited, talk}

• ctx event = {event, individual, concrete, processual, structure, occurrent, process}
Overlapping the context of the concepts with all their WordNet synsets, the closer synsets are = {SID-01048697-N (presentation)} and {SID-00029378-N (event)}. As they are different synsets, the equivalence between them can not be verified. Hence, we look for the Super synset of the concept presentation (from domain ontology) which is = {SID-01048697-N (presentation), SID-01027379-N (ceremony), SID-00407535-N (activity), SID-00030358-N (act, deed, human action, human activity), SID-00029378-N (event)}. As there is an overlap between this Super synset and the synset for event (SID-00029378-N (event)) then we assume that Presentation Con f erence subsumes Event GFO .

Experiments

4.1. Data set and matchers OAEI Conference data set. The OAEI Conference set4 contains 16 ontologies covering the domain of conference organization. We have chosen this data set because it contains expressive ontologies and is one of the most popular data set in the field [START_REF] Cheatham | Conference v2.0: An Uncertain Version of the OAEI Conference Benchmark[END_REF]. In our experiments, we have used only the Conference ontology5 . This ontology has 60 concepts, 46 object properties and 18 data properties.

Ontology matching tools. A set of tools, publicly available, from previous OAEI campaigns (not limited to Conference track top participants), and implementing different matching strategies was selected. Even though they are not exhaustive and were not exactly developed for that purpose, their output might help us to investigate the problem of aligning domain and top-level ontologies. Aroma 6 is a hybrid tool based on association rules; Falcon-AO 7 applies linguistic and structural approaches, as Lily 8 , which includes debugging strategies; LogMap 9 applies logical reasoning and repair strategies and its variant LogMap-Lite is essentially based on string similarities; MaasMatch adopts a similar-ity cube and a disambiguation phase as described in [START_REF] Schadd | Coupling of Wordnet Entries for Ontology Mapping Using Virtual Documents[END_REF]; WeSeE-Match 10 uses web search results for improving similarity measures; WikiMatch 11 uses Wikipedia as external knowledge source and YAM++ 12 applies linguistic, graph-based and machine learning approaches. MaasMatch and YAM++ use WordNet as background knowledge (see §5). All the tools were run with their default configuration settings.

Results and discussion

Manual analysis. We first qualitatively analysed how the available matching tools perform when aligning domain with top-level ontologies, based on a manual validation of the generated alignments, by 3 evaluators. For our experiments, we ran each of the above mentioned systems for the pairs composed by the Conference ontology against each toplevel ontology. We then merge the alignments generated by the matchers, resulting in 28 correspondences, and submitted the resulting merge to the analysis of three evaluators. The evaluators are researchers that have common-sense knowledge about the domain of conferences, with a strong background in Computer Science and well-familiarised with ontology matching. The evaluators analysed each correspondence and selected one type of relation (Equivalent, Subsumption or None), according to the relation they judged as correct, based on the concept description provided in the top-level ontology (see more details in [START_REF] Schmidt | Analysing Top-level and Domain Ontology Alignments from Matching Systems[END_REF]). Regarding the evaluators judgement, there was a total agreement among them in 21 (out of 28) correspondences. For 15 of them, no relation has been identified so that more than a half of the automatically aligned concepts were considered neither equivalent or subsumed. In 3 cases there was total agreement regarding subsumption, and in 3 cases total agreement for equivalence. For the 7 pairs, a partial agreement was achieved as subsumption (see Table 2, column 'Manual evaluation'). In the following, we quantitatively analyse the results obtained by the matchers, using precision and considering 4 different sets:

• P 1 considers the cases of total agreement among the judges (21 correspondences),

where the correspondence has been marked either as equivalent or subsumed; • P 2 considers both total and partial agreements (for equivalent or subsumed); • P 3 considers total agreement for equivalences (matchers generated only equivalences); • P 4 considers both total and partial agreements only for equivalences. 1 shows the matchers results for these 4 sets, in terms of precision. From 9 matchers, 2 of them (MaasMatch and YAM++) have used WordNet in their matching approaches (in particular, MassMatch with a disambiguation phase). As expected, the best results were obtained for P 2 for both systems. However, the best results for this set have been obtained by LogMap. Although, ideally, avoiding a bias in the evaluation is highly desirable and the background resources used in the validation process should not be used for validating correspondences generated on basis of them, our evaluation is not limited to matchers relying on WordNet. We have used a set of available matchers using different matching strategies and tried to maximize the testing set by merging their output. We can in fact observe that MassMatch and YAM++ were able to generate more correspondences than the other systems (with LogMap and its variant coming just behind).

Contrary to what would be expected, these systems (and all others, in fact) were not able to generate subsumption (even though some have been designed to). They generated only equivalences, even when they were in fact subsumptions. This is actually an important distinction that our validation tries to identify.

Automatic validation. We have submitted the 28 automatically generated correspondences to the automatic validation and compared the results with the manual evaluation (Table 2). Although, by definition, top-level ontologies should be able to cover most domain concepts, the matchers were not able to generate correspondences for most of the concepts (42 in a total of 60). A total of 8 pairs were automatically validated. From these pairs, 5 were correspondences validated manually by the evaluators. While the automatic validation distinguishes relations of equivalence and subsumption, it is still not able to distinguish as much as the manual analysis. The comparison of the automatic with the manual validation is given in terms of precision, recall, f-measure, and accuracy, in Table 3. Since the matchers do not distinguish equivalences and subsumptions, when evaluating our automatic approach, P 3 and P 4 have not been considered.

Looking at the results in detail (Table 2), we see 5 pairs with agreement between automatic and manual validation:

• Equivalence: Poster and Poster (SUMO), Publisher and Publisher (SUMO); • Subsumption: Organizer and Organism (SUMO), Presentation and Event (GFO), and

Person and Individual (GFO).

For the first 4 pairs above, the evaluators totally agreed on equivalence or subsumption relations and for the fifth pair, they partially agreed on subsumption. One of them has been generated by MassMatch (pair Presentation and Event(GFO)) and the other 4 by YAM++. In the automatically validated relations, the pairs involving an equivalence (Poster and Publisher), the same WordNet synset for both top-level and domain concepts was selected in the disambiguation step -respectively, SID-06793426-N (poster, posting, placard, notice, bill, card) and SID-08062623-N (publisher, publishing house, publishing firm, publishing company). For subsumption relations, for the pair Organizer and Organism(SUMO), the selected synsets were not the same -respectively, SID-10383237-N (organizer, organiser, arranger) and SID-00004475-N (organism, being) but the domain synset is related to the top-level synset via a hypernym relation (Organizer is-a Organism). The same was observed for the pairs Presentation and Event, and Person and Individual.

For the 3 pairs of concepts automatically validated but manually annotated as 'None', the concept Abstract appears in 2 pairs, and the third pair is related to the concept Workshop. For the first pair involving Abstract (GFO), 2 contexts intersect both domain and top-level concept contexts with the same number of words. However, the wrong synset was selected for the domain concept. While Abstract in the domain ontology corresponds to the sense SID-06468951-N (outline, synopsis, abstract, precis) and Abstract in the top-level ontology to the sense SID-05854150-N (abstraction,abstract), the selected synset for the domain concept was SID-05854150-N (abstraction,abstract). This is due to the fact that the domain concept context available was not enough for the disambiguation step and intersects with both SID-05854150-N and SID-06468951-N, with an intersection set containing the same number of elements. A similar behaviour was observed for the second pair involving Abstract(SUMO) and again for the pair involving the concept Workshop. For the latter, the same synset was selected for both domain and top-level ontology, SID-04603081-N (workshop,shop). The concept Abstract appears once more in another correspondence, for DOLCE, but it was not validated automatically nor manually. For 11 pairs (out the 28), very specific terms are used to express either domain or top-level concepts, and there are no respective entries in WordNet. As a general purpose resource, it does not cover as well domain specialized vocabularies. These specialized terms are usually expressed by noun compounds and represent 39% of correspondences that could not be validated. These limitations could be addressed by extending the validation to additional external resources.

Among the 13 pairs annotated as correct by the evaluators, 5 of them were validated automatically; 5 others belong to very specific terms for which there are no entries in WordNet, and 3 were found in WordNet, but not automatically validated: Organization and Organization (SUMO), Presentation and Proposition (DOLCE), and Topic and Concept (GFO). For Organization in the domain ontology, the synset SID-08008335-N (organization,organisation) was selected, which represents a group of people working together, but for the top-level, a wrong synset was selected, SID-08164585-N (administration, governance, governing body, establishment, brass, organization, organisation). For the pair Presentation and Proposition, the context was not enough to identify the correct synset. While for the domain concept the synset SID-01048697-N (presentation) was selected, for the top-level the synset SID-06750804-N (proposition) has been chosen and there was no hierarchical relation between them. For the pair Topic and Concept, the synset SID-06599788-N (subject,topic,theme) and SID-05835747-N (concept,conception,construct) were selected and, no relation was found between them in WordNet.

We could also observe that the domain ontology is not terminologically rich enough (i.e., entities have no labels nor comments) for helping the disambiguation and selection of the appropriate synsets. In some cases, only the identifier of the concept is available, once it is a root node in the hierarchy. For instance, the domain concept Organization, which has 7 WordNet synsets, has no annotations and no neighbours in the ontology hierarchy. Furthermore, the inconsistencies introduced in the resulting alignments (merge) should be taken into account. For instance, it seems contradictory that Conference applicant matches Non physical object and Registered applicant to Physical object, considered that the latter is a subclass of Conference applicant in the domain ontology. Finally, we could enrich the generated set of alignments by introducing simple hierarchical reasoning (if Conference applicant is a Physical object, all its subclasses are as well). Thus, covering most domain concepts.

Related work

Background knowledge from external resources such as WordNet has been largely exploited in matching domain ontologies, as a way for improving similarity measures [START_REF] Lin | A Survey of Exploiting WordNet in Ontology Matching[END_REF]. In [START_REF] Kwak | Ontology Matching based on Hypernym, Hyponym, Holonym and Meronym Sets in WordNet[END_REF], a lexical similarity for ontology matching considers the rate of including names of ontology entities and WordNet synset's words in an aggregated set (including hypernyms, hyponyms, holonyms and meronyms relations). Similar to us, they overlap word sets built from the available information on ontology entities and synsets. However, we exploit the context of ontology entities, including their sub-concepts, super-concepts and annotations but are limited to hypernym relations. In [START_REF] Yatskevich | Element level semantic matching using Word-Net[END_REF], a set of twelve element-level matchers using WordNet as background knowledge is proposed. The authors distinguish knowledgebased matchers (which exploit the structural properties of WordNet, often combined with statistics from large scale corpora) and gloss-based matchers (which exploit WordNet synset descriptions). We also exploit the structural properties of WordNet (but focusing on hypernym relations) and the glosses of synsets. However, they do not exploit the notion of context of ontology entities. As in our case, both works distinguish equivalence and subsumption relations. None of the matchers here indicated subsumption ( §4.2).

A closer approach to ours is proposed in [START_REF] Schadd | Coupling of Wordnet Entries for Ontology Mapping Using Virtual Documents[END_REF], where virtual documents represent the meaning of ontology entities and WordNet entries and entities are coupled according to their document similarities. A document is constructed from entities naming and annotation properties and information on the neighbours of the ontology entity, as we do in this paper. However, we exploit the WordNet hypernym relations in another way (not for constituting the virtual document associated to a synset), but in the step of identifying the relation between synsets. As in their approach, ours is related to the field of Word Sense Disambiguation, which can be carried out using several different techniques [START_REF] Navigli | Word Sense Disambiguation: A Survey[END_REF]]. Although it is possible to tackle this problem from various angles and relying on different similarity metrics, here we adopt a naive method based on the exact match of words in a context. The notion of context has also been exploited in [START_REF] Wang | Lily Results on SEALS Platform for OAEI 2011[END_REF], where semantic description documents (SDD) refer to the information about concept hierarchies, related properties and instances, or in [START_REF] David | AROMA results for OAEI[END_REF]] where a bag of words describing a concept is exploited within a mining approach. Other matching approaches exploiting WordNet include YAM++ [START_REF] Ngo | YAM++ -Results for OAEI 2013[END_REF] and XMAP [START_REF] Djeddi | A Novel Approach Using Context-Based Measure for Matching Large Scale Ontologies[END_REF] systems. YAM++ applies diverse strategies coming from machine learning, information retrieval and graph matching. For terminological similarity measures, YAM++ includes Wordnet-based metrics as Lin and Wu-Palmer [START_REF] Budanitsky | Evaluating WordNet-based Measures of Lexical Semantic Relatedness[END_REF]. XMAP defines a semantic similarity measure, defined using a domain-specific resource (UMLS) and WordNet. In order to deal with lexical ambiguity, the notion of scope is introduced, which represents the context where a concept occurs (i.e., the set of those concepts that are close to a given concept in therms of shortest path in a semantic network). They exploit super-concepts and sub-concepts in a hierarchy, as we did, but they do not take into account entity annotations as comments or definitions.

Our approach is inspired from those WordNet-based matching and sense disambiguation approaches for automatically confirming or not generated alignments that rely on different strategies. There exist different ways to evaluate alignments generated by matchers [START_REF] Hong-Hai | Comparison of schema matching evaluations[END_REF]. One classical way consists of comparing alignments to reference ones (gold standard). However, constructing such references is a timeconsuming task. They are not always available or may suffer of imperfections or low coverage. In the lack of such resources, alternatives include manual labeling on sample alignments, alignment coherence measurements [START_REF] Meilicke | Alignment incoherence in ontology matching[END_REF]], and correspondence patterns mining. Furthermore, the quality of a matcher can be assessed regarding its suitability for a specific task or application [START_REF] Isaac | Putting Ontology Alignment in Context: Usage Scenarios, Deployment and Evaluation in a Library Case[END_REF][START_REF] Hollink | Two Variations on Ontology Alignment Evaluation: Methodological Issues[END_REF]]. Finally, alternative approaches for validating alignments consider the generation of natural language questions to support end-users in the validation task [START_REF] Abacha | Question Generation for the Validation of Mapping Adaptation[END_REF] or validation of correspondences using graph-based algorithms in a semi-automatic way [START_REF] Serpeloni | Ontology mapping validation[END_REF]].

Final remarks and future work

This paper presented an approach for validating alignments between top-level and domain ontologies, using WordNet. We presented preliminary results that point to the strengthen and weaknesses of our approach. In particular, we do not mainly treat terms (but single words); the appropriate synset may not be selected if a wrong synset overlaps with the context of a concept, with the same number of elements in the overlapping set; sometimes the disambiguation process does not help due to the lack of context (cases where the ontologies have not enough terminological information or are structurally flat); we can not validate correspondences involving concepts with no entries in the resource; we do not take into account logical inconsistency nor simple hierarchical reasoning for filtering out and enhancing the set of correspondences. For overcoming these weaknesses, we plan to enrich the contexts by adding the contexts of neighbours, use distributional resources within the disambiguation process for better measuring the overlap of contexts, apply alternative similarity metrics for measuring the overlap between contexts, and deal with logical reasoning. We also plan to combine different background resources, including indirect alignments between WordNet and top-level ontologies and the lexico-semantic resource BabelNet, which integrates several lexicons and encyclopedias, and explore the superior layer of concepts in domain ontology to retrieve the more appropriate synset.

  Net synsets expressing, respectively, the meaning of the entities e d and e t , we verify if synset e d i = synset e t i . In this case, we assume that e d and e t are equivalent (r = equivalence). Otherwise, we construct the set Super synset e d i which is composed of all the hypernym synsets of synset e d i of rank k (k being the maximum length of the path from synset e d i to one of its hypernym synsets in WordNet, based on a depth-first search strategy). The intuition here is that if the concept in the top-level ontology belongs to the set of hypernyms of the domain concept, then a subsumption relation exists between them. Hence, synset e d

	number of synsets of e):	e i is calculated as follows (where n is the
	overlap(ctx e , ctx synset e i ) = max 1≤i≤n	|ctx e ∩ ctx synset e i |
	Synset relation identification. Having selected synset e d i and synset e t i , the closest Word-

i

subsumes synset e t i if synset e t i belongs to the set Super synset e d i (r = subsumption).

Table 1 . Precision of systems for their complete alignments with the 3 top-level ontologies. Systems marked with * use WordNet in their matching strategies.

 1

	System	P 1	P 2	P 3	P 4
	Aroma	0	.33	0	0
	Falcon-AO	0	0	0	0
	Lily	-	-	-	-
	LopMap	.33	.55 .33 .27
	LogMapLite	.33	.33 .33 .33
	MaasMatch*	.30	.42	0	.08
	WeSeE-Match	-	-	-	-
	WikiMatch	-	-	-	-
	Yam++*	.27	.38 .18 .15
	Total	.29	.39 .19 .18

10 http://www.ke.tu-darmstadt.de/resources/ontology-matching/wesee-match 11 http://www.ke.tu-darmstadt.de/resources/ontology-matching/wikimatch 12 http://www.lirmm.fr/yam-plus-plus/ Table

Table 3 . Precision, Recall, and F-measure of automatically validated pairs.

 3

	None	None

http://www.loa.istc.cnr.it/old/DOLCE.html

http://onto.eva.mpg.de/gfo-bio/gfo-bio.owl

http://www.adampease.org/OP/SUMO.owl

http://oaei.ontologymatching.org

http://oaei.ontologymatching.org/2015/conference/data/Conference.owl

https://exmo.inrialpes.fr/software/aroma/

http://ws.nju.edu.cn/falcon-ao/

http://cse.seu.edu.cn/people/pwang/lily.htm

https://www.cs.ox.ac.uk/isg/tools/LogMap/