Guillaume Aucher

François Schwarzentruber

On the Complexity of Dynamic Epistemic Logic (Extended Version)

Keywords: Dynamic epistemic logic, computational complexity, model checking, satisfiability Logique épistémique dynamique, méthode tableau, complexité calculatoire

Although Dynamic Epistemic Logic (DEL) is an influential logical framework for representing and reasoning about information change, little is known about the computational complexity of its associated decision problems. In fact, we only know that for public announcement logic, a fragment of DEL, the satisfiability problem and the model-checking problem are respectively PSPACE-complete and in P. We contribute to fill this gap by proving that for the DEL language with event models, the model-checking problem is, surprisingly, PSPACE-complete. Also, we prove that the satisfiability problem is NEXPTIME-complete. In doing so, we provide a sound and complete tableau method deciding the satisfiability problem.

Introduction

Research fields like distributed artificial intelligence, distributed computing and game theory all deal with groups of human or non-human agents which interact, exchange and receive information. The problems they address range from multi-agent planning and design of distributed protocols to strategic decision making in groups. In order to address appropriately and rigorously these problems, it is necessary to be able to provide formal means for representing and reasoning about such interactions and flows of information. The framework of Dynamic Epistemic Logic (DEL for short) is very well suited to this aim. Indeed, it is a logical framework where one can represent and reason about beliefs and knowledge change of multiple agents, and more generally about information change.

The theoretical work of the above mentioned research fields has already been applied to various practical problems stemming from telecommunication networks, World Wide Web, peer to peer networks, aircraft control systems, and so on. . . In general, in all applied contexts, the investigation of the algorithmic aspects of the formalisms employed plays an important role in determining whether and to what extent they can be applied. For this reason, the algorithmic aspects of DEL need to be studied.

To this aim, a preliminary step consists in studying the computational properties of its main associated decision problems, namely the model checking problem and the satisfiability problem.

Indeed, it will indirectly provide algorithmic methods to solve these decision problems and give us a hint of whether and to what extent our methods can be applied. However, surprisingly little is known about the computational complexity of these problems. We only know that for public announcement logic, a fragment of DEL [Plaza, 1989], the model checking problem is in P and the satisfiability problem is PSPACE-complete. Here, we aim to fill this gap for the full language of DEL with event models.

DEL is built on top of epistemic logic. An epistemic model represents how a given set of agents perceive the actual world in terms of beliefs and knowledge about this world and about the other agents' beliefs. The insight of the DEL approach is that one can describe how an event is perceived by agents in a very similar way: an agent's perception of an event can also be described in terms of beliefs and knowledge. For example, at the battle of Waterloo, when marshal Blücher received the message of the duke of Wellington inviting him to join the attack at dawn against Napoleon, Wellington did not know at that very moment that Blücher was receiving his message, and Blücher knew it. This is a typical example of announcement which is not public. This led Baltag, Moss and Solecki to introduce the notion of event model [START_REF] Baltag | The logic of common knowledge, public announcement, and private suspicions[END_REF]. The definition of an event model, denoted (M ′ , w ′ ), is very similar to the definition of an epistemic model. They also introduced a product update, which defines a new epistemic model representing the situation after the event. Then, they extended the epistemic language with dynamic operators [M ′ , w ′ ]ϕ standing for 'ϕ holds after the occurrence of the event represented by (M ′ , w ′ )'.

Using the so-called reduction axioms, it turns out that any formula with dynamic operator(s) can be translated to an equivalent epistemic formula without dynamic operator. As a first approximation, we could be tempted to use these reduction axioms to reduce both the model checking problem and the satisfiability problem of DEL to the model checking problem and the satisfiability problem of epistemic logic, because optimal algorithmic methods already exist for these related problems. However, the reduction algorithm induced by the reduction axioms is exponential in the size of the input formula. Therefore, for the satisfiability problem, we only obtain an algorithm which is in EXPSPACE (because the satisfiability problem of epistemic logic is PSPACE-complete), and for the model checking problem, we only obtain an algorithm which is in EXPTIME (because the model checking problem of epistemic logic is in P). These algorithms are not optimal because, as we shall see, there exists an algorithm solving the satisfiability problem which is in NEXPTIME⊆ EXPSPACE and also an algorithm solving the model checking problem which is in PSPACE⊆ EXPTIME. Our algorithm for solving the satisfiability problem is based on a sound and complete tableau method which does not resort to the reduction axioms.

The paper is organized as follows. In Section 2, we recall the core of the DEL framework and the different variants of languages with event models which have been introduced in the literature. In Section 3, we prove that the model checking problem of DEL is PSPACE-complete, and in Section 4 we prove that the satisfiability problem is NEXPTIME-complete. In Section 5, we discuss related works and whether our results still hold when we extend the expressivity of the language with common belief and 'star' iteration operators. We conclude in Section 6.

Dynamic Epistemic Logic

Following the methodology of DEL, we split the exposition of the DEL logical framework into three subsections. In Section 2.1, we recall the syntax and semantics of the epistemic language. In Section 2.2, we define event models, and in Section 2.3, we define the product update. In Section 2.4, we recall the different languages that have been introduced in the DEL literature and we introduce our language L DEL .

Epistemic language

In the rest of the paper, ATM is a countable set of atomic propositions and AGT is a finite set of agents.

A (pointed) epistemic model (M, w) represents how the actual world represented by w is perceived by the agents. Intuitively, in this definition, vR a u means that in world v agent a considers that world u might be the actual world.

Definition 1 (Epistemic model). An epistemic model is a tuple M = (W, R, V ) where W is a non-empty set of possible worlds, R maps each agent a ∈ AGT to a relation R a ⊆ W × W and V : ATM → 2 W is a function called a valuation. We abusively write w ∈ M for w ∈ W and we say that (M, w) is a pointed epistemic model. We also write v ∈ R a (w) for wR a v.

Then, we define the following epistemic language L EL . It can be used to describe and state properties of epistemic models:

Definition 2 (Epistemic language). The language L EL of epistemic logic is defined as follows:

L EL : ϕ ::= p | ¬ϕ | (ϕ ∧ ϕ) | B a ϕ
where p ranges over ATM and a ranges over AGT. A formula of L EL is called an epistemic formula. The formula ⊥ is an abbreviation for p ∧ ¬p, and ⊤ is an abbreviation for ¬⊥. The formula B a ϕ is an abbreviation of ¬B a ¬ϕ. The size of a formula ϕ ∈ L EL is defined by induction as follows:

|p| = 1; |¬ϕ| = 1 + |ϕ|; |ϕ ∧ ψ| = 1 + |ϕ| + |ψ|; |B a ϕ| = 1 + |ϕ|.
Intuitively, the formula B a ϕ reads as 'agent a believes that ϕ holds in the current situation'.

Definition 3 (Truth conditions). Given an epistemic model M = (W, R, V ) and a formula ϕ ∈ L EL , we define inductively the satisfaction relation |=⊆ W × L EL as follows: for all w ∈ W ,

M, w |= p iff w ∈ V (p) M, w |= ϕ ∧ ψ iff M, w |= ϕ and M, w |= ψ M, w |= ¬ϕ iff not M, w |= ϕ M, w |= B a ϕ iff for all v ∈ R a (w), we have M, v |= ϕ
We write M |= ϕ when for all w ∈ M, it holds that M, w |= ϕ. Also, we write |= ϕ, and we say that ϕ is valid, when for all epistemic model M, it holds that M |= ϕ. Dually, we say that ϕ is satisfiable when ¬ϕ is not valid.

Example 1. Our running example is inspired by the coordinated attack problem from the distributed systems folklore [START_REF] Fagin | Reasoning about knowledge[END_REF]. Our set of atomic propositions is ATM = {p} and our set of agents is AGT = {1, 2}. Agent 1 is the duke of Wellington and agent 2 is marshal Blücher; p stands for 'Wellington wants to attack at dawn'. The initial situation is represented in Figure 1 by the pointed epistemic model

(M, w) = ({w, u}, R 1 = {(w, w), (u, u)}, R 2 = {(w, w), (w, u)}, V (p) = {w}).

Event model

A (pointed) event model (M ′ , w ′ ) represents how the actual event represented by w ′ is perceived by the agents. Intuitively, in this definition, u ′ R ′ a v ′ means that while the possible event represented by u ′ is occurring, agent a considers possible that the event represented by v ′ is in fact occurring.

# " ! w : p 2 1,2 Õ Õ # " ! × Ö Õ Ô Ð Ñ Ò Ó (w, w ′ 1 ) : p 1 2 Ø Ø # " ! × Ö Õ Ô Ð Ñ Ò Ó (w, w ′ 1 , w ′ 2 ) : p 2 # " ! u : ¬p 1 # " ! p 1,2 z z 2 # " ! p 2 z z 1 # " ! ¬p 1 # " ! p 1,2 z z 2 # " ! ¬p 1 Figure 1: Pointed epistemic models (M, w) (left), ((M ⊗ M ′ 1 ), (w, w ′ 1 )) (center ) and (M ⊗ M ′ 1 ⊗ M ′ 2 , (w, w ′ 1 , w ′ 2 )) (right) # " ! w ′ 1 : p 1 2 × × # " ! × Ö Õ Ô Ð Ñ Ò Ó w ′ 2 : B 2 p 2 1 × × # " ! u ′ 1 : ⊤ 1,2 # " ! u ′ 2 : ⊤ 1,2 Figure 2: Pointed event models (M ′ 1 , w ′ 1 ) (left) and (M ′ 2 , w ′ 2 ) (right)
Definition 4 (Event model). An event model is a tuple M ′ = (W ′ , R ′ , P re) where W ′ is a nonempty and finite set of possible events, R ′ maps each agent a ∈ AGT to a relation R ′ a ⊆ W ′ × W ′ and P re : W ′ → L EL is a function that maps each event to a precondition expressed in the epistemic language.

We abusively write w ′ ∈ M ′ for w ′ ∈ W ′ and we say that (M ′ , w ′ ) is a pointed event model. The size of an event model M ′ = (W ′ , R ′ , P re) is noted |M ′ | and is defined as follows:

card(W ′ ) + a∈AGT card(R ′ a ) + w ′ ∈W ′ |P re(w ′ )|. Example 2. In Figure 2 are represented two pointed event models. The first, (M 1 , w ′ 1 ) = ({w ′ 1 , u ′ 1 }, R 1 = {(w ′ 1 , u ′ 1 ), (u ′ 1 , u ′ 1 )}, R 2 = {(w ′ 1 , w ′ 1 ), (u ′ 1 , u ′ 1 )}, P re, w ′ 1 )
where P re(w ′ 1 ) = p and P re(u ′ 1 ) = ⊤, represents the event whereby Blücher receives the message of Wellington that he wants to attack at dawn. When this happens, Wellington believes that nothing happens and believes that this is even common knowledge. The second,

(M 2 , w ′ 2 ) = ({w ′ 2 , u ′ 2 }, R 1 = {(w ′ 2 , w ′ 2 ), (u ′ 2 , u ′ 2 )}, R 2 = {(w ′ 2 , u ′ 2 ), (u ′ 2 , u ′ 2 )}, P re, w ′ 2 )
, where P re(w ′ 2 ) = B 2 p and P re(u ′ 2 ) = ⊤, represents the event whereby Wellington receives the message of Blücher telling him that he 'knows' that Wellington wants to attack at dawn.

Product update

The following product update yields a new pointed epistemic model M⊗M ′ , (w, w ′ ) representing how the new situation which was previously represented by (M, w) is perceived by the agents after the occurrence of the event represented by (M ′ , w ′ ).

Definition 5 (Product update). Let M = (W, R, V ) be an epistemic model and let M ′ = (W ′ , R ′ , P re) be an event model. The product update of M by M ′ is the epistemic model M ⊗ M ′ = (W ′′ , R ′′ , V ′′ ) defined as follows (p and a range over ATM and AGT respectively):

W ′′ ={(w, w ′ ) ∈ W × W ′ | M, w |= P re(u ′ )} R ′′ a ={ (w, w ′ ), (v, v ′ ) ∈ W ′′ × W ′′ | wR a v and w ′ R ′ a v ′ } V ′′ (p) ={(w, w ′ ) ∈ W ′′ | w ∈ V (p)}
Given a pointed epistemic model (M, w), and a pointed event model (M ′ , w ′ ), we say that (M ′ , w ′ ) is executable in (M, w) when M, w |= P re(w ′ ). If M is an epistemic model and M ′ 1 , . . . , M ′ n are event models, we abusively write

M ⊗ M ′ 1 ⊗ • • • ⊗ M ′ n for (. . . ((M ⊗ M ′ 1 ) ⊗ M ′ 2 ) ⊗ . . .) ⊗ M ′ n and (w, w ′ 1 , . . . , w ′ n ) for (. . . ((w, w ′ 1 ), w ′ 2 ), . . .), w ′ n ). Example 3. The pointed epistemic models ((M⊗M ′ 1 ), (w, w ′ 1 )) and (M⊗M ′ 1 ⊗M ′ 2 , (w, w ′ 1 , w ′ 2
)) are represented in Figure 1. After Blücher receives the message of Wellington, Blücher 'knows' that Wellington wants to attack at dawn, but Wellington does not 'know' that Blücher 'knows' it:

M⊗M ′ 1 , (w, w ′ 1 ) |= p∧B 2 p∧¬B 1 B 2 p.
Likewise, after Wellington receives the message of Blücher telling him that he 'knows' that he wants to attack at dawn (B 2 p), Wellington 'knows' that Blücher 'knows' that he wants to attack at dawn, but Blücher does not 'know' that Wellington 'knows' it:

M ⊗ M ′ 1 ⊗ M ′ 2 , (w, w ′ 1 , w ′ 2 ) |= p ∧ B 2 p ∧ B 1 B 2 p ∧ ¬B 2 B 1 B 2 p. Hence, in particular, M, w |= ¬[M ′ 1 , w ′ 1 ][M ′ 2 , w ′ 2 ]B 2 B 1 B 2 p.

Languages of DEL

In [START_REF] Baltag | The logic of common knowledge, public announcement, and private suspicions[END_REF]], the language is defined as follows:

ϕ ::= p | ¬ϕ | (ϕ ∧ ϕ) | B a ϕ | [M ′ , w ′ ]ϕ
where p ranges over ATM , a ranges over AGT and (M ′ , w ′ ) is any pointed and finite event model. The formula M ′ , w ′ ϕ is an abbreviation for ¬[M ′ , w ′ ]¬ϕ.

Intuitively, [M ′ , w ′ ]ϕ reads as 'ϕ will hold after the occurrence of the event represented by (M ′ , w ′ )' and M ′ , w ′ ϕ reads as 'the event represented by (M ′ , w ′ ) is executable in the current situation and ϕ will hold after its execution'.

However, note that in this definition, preconditions of event models are necessarily epistemic formulas. In [START_REF] Baltag | Logic for epistemic programs[END_REF]], another language is introduced which can deal with event models whose preconditions may involve formulas with event models. This language relies on the notion of event signature and the epistemic language is extended with a modality [Σ, ϕ 1 , . . . , ϕ n ]ϕ, where Σ is an event signature. The language of [START_REF] Baltag | Logic for epistemic programs[END_REF]] also includes PDL-like program constructions such as sequential composition, union and 'star' operation of event models (see Section 5 for a definition of these program constructions).

In [van Ditmarsch et al., 2007], preconditions can also be formulas involving event models, but only union of programs is allowed. It is therefore a fragment of the language of [START_REF] Baltag | Logic for epistemic programs[END_REF] since it does not include sequential composition nor the 'star' operation. This will be our language in this paper.

Definition 6 ([van Ditmarsch et al., 2007]). The language L DEL is the union of the formulas ϕ ∈ L stat ⊗ and the events (or epistemic events) π ∈ L dyn ⊗ defined by the following rule:

L stat ⊗ : ϕ ::= p | ¬ϕ | (ϕ ∧ ϕ) | B a ϕ | [π]ϕ L dyn ⊗ : π ::= M ′ , w ′ | (π ∪ π)
where p ranges over ATM , a ranges over AGT and (M ′ , w ′ ) is a pointed and finite event model such that for all w ′ ∈ M ′ , P re(w ′ ) is a formula of L stat ⊗ that has already been constructed in a previous stage of the inductively defined hierarchy.

The size of ϕ ∈ L DEL is defined as for the epistemic language together with the induction case

|[π]ϕ| = 1 + |π| + |ϕ| where |M ′ , w ′ | = |M ′ |,
M, w |= [M ′ , w ′ ]ϕ iff M, w |= P re(w ′ ) implies M ⊗ M ′ , (w, w ′ ) |= ϕ M, w |= [π ∪ γ]ϕ iff M, w |= [π]ϕ and M, w |= [γ]ϕ.
The other induction steps are identical to the induction steps of Definition 3.

The results in this paper are the same whether or not the formulas of the preconditions involve event models. However, the result of NEXPTIME-completeness of the satisfiability problem of Section 4 holds only if we consider union of event models as a program construction in the language.

Model checking problem

The model checking problem of L DEL is defined as follows:

Input: a pointed epistemic model (M, w) and a formula ϕ ∈ L DEL ;

Output: yes iff M, w |= ϕ.

Whereas the model checking problem with an epistemic formula of L EL is in P, model checking with a formula of L DEL is surprisingly PSPACE-complete. This shows that the addition of dynamic modalities with event models to L EL increases tremendously the computational complexity of the model checking problem.

Upper bound

In Figure 3 is defined a deterministic algorithm M-Check( w M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i , ϕ) that checks whether we have M ⊗ M ′ 1 ⊗ . . . M ′ i , (w, w ′ 1 , . . . , w ′ i ) |= ϕ, where (M, w) is a pointed epistemic model and for all j ∈ {1, . . . , i}, (M ′ j , w ′ j ) is a pointed event model. The precondition of a call to the function M-Check(. . . ) is that (w, w ′ 1 , . . . , w ′ i ) ∈ M ⊗ M ′ 1 ⊗ . . . M ′ i , that is, the sequence (M ′ 1 , w ′ 1 ) . . . , (M ′ i , w ′ i ) is executable in (M, w).
In order to check whether M, w |= ϕ, we just call M-Check(w, ϕ).

Theorem 1. The model checking problem of L DEL is in PSPACE.

RR n°8164

Proof. Terminaison and correction of the algorithm M-Check are easily proved over the size of the input defined by:

|M| + i k=1 |M ′ k | + |ϕ|.
The only case worth mentionning is when ϕ is of the form [M ′ , w ′ ]ψ. In that case, the number

of recursive calls of M-Check(w M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i ; M ′ , w ′ ψ) is of size |M| + i k=1 |M ′ k | + |M ′ | + |ψ|.
This quantity is indeed smaller than the size of the call of ϕ, because it is equal to

|M| + i k=1 |M ′ k | + |ϕ| = |M| + i k=1 |M ′ k | + |M ′ | + |ψ| + 1.
The algorithm requires a polynomial amount of space in the size of the input. Indeed, as the size of the input is strictly decreasing at each recursive call, the number of recursive calls in the call stack is linear in the size of the input. Then each of the current call requires a polynomial amount of space in the size of the input for storing the value of local variables: the most consuming case is B a ψ where we have to save all the current values of u, u 1 , . . . , u i in the loop for.

Lower bound

We prove that the algorithm of the previous section is optimal. To do so, we provide a polynomial reduction of the quantified Boolean formula satisfiability problem, known to be PSPACE-complete [Papadimitriou, 1995, p. 455] to the model-checking problem of L DEL .

Theorem 2. The model checking problem of L DEL is PSPACE-hard.

Proof. Without loss of generality, we only consider in this proof quantified Boolean formulas of the form ∀p 1 ∃p 2 ∀p 3 . . . ∀p 2k-1 ∃p 2k ψ(p 1 , . . . p 2k ), where ψ(p 1 , . . . , p 2k ) is a Boolean formula over the atomic propositions p 1 , . . . , p 2k . The formula ∀p 1 ∃p 2 ∀p 3 . . . ∀p 2k-1 ∃p 2k ψ(p 1 , . . . p 2k ) is satisfiable iff for both truth values of the atomic proposition p 1 there is a truth value for the atomic proposition p 2 such that for both truth values of the atomic proposition p 3 , and so on up to p 2k , the formula ψ(p 1 , . . . p 2k ) is true in the overall truth assignment.

We can restrict ourselves to L DEL where there is only one agent a. The quantified Boolean formula satisfiability problem is defined as follows:

Input:

a natural number k and a quantified Boolean formula ϕ ∀p 1 ∃p 2 ∀p 3 . . . ∀p 2k-1 ∃p 2k ψ(p 1 , . . . , p 2k );

Output: yes iff ϕ is satisfiable. Let ϕ = ∀p 1 ∃p 2 ∀p 3 . . . ∀p 2k-1 ∃p 2k ψ(p 1 , . . . p 2k ) be a quantified Boolean formula. We define a pointed epistemic model (M, w 0 ), 2k pointed event models (M ′ 1 , w ′0 1 ), . . . , (M ′ 2k , w ′0 2k )
, a pointed event model M ′ , w ′0 and an epistemic formula ψ ′ that are computable in polynomial time in the size of ϕ such that: The corresponding instance of the model checking problem of L DEL is computable in polynomial time in the size of ϕ. Now, let us describe M, w 0 , the event models M ′ 1 , w ′0 1 , . . . , M ′ 2k , w ′0 2k , the event model M ′ , w ′0 and ψ ′ .

ϕ is satisfiable in quantified Boolean logic iff M, w 0 |= [M ′ 1 , w ′0 1 ∪ M ′ , w ′0 ] M ′ 2 , w ′0 2 ∪ M ′ , w ′0 . . . [M ′ 2k-1 , w ′0 2k-1 ∪ M ′ , w ′0 ] M ′ 2k , w ′0 2k ∪ M ′ , w ′0 ψ ′ . RR n°8164 function M-Check(w M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i ϕ) match (ϕ) case p: return w ∈ V (p); case ¬ψ: return not M-Check(w M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i ψ); case ψ 1 ∧ ψ 2 : return (M-Check(w M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i ψ 1 ) and M-Check(w M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i ψ 2 )); case B a ψ: for u ∈ R a (w) for u ′ 1 ∈ R ′ a (w ′ 1 ) if M-Check(u, P re(u ′ 1 )) . . . for u ′ i ∈ R ′ a (w ′ i ) if M-Check(u M ′ 1 , u ′ 1 ; . . . ; M ′ i-1 , u ′ i-1 P re(u ′ i )) if not M-Check(u M ′ 1 , u ′ 1 ; . . . ; M ′ i , u ′ i ψ); return false ; endIf endIf endFor . . . endIf endFor endFor return true ; case [M ′ , w ′ ]ψ: if M-Check(w M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i P re(w ′ )) return M-Check(w M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i ; M ′ , w ′ ψ); endIf return true ; case [π ∪ γ]ψ: return (M-Check(w M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i [π]ψ) and M-Check(w M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i [γ]ψ)); endMatch endFunction
• M = (W, R, V ) is defined by:

-W = {w 0 , w 1 , . . . , w 2k+1 }; -R a = {(w j , w j+1 | j ∈ {0, . . . , 2k}}; -and V (p) = ∅ for all p ∈ ATM • For all i ∈ {1, . . . , 2k}, M ′ i = (W ′ i , R ′ i , P re i ) is defined by: -W ′ i = {w ′0 i , w ′1 i , . . . , w ′i i , w ′ i } -R i ′ a = {(w ′j i , w ′j+1 i ) | j ∈ {0, . . . , i -1}} ∪ {(w ′0 i , w ′ i ), (w ′ i , w ′ i )} -and P re i (u ′ ) = ⊤ for all u ′ ∈ W ′ i • M ′ , w ′0 = (W ′ , R ′ , P re ) is defined by: RR n°8164 -W ′ = {w ′0 } -R ′ a = {(w ′0 , w ′0 )} -P re (w ′0 ) = ⊤ • ψ ′ = ψ(p 1 ← B a B a ⊥, . . . , p 2k ← ( B a ) 2k B a ⊥)
, that is, ψ ′ is the formula ψ where all p i occurrences are substituted by ( B a ) i B a ⊥. (The formula B a i ϕ is an abbreviation for B a . . . B a ϕ with i operators B a .)

The semantics is simulated in the following way. The proposition p i is interpreted as the presence of a chain of length exactly i from the root of a given epistemic model. That is why in ψ ′ , the proposition p i is substituted by ( B a ) i B a ⊥, which is true in the root of the final epistemic model iff there exists a chain of length i in that model.

Note that updating an epistemic model where there is a chain of length 2k + 1 by M ′ i , w ′0 i where i ∈ {1, . . . , 2k}:

• preserves the presence or absence of any chain of length j = i; in particular, it always preserves the presence of the chain of length 2k + 1;

• adds a chain of length i, that is p i becomes true;

Note also that updating an epistemic model where there is a chain of length 2k+1 by M ′ , w ′0 preserves the presence or absence of any chain. So, it will keep p i false if it was already false and it will keep any p i true if it was already true. In other words, the M ′ , w ′0 is a neutral element for the product update.

The crucial invariant property (Inv) of an epistemic model is the existence of a chain of length 2k + 1 in any update of M, w 0 by any sequence of M ′ , w ′0 and M ′ i , w ′0 i .

The behavior of ∀p i in quantified Boolean logic consists in a universal choice of a truth value for p i . It is translated by the update operator [M ′ i , w ′0 i ∪ M ′ , w ′0 ] whose semantics is to choose universally the update of the epistemic model by M ′ i , w ′0 i , that will give a new updated epistemic model with a chain of length i, that is p i is true, or by M ′ , w ′0 that will let the new updated epistemic model without a chain of length i, that is p i is false.

The behavior of ∃p i in quantified Boolean logic consists in an existential choice of a truth value for p i . It is translated by the update operator M ′ i , w ′0 i ∪ M ′ , w ′0 whose semantics is to choose existentially the update of the epistemic model by M ′ i , w ′0 i , that will give a new updated epistemic model with a chain of length i, that is p i is true, or by M ′ , w ′0 , that will let the new updated epistemic model without a chain of length i, that is p i is false.

Remark. Note that the reduction used to prove that the model checking problem of L DEL is PSPACE-hard uses only the precondition ⊤.

Satisfiability problem

The satisfiability problem of L DEL is defined as follows:

Input: a formula ϕ ∈ L DEL ;

Output: yes iff there exists a pointed epistemic model (M, w) such that M, w |= ϕ.

RR n°8164

The satisfiability problem is known to be decidable. Indeed, the standard reduction axioms of DEL [Baltag and Moss, 2004, p. 214] induce a translation tr : L DEL → L EL such that ϕ ∈ L DEL is satisfiable iff tr(ϕ) ∈ L EL is satisfiable. Since the size of tr(ϕ) is at most exponential in the size of ϕ [Lutz, 2006] and the satisfiability problem of L EL is PSPACE-complete, the satisfiability problem of L DEL is in EXPSPACE. This upper bound is nevertheless not optimal: we are going to prove in this section that the satisfiability problem of L DEL is NEXPTIME-complete.

Upper bound

In this subsection we present a tableau method that does not rely on reduction axioms and we prove that it provides a NEXPTIME procedure deciding the satisfiability problem.

Tableau method

Let Lab be a countable set of labels designed to represent worlds of the epistemic model (M, w). Our tableau method manipulates terms that we call tableau terms and they are of the following kind:

• (σ M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i ϕ)
where σ ∈ Lab is a node (that represents a world in the initial model) and for all j ∈ {1, . . . , i}, M ′ j , w ′ j is an event model. This term means that ϕ is true in the world denoted by σ after the execution of the sequence M ′ 1 , w ′ 1 , . . . , M ′ i , w ′ i and that the sequence is executable in the world denoted by σ;

• (σ M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i ) means that the sequence M ′ 1 , w ′ 1 , . . . , M ′ i , w ′ i is executable in the world denoted by σ; • (σ M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i ⊗) means that the sequence M ′ 1 , w ′ 1 , . . . , M ′ i , w ′
i is not executable in the world denoted by σ;

• (σR a σ 1 ) means that the world denoted by σ is linked by R a to the world denoted by σ 1 ;

• ⊥ denotes an inconsistency.

A tableau rule is represented by a numerator N above a line and a finite list of denominators D 1 , . . . , D k below this line, separated by vertical bars:

N D 1 | . . . | D k
The numerator and the denominators are finite sets of tableau terms. A tableau tree is a finite tree with a set of tableau terms at each node. A rule with numerator N and denominator D is applicable to a node carrying a set Γ if Γ contains an instance of N but not the instance of its denominator D. If no rule is applicable, Γ is said to be saturated. We call a node σ an end node if the set of formulas Γ it carries is saturated, or if ⊥ ∈ Γ. The tableau tree is extended as follows:

1. Choose a leaf node n carrying Γ where n is not an end node, and choose a rule ρ applicable to n.

(a)

If ρ has only one denominator, add the appropriate instantiation to Γ.

(b) If ρ has multiple denominators, choose one of them and add to Γ the appropriate instantiation of this denominator.

RR n°8164 A branch in a tableau tree is a path from the root to an end node. A branch is closed if its end node contains ⊥, otherwise it is open. A tableau tree is closed if all its branches are closed, otherwise it is open. The tableau tree for a formula ϕ ∈ L DEL is the tableau tree obtained from the root {(σ 0 ǫ ϕ)} when all leafs are end nodes. We write ⊢ ϕ when the tableau for ¬ϕ is closed.

(σ Σ ′ ϕ ∧ ψ) (σ Σ ′ ϕ) (σ Σ ′ ψ) (∧) (σ Σ ′ ¬¬ϕ) (σ Σ ′ ϕ) (¬¬) (σ Σ ′ ¬(ϕ ∧ ψ)) (σ Σ ′ ¬ϕ) | (σ Σ ′ ¬ψ) (¬∧) (σ Σ ′ p)(σ Σ ′ ¬p) ⊥ (⊥) (σ Σ ′ p) (σ ǫ p) (← p ) (σ Σ ′ ¬p) (σ ǫ ¬p) (← ¬p ) (σ M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i B a ϕ) (σ R a σ 1 ) (σ 1 M ′ 1 , u ′ 1 ; . . . ; M ′ i , u ′ i ) (σ 1 M ′ 1 , u ′ 1 ; . . . ; M ′ i , u ′ i ϕ) (σ 1 M ′ 1 , u ′ 1 ; . . . ; M ′ i , u ′ i ⊗) (B a ) (σ M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i ¬B a ϕ) (σ R a σ new ) (σ new M ′ 1 , u ′ 1 ; . . . ; M ′ i , u ′ i ) (σ new M ′ 1 , u ′ 1 ; . . . ; M ′ i , u ′ i ¬ϕ) (¬B a ) (σ Σ ′ ¬[M ′ , w ′ ]ϕ) (σ Σ ′ ; M ′ , w ′ ) (σ Σ ′ ; M ′ , w ′ ¬ϕ) (¬[M ′ , w ′ ]) (σ Σ ′ [M ′ , w ′ ]ϕ) (σ Σ ′ ; M ′ , w ′ ⊗) (σ Σ ′ ; M ′ , w ′ ) (σ Σ ′ ; M ′ , w ′ ϕ) ([M ′ , w ′ ]) (σ Σ ′ ; M ′ , w ′ ) (σ Σ ′ P re(w ′ )) (σ Σ ′ ) ( ) (σ Σ ′ ; M ′ , w ′ ⊗) (σ Σ ′ ) (σ Σ ′ ¬P re(w ′ )) (σ Σ ′ ⊗) (⊗) (σ Σ ′ ⊗)(σ Σ ′ ) ⊥ (clash ,⊗ ) (σ ǫ ⊗) ⊥ (ǫ ⊗ ) (σ Σ ′ [π ∪ γ]ϕ) (σ Σ ′ [π]ϕ) (σ Σ ′ [γ]ϕ) ([π ∪ γ]) (σ Σ ′ ¬[π ∪ γ]ϕ) (σ Σ ′ ¬[π]ϕ) | (σ Σ ′ ¬[γ]ϕ) (¬[π ∪ γ])
The tableau rules of our tableau method are represented in Figure 4. In these rules, Σ ′ is a list of pointed event models M ′ 1 , w ′ 1 , . . . , M ′ i , w ′ i and ǫ is the empty list. The tableau method contains the classical Boolean rules (∧), (¬¬), (¬∧). The rules (← p ) and (← ¬p ) handle atomic propositions. The rule (⊥) makes the current execution fail. The rule for (B a ) is applied for all j ∈ {1, . . . i} and all u ′ j such that w ′ j R ′ a u ′ j . Similarly, the rule for (¬B a ) is applied by choosing non-deterministically for all j ∈ {1, . . . i} some u ′ j such that w ′ j R ′ a u ′ j and creating a new fresh label σ new . The rules ( ), (⊗), (clash ,⊗ ) and (ǫ ⊗ ) handle the preconditions. The last two rules

([π ∪ γ]) and (¬[π ∪ γ]) handle the union operator. Proposition 1 (Soundness). Let ϕ ∈ L DEL . If ⊢ ϕ, then |= ϕ.
Proof. We prove it by contrapositive. Suppose that ϕ, that is, there exists a pointed epistemic model (M, w) such that M, w |= ¬ϕ. We must prove that every tableau for (σ 0 ǫ ¬ϕ) has an open branch (the proof of termination is in the proof of Theorem 3).

We say that a set Γ f of tableau terms is interpretable if there exists a pointed epistemic model M = (W, R, V ), a partial function ν : Lab → W such that (M, ν) makes all the tableau terms in Γ f true for the following semantics |= T :

(M, ν) |= T (σ M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i ϕ) iff the sequence (M ′ 1 , w ′ 1 ), . . . , (M ′ i , w ′ i ) is executable in (M, ν(σ)) and M ⊗ M ′ 1 ⊗ . . . ⊗ M ′ i , (ν(σ), w ′ 1 , . . . , w ′ i ) |= ϕ (M, ν) |= T (σ M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i ) iff the sequence (M ′ 1 , w ′ 1 ), . . . , (M ′ i , w ′ i ) is executable in (M, ν(σ)) (M, ν) |= T (σ M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i ⊗) iff the sequence (M ′ 1 , w ′ 1 ), . . . , (M ′ i , w ′ i ) is not executable in (M, ν(σ)) (M, ν) |= T (σ R a σ 1 ) iff ν(σ) R a ν(σ 1 ) (M, ν) |= T ⊥ iff false

Since

ϕ, the set Γ = {(σ 0 ¬ϕ)} is interpretable. Moreover, if a set of formulas is interpretable, it does not contain ⊥. So, if we prove that when the numerator of a rule is interpretable, one of the denominators also is, then we have that every tableau for (σ 0 ǫ ¬ϕ) has an open branch. In that case, we say that the rule is sound. We only prove it for (¬B a ), (B a ), the proof for the other rules being similar. In the following, when ν is a function, we let ν(x → a) be the function that maps x to a and y to ν(y) if y = x.

• Rule (¬B a ):

If (M, ν) |= T (σ M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i ¬B a ψ), then M ⊗ M ′ 1 ⊗ . . . ⊗ M ′ i , (ν(σ), w ′ 1 , . . . , w ′ i ) |= ¬B a ψ. So, there exists (u, u ′ 1 , . . . , u ′ i ) ∈ R a (ν(σ), w ′ 1 , . . . , w ′ i ) such that M⊗ M ′ 1 ⊗ . . . ⊗M ′ i , (u, u ′ 1 , . . . , u ′ i ) |= ¬ψ. So, u ∈ R a (ν(σ)), the sequence (M ′ 1 , u ′ 1 ), . . . , (M ′ i , u ′ i ) is executable in (M, w) and M ⊗ M ′ 1 ⊗ . . . ⊗ M ′ i , (u, u ′ 1 , . . . , u ′ i ) |= ¬ψ. Let σ new be a new fresh label and let ν + := ν(σ new → u). Then, we have that (M, ν + ) |= T (σR a σ new ), (M, ν + ) |= T (σ new M ′ 1 , u ′ 1 ; . . . ; M ′ i , u ′ i ) and (M, ν + ) |= T (σ new M ′ 1 , u ′ 1 ; . . . ; M ′ i , u ′ i ¬ψ). So, the rule (¬B ) is sound. • Rule (B a ): If (M, ν) |= T (σ M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i B a ϕ) and (M, ν) |= T (σ R a σ 1 ), then M ⊗ M ′ 1 ⊗ . . . ⊗ M ′ i , (ν(σ), w ′ 1 , . . . , w ′ i ) |= B a ϕ and ν(σ)R a ν(σ 1 ). Let u ′ 1 ∈ R a (w ′ 1 ), . . . , u ′ i ∈ R a (w ′ i ). Either the sequence (M 1 , u ′ 1 ), . . . , (M ′ i , u ′ i ) is executable in (M, ν(σ 1 )) or it is not. In • if ¬ψ ∈ CL(ϕ), then ψ ∈ CL(ϕ); • if χ ∧ ψ ∈ CL(ϕ), then χ, ψ, ¬χ, ¬ψ ∈ CL(ϕ); • if B a ψ ∈ CL(ϕ), then ¬ψ, ψ ∈ CL(ϕ); • if [M ′ , w ′ ]ψ ∈ CL(ϕ)
, then ψ, ¬ψ ∈ CL(ϕ) and all the precondition formulas are in CL(ϕ), that is, if M ′ = (W ′ , R ′ , P re), then for all w ′ ∈ W ′ , P re(w ′ ) ∈ CL(ϕ);

• if [π ∪ γ]ψ ∈ CL(ϕ) then [π]ψ, [γ]ψ ∈ CL(ϕ).
The cardinality of the closure CL(ϕ) is linear in |ϕ|. Now let us give an upper bound for the cardinality of the set of possible lists Σ ′ of pointed event models. Such a list is of the following form

M ′ 1 , u ′ 1 , . . . , M ′ n , u ′ n ,
where: • n is bounded by the size of ϕ;

• M ′ i are event models that appear in the formula ϕ; • each u ′ i are possible events of M ′ i . Let us assume that n is chosen. The number of event models appearing in ϕ is bounded by |ϕ|, so there are at most |ϕ| choices for M ′ 1 . The number of possible choices for u ′ 1 is bounded by |M ′ 1 | ≤ |ϕ|. So there are at most |ϕ| choices for u ′ 1 . Hence, there are at most |ϕ| 2 choices for M ′ 1 , u ′ 1 . We can repeat the same reasoning for counting the number of choices for

M ′ 2 , u ′ 2 , . . . , M ′ n-1 , u ′ n-1 and M ′ n , u ′ n .
By multiplying all the number of choices, we see that there are at most (|ϕ| 2 ) n = O(|ϕ| 2|ϕ| ) possible lists Σ ′ for a given n. Since there are at most |ϕ| choices for n, there are at

most |ϕ| × O |ϕ| 2|ϕ| = O |ϕ| 2|ϕ|+1 = O 2 |ϕ| 2 possible lists Σ ′ . So, the number of possible sequences Σ ′ is exponential in the size of ϕ.
Combining these two intermediary results, we obtain that the set of all possible terms in a given node of T is in O (|ϕ|) × O 2 |ϕ| 2 = O 2 |ϕ| 2 , so at most exponential in the size of ϕ.

Proof of 2 The worse case is when there is an exponential number of terms of the form (σ Σ ′ ¬B a ψ). Indeed, in that case, an exponential number of new symbols σ new will arise from the applications of rule (¬B a ) on terms concerning σ. In other words, the arity of T is at most exponential in the size of ϕ.

Proof of 3 First, we warn the reader about the following fact: it is false that the modal depth of the subformulas decreases strictly from a node to its children, because of the rules ( ) and (⊗). The idea is that once all modal operators of the form B a ψ and [M ′ , w ′ ]ψ have been treated, the rules ( ) and (⊗) stop to be applicable for the corresponding formulas.

Let us define a quantity that is strictly decreasing during the execution of the tableau method. Let us consider a given term (σ Σ ′ ψ). The size of a term t = (σ Σ ′ ψ) is defined by

|t| = 1 + (M ′ ,w ′ )∈Σ ′ (|M ′ | + 1) + |ψ| where | | = | ⊗ | = 1 and (M ′ , w ′ ) ∈ Σ ′ means that the event model (M ′ , w ′ ) appears in Σ ′ .
Now, following Fitting's terminology [Fitting, 1983], all the rules of the tableau method are strictly analytic: all terms t that are in the denominator of a rule are such that there exists a term c in the numerator such that |t| < |c|. For instance let us consider the following rule:

(σ Σ ′ [M ′ , w ′ ]ϕ) (σ Σ ′ ; M ′ , w ′ ⊗) (σ Σ ′ ; M ′ , w ′ ) (σ Σ ′ ; M ′ , w ′ ¬ϕ) ([M ′ , w ′ ]) We have |(σ Σ ′ ; M ′ , w ′ ⊗)| < A, |(σ Σ ′ ; M ′ , w ′ )| < A and |(σ Σ ′ ; M ′ , w ′ ¬ϕ)| < A where A = |(σ Σ ′ [M ′ , w ′ ]ϕ)|.
To each node of the tree T that corresponds to a given symbol σ, we attach the following quantity: the maximum of |t| where t is a term concerning σ. As rules are strictly analytic, this quantity will decrease strictly on a branch of the tree. Furthermore, for the root of the tree, this quantity is |(σ 0 ǫ ϕ)| = 1 + |ϕ|. As this quantity is positive, it proves the terminaison of the procedure and also that the depth of the tree T is linear in the size of ϕ.

To sum up, the depth of the tree T is linear whereas the arity may be exponential. As a consequence, the tree T has at most an exponential number of nodes in the size of ϕ. Indeed, because of point 1, the number of nodes of the tree T is in O

2 |ϕ| 2 |ϕ| = O 2 |ϕ| 3 which is expo- nential in the size of ϕ.
Moreover, constructing such a tree T can be done non-deterministically in an exponential amount of time, for each execution of the tableau method. So, the procedure is in NEXPTIME.

Lower bound

We prove that the algorithm based on our tableau method of the previous section is optimal in terms of computational complexity. To do so, we prove that the satisfiability problem of L DEL is NEXPTIME-hard by reducing a NEXPTIME-complete tiling problem to it [Boas, 1997].

Let C be a countable and infinite set of colors. A tile type t is a 4-tuple of colors, denoted t = (lef t(t), right(t), up(t), down(t)) ∈ C 4 . We consider the following tiling problem: Input: a finite set T of tile types, t 0 ∈ T and a natural number k written in its binary form.

Output: yes iff there exists a function τ from {0, . . . k} 2 to T satisfying the following constraints: τ (0, 0) = t 0 ;

(1) for all x ∈ {0, . . . , k} and y ∈ {0, . . . , k -1}:

up(τ (x, y)) = down(τ (x, y + 1));

(2) for all x ∈ {0, . . . , k -1} and y ∈ {0, . . . , k}: right(τ (x, y)) = lef t(τ (x + 1, y)).

(3)

In other words, the problem is to decide whether we can tile a (k + 1) × (k + 1) grid with the tile types of T , t 0 being placed onto (0, 0).

Σ 14 := Σ 13 ∪ (σ 2 ǫ ), (σ 2 ǫ ⊤)   (¬∧,¬¬) Σ 15 := Σ 14 ∪ (σ 2 ǫ p)   (¬Ba) Σ 16 := Σ 15 ∪    (σ 2 R 2 σ 3 ) (σ 3 M ′ 1 , u ′ 1 ; M ′ 2 , u ′ 2 ) (σ 3 M ′ 1 , u ′ 1 ; M ′ 2 , u ′ 2 ¬p)      (→¬p) Σ 17 := Σ 16 ∪ (σ 3 ǫ ¬p)   ( ) Σ 18 := Σ 17 ∪ (σ 3 M ′ 1 , u ′ 1 ) (σ 3 M ′ 1 , u ′ 1 ; M ′ 2 , u ′ 2 ¬(p ∧ ¬p))   ( ) Σ 19 := Σ 18 ∪ (σ 3 ǫ ¬(p ∧ ¬p)   (¬∧,¬¬) Σ 20 := Σ 19 ∪ (σ 3 ǫ ¬p)   (¬∧,¬¬) Σ 21 := Σ 20 ∪ (σ 3 M ′ 1 , u ′ 1 ; M ′ 2 , u ′ 2 ¬p)   (→¬p)
Σ 22 := Σ 21 ∪ (σ 3 ǫ ¬p)

Figure 5: An open branch of the tableau for ϕ Proof. Without loss of generality, we assume that k = 2 n . Let us consider an instance of the NEXPTIME-hard tiling problem described above. Our goal is to provide a polynomial translation from this instance to an instance of the satisfiability problem of L DEL .

The idea is to embed two identical k × k-tilings into a single tree. Each leaf of the tree represents both a position (x 1 , y 1 ) in the first tiling and a position (x 2 , y 2 ) in the second tiling. We need to encode two identical tilings because, in order to check constraints 2 and 3, we will need to refer to the tile located to the right or to the left of a given position in a tiling, and also to refer to the tile located above or below it. This is hardly possible if we encode a single tiling at the leafs of a tree, because we would need to 'backtrack' in the tree to access these other positions.

We start by showing how to encode two identical tilings at the leafs of a tree. Then we will show how to express the three constraints 1, 2 and 3 in the definition of a tiling.

1. The coordinates (x 1 , y 1 ) and (x 2 , y 2 ) of the two tilings are represented by the valuations of atomic propositions p 0 , . . . , p 4n-1 . More precisely, the set X 1 = {p 0 , . . . , p n-1 } contains the atomic propositions encoding the binary representation of the integer x 1 , Y 1 = {p n , . . . , p 2n-1 } contains the atomic propositions encoding the binary representation of the integer y 1 , X 2 = {p 2n , . . . , p 3n-1 } contains the atomic propositions encoding the binary representation of the integer x 2 , and Y 2 = {p 3n , . . . , p 4n-1 } contains the atomic propositions encoding the binary representation of the integer y 2 . For instance, for n = 4, the coordinates (x 1 , y 1 ) = (4, 3) and (x 2 , y 2 ) = (11, 2) are represented at a leaf of the tree by the following valuation. We recall that in binary notation, 4 is represented by 100, 3 is represented by 11, 12 is represented by 1100 and 2 is represented by 10. We then encode the existence of all valuations over X 1 ∪ Y 1 ∪ X 2 ∪ Y 2 with the following formula:

¬p 0 ,
l<4n B l a B a p l ∧ B a ¬p l ∧ i<l ((p i → B a p i ) ∧ (¬p i → B a ¬p i )) . ( 4
)
Formula 4 is true at a pointed epistemic model iff this pointed epistemic model is bisimilar up to modal depth 4n to a binary tree of depth 4n whose leafs contain all the possible valuations associated to p 0 , . . . , p 4n-1 .

In order to check Constraints 2 and 3 in the definition of a tiling, we will need to refer to the tile located to the right or to the left of a given position in a tiling, and also to refer to the tile located above or below it. The following formulas encode the fact that any pair of coordinates (x 1 , x 2 ) and (y 1 , y 2 ) of the two tilings satisfy the properties x 1 = x 2 , x 1 = x 2 + 1, y 1 = y 2 and y 1 = y 2 + 1 respectively:

(x 1 = x 2 ) i<n (p i ↔ p i+2n ) (5) (y 1 = y 2 ) n≤i<2n (p i ↔ p i+2n ) (6) (x 1 = x 2 + 1) i<n j<i (p j+2n ↔ p j ) ∧ ¬p i+2n ∧ p i ∧ i<j<n (p j+2n ∧ ¬p j ) (7)
(y 1 = y 2 + 1)

n≤i<2n n≤j<i (p j+2n ↔ p j ) ∧ ¬p i+2n ∧ p i ∧ i<j<2n (p j+2n ∧ ¬p j ) (8)
The tile types of the first tiling are represented by atomic propositions 1 t and the tile types of the second tiling are represented by atomic propositions 2 t ′ , where t and t ′ range over T . They hold at a leaf of the tree whose coordinates correspond to (x 1 , y 1 ) and (x 2 , y 2 ) when the tile type of the first tiling at coordinate (x 1 , y 1 ) is t and the tile type of the second tiling at coordinate (x 2 , y 2 ) is t ′ .

Formulas 9 and 10 below encode the fact that, at each leaf of the tree, there is exactly one tile type for the first tiling and exactly one tile type for the second tiling. Formula 11 below encodes the fact that when these two pairs of coordinates coincide, that is when x 1 = x 2 and y 1 = y 2 ,

RR n°8164

then the tile type of the first tiling and the tile type of the second tiling are identical.

B 4n

a t∈T

1 t ∧ t∈T 2 t (9) B 4n a {(1 t → ¬1 t ′ ) ∧ (2 t → ¬2 t ′ ) | t, t ′ ∈ T, t = t ′ } (10) B 4n a (x 1 = x 2 ) ∧ (y 1 = y 2 ) → t∈T (1 t ↔ 2 t ) (11)
However, it may be the case that in the tree, two different leafs with the same valuation have different tile types. Therefore, we also have to constrain the tree so that the leafs denoting the same position in the first tiling (resp. second tiling) contain the same tile type for the first tiling (resp. second tiling). This is expressed by the following two formulas:

[M ′ p0 ∪ M ′ ¬p0 ] . . . [M ′ p2n-1 ∪ M ′ ¬p2n-1 ] t∈T B 4n a 1 t (12) [M ′ p2n ∪ M ′ ¬p2n ] . . . [M ′ p4n-1 ∪ M ′ ¬p4n-1 ] t∈T B 4n a 2 t ( 13
)
where for a given a literal ℓ (p or ¬p), the pointed event model

M ′ ℓ = (W ′ , R ′ , P re, w ′ 0 ) is defined as follows: W ′ = {w ′ i | i ∈ {0, . . . , 4n}}; R ′ a = {(w ′ i , w ′ i+1 ) | i ∈ {0, .
. . , 4n -1}}; and P re(w ′ i ) = ⊤ for all i < 4n and P re(w ′ 4n ) = ℓ. In formula 12, the sequence of pointed event models

[M ′ p0 ∪ M ′ ¬p0 ] . . . [M ′ p2n-1 ∪ M ′ ¬p2n-1
] non-deterministically picks a valuation v over X 1 ∪ Y 1 and selects the branches of the tree whose leafs satisfy this valuation. Then, the formula t∈T B 4n a 1 t checks that these leafs, which denote the same position in the first tiling, are of the same tile type t. Likewise with formula 13 for the second tiling.

So, with formulas 9, 10, 11, 12 and 13, we have encoded in the tree two identical tilings in a single tree. Importantly, note that the tree is defined so that each leaf refers to two coordinates of the tiling, which can possibly be identical or consecutive. It is this feature which will allow us to express that constraints 2 and 3 of the definition of a tiling hold.

2. Constraints 1, 2 and 3 of the definition of a tiling are expressed respectively by the following formulas:

B 4n a i<4n ¬p i → t 0 (14) B 4n a (x 1 = x 2 ) ∧ (y 1 = y 2 + 1) → t∈T 1 t → {2 t ′ | t ′ ∈ T, down(t ′ ) = up(t)} (15) B 4n a (x 1 = x 2 + 1) ∧ (y 1 = y 2 ) → t∈T 1 t → {2 t ′ | t ′ ∈ T, lef t(t ′ ) = right(t)} (16)
As we said at the beginning of the proof, these two constraints motivate the need to encode two tilings: for a given position in a tiling, we need to refer to the tile located to the right or to the left of it, and to refer to the tile located above or below it. This would not be possible with our epistemic language if the tiling was encoded by a single tree.

The sequence and 'star' iteration operators

The sequence and 'star' iteration operators are constructions enabling to build complex programs as in Propositional Dynamic Logic (PDL [START_REF] Harel | Dynamic Logic[END_REF]). The truth conditions are defined as follows: We do not know about the computational complexity of the model-checking problem when the operator [π * ]ϕ is added to the language. In fact, we do not even know whether it is decidable. The computational complexity of the satisfiability problem remains the same when the sequential composition operator is added. However, adding a 'star' operator makes the satisfiability problem undecidable. This result is not really surprising, it is a direct corollary of the result of [START_REF] Miller | The undecidability of iterated modal relativization[END_REF] stating that Public Announcement Logic with the 'star' operator is already undecidable.

The common belief operator

We may extend the language with the common belief operator C G ϕ, where G ⊆ AGT. The truth conditions are defined as follows:

M, w |= C G ϕ iff for all v ∈ a∈G R a + (w), M, v |= ϕ
Intuitively, C G ϕ is an abbreviation of an infinite conjunction [START_REF] Fagin | Reasoning about knowledge[END_REF]:

C G ϕ = E 1 G ϕ ∧ E 2 G ϕ ∧ E 3 G ϕ ∧ . . .
, where E k G ϕ is defined inductively as follows: E 1 G ϕ = a∈G B a ϕ and

E k+1 G ϕ = E 1 G E k G ϕ.
We do not know about the computational complexity of the satisfiability problem when the common belief operator is added to the language L DEL . However, we know that it is decidable and that the language with common belief operator is more expressive than the epistemic language L EL with common belief [START_REF] Baltag | The logic of common knowledge, public announcement, and private suspicions[END_REF], Baltag et al., 1999].

Implementation

There exist two implementations of our decision problems:

1. The model-checker DEMO [van Eijck, 2007], standing for Dynamic Epistemic MOdeling tool, can evaluate formulas of L DEL in epistemic models, display graphically epistemic models, event models and updates of epistemic models by event models, translate formulas of L DEL to formulas of PDL. DEMO is written in Haskel and has been applied in [van Ditmarsch et al., 2005] and[van Ditmarsch et al., 2006]. Also, it has been used to investigate the pros and cons of modeling some well-known problems of computer security within the DEL framework [van Eijck and Orzan, 2007].

2. The program Aximo [START_REF] Richards | Aximo: Automated axiomatic reasoning for information update[END_REF], written in C++, implements an algorithm for proving properties of interactive multi-agent scenarios encoded in epistemic systems. Epistemic systems provide an algebraic semantics to DEL and were developed together with a sound and complete sequent calculus [START_REF] Baltag | Epistemic actions as resources[END_REF].

Concluding remarks

Our work contributes to the proof theory and the study of the computational complexity of DEL, which has been rather neglected so far. Although our results show that our decision problems are not tractable, it turns out that the DEMO implementation does not fare worse and often even better in terms of time of execution than other model-checkers modeling the same problems, without resorting to the DEL methodology [van Ditmarsch et al., 2006].

We still need to investigate whether or not the computational complexity remains the same when we consider other epistemic logics as the basis of DEL, such as S5. Moreover, our results rely on the fact that we use the union operator in the language, an open problem is to obtain similar results without this operator. Finally, we plan to implement our tableau method in LotrecScheme [Schwarzentruber, 2011].

  and |π ∪ γ| = 1 + |π| + |γ|. Definition 7 (Truth conditions). Given an epistemic model M = (W, R, V ) and a formula ϕ ∈ L DEL , we define inductively the satisfaction relation |=⊆ W × L DEL as follows:

Figure 3 :

 3 Figure 3: PSPACE algorithm for model checking

Figure 4 :

 4 Figure 4: Tableau rules

Theorem 4 .

 4 The satisfiability problem of L DEL is NEXPTIME -hard.

M

  , w |= [π; γ]ϕ iff M, w |= [π][γ]ϕ M, w |= [π * ]ϕiff there is a finite sequence π; . . . ; π such that M, w |= [π; . . . ; π]ϕ

  In this pointed epistemic model, it holds that M, w |= p ∧ B 1 p: Wellington 'knows' that he wants to attack at dawn. It also holds that M, w |= ¬B 2 p: Blücher does not 'know' that Wellington wants to attack at dawn; and M, w |= B 1 ¬B 2 p: Wellington 'knows' that Blücher does not 'know' that he wants to attack at dawn.

  p 1 , ¬p 2 , ¬p 3 4 ¬p 4 , ¬p 5 , p 6 , p 7 3 p 8 , p 9 , ¬p 10 , ¬p 11 12 ¬p 12 , ¬p 13 , p 14 , ¬p 15 2

RR n°8164

Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

Acknowledgment. We thank the reviewers for their comments and Sophie Pinchinat for discussions.

the second case, (M, ν) |= T (σ M ′ 1 , w ′ 1 ; . . . ; M ′ i , w ′ i ⊗) by definition of |= T and the denominator is interpretable. If the sequence is executable, then (M, ν)

So, in the first case, the denominator is also interpretable. Hence, the rule (B a ) is sound.

Proposition 2 (Completeness). Let ϕ ∈ L DEL . If |= ϕ, then ⊢ ϕ.

Proof. We prove it by contrapositive. Suppose that there is a tableau for ϕ that has an open branch. We prove that there is a pointed epistemic model (M, w) such that M, w |= ϕ. Let Γ f be the set of tableau terms carried by the end node of the open branch. We define the pointed epistemic model (M, w) = (W, R, V, w) as follows:

For all n ∈ N, let P(n) be the induction hypothesis defined as follows: P(n)="let ϕ ∈ L DEL and let (M ′ 1 , w ′ 1 ), . . . , (M ′ i , w ′ i ) be i pointed event models such that i k=1

In that case, we necessarily have that ϕ = p for some p ∈ ATM and i = 0. So, (σ ǫ p) ∈ Γ f , and therefore M, w σ |= p by definition of M. n + 1. If i = 0, then by saturation of rule ( ), we have that

. So, we have proved the first part of the induction step. Now, we prove the second part, namely that

We only prove it for i = 0, the case i = 0 being similar. We reason by cases depending on the structure of ϕ. Note that we do not introduce another sub-reasoning by induction, we only reason by distinguishing sub-cases.

The case ϕ = ¬p is dealt with similarly. As for the case ϕ = ϕ 1 ∧ ϕ 2 , by saturation of rule (∧), Γ f also contains the tableau term

). So, by Induction Hypothesis, we have that

The case ϕ = ¬(ϕ 1 ∧ ϕ 2 ) and ϕ = ¬¬ψ are proved similarly.

• If ϕ = ¬B a ψ, then by saturation of rule (¬B a ), we have the existence of σ new such that (σR a σ new ) ∈ Γ f and the existence of

We are going to show that

In the first case, by saturation of rule (⊗), either there is

So, in both cases, we reach a contradiction. Hence,

We have proved this induction step.

In the first case, by saturation of the rule (⊗), either it holds that (σ

) ∈ Γ f , the branch carrying Γ f would be closed. Therefore, the subcase where

Then, by saturation of rule (¬¬), we also have that

we have that the sequence

]ψ, then one can prove this induction step similarly to the second case of the previous induction step (ϕ = [M ′ , w ′ ]ψ).

• If ϕ = [π ∪γ]ψ, then by saturation of ([π ∪γ]), we have that

Then, by Induction Hypothesis, the sequence

Example 4. We prove with our tableau method that the formula ϕ

2 are defined in Example 2. In Figure 5, an open branch of the tableau tree for ϕ is represented. The set Σ 22 is saturated: no more tableau rule is applicable. From this branch, we may extract a pointed epistemic model (M, σ 0 ) such that M, σ 0 |= ϕ.

NEXPTIME-membership

Theorem 3. The satisfiability problem of L DEL is in NEXPTIME.

Proof. Let ϕ ∈ L DEL and let T be the tableau tree for ϕ. The tableau method is a non-deterministic procedure. Indeed, rules (¬∧), (B a ), (⊗), (¬[π ∪ γ]) are non-deterministic rules. Each node of the tree T is the saturation of all rules concerning a specific symbol σ: (∧), (¬¬), (¬∧), (⊥), (← p ), (← ¬p ), (¬[M ′ , w ′ ]), ([M ′ , w ′ ]), ( ), (⊗), ([π ∪ γ]), (¬[π ∪ γ]). There is an edge from a node corresponding to σ to a node corresponding to σ ′ if (σ R a σ ′ ) is in the set of terms in the current execution. In other terms, an edge corresponds to an application of the rule (¬B a ). Rule (B a ) is a propagation rule: from terms concerning σ, it adds terms concerning σ ′ where (σ R a σ ′ ). In this proof, we show that:

1. at each node of T concerning a specific symbol σ, there are at most an exponential number of terms;

2. the arity of T is at most exponential;

3. the depth of T is linear.

Each step of the algorithm is an application of a rule and it will add new terms. So, the construction of the tree T is done non-deterministically in exponential time.

Proof of 1 Except terms of the form (σ R a σ ′ ), all other terms are of the form (σ Σ ′ ψ) where:

• ψ is a formula in a closure CL(ϕ) of the initial formula ϕ (this includes the fact that ψ can be in the closure of a precondition appearing in an event model of ϕ);

Formally, the closure CL(ϕ) of a formula ϕ is the smallest set of formulas containing ϕ and satisfying all those constraints:

One can then check that there exists a tiling for the instance of the tiling problem iff the formula ϕ, which is the conjunction of fomulas 4, 9, 10, 11, 12, 13, 14, 15, and 16 is satisfiable in L DEL .

3. Finally, we show that the reduction is polynomial in the size of the instance of the tiling problem. The formula of Equation 4 is of size O(n 2 ). The formulas of Equations 12, 13 are of size O(n 2 + |T | × n). The other formulas are clearly of size polynomial in the size of the input, so the result follows. Importantly, note that if we decided to rewrite the formulas 12 and 13 without using the union operator ∪, then the corresponding formula would be exponential in the size of the input. So, the use of the union operator is really crucial in order to have a polynomial reduction from the tiling problem to our satisfiability problem.

Related work 5.1 Theory

There exists a terminating tableau method solving the satisfiability problem of L DEL [Hansen, 2010].

This method writes subformulas by applying the reduction axioms [Baltag and Moss, 2004, p. 214]. It is therefore mainly a variant of the tableau method of classical multi-modal logic K n . Even if we know that tr blows up exponentially the size of the input formula, the computational complexity of this tableau method is not studied. In this section, we review the existing results about computational complexity of DEL.

Public Announcement Logic (PAL)

Public Announcement Logic (PAL) [Plaza, 1989] is an extension of epistemic logic with a dynamic operator [ψ!]ϕ whose truth conditions are defined as follows:

where M ψ is the restriction of M to the worlds which satisfy ψ. PAL is a fragment of DEL: the language of PAL is L DEL restricted to event models consisting of a single possible event with reflexive arrows for all agents. There is a gap between PAL and DEL in terms of computational complexity, both for the model checking problem and the satisfiability problem. Indeed, the model checking of PAL is in P (also with common belief) [van Benthem and Kooi, 2004] and the satisfiability problem for PAL is PSPACE-complete [Lutz, 2006]. Despite the fact that there exist reduction axioms for PAL, it is difficult to implement a direct translation using reduction axioms. In fact, there are properties that can be expressed exponentially more succinctly in PAL than in epistemic logic [START_REF] French | Succinctness of epistemic languages[END_REF]. Note that there exist PSPACE tableau methods for solving the satisfiability problem in PAL [de Boer, 2007, Balbiani et al., 2010].

DEL-sequents

DEL-sequents [Aucher, 2011] are triples of the form ϕ, ϕ ′ |= ϕ ′′ where ϕ, ϕ ′′ ∈ L EL and ϕ ′ is a formula of a language for event models. A DEL-sequent ϕ, ϕ ′ |= ϕ ′′ holds when for all pointed epistemic model (M, w) such that M, w |= ϕ, for all pointed event model (M ′ , w ′ ) such that M ′ , w ′ |= ϕ ′ , if (M ′ , w ′ ) is executable in (M, w), then M ⊗ M ′ , (w, w ′ ) |= ϕ ′′ . The problem of determining whether a DEL-sequent holds is NEXPTIME-complete and there exists a tableau method for it. DEL-sequents have been generalized to sequences of the form ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n i 1 ψ and ϕ 0 , ϕ ′ 1 , ϕ 1 , [4] . . . , ϕ ′ n , ϕ n i 2 ψ ′ . The corresponding satisfiability problem is also NEXPTIME-complete [START_REF] Aucher | Generalized DEL-sequents[END_REF].


Khaled Jerbi

Mickael Raulet

Olivier Deforges

Mohamed Abid

AUTOMATIC GENERATION OF SYNTHESIZABLE HARDWARE IMPLEMENTATION FROM HIGH LEVEL RVC-CAL DESCRIPTION

Keywords: RVC-CAL, Data flow computing, CAL compiler, Automatic transformation

Data process algorithms are increasing in complexity especially for image and video coding. Therefore, hardware development using directly hardware description languages (HDL) such as VHDL or Verilog is a difficult task. Current research axes in this context are introducing new methodologies to automate the generation of such descriptions. In our work we adopted a high level and target-independent language called CAL (Caltrop Actor Language). This language is associated with a set of tools to easily design dataflow applications and also a hardware compiler to automatically generate the implementation. Before the modifications presented in this paper, the existing CAL hardware back-end did not support some high-level features of the CAL language. The generated HDL language had to be manually transformed to be synthesizable. In this paper, we introduce a general automatic transformation of CAL descriptions to make these structures compliant and synthesizable. This transformation analyses the CAL code, detects the target features and makes the required changes to obtain synthesizable code while keeping the same application behavior. This work resolves the main bottle-neck of the hardware generation flow from CAL designs.

INTRODUCTION

Watching and exchanging videos on the Internet or mobile gadgets by billions of people all over the world is the current phenomenon. Moreover, user requirements of high quality are also growing which has caused a noteworthy increase in the complexity of the algorithms of video codecs. To be used, these algorithms have to be implemented on a target architecture that specifies the description language depending on its nature: hardware or software. In this context, CAL Actor Language [START_REF] Eker | CAL Language Report[END_REF] was introduced in the Ptolemy II project [START_REF] Brooks | PtolemyII -heterogeneous concurrent modeling and design in java (volume 1: Introduction to ptolemyII)[END_REF] as a dataflow target agnostic language. The MPEG community standardized the RVC-CAL language [START_REF]Information Technology -MPEG systems technologies -Part 4: Codec Configuration Representation[END_REF] in the MPEG-RVC (Reconfigurable Video Coding) standard [START_REF] Bhattacharyya | Overview of the mpeg reconfigurable video coding framework[END_REF]. This standard provides a framework to describe the different functions of a codec as a network of functional blocks developed in RVC-CAL and called actors. Xilinx developed a hardware compiler called OpenForge1 [START_REF] Gu | Exploring the concurrency of an MPEG RVC decoder based on dataflow program analysis[END_REF] that generates hardware implementation using an Intermediate Representation (IR) called XLIM. The bottle-neck of hardware generation using OpenForge is the fact that RVC-CAL code generally contains high level structures that are not compatible with this hardware compiler.

On the other hand, an RVC-CAL compiler called Orcc2 [START_REF] Janneck | Reconfigurable video coding a stream programming approach to the specification of new video coding standards[END_REF] is in development as a tool that compiles a network of actors and generates several backends: C, LLVM, Java and notably Xlim. Therefore, we proposed to work on the IR of Orcc to add automatic transformations making any RVC-CAL design synthesizable.

This paper presents an automatic transformation of RVC-CAL code to modify the unsupported structures in the IR of Orcc. The transformation tool analyzes the RVC-CAL code and achieves the required transformations to obtain synthesizable code what ever the complexity of the considered actor. In section 2, we explain the main notions of the RVC-CAL language and its functioning structures and mechanisms. The proposed transformation process is detailed in section 3 and finally hardware implementation results of MPEG4 Part2 decoder case study are presented in section 4.

BACKGROUND

The execution of an RVC-CAL code is based on the exchange of data tokens between computational entities called actors. Each actor is independent from the others since it has its own parameters and finite state machine if needed. Actors are connected to form an application or a design, this connection is insured by FIFO channels. Executing an actor is based on firing elementary functions called actions. This action firing may change the state of the actor in case of an FSM. An RVC-CAL dataflow model is shown in the network of Figure 1. The actor execution, so called firing, is based on the Dataflow Process Network (DPN) principle [START_REF] Lee | Dataflow process networks[END_REF] derived from the Kahn Process Network (KPN) [START_REF] Kahn | The Semantics of a Simple Language for Parallel Programming[END_REF]. Let Ω be the universe of all tokens values exchanged by the actors and S=Ω* the set of all finite sequences in Ω. We denote the length of a sequence s ∈ S k by |s| and the empty sequence by λ. Considering an actor with m inputs and n outputs, S m and S n are the set of m-tuples and n-tuples consumed and produced. For example,

s 0 =[λ,[t 0 ,t 1 ,t 2 ]] and s 1 =[[t 0 ],[t 1 ]]
are sequences of tokens that belong to S 2 and we have

|s 0 |=[0,3] and |s 1 |=[1,1]. A firing rule is called multi-token if f : ∃e ∈ |s| : e > 1 otherwise it is called a mono-token rule.
The limitation of Openforge is the fact that it does not support multi-token rules which are omnipresent in most actors. Our work consists of automatically transforming the data consumption from multi-token to mono-token while preserving the same actor behavior: firing rules and transitions are detailed below.

Actor firing

A dataflow actor is defined with a pair < f, R > such as: * f : S m → S n is the firing function * R ⊂ S m are the firing rules * For all r ∈ R, f (r) is finite An actor may have N firing rules which are finite sequences of m patterns (one for each input port). A pattern is an acceptable sequence of tokens for an input port. It defines the nature and the number of tokens necessary for the execution of at least one action. RVC-CAL also introduces the notion of guard as additional conditions on tokens values. An example of firing rule r j in S 2 is:

g j,k : [x]|x > 0 r j = [t 0 ∈ g j,k , [t 1 , t 2 , t 3 ]]
which means that if there is a positive token in the FIFO of the first input port and 3 tokens in the FIFO of the second input port then the actor will select and execute a fireable action. An action is fireable or schedulable if f :

• The execution is possible in the current state of the FSM (if an FSM exists)

• There are enough tokens in in the input FIFO

• A guard condition returns true An action may be included in a finite state machine or untagged making it higher priority than FSM actions.

Actor transition

The FSM transition system of an actor is defined with < σ 0 , Σ, τ, ≺> where Σ is the set of all the states of the actor, σ 0 is the initial state, ≺ is a priority relation and τ ⊆ Σ × S m × S n × Σ is the set of all possible transitions. A transition from a state σ to a state σ ′ with a consumption of sequence s ∈ S m and a produced sequence s ′ ∈ S n is defined with (σ, s, s ′ , σ ′ ) and denoted:

σ s →s ′ ---→ τ σ ′
To solve the problem of the existence of more than one possible transition in the same state, RVC-CAL introduced the notion of priority relation such as for the transitions t 0 , t 1 ∈ τ , t 0 a higher priority than t 1 is written t 0 ≻ t 1 . As explained in [START_REF] Eker | A structured description of dataflow actors and its application[END_REF] a transition σ

s →s ′ ---→ τ σ ′ is enabled if f : ¬∃σ p →q ---→ τ σ ′′ ∈ τ : p ∈ S ∧ σ s →s ′ ---→ τ σ ′′ ≻ σ s →s ′ ---→ τ σ ′
This section presented and explained the main RVC-CAL principles. In the next section we present an automatic transformation as a solution to avoid these limitations without changing the overall macro-behavior of the actor.

THE PROPOSED METHOD

As shown in Figure 2, our transformation acts on the IR representation of the front-end. The HDL implementation is later generated using the Xlim back-end of Orcc followed by OpenForge.

Front-end

Xlim Back-end

Automatic transformation

RVC-CAL

IR Xlim

OpenForge Verilog Fig. 2. Automatic transformation localization in Orcc compiling process

Actor transformation principle

Let us consider an actor with a multi-token firing rule r ∈ S k such as |r| = [r 0 , r 1 , .., r k-1 ], this rule fires a multi-token action a realizing the transition source a -→ τ target and I the set of all input ports. The transformation creates for every input port an internal buffer with read and write indexes and clips r into a set R of k firing rules so that :

∀i ∈ I, ∃!ρ ∈ R :      ρ : S 1 → S 0 |r| = 1 g ρ : IdxW rite i -IdxRead i ≤ sz i
with ρ a mono-token firing rule of an untagged action untagged i , g ρ is the guard of ρ and sz i the size of the associated internal buffer defined as the closest power of 2 of r i . This guard checks that the buffer contains an empty place for the token to read. The multi-token action is consequently removed, and new read actions that read one token from the internal buffers are created. While reading tokens another firing rule may be validated and causes the firing of an unwanted action. To avoid the non-determinism of such a case, we use an FSM to put the actor in a reading loop so it can only read tokens. The loop is entered using a transition action realizing the FSM passage source transition -------→ τ read and has the same priority order of the deleted multi-token action but has no process. The read actions loops in the read state with the transition t = read For example, the actor A of Figure 3 is defined with f : S 3 → S 2 with a multi-token firing rule:

r ∈ S 3 : r = [[t 0 , t 1 ], [t 2 , t 3 , t 4 ], [t 5 ]]. actor A () int IN1, int IN2, int IN3 ==> int OUT1, int OUT2: a: action in1:[in1] repeat 2, IN2:[in2] repeat 3, IN3:[in3] ==> OUT1:[out1], OUT2:[out2] repeat 2 do {treatment} end end

FSM creation cases

We consider an example of an actor defined as f : S 3 → S 2 containing the actions a1..a5 such as a3 is the only action applying a multi-token firing rule r ∈ S 3 . Creating an FSM only for action a3 is not appropriate because a1, a2, a4, a5 will be a higher priority which may not be true. The solution is to create an initial state containing all the actions and add the created FSM macro-block of a3 (previously presented in Figure 4). The resulting FSM is presented in Figure 5. We

RESULTS

The achieved automatic transformation was applied on MPEG4 Part2 intra decoder (see design in Orcc Applications 3 ) which

CONCLUSION

This paper presented an automatic transformation of RVC-CAL from high to low level description. This transformation allows avoiding structures that are not understandable by RVC-CAL hardware compilers. We applied this automatic transformation on the 29 actors of MPEG4 part2 video intra decoder and successfully obtained the same behavior of the multi-token design and a synthesizable hardware implementation. Currently, we are optimizing the transformation to reduce the memory consumption. The transformation process is generalized for all actors. Therefore, improvements are also in progress to customize the transformation depending on the actor complexity analysis. A future work will be the study of the impact of the transformation on the power consumption of the generated implementation.

Fig. 1 .

 1 Fig. 1. CAL actor model

  Then the loop is exited when all necessary tokens are read using a read done action and a transition to the process state t´= read readDone ------→ τ process ≻ t. The treatment of the multi-token action is put in a process action with a transition process process -----→ τ write. The multi-token outputs are also transformed into a writing loop with write actions that store data directly in the output FIFO associated with a transition w = write write ---→ τ write and a write done action that insures the FSM transition w´= write writeDone -------→ τ target ≻ w.

Fig. 3 .

 3 Fig. 3. RVC-CAL code of actor A

Fig. 4 .

 4 Fig. 4. Created FSM macro-block

Fig. 5 .Fig. 6 .

 56 Fig. 5. FSM with created initial state

  Fig. 7. Resulting FSM transformation

Table 1 .

 1 Design area consumption the synthesis of the design, we applied a simulation stream of compressed videos. Table2below presents the timing results of a 176x144 image size video. The synthesis tool indicates a maximum frequency of 27 MHz. Consequently, we applied it as a frequency of the input data stimulus.

	7. Resulting FSM transformation
	contains 29 actors. The HDL generated code was imple-
	mented on a virtex4 (xc4vlx160-12ff1148) and the area con-
	sumption results we obtained are presented in table1. After
	Criterion		value
	Slice Flip Flops	21,624/135,168 (15%)
	Occupied Slices	45,574/67,584 (67%)
	4 input LUTs	68,962/135,168 (51%)
	FIFO16/RAMB16s	14/288 (4%)
	Bonded IOBs	107/768 (13%)
	Image size		176x144
	Output frequency(MHz)	2
	Latency(µs)	328
	processing time(ms/image)	11,7

Table 2 .

 2 Timing results

http://openforge.sf.net

http://orcc.sf.net

ACKNOWLEDGMENTS

Special thanks for Matthieu Wipliez, Damien De Saint-Jorre and Herve Yviquel for their relevant contribution in the transformation code.


A Khodorov

A G Rolo

El-Kebir K Hlil

J Ayres De Campos

O Karzazi

S Levichev

M R Correia

A Chahboun
email: chahboun@fisica.uminho.pt

M J M Gomes

Effect of

come   L'archive ouverte pluridisciplinaire

Introduction:

The use of both charge and spin degrees of freedom in semiconductors is expected to enable a revolutionary class of electronics whose functionality will surpass existing semiconductor technology. Spin electronics combines semiconductor microelectronics with spin-dependent effect that arises from the interaction between electrons and magnetic field. ZnO based materials have shown a big potential for spintronic applications [1][2][3]. ZnO thin films are attracting considerable attention due to its typical properties such as excellent substrate adherence, piezoelectric properties, and high transparency in visible and near infrared region [4]. ZnO with Wurtzite structure is an n-type semiconductor material with both electrical and optical properties due to the deviation from the stoichiometry produced by the existence of intrinsic defects such as oxygen vacancies and Zn vacancies. The current study is motivated the desire to investigate the influence of oxygen on the structural, electrical and magnetic properties of thin doped ZnO, and to identify a mean of better controlling the introduction of defects.

In this work, Zn 0.98 Mn 0.02 O thin layers were grown by pulsed laser deposition (PLD) technique. The structural properties of the grown samples were characterized by X-ray diffraction (XRD) and Raman techniques. Carrier's concentration and conductivity were estimated by Hall effect technique. The magnetic moment was measured as a function of temperature. The O 2 pressure during the growth is shown to govern the structural and the electrical properties of the grown samples. Electronic and magnetic structures were calculated using the Korringa-Kohn-Rostoker coherent-potential-approximation (KKR-CPA) method [5].

Experimental conditions

The Zn 0.98 Mn 0.02 O thin films with thicknesses around 200-300 nm were deposited on glass substrate by PLD technique. The deposition was performed with the help of KrF laser (248 nm) in an oxygen atmosphere at room temperature. The used targets were 2% Mn-doped ZnO, prepared by standard ceramic procedures from ZnO and MnO2 powders [6]. The deposition of Zn 0.98 Mn 0.02 O was performed with energy density of about 5 J/cm 2 at frequency of 1 Hz. Different oxygen pressures were applied during the growth. The details of the studied samples are summarized in table 1.

The structural properties of the films were determined by X-ray diffraction using Cu Kα X-rays. The Raman spectra were obtained at room temperature in backscattering configuration with a Jobin-Yvon LabRaman HR equipped with a Multichannel air cooled (-70 ºC) CCD detector with the 325 nm He-Cd laser line, and the Jobin-Yvon T64000 spectrometer equipped with a cooled CCD detector with the 514 nm laser line. An objective was used to focus the exciting light to 1µm on the surface of the sample. The electrical measurements were made with the standard four probes van der Pauw geometry. Low intensity currents (1 µA -1 mA) were used to avoid the heating of the samples. Hall carriers and Hall mobility were measured at room temperature using a magnetic field of 1 T. The magnetic properties were experimentally investigated by measurements versus temperature under magnetic field fixed at 0.07 T.

Measurements were performed in BS2 magnometer, developped in Luis Néel laboratory of Grenoble (France).

Electronic structure calculation details

Electronic structure calculations were performed within the fully relativistic (KKR) method [5]. To simulate the chemical disorder, coherent potential approximation (CPA) was considered for, and the exchange-correlation energy was used within the framework of the Local Spin Density Approximation. Muffin-tin form for the electron charge density and the crystal potential was assumed. Calculation were performed for Zn 0.98 Mn 0.02 O considered fully disordered systems where the 2b site (1/3, 2/3, 0) is randomly shared by both Zn and Mn atoms with occupation probabilities 0.98 and 0.02 for Zn and Mn atoms, respectively, while 2b site (1/3, 2/3, 0.345) is perfectly ordered and occupied by oxygen. Calculation were also performed on Zn 0.98 Mn 0.02 O 0.8 Vc 0.2 (Vc = vacancy) where 2b sites are shared by oxygen and Vc vacancies with occupation probabilities 0.8 and 0.2, respectively.

Results and discussion

The XRD patterns of the studied samples show dominant peak for the ZnO (002) plane.

The results confirmed that the films are well oriented along the c-axis. Within the XRD detection limit no extra diffraction peaks from any Mn x O y related to secondary phases or impurities can be detected in the XRD pattern. This indicates that these Zn 0.98 Mn 0.02 O thin films show a good cristallinity with a wurtzite structure and a c-axis preferred orientation. The full width at half maximum (FWHM) value of the XRD peak is influenced by many factors such as grain size, stress distribution, and crystal imperfection. Regardless of the influencing factor, the FWHM value is widely used as a negative indicator of film quality. In general, the grain becomes small with the addition of impurities to the matrix material due to the induced defects and imperfections that behave as the source for forming grain boundaries. The mean grain size (D) perpendicular to the reflecting plane in the film estimated by Scherer's formula. Fig. 1 shows the evolution of the grain size as a function of the oxygen pressure for the different studied samples. It is clearly seen that the size increases by increasing the pressure. These results indicate that O 2 pressure during the PLD growth promotes the formation of big grains. At low O 2 pressure, it seems that the lack of O 2 generates dangling bond defects and promotes the formation of small cristallites grains.

In order to investigate the role of defects in the electrical properties of Zn 0.98 Mn 0.02 O thin layers, four probes resistivity and Hall measurements were performed. Fig. 2 shows the evolution of electron concentration (n) and room temperature resistivity as a function of the growth oxygen pressure. For sample A (highest O2 pressure) it was not possible to estimate the carrier's concentration due to the high resistivity of the thin film (see inset Fig. 2).

It is clear that n decreases by increasing O 2 pressure and then lowering defect's concentration. This could be explained by the fact that the thin ZnO films present oxygen vacancies excess which are passivated by increasing the O 2 pressure during the growth. Another feature observed in this graph is the reverse tendency of carrier's mobility (µ) which decreases at low O2 pressure. Indeed, the increase in the n value is generally associated with the decrease in the µ value because of the increased probability of carrier scattering due defects. In fact, high n values were obtained for low O2 pressure and then small Zn 0.98 Mn 0.02 O grain's size. An excess of Zn 2+ donors could be responsible for the observed high n at low O 2 pressure. By increasing the pressure more oxygen vacancy are passivated and less free carriers are available.

Our results are in good agreement with earlier finding which report that O vacancies and Zn interstitial are an important source of n-type conductivity in ZnO [7]. In fact, the oxygen depletion in the doped ZnO indicates the creation of oxygen vacancies. These oxygen vacancies are known to create shallow donor states and thus would add electrons to the system, doping the n-type carriers. We suggest that oxygen depletion owns the sole responsibility of charge neutrality factor in the lattice.

ZnO with wurtzite structure belongs to the space group C 4 6v with A 1 (z)+2B 1 +E 1 (x,y)+2E 2 optical modes at the Γ point of the Brillouin zone. The two E 2 modes are Raman active, the A 1 and E 1 modes are both Raman and infrared active, and the two B 1 modes are silent. Since the A 1 and E 1 modes are polar, they split into LO and transverse optical TO components. According to the selection rules in Raman spectra, only E 2 (E 2 (low) and E 2 (high)) and A 1 (LO) phonon modes can be observed in the unpolarized Raman spectra of the caxis oriented ZnO thin film in the back scattering geometry, and their respective frequencies reported for bulk ZnO are 101, 437, and 574 cm -1 [8,9]. Fig. 3a shows Raman spectra of the studied samples. Two major peaks are clearly seen centered at 527 cm -1 and 571 cm -1 , with large bandwidth which could be explained [10] by Fröhlich electron-phonon scattering. The peak observed at 571 cm -1 in our spectra could be attributed to A 1 (LO). The small observed shift (3 cm -1 ) comparatively to the bulk A 1 (LO) was already reported and explained by electron-phonon interaction [11,12]. The A 1 (LO) mode is known to be related to the defects such as oxygen vacancies, interstitial Zn in ZnO. As a result, we think the appearance of A 1 (LO) mode at 571 cm -1 can be attributed to defects introduced by Mn doping. Additional mode (AMs) in the Raman spectra of Mn doped ZnO samples at 523 cm -1 was reported by Zhong et al. [13] and it was attributed to the Zn related vibration due to Mn incorporation in ZnO. These peaks were considered to have an origin related to the vibration of Mn atoms. The occurrence of AMs is generally assigned to the activation of density of states due to the introduction of Mn on the network [14,15]. These experimental facts strongly support our argument that this mode should be attributed to Mn at substitutional sites. The inset of Fig. 3 shows the evolution of the ratio between the A 1 (LO) mode peak and the AM peak as a function of the grain size. It is well seen that this ratio increases with defects like dangling bonds and vacancies. This confirms that the increase on the intensity of A 1 (LO) mode observed in our samples is related to defects induced in thin ZnO films by the incorporation of Mn ions. These results are in agreement with earlier finding by Exarhos et al. [16] who reported similar results concerning A 1 (LO) mode that they explained by the presence of O 2 vacancies or Zn excess in the deposited films. Another interesting feature was observed in Raman spectra at low frequencies is the appearance of a broad peak centered around 183 cm -1 for samples grown at low O 2 pressure and then high carriers concentration, as it is illustrated in Fig. 3b. In fact, this peak disappears for high resistive samples.

Oxygen depletion is a direct indicator of oxygen vacancies in the samples. However, upon heating in air the oxygen content is recovered. Annealing the samples in air at 600 ºC seems to improve the crystalline quality of the samples by rearrangement of dense crystalline size. Fig. 4 shows the evolution of the Raman spectrum after annealing. It is well seen that the AM mode become more preponderant than the A 1 (LO) mode due to a better incorporation of Mn in ZnO structure. Moreover, the E1 (LO) peak becomes visible. This is demonstrates the improvement of the crystalline quality of the ZnO thin film by the incorporation of oxygen.

Another low intensity Raman band at 380 cm -1 that matches the A 1 (TO) of ZnO which would be forbidden in this geometry. The existence of forbidden modes also could arise from ZnO grains no perfectly aligned along the c-axis after annealing.

Resonant Raman Scattering (RSS) has been proven to be an important tool for the study of basic physical properties of thin films and nanocrystal materials. It provides information about the electronic structure, electron-phonon coupling, and radiation coupling damage. The electron-phonon interaction could be straightly probed by the RRS when the exciting photon energy (E i ) or the scattering photon energy (E s ) is resonant with the electronic interband transition energy of the wurtzite ZnO (E g ~ 3.3 eV < E i ). Fig. 5 shows RSS spectra obtained under resonant excitation by the 325 nm (E i = 3.8 eV) laser line. Up to 6 LO replica are observed for the samples grown at high O 2 pressure, while a higher background PL emission is observed for samples with high defect concentration. Normally, the increase of the density of structural defects leads to the redistribution of the recombination channels from radiative to non-radiative. However, we see that the PL band increases with defect concentrations (small grain size). The increase in UV emission suggests that more electron-hole pairs recombine through radiative recombination than non-radiative, which is in agreement with the decrease in resistivity.

As we have seen with Hall Effect measurements, these samples present high carrier's concentration. One of the reasons could be deep defect levels in the ZnO band gap when excited participate to the PL band. The electron-phonon coupling effect is enhanced when the exciting photon energy is resonant with the electronic states of the material. There are two mechanisms of electron-phonon coupling: (1) deformation potential (2) Fröhlich coupling. The deformation potential is effective when the short range interaction arises between the lattice displacement and the electrons, whereas, the Fröhlich coupling involves the long-range interaction generated by the macroscopic electric field associated with LO phonons. The presence of high carrier's concentration in samples grown at low O2 pressure confirms our arguments to explain the different behaviors observed in Raman spectra and we attributed it to electron-phonons interactions.

Fig. 6 show the magnetic moment against temperature for samples B and D. Sample B (grain size ~ 51nm) shows a beginning of transition at 100K while sample D (grain size ~ 39 nm)

shows such transition at 30K. We were expecting magnetic transition at higher temperature for high defect samples. In fact, oxygen vacancies were suggested to play a major role in the inducement of ferromagnetism [17 -19]. Recents reports also indicate that grain boundaries and intrinsic defects, especially the oxygen vacancies are important factor to enhance the ferromagnetism [20,21]. The absence of any clear effect of defects on the magnetic behavior for the studied samples could be related to low Mn doping.

We have been interested in electronic structure calculations in order to compute both magnetic moment in the cell and magnetic moment localized on Mn atom in disordered ferromagnetic Zn 0.98 Mn 0.02 O system. Density of state of both ZnO and Zn 0.98 Mn 0.02 O systems are reported in Fig. 7. As seen in Fig. 7(b), partial substitution of Zn by Mn introduces a polarization of DOS pointing out to ferromagnetic state of Zn 0.98 Mn 0.02 O. DOS close to Fermi level is originating mainly from like-states Mn(3d) which contribute only to major spins. The computed magnetic moment in the cell is found equal to 0.17  B with substantial value of 3.04  B for magnetic moment localized on Mn atom. The observed lack of magnetism when oxygen pressure was applied during the growth could be explained by the expected vacancies presence on oxygen sites. These vacancies could enhance the films magnetism and their elimination induces a magnetism increase. Mounkachi et al. [22] performed similar calculations on Zn 0.98 Mn 0.02 O 1-y N y and reported that the magnetism is sensitive the hole concentrations on site oxygen. To shed light on this magnetism absence in Zn 0.98 Mn 0.02 O, we performed calculations with Vc (vacancies) on oxygen sites; so that the system is Zn 0.98 Mn 0.02 O 1-y V cy with y=0.1. As expected result, magnetism increases, which means magnetic moment in the cell changes from 0.17 to 0.18  B while Mn magnetic moment increases from 3.04 to 3.15 B .

Conclusion

Thin Zn 0.98 Mn 0.02 O films were grown by PLD technique under O2 pressure. The grown samples were characterized by XRD, Raman spectroscopy and Hall effect. The structural and electrical properties of the grown films were shown to be dramatically influenced by the growth O2 pressure. This influences the Zn 0.98 Mn 0.02 O grain's size and the carrier's concentration in the films. No effect was observed for the magnetic properties and this conclusion is confirmed by electronic structure calculations. Indeed, these calculations point out that the vacancies presence on oxygen sites enhances magnetism in the Zn 0.98 Mn 0.02 O system.

Captions:

Table 1: Details of the studied samples.

Fig. 1 :

 1 Fig. 1: Evolution of the grain size as a function of O 2 growth pressure.

Fig. 2 :

 2 Fig. 2: Evolution of electron concentration as a function of O 2 pressure. The inset shows the evolution of the resistivity against O 2 pressure.

Fig. 3a :

 3a Fig. 3a: Raman spectra of samples A and D. The dashed lines indicate the position 1LO and AM

Fig. 3b :

 3b Fig. 3b: Raman spectra of samples A and D for low frequencies.

Fig. 4 :Fig. 5 :

 45 Fig. 4: Raman spectra of an as grown sample (A) and after annealing in air at 600 ºC

Fig. 6 :

 6 Fig. 6: Magnetic moment as a function of the temperature for samples B and D.

Fig. 7 :

 7 Fig. 7: Total DOS of ZnO (a); Total DOS and l-decomposed DOS of like-states Mn(3d) in the ferromagnetic Zn 0.98 Mn 0.02 O for spin up and spin down (b)

Fig. 1 :Fig. 2 :Fig 3a :

 123a Fig. 1: Evolution of the grain size as a function of O 2 growth pressure.

Fig. 3b :

 3b Fig. 3b: Raman spectra of samples A and D for low frequencies.

Fig. 4 :Fig. 5 :Fig. 6 : 20 Fig. 7 :

 456207 Fig. 4: Raman spectra of an as grown sample (A) and after annealing in air at 600 ºC

Table 1 :

 1 Details of the studied samples.

	Sample Oxygen pressure	FWHM Grain sizes	Resistivity	Carriers
		P ( 10 -3 mbar)	(degree)	D(nm)	ρ (Ohm.cm)	n (10 20 cm -3 )
	A	0.05	0.203	71.3	5.2 10 3	concentrations very high resistance
	B	0.025	0.282	51.4	1.6 10 -2	0.73
	C	0.01	0.319	45.3	4.7 10 -3	0.69
	D	0.005	0.366	39.6	4.3 10 -3	1

Acknowledgement

This work has been partially funded through the projects PTDC/FIS/098943/2008 financed by Portuguese Foundation for Science and Technology (FCT) and by European Commission through project ELIARE NETWORK SUDOE INTERREG IV B (2009-2011), and the Scientific and Technological Cooperation Program between Portugal (FCT) and Morocco (CNRST)-2010/2011. SL thanks FCT for the financial support through the grant SFRH/BPD/26532/2006.