Hanlin Goh
email: hanlin.goh@lip6.fr

Nicolas Thome
email: nicolas.thome@lip6.fr

Matthieu Cord
email: matthieu.cord@lip6.fr

Biasing Restricted Boltzmann Machines to Manipulate Latent Selectivity and Sparsity

This paper proposes a modification to the restricted Boltzmann machine (RBM) learning algorithm to incorporate inductive biases. These latent activation biases are ideal solutions of the latent activity and may be designed either by modeling neural phenomenon or inductive principles of the task. In this paper, we design activation biases for sparseness and selectivity based on the activation distributions of biological neurons. With this model, one can manipulate the selectivity of individual hidden units and the sparsity of population codes. The biased RBM yields a filter bank of Gabor-like filters when trained on natural images, while modeling handwritten digits results in filters with stroke-like features. We quantitatively verify that the latent representations assume the properties of the activation biases. We further demonstrate that RBMs biased with selectivity and sparsity can significantly outperform standard RBMs for discriminative tasks.

Introduction

Restricted Boltzmann machines (RBMs) [START_REF] Smolensky | Information processing in dynamical systems: Foundations of harmony theory[END_REF] are generative neural networks that form distributed representations capturing the latent structure of input data by approximating the maximum likelihood (ML) objective. However, given the nature of a task, learning based on ML alone may not be the most desirable approach. To manipulate the representations during learning, suitable inductive biases [START_REF] Mitchell | The Need for Biases in Learning Generalizations[END_REF] should be incorporated so that an RBM can inherit certain desirable representational properties. The inductive biases are a priori assumptions about the nature of the target function and should be exploited to facilitate the learning process. In this paper, we will introduce a simple modification to incorporate generic inductive biases into RBM learning. With this, we design the biases to manipulate the selectivity and sparsity of latent representations. Through a series of experiments, we quantitatively show the importance of having both selectivity and sparsity in our representations.

Restricted Boltzmann Machines

An RBM consists of a layer of I visible units v and a layer of J hidden units h. The layers are linked via symmetric weighted connections W ∈ R I×J . Additionally, each visible v i and hidden h j unit receives input from a bias -c i and b j respectively. For an RBM with binary units, the activation probabilities of units in one layer are computed based on the states of the opposite layer, fed through a sigmoid activation function sigm(•):

Pr (h j | v) = sigm b j + I i=1 w ij v i , (1) Pr (v i | h) = sigm   c i + J j=1 w ij h j   . (2)
An energy function defines the negative log probability of a configuration of states (v, h):

-log Pr (v, h) = E (v, h) = - I i=1 J j=1 v i w ij h j - I i=1 c i v i - J j=1 b j h j . (3)
By modifying the parameters W, b and c, the energy of samples from the data distribution can be decreased, while raising the energy of reconstructions that the network prefers to real data.

RBM Learning Using Contrastive Divergence

To train an RBM, one employs the contrastive divergence (CD) learning algorithm [START_REF] Hinton | Training products of experts by minimizing contrastive divergence[END_REF] to approximate the ML of the data and update parameters W, b and c. The RBM learning algorithm with one iteration of stochastic Gibbs sampling (CD-1) is described in Figure 1. Given a set of K training examples, V + ∈ R I×K and H + ∈ R J×K are visible and hidden states resulting from sampling from the data distribution, while V -∈ R I×K and H -∈ R J×K are reconstructed states. The parameters are updated using the following update rules:

∆w ij = ε v + i h + j -v - i h - j , (4)
∆b j = ε h + j -h - j , (5)
∆c i = ε v + i -v - i , ( 6
)
where ε is the learning rate and • is defined as the average over the set of K examples. The activation probabilities of v i and h j may be used in place of their binary states for parameter updates (see [START_REF] Hinton | A practical guide to training restricted Boltzmann machines[END_REF]). This process, known as Rao-Blackwellization [START_REF] Blackwell | Conditional expectation and unbiased sequential estimation[END_REF], results in an estimator with lower variance [START_REF] Swersky | A tutorial on stochastic approximation algorithms for training restricted boltzmann machines and deep belief nets[END_REF]. During parameter updates we will adopt this convention.

- ε V -H - ΔW = - 1 . . . j . . . 1 . . . J j . . . ε h - h + Δb = J - 1 . . . I i . . . 1 . . . I i . . . ε v - v + Δc = (b) Parameter updates.
Figure 1: The RBM learning algorithm (CD-1). (a) In the positive phase, hidden units H + are activated based solely on inputs V + . The negative phase involves the reconstruction of V -from H + and subsequently H -from V -. (b) The parameters W, b and c are updated based on the gradients from the positive and negative phases.

Motivation of Inducing Both Selectivity and Sparsity

Selectivity and sparsity are important properties of neural coding. Neural activity can be characterized in the lifetime or population domains [START_REF] Willmore | Characterizing the sparseness of neural codes[END_REF], resulting in the properties of selectivity and sparsity respectively (Figure 2(a)). Selectivity is the property of a single neuron given a series of stimuli over time. In contrast, sparsity is defined across a population of neurons given a single stimulus [START_REF] Földiák | Neural coding: non-local but explicit and conceptual[END_REF]. The two properties are not necessarily correlated [START_REF] Willmore | Characterizing the sparseness of neural codes[END_REF] and are related only by their average values [START_REF] Földiák | Neural coding: non-local but explicit and conceptual[END_REF].

Narrowly selective neurons do not guarantee the generation of sparse population codes (Figure 2(c)). Likewise, sparse codes may be induced from neurons that may not be highly selective (Figure 2(d)). We can visually observe from Figure 2(b) that when the code is both highly selective and sparse, there is activation diversity in the population and across samples. Sparsity causes lateral inhibition and encourages competition between hidden units, while selectivity prevents over-dominance by any individual unit. When this occurs, the standard deviation is low for selectivity in the population and sparsity across examples.

h (1) h (2) h (3) h (4) h (5) h (6) h (7) h (8) h (9) h (10) h 1 01 0 0 0 0 0 0 0 1 0.2 h 2 1 0 0 0 1 0 0 0 1 0 0.3 h 3 0 0 0 0 0 0 0 0 1 0 0.1 h 4 0 1 0 1 0 1 0 0 0 1 0.4 h 5 0 0 0 0 0 0 1 0 1 0 0.2 h 6 0 0 1 0 0 0 1 0 0 0 0.2 h 7 1 0 0 0 0 1 0 1 0 0 0.3 h 8 0 0 0 0 0 0 0 0 1 0 0.1 h 9 0 1 0 0 1 0 1 0 1 1 0.5 h 10 0 0 0 1 0 0 0 1 0 0 0. (a) Distinguishing selectivity and sparsity.

h (1) h (2) h (3) h (4) h (5) h (6) h (7) h (8) h (9) h (10) h 1 0 0 0 0 0 1 0 0 0 1 0.2 h 2 0 0 1 0 0 0 0 1 0 0 0.2 h 3 1 0 0 0 1 0 0 0 0 0 0.2 h 4 0 0 0 1 0 0 1 0 0 0 0.2 h 5 0 0 0 0 0 0 0 1 0 1 0.2 h 6 0 1 0 0 1 0 0 0 0 0 0.2 h 7 1 0 0 0 0 0 0 0 1 0 0.2 h 8 0 0 1 0 0 0 1 0 0 0 0.2 h 9 0 0 0 1 0 0 0 0 1 0 0.2 h 10 0 1 0 0 0 1 0 0 0 0 0. (b) Narrowly selective sparse codes. 6) h (7) h (8) h (9) h (10) h 1 0 0 1 0 0 0 1 0 0 0 0.2 h 2 0 0 1 0 1 0 0 0 0 0 0.2 h 3 0 0 0 0 1 0 1 0 0 0 0.2 h 4 0 0 1 0 0 0 1 0 0 0 0.2 h 5 0 0 0 0 1 0 1 0 0 0 0.2 h 6 0 0 1 0 0 0 1 0 0 0 0.2 h 7 0 0 1 0 1 0 0 0 0 0 0.2 h 8 0 0 0 0 1 0 1 0 0 0 0.2 h 9 0 0 1 0 1 0 0 0 0 0 0.2 h 10 0 0 1 0 0 0 1 0 0 0 0. (c) Narrow selectivity but not sparse coded. 6) h (7) h (8) h (9) h (10) h 1 0 0 0 0 0 0 0 0 0 0 0 h 2 1 0 1 1 1 0 1 0 1 0 0.6 h 3 0 0 0 0 0 0 0 0 0 0 0 h 4 1 1 0 0 1 1 0 1 1 1 0.7 h 5 0 0 0 0 0 0 0 0 0 0 0 h 6 0 0 0 0 0 0 0 0 0 0 0 h 7 0 0 0 0 0 0 0 0 0 0 0

h (1) h (2) h (3) h (4) h (5) h (
h (1) h (2) h (3) h (4) h (5) h (
h 8 0 1 1 1 0 1 1 1 0 1 0.7

RBM Learning with Latent Activation Biasing

An RBM does not explicitly consider the nature of the task or that it may be part of a more complex network, such as deep belief nets (DBN) [START_REF] Hinton | A fast learning algorithm for deep belief networks[END_REF] or other hierarchical architectures. If we have a priori knowledge of the desired latent representational properties for a particular task, such as selectivity and sparsity, how can this information be included during RBM learning? For this purpose, we extend existing work on regularizing RBMs [START_REF] Lee | Sparse deep belief net model for visual area V2[END_REF][START_REF] Nair | 3D object recognition with deep belief nets[END_REF] and design a more generic model to incorporate any inductive principle as latent activation biases during RBM learning.

RBMs with Selective Regularization

There are several ways to achieve selectivity in RBMs. 1 Lee et al. [START_REF] Lee | Sparse deep belief net model for visual area V2[END_REF] proposed to couple the ML approximation of contrastive divergence with a regularization term that penalizes non-selective hidden units. Similarly, Nair & Hinton [START_REF] Nair | 3D object recognition with deep belief nets[END_REF] used the cross-entropy measure between the actual and desired distributions to compute the penalty. In both cases, the additional update is a penalty proportional to qp, where p is the target selectivity of each unit and q is the observed selectivity. The selectivity of a hidden unit is computed by a process of averaging its activation across training examples. A term η is included to scale the learning of the regularizer.

For a hidden unit to be selective, it should respond strongly to only a few examples and have low activation probabilities for the other examples. However, these methods merely regularize the learning such that the activation probabilities are low on the average. Even when the selectivity objective p is satisfied, the unit's activation may not be selective (for example, h (k)+ j = p, ∀k ∈ K). As such, the hidden units need to be stochastic and binary. In the case where the activations are selective but the average is higher than p, the penalty term penalizes all activations equally to bring the average down. By penalizing the high activations, one sends a signal for it to be less selective. Furthermore, since the regularizer considers only selectivity and not sparsity, we may get units that lack differentiation between each other. A population of hidden units that respond selectively but similarly to a few examples will still satisfy the regularization objectives individually (see Figure 2(c)). We propose to have a more precise and fine-grained control of the regularization process to overcome these issues.

Precise Biasing of Latent Activations

To have a more precise control of the regularization, we realize the target p as a spatiotemporal matrix P ∈ R J×K , where each element p (k) j ∈ [0, 1] is a latent activation bias encoding the desired activation of h j in response to input example k. Each row p j represents the desired temporal activation sequence of h j , while a column p (k) is the ideal population code of hidden units given example k. More generally, P can be designed based on any inductive principle, not just selectivity. Inspired by Nair & Hinton [START_REF] Nair | 3D object recognition with deep belief nets[END_REF], we adopted the cross-entropy error between the desired and actual activation probabilities for the penalty term. We now pose the following optimization problem:

arg min {W,c,b} - K k=1 log h Pr v (k) , h (k) + λ J j=1 p (k) j log h (k)+ j + 1 -p (k) j log 1 -h (k)+ j , (7)
The averaged update for w ij and b j across K examples can then be modified and rearranged:

∆w ij = ε v + i h + j -v - i h - j -η v + i h + j -p j = ε v + i s j -v - i h - j , (8)
∆b j = ε h + j -h - j -η h + j -p j = ε s j -h - j . (9)
Here, we let s

(k) j = φp (k) j + (1 -φ) h (k)+ j , (10)
where φ = η ε is a hyperparameter. This modified algorithm is illustrated in Figure 3.

The influences of p . Because the biases are directly the desired activation probabilities of the hidden units given an example, Rao-Blackwellization can still be employed and we do not need to assume hidden units to be binary. When φ = 0 or if the activation bias is met (i.e. p

(k) j = h (k)+ j
), the parameter update equations simplify to those of the original contrastive divergence algorithm. Comparing Equations ( 8) and [START_REF] Hinton | A fast learning algorithm for deep belief networks[END_REF] with the original updates (Equations ( 4) and ( 5)), we observe an asymmetry in the new updates, which generates a learning signal that is guided by the latent activation biases. Note that biasing is only done in the training step.

Designing Latent Activation Biases for Selectivity and Sparsity

To manipulate the selectivity and sparsity of the representations, we turn to biology for inspiration. From neuronal recordings, it was found that the activity distributions for both selectivity and sparsity are positively skewed with heavy tails, such as the exponential and gamma distributions [START_REF] Franco | Neuronal selectivity, population sparseness, and ergodicity in the inferior temporal visual cortex[END_REF]. By adapting the activation probabilities of hidden units to fit such distributions in the lifetime (rows) or population (columns) domains, we can model their latent activity biases P.

Modeling Selectivity and Sparsity

We transform the latent activations to fit desired distributions. Let h ∈ R N be either row h + j for selectivity or column h (k)+ for sparsity. The latent activation bias p n for h n is computed as

p n = (rank (h n , h)) (1/µ)-1 . ( 11
)
where rank (h n , h) assigns a value from 0 to 1 based on the rank of h n in h, with smallest given a value of 0 and the largest with 1. The target mean 0 < µ < 1 creates the power-law expression such that when µ < 0.5, the distribution will be positively skewed. Instead of merely getting the RBM to have low average activations [START_REF] Lee | Sparse deep belief net model for visual area V2[END_REF][START_REF] Nair | 3D object recognition with deep belief nets[END_REF], we bias individual activations based on positively skewed distributions so that only a few activations are high while most remain low. This is more precise.

Unlike methods that produce stochastic spiking activations [START_REF] Nair | 3D object recognition with deep belief nets[END_REF][START_REF] Ranzato | Efficient learning of sparse representations with an energy-based model[END_REF], our method does not depend on the order of the inputs. It also preserves the ranking between activation probabilities. Moreover, it can be applied in both the lifetime and population domains to achieve both selectivity and sparsity.

Combining Selectivity and Sparsity

Because selectivity and sparseness are not highly correlated Willmore & Tolhurst [START_REF] Willmore | Characterizing the sparseness of neural codes[END_REF], we need to combine the latent activation biases in both domains. We take H + and progressively induce column-wise sparsity followed by row-wise selectivity with Equation [START_REF] Lecun | Gradient-based learning applied to document recognition[END_REF]. We use the same µ since the properties will produce the same mean values. This yields activation biases P that are consistent in both domains, such as the example shown in Figure 2(b).

Experiments

One of the advantages of RBMs is the ability to find correlations between input units, even though there are no direct connections between them. As a result, they are very suited to model the spatialappearance of images. We study the properties and performance of our method using two image data sets, namely the Kyoto natural images data set [START_REF] Doi | Spatiochromatic receptive field properties derived from information-theoretic analyses of cone mosaic responses to natural scenes[END_REF] and the MNIST handwritten digits database [START_REF] Lecun | Gradient-based learning applied to document recognition[END_REF].

Visualization: Modeling Natural Images

We trained RBMs biased with selectivity and sparsity to efficiently represent natural image patches.

The training data consists of 100,000 randomly sampled patches of size 14 × 14 pixels from the Kyoto natural images data set [START_REF] Doi | Spatiochromatic receptive field properties derived from information-theoretic analyses of cone mosaic responses to natural scenes[END_REF]. The result a set of Gabor-like filters (Figure 4), which is consistent with other related methods [START_REF] Doi | Sparse coding of natural images using an overcomplete set of limited capacity units[END_REF][START_REF] Lee | Sparse deep belief net model for visual area V2[END_REF][START_REF] Olshausen | Emergence of simple-cell receptive field properties by learning a sparse code for natural images[END_REF][START_REF] Ranzato | Efficient learning of sparse representations with an energy-based model[END_REF][START_REF] Teh | Energy-based models for sparse overcomplete representations[END_REF]. Additionally, as a gauge of the generality of these filters, we adopted a transfer learning framework and reconstructed similar-sized patches from the MNIST data set. We obtained a 43% decrease in the reconstruction error as compared to the standard RBM, probably because these edge detectors are localized and some resemble handwritten strokes.

Evaluation: Modeling Handwritten Digits

The MNIST database [START_REF] Lecun | Gradient-based learning applied to document recognition[END_REF] consists of 60,000 training and 10,000 test images of handwritten digits of size 28 × 28 pixels. For the data set, we used the training set to train RBMs with 1000 hidden units, while the test set is used for evaluation.When target mean µ of the activation biases was set sufficiently low, the learned filters appear to encode localized handwritten strokes (Figure 5). Selectivity and sparsity are transferred from biases to parameters. The selectivity and sparsity of a set of activation probabilities can be measured using the activity ratio [START_REF] Treves | What determines the capacity of autoassociative memories in the brain?[END_REF], which is a quantitative measure of length of the tail of the distribution of activations. It can be computed using either the continuous-valued activation probabilities or the binary activation states. Given a set of activations x ∈ R N in the lifetime or population domain, the activity ratio a ∈ [0, 1] is defined as

a = 1 N N n=1 x n 2 1 N N n=1 x 2 n , (12)
where a value nearer 0 indicates either a more selective unit or a sparser population code. Using input data from the test set we activated the hidden units with the standard sigmoid activation function.

We varied the degree of selectivity and sparsity by changing µ and measured the activity ratios in both the lifetime and population domains. As illustrated in Figure 6(a), as µ is decreased, both activity ratios also decrease. The properties of selectivity and sparsity in the latent activation biases are transferred to the learned parameters, which induces latent representations with those properties.

Benefits of manipulating both selectivity and sparsity. Biasing the RBM with only selectivity or only sparsity, we analyzed their activity ratios in relation to µ. Biasing only for selectivity results in activity ratios with a large spread in the population domain (Figure 6(b)). Likewise, biasing only for sparsity results in a high variations in the lifetime domain (Figure 6(c)). We found that this result is due to activations being consistently high or low in the non-biased domain. We refer to Figure 2 for a toy example of this phenomenon and Section 1.3 for a discussion. Increasing the selectivity and sparsity explicitly improves the diversity between hidden units in their own domains, but does not explicitly induce diversity in the other domain. Both selectivity and sparsity are required to reduce the number of overly active or silent units, and superfluously or inadequately represented examples. Biasing RBMs improves discriminative performance. While many deep learning methods use MNIST as a benchmarking data set, we adopt a shallow architecture to analyze the performance gain of a biased RBM over the standard RBM. For each hidden unit, the activation with respect to each class is totaled and normalized across classes. We then computed the Shannon entropy of each hidden unit and finally averaged it across the population. This metric H gives us an indication of the level of class-based discrimination of the hidden units, where lower H values signify fewer the number of classes each unit encodes. We also trained a simple multinomial logistic regression classifier from the activations of the hidden layer (without backpropogating the features) and computed the classification error rate. Since there are 10 classes, one for each digit and roughly uniformly distributed, we consider that for a unit to be selective, it should respond to less than 10% of the samples. Hence, we conducted our study in the range of 0.001 ≤ µ ≤ 0.12. From Figure 7(a), we observe a clear monotonic relationship of H with respect to µ. When µ is lowered, a unit responds to fewer examples, so if examples from the same class have similar appearances, then it is more likely that these examples belong to the same class, thus lowering H . Figure 7(b) shows that the relation between the classification error and µ is no longer monotonic. The model has poor generalization when µ nears 0 as units encode individual examples too specifically, just like "grandmother cells" [START_REF] Gross | Genealogy of the "grandmother cell[END_REF]. For this data set, the biased RBM achieves better result than the standard RBM in the approximate range of 0.01 ≤ µ ≤ 0.1. At its minimum, the biased RBM significantly outperforms the standard RBM by 29% (1.25% improvement in error rate). Interestingly, the classification performance of this simple semi-supervised method without fine-tuning is comparable to other reported results using similarly simple yet completely supervised approaches [START_REF] Lecun | Gradient-based learning applied to document recognition[END_REF]. There is a range of µ whereby biasing the RBM improves generalization performance.

Conclusions

Selectivity and sparsity are important properties of neural coding. In this paper, we introduced a modification to the RBM learning algorithm that can incorporate generic latent activation biases to guide the learning process. The RBM parameters are encouraged to encode the representational properties defined by these biases. The activation biases are designed based on prior knowledge of the task or nature of the problem. Here, we described the activation biases to manipulate latent selectivity and sparsity. We quantitatively verified that selectivity and sparsity were indeed encoded after training and presented the benefits of selectivity and sparsity for modeling handwritten digits. We are currently working on modeling other latent activation biases that are inspired from neural phenomenon, such as topographical organization [START_REF] Hyvärinen | A two-layer sparse coding model learns simple and complex cell receptive fields and topography from natural images[END_REF] and explicitness [START_REF] Földiák | Neural coding: non-local but explicit and conceptual[END_REF].

  Population Code) Mean sparsity: 0.2 Std dev: 0 Mean selectivity: 0.2 Std dev: 0.32 (d) Sparsely coded but not narrowly selective.

Figure 2 :

 2 Figure 2: Examples of binary unit activations h (k) j relating selectivity and sparsity. (a) Selectivity is a property of a single unit, given the set of input samples. Sparsity is a property of the population of hidden units, given one input example. The two properties are related only by their average values. (Terminology adapted from [4]) (b) An example of units with narrow selectivity and sparse population codes. (c) When units have narrow selectivity, the population may not induce sparse codes. (d) Likewise, sparse activations are not necessarily the product of units with narrow selectivity.

  φ. If φ is constrained to be between 0 and 1, then 0 ≤ s (k) j ≤ 1 and s (k) j can be seen as the revised activation probability of h (k)+ j

  (a) Visible and hidden unit activations and inclusion of latent activation biases.

  Modified parameter updates.

Figure 3 :

 3 Figure 3: The modified RBM learning algorithm with biased latent activations. (a) In the positive phase, hidden units H + are re-activated as S with additional influences from latent activation biases P interpolated by φ. (b) When updating parameters W and b, the modified activation S replaces H + , only the positive phase. ∆c is unmodified from the original algorithm.

Figure 4 :

 4 Figure 4: An example of a filter bank learned by an RBM with selectivity and sparsity biases. The filters are Garbor-like with varying orientation, spatial location and spatial frequency.

Figure 5 :

 5 Figure 5: Examples of filters learned by the biased RBM when trained on handwritten digits.

111111

  Sparsi ty (b oth bi ase s) Me an of ac ti vati on bi ase s µ Ac ti v i ty rati o a (popul ati on) Se l e c ti v i ty (b oth bi ase s) Me an of ac ti vati on bi ase s µ Ac ti v i ty rati o a (l i fe ti me ) Sparsi ty (bi ase d se l e c ti v i ty ) Me an of ac ti vati on bi ase s µ Ac ti v i ty rati o a (popul ati on) Se l e c ti v i ty (bi ase d se l e c ti v i ty ) Me an of ac ti vati on bi ase s µ Ac ti v i ty rati o a (l i fe ti me ) Sparsi ty (bi ase d sparsi ty ) Me an of ac ti vati on bi ase s µ Ac ti v i ty rati o a (popul ati on) Se l e c ti v i ty (bi ase d sparsi ty ) Me an of ac ti vati on bi ase s µ Ac ti v i ty rati o a (l i fe ti me ) (c) Sparsity only

Figure 6 :

 6 Figure 6: Analysis of activity ratio with respect to the target mean µ of the activation biases. (a) Both activity ratios decrease in relation to µ, showing a transfer in representational properties from the biases to the actual latent activations. As a reference, the activity ratios for the standard RBM are plotted. (b) By biasing only for selectivity, the spread of activation ratios in the population domain is high. (c) In contrast, biasing only for sparsity results in high variations in lifetime activity ratios.

1

  Me an of ac ti vati on bi ase s µ Avg . c l ass-base d e ntropy H RBM bi a se d RBM (a) Class-based entropy Me an of ac ti vati on bi ase s µ Cl assi fic ati on e rror rate RBM bi as e d RBM (b) Classification error

Figure 7 :

 7 Figure 7: Discriminative performance of RBMs biased with selectivity and sparsity. (a) H varies monotonically with µ. (b) Classification error is minimum when µ is low, but not at the lowest.There is a range of µ whereby biasing the RBM improves generalization performance.

In the literature, the terms "sparsity" and "selectivity" are sometimes used interchangeably, sometimes leading to confusion[START_REF] Földiák | Neural coding: non-local but explicit and conceptual[END_REF]. We use "selectivity" to describe the activity of an individual unit across examples and "sparsity" to describe the activity of a population in response to a single example.

Acknowledgments

We thank Joo-Hwee Lim for fruitful discussions. This work was supported in part by the Embassy of France in Singapore under the Merlion 2009 Project and PhD program.


Hanlin Goh
email: hlgoh@i2r.a-star.edu.sg

Łukasz Kuśmierz

Joo-Hwee Lim

Nicolas Thome

Matthieu Cord

LEARNING INVARIANT COLOR FEATURES WITH SPARSE TOPOGRAPHIC RESTRICTED BOLTZMANN MACHINES

Keywords: Unsupervised feature learning, invariant features, sparse coding, topographic coding, color features

Our objective is to learn invariant color features directly from data via unsupervised learning. In this paper, we introduce a method to regularize restricted Boltzmann machines during training to obtain features that are sparse and topographically organized. Upon analysis, the features learned are Gaborlike and demonstrate a coding of orientation, spatial position, frequency and color that vary smoothly with the topography of the feature map. There is also differentiation between monochrome and color filters, with some exhibiting coloropponent properties. We also found that the learned representation is more invariant to affine image transformations and changes in illumination color.

INTRODUCTION

There is a recent bloom in the field of learning deep architectures [START_REF] Benjio | Learning deep architectures for AI[END_REF], whereby the input data is represented by a hierarchical network of several layers. A popular deep architecture is the deep belief net (DBN) [START_REF] Hinton | A fast learning algorithm for deep belief networks[END_REF], which stacks restricted Boltzmann machines (RBMs) in a greedy layer-by-layer manner. Each RBM is trained via unsupervised learning and the entire network is subsequently fine-tuned via supervised learning.

In traditional RBMs, features are learned by approximating the maximum likelihood of the data distribution. Sparsity may be used as a regularization criterion to increase feature differentiation and discriminative power [START_REF] Lee | Sparse deep belief net model for visual area V2[END_REF][START_REF] Nair | 3D object recognition with deep belief nets[END_REF][START_REF] Goh | Biasing restricted Boltzmann machines to manipulate latent selectivity and sparsity[END_REF]. However, the representations are not invariant to input transformations. We propose that if there is structured similarity between the features, then representations will smoothly vary with respect to the transformations and invariance can be achieved.

In this paper, we present a method to regularize RBM learning to achieve with sparseness and topographical orga-nization. The features learned exhibit invariance to affine image transformations and illumination color, while maintaining differentiation when the transformations are significant.

RESTRICTED BOLTZMANN MACHINES

An RBM is a bipartite neural network that represents input data with a layer of hidden units via symmetric weights. An input example k is represented by visible units v (k) i and the latent representation by hidden units h (k) j . By fixing one layer, activation probabilities of the other layer can be computed:

Pr h (k) j | v (k) = sigmoid I i=1 v i w ij + b j , (1)
Pr v (k) i | h (k) = sigmoid   J j=1 h j w ij + c i   , (2)
where sigmoid (•) is the logistic function and b j and c i are biases contributing to hidden and visible units. The parameters of the RBM are learned via contrastive divergence [START_REF] Hinton | Training products of experts by minimizing contrastive divergence[END_REF], whereby the maximum likelihood of the data is approximated. Given a training set of K examples, the visible states v + i and hidden states h + j are sampled from the data distribution, while v - i and h - j are reconstructed states. The parameter update equations are

∆w ij = ε (v + i h + j -v - i h - j ), (3)
∆b j = ε (h + j -h - j ), (4)
∆c i = ε (v + i -v - i ), (5)
where ε is a learning rate and • averages over K samples. Early work of regularizing RBMs focused on achieving sparse representations [START_REF] Lee | Sparse deep belief net model for visual area V2[END_REF][START_REF] Nair | 3D object recognition with deep belief nets[END_REF]. Building on those, Goh et al. [START_REF] Goh | Biasing restricted Boltzmann machines to manipulate latent selectivity and sparsity[END_REF] formulated a general method to regularize RBMs with more precision. These regularizers can be designed based on any inductive principle, such as sparsity and selectivity as originally demonstrated. The new update rules for W and b are:

∆w ij = ε (v + i s j -v - i h - j ), (6)
∆b j = ε (s j -h - j ), (7)
where

s (k) j = φp (k) j + (1 -φ)h (k)+ j (8)
and φ is a hyperparameter that interpolates the observed hidden activation probabilities H with the desired activation probabilities P. The resulting features learned will take on the representational properties defined by the regularizers P.

SPARSE TOPOGRAPHIC REGULARIZATION

The regularization method drives the learning of features to be dependent on both the data distribution V + and the regularizer P. We adapt an two-layered scheme [START_REF] Hyvärinen | A two-layer sparse coding model learns simple and complex cell receptive fields and topography from natural images[END_REF][START_REF] Kavukcuoglu | Learning invariant features through topographic filter maps[END_REF] to regularize the RBM (Fig. 1). From hidden representation H + , we compute a new set of activations H based on fixed topographically pooled weights (see Section 3.1). Subsequently, sparsity is induced in both the temporal and spatial domains to obtain P (see Section 3.2). P can then be used to regularize updating of parameters for the RBM. + + Fig. 1. The framework for inducing both sparseness and topographical organization. From a batch of pixel inputs V + , the latent units are activated H + via learned weights. The activations are then topographically pooled based on the locality of h j in the feature map via fixed weights. Subsequently, population and lifetime sparseness are induced to obtain P. Finally, P is used to regularize the learning of the parameters.

Inducing Topographic Organization

As shown in Fig. 1, we induce topographical structure in the feature map by introducing a dependence between the hidden units via a new layer H, where each h . Each unit in H + activates units in H depending on the relative locality of the units, which has the same effect as filtering the feature map. The modified activations h are computed as

h (k) j = M m=1 h (k)+ m ω (j, m) (9)
where the fixed topographic pooling weights ω (•, •) are functions of the topographic distance between two units. A Gaussian kernel with wrap around was used for this paper. Each pixel shows the activation of a unit in the feature map, where darker color denotes a higher activation. When topographic organization is induced, the activations are spatially grouped within the feature map.

Inducing Lifetime and Population Sparseness

After inducing topographical organization, we sparsify the activation probabilities to obtain the final modified activation probabilities P. We follow the method by Goh et al. [START_REF] Goh | Biasing restricted Boltzmann machines to manipulate latent selectivity and sparsity[END_REF] to inducelifetime and population sparseness in our representations. This is done by the following sequence of data transformations:

p (k) j = rank h (k) j , h (k) (1/µ)-1 , (10)
p (k) j = rank p (k) j , p j (1/µ)-1 , (11)
where µ denotes the target mean of the latent activations and rank (x n , X) is the normalized rank of element x n in vector

x such that the highest x n is assigned a value of 1, the smallest the value of 0 and all others are uniformly distributed between 0 and 1 depending on their rank in the vector. The rank (•) function has the same effect as histogram equalization.

EXPERIMENTAL RESULTS

We trained an RBM with sparse topographic regularization using 100,000 natural image patches. The patches were of size 10 × 10 and taken from the McGill Calibrated Colour Image Database [START_REF] Olmos | McGill calibrated colour image database[END_REF] (Fig. 3(a)). The RBM consists of 300 visible units and 400 hidden units, which are structured in a two-dimensional 20 × 20 feature map. The resulting feature map consists of Gabor-like filters with varying spatial frequency, position, orientation and color (Fig. 4(b)). The appearance of filters vary smoothly across the feature map. This was also demonstrated in other related models [START_REF] Welling | Learning sparse topographic representations with products of student-t distributions[END_REF][START_REF] Hyvärinen | Topographic independent component analysis[END_REF][START_REF] Kavukcuoglu | Learning invariant features through topographic filter maps[END_REF]. Additionally, our feature map models color information. As a comparison, another RBM was also trained with sparse but independent regularization (Fig. 4(a)).

Analysis of Topographic Feature Maps

We fitted Gabor functions to the filters of the feature map to analyze their orientations, spatial positions and spatial frequencies (Fig 5). At the level of these visual components, one clearly observes a smooth topographical organization of filters in the feature map. There is also a presence of several pinwheel structures in the orientation map (Fig. 5(b)).

From Fig. 5(d), we can see that the filters are clustered by color. We also observe that some exhibit color-opponeny, while others encode single colors. The predominant opponent pairs based-on are red-green, yellow-blue and black-white. From Fig. 5(b), we observe that each color-opponent pair has filters with different orientation coding. The red-green and yellow-blue opponent pairs tend code for lower frequency. We also note the existence of some single-colored filters that are mostly green, cyan and violet, with high frequency textured appearances.

Evaluating the Invariance of Features

We evaluate the features learned based on their invariance to affine transformations (translation, rotation, scaling) and changes to illumination color. For affine transformations, new patches were sampled from the McGill database [START_REF] Olmos | McGill calibrated colour image database[END_REF] (Fig. 3(a)), while patches were drawn from the ALOI data set [START_REF] Geusebroek | The Amsterdam library of object images[END_REF] (Fig. 3(b)) for the illumination color task. For each evaluation task, we extracted 500 evaluation batches. Each evaluation batch consists a set of patches sampled via transformations for the given task.

An evaluation batch for rotation consists of 13 patches sampled about a fixed point with rotation ranging from -30 to 30 degrees at 5 degree intervals. The samples for translation was drawn via horizontal translations from -3 to 3 pixels. For scaling, a progressive scaling factor of 1.1× was used to upsample and down-sample a patch. To produce patches with varying illumination color, we sampled a set of images produced by different illumination from the same coordinate.

For every input patch, the output signature of hidden unit activations were recorded. To quantitively measure invariance, we took the mean squared difference (MSD) between the signatures of the transformed input and that of the untransformed input. The MSD was then averaged across the samples and plotted in Fig. 6. In every evaluation task, when the transformation is low, topographic features are more invariant than independent ones. There is little difference between the two feature types under large transformations. The signature of a slightly transformed input is highly similar the original signature. As the amount of transformation increases, the signature gradually shifts and invariance reduces (Fig. 7). Hence, the features retain the necessary differentiation for recognition tasks.

CONCLUSIONS

We introduced a method to regularize the learning of RBMs by encouraging activations to be topographic organized. The appearance of the resulting color features vary smoothly across the feature map. The representations exhibit invariance to affine transformations and changes in illumination color.

Fig. 2 .

 2 Fig. 2. Comparing activations of independent coding (a) and topographic coding (b). Each pixel shows the activation of a unit in the feature map, where darker color denotes a higher activation. When topographic organization is induced, the activations are spatially grouped within the feature map.

  (a) The McGill calibrated color image database has 9 categories -flowers, animals, foliage, textures, fruits, landscapes, winter, man made and shadows. (b) The subset of the Amsterdam library of object images used have been photographed under different illumination color.

Fig. 3 .

 3 Fig. 3. Sample images from data sets used.

Fig. 4 .

 4 Fig. 4. Feature maps learned with (a) sparse but independent regularizers and (b) sparse topographic regularizers.

Fig. 5 . 2 .Fig. 6 .

 526 Fig. 5. Appearance of filters vary smoothly across the feature map when broken down to their component properties of (a) spatial position, (b) orientation, (c) spatial frequency and (d) color.

  (a) Original signature (b) Slightly transformed (c) Highly transformed

Fig. 7 .

 7 Fig. 7. Variations of signatures in the sparse topographic feature map under different amounts of transformation.


Guillaume Aucher

Bastien Maubert

François Schwarzentruber

Generalized DEL-sequents

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

Let us consider a sequence of formulas providing partial information about an initial situation, about a set of events occurring sequentially in this situation, and about the resulting situation after the occurrence of each event. From this whole sequence, we want to infer more information, either about the initial situation, or about one of the events, or about the resulting situation after one of the events. Within the framework of Dynamic Epistemic Logic (DEL), we show that these different kinds of problems are all reducible to the problem of inferring what holds in the final situation after the occurrence of all the events. We then provide a tableau method deciding whether this kind of inference is valid. We implement it in LotrecScheme and show that these inference problems are NEXPTIME-complete. We extend our results to the cases where the accessibility relation is serial and reflexive and illustrate them with the coordinated attack problem.

Introduction

Assume that a sequence of n events has occured in a situation. We have some information about each event and about the resulting situation after the occurrence of each event, in the form of a sequence of formulas ϕ ′ i and ϕ i respectively: ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ i , ϕ i , . . . , ϕ ′ n , ϕ n Our aim is to infer some more information about one of the events or about one of the resulting situations from the rest of information provided by this sequence. This defines respectively two different kinds of inference problems.

In the first kind of inference problem, we want to infer more information about the i th resulting situation. That is, given a formula ψ describing (incompletely) a situation, we want to verify whether or not we can infer that this property ψ necessarily held at the i th resulting situation:

ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n i 1 ψ ?
In the second kind of inference problem, we want to infer more information about the i th event. That is, given a formula ψ ′ describing (incompletely) this event, we want to verify whether or not we can infer that this property ψ ′ necessarily held during the occurrence of the i th event:

ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n i 2 ψ ?
Solving these problems is relevant for dynamic diagnosis for instance (see [START_REF] Brusoni | A spectrum of definitions for temporal model-based diagnosis[END_REF] for an early survey of dynamic diagnosis). In this field, one is interested in looking for and verifying that plausible diagnoses of a faulty system 'fit' a given history that contains some abnormal behaviours. A diagnosis is a series of faults together with the time when they occur. Within our setting, this verification problem amounts to deciding about the satisfiability of a sequence of formulas.

We moreover assume that our situations involve several agents and we are interested in reasoning about the beliefs and knowledge of these agents. Our formulas ϕ ′ i and ϕ i will therefore express beliefs of several agents about events and about the resulting situations. For these reasons, we address our two problems above within the framework of Dynamic Epistemic Logic (DEL for short), since this logical framework is very well suited to express and reason about the beliefs of several agents in a dynamic setting.

The paper is organised as follows. In Section 2, we recall the core of dynamic epistemic logic and define our two kinds of inference problems. We show that these two kinds of inference problems are actually both reducible to the problem of inferring what holds in the final situation after the occurrence of all the events from the rest of the sequence. In Section 3, we provide a terminating, sound and complete tableau method that decides whether this kind of inference is valid. In Section 4, we show that our tableau method is optimal, first by proving that it is in NEXPTIME, and then by proving that our inference problem is NEXPTIME-hard. We also provide in this section a link to an implementation of our tableau method in LotrecScheme together with some details about its implementation. In Section 5, we extend our results to richer semantics where the accessibility relations are reflexive and serial. In Section 6, we apply our generalized DEL-sequents to the coordinated attack problem of the distributed system literature. Finally, in Section 7, we discuss some related work, and then conclude.

Dynamic Epistemic Logic: DEL-sequents

Following the methodology of DEL, we split the exposition of the logical framework into three subsections. We then define our generalized DEL-sequents in Section 2.4.

Representation of the initial situation: L-model

In the rest of this paper, Φ is a countably infinite set of propositional letters called atomic facts which describe static situations, and Agt is a finite set of agents.

An L-model is a tuple M = (W, R, V ) where:

• W is a non-empty set of possible worlds,

• R : Agt → 2 W ×W is a function assigning to each agent a ∈ Agt an accessibility relation on W ,

• V : Φ → 2 W is a function assigning to each propositional letter of Φ a subset of W . The function V is called a valuation.

We write w ∈ M for w ∈ W , and (M, w) is called a pointed L-model (w often represents the actual world). If w, v ∈ W , we write wR a v for R(a)(w, v) and R a (w) = {v ∈ W | wR a v}.

Intuitively, wR a v means that in world w agent a considers that world v might be the actual world.

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

L : ϕ ::= p | ¬ϕ | ϕ ∧ ϕ | B a ϕ
where p ranges over Φ and a over Agt. We define ϕ ∨ ψ def = ¬(¬ϕ ∧ ¬ψ) and B a ϕ def = ¬B a ¬ϕ. The symbol ⊤ is an abbreviation for p ∨ ¬p for a chosen p ∈ Φ. Let M be an L-model, w ∈ M and ϕ ∈ L. M, w |= ϕ is defined inductively as follows:

M, w |= p iff w ∈ V (p) M, w |= ¬ϕ iff not M, w |= ϕ M, w |= ϕ ∧ ψ iff M, w |= ϕ and M, w |= ψ M, w |= B a ϕ iff for all v ∈ R a (w), M, v |= ϕ
The formula B a ϕ reads as "agent a believes ϕ". Its truth conditions are defined in such a way that agent a believes ϕ holds in a possible world when ϕ holds in all the worlds agent a considers possible. Dually, the formula B a ϕ reads as "agent a considers ϕ is plausible". Agent a considers that ϕ is plausible in a possible world when ϕ holds in at least one of the worlds agent a considers possible.

Representation of the event: L ′ -model

The propositional letters p ′ describing events are called atomic events and range over an infinite set Φ ′ . To each atomic event p ′ , we assign a formula of the language L, which is called the precondition of p ′ . This precondition corresponds to the property that should be true in any world w of an L-model so that the atomic event p ′ can 'physically' occur in this world w. To do so we define a surjection Pre : Φ ′ → L that is called the precondition function. We take it surjective so that we have an atomic event for every possible precondition.

An

L ′ -model is a tuple M ′ = (W ′ , R ′ , V ′ ) where: • W ′ is a non-empty set of possible events, • R ′ : Agt → 2 W ′ ×W ′ is a function assigning to each agent a ∈ Agt an accessibility relation on W ′ , Inria • V ′ : Φ ′ → 2 W ′
is a function assigning to each propositional letter of Φ ′ a subset of W ′ such that for all w ′ ∈ W ′ , there is at most one p ′ such that w ′ ∈ V ′ (p ′ ) (Exclusivity).

We write w ′ ∈ M ′ for w ′ ∈ W ′ , and (M ′ , w ′ ) is called a pointed L ′ -model and w ′ represents the actual event of (M ′ , w ′ ).

If w ′ , u ′ ∈ W ′ , we write w ′ R ′ a u ′ for R ′ (a)(w ′ , u ′ ) and R ′ a (w ′ ) = {u ′ ∈ W ′ | w ′ R ′ a u ′ }. Intuitively, u ′ ∈ R ′ a (w ′
) means that while the possible event represented by w ′ is occurring, agent a considers possible that the possible event represented by u ′ is actually occurring. Our definition of an L ′ -model is equivalent to the definition of an action signature in the logical framework of [START_REF] Baltag | Logic for epistemic programs[END_REF]. 1 Just as we defined a language L for L-models, we also define a language L ′ for L ′ -models (L ′ was already introduced in [START_REF] Baltag | The logic of public announcements, common knowledge and private suspicions[END_REF]):

L ′ : ϕ ′ ::= p ′ | ¬ϕ ′ | ϕ ′ ∧ ϕ ′ | B a ϕ ′
where p ′ ranges over Φ ′ and a over Agt. In the sequel, formulas of L ′ are always indexed by the quotation mark ′ , unlike formulas of L. The truth conditions of the language L ′ are identical to the ones of the language L. Let M ′ be an L ′ -model, w ′ ∈ M ′ and ϕ ′ ∈ L ′ . M ′ , w ′ |= ϕ ′ is defined inductively as follows:

M ′ , w ′ |= p ′ iff w ′ ∈ V ′ (p ′ ) M ′ , w ′ |= ¬ϕ ′ iff not M ′ , w ′ |= ϕ ′ M ′ , w ′ |= ϕ ′ ∧ ψ ′ iff M ′ , w ′ |= ϕ ′ and M ′ , w ′ |= ψ ′ M ′ , w ′ |= B a ϕ ′ iff for all u ′ ∈ R ′ a (w ′ ), M ′ , u ′ |= ϕ ′

Update of the initial situation by the event: product update

The precondition function Pre of the previous section induces a precondition function for L ′models, which assigns to each possible event w ′ of an L ′ -model a formula Pre(w ′ ) of L. The precondition function induced by the L ′ -model M ′ = (W ′ , R ′ , V ′ ) is defined as follows: Pre(w ′ ) = Pre(p ′ ) if there is p ′ such that M ′ , w ′ |= p ′ ; Pre(w ′ ) = ⊤ otherwise.

We then redefine equivalently in our setting the BMS product update of [START_REF] Baltag | The logic of common knowledge, public announcement, and private suspicions[END_REF] as follows. Let (M, w) = (W, R, V, w) be a pointed L-model and let (M ′ , w ′ ) = (W ′ , R ′ , V ′ , w ′ ) be a pointed L ′ -model such that M, w |= Pre(w ′ ). The product update of (M, w) and (M ′ , w ′ ) is the pointed L-model (M, w) ⊗ (M ′ , w ′ ) = (W ⊗ , R ⊗ , V ⊗ , (w, w ′ )) defined as follows:

W ⊗ = {(u, u ′ ) ∈ W × W ′ | M, u |= Pre(u ′ )}, R ⊗ a (u, u ′ ) = {(v, v ′ ) ∈ W ⊗ | v ∈ R a (u) and v ′ ∈ R ′ a (u ′ )}, V ⊗ (p) = {(u, u ′ ) ∈ W ⊗ | M, u |= p}.
This product update yields a new L-model (M, w)⊗(M ′ , 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 ′ ).

Generalized DEL-sequents

In this section we define two different inference relations on formulas of L and L ′ representing an initial situation, a series of events and resulting epistemic situations. One relation enables to infer information about one of the epistemic situations, the other about one of the events:

1 Let Σ = (W ′ , R ′ , (w ′ 1 , . . . , w ′ n )
) be an action signature and let ϕ 1 , . . . , ϕn ∈ L. The L ′ -model associated to (Σ, ϕ 1 , . . . , ϕn) is the tuple M ′ = (W ′ , R ′ , V ′ ) where the valuation V ′ is defined as follows. We pick q ′ ∈ Φ ′ such that P re(q ′ ) = ⊤, and for all i ∈ {1, . . . , n}, we pick p ′ i ∈ Φ ′ such that P re(p ′ i ) = ϕ i . Then, for all i ∈ {1, . . . , n} we set

V ′ (p ′ i ) = {w ′ i }, we also set V ′ (q ′ ) = W ′ -{w ′ 1 , . . . , w ′ n }, and for all p ′ ∈ Φ ′ -{q ′ , p ′ 1 , . . . , p ′ n } we set V ′ (p ′ ) = ∅. Definition 1 Let ϕ 0 , ϕ 1 , . . . , ϕ n , ψ ∈ L, ϕ ′ 1 , . . . , ϕ ′ n , ψ ′ ∈ L ′ . We define the logical consequence relations ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n k 1 ψ where 0 ≤ k ≤ n, and ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n k 2 ψ ′ where 1 ≤ k ≤ n.
In the following i ranges over {0, . . . , n} and j ranges over {1, . . . , n}.

ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n k 1 ψ if for all pointed L-models (M 0 , w 0 ) and L ′ -models (M ′ j , w ′ j ), if we have for all i that (M i , w i ) = (M 0 , w 0 )⊗(M ′ 1 , w ′ 1 )⊗. . .⊗(M ′ i , w ′ i ) is defined 2 and M i , w i |= ϕ i , and for all j that M ′ j , w ′ j |= ϕ ′ j , then M k , w k |= ψ k . ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n k 2 ψ ′ if for all pointed L-models (M 0 , w 0 ) and L ′ -models (M ′ j , w ′ j ), if we have for all i that (M i , w i ) = (M 0 , w 0 )⊗(M ′ 1 , w ′ 1 )⊗. . .⊗(M ′ i , w ′ i ) is defined and M i , w i |= ϕ i , and for all j that M ′ j , w ′ j |= ϕ ′ j , then M ′ k , w ′ k |= ψ ′ k .
In fact, those two DEL-sequent relations are interdefinable:

Proposition 1 For all ϕ 0 , . . . , ϕ n ∈ L, ϕ ′ 1 , . . . , ϕ ′ n , ψ ′ ∈ L ′ and k ∈ {1, . . . , n}, ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n k 2 ψ ′ iff ϕ 0 , . . . , ϕ ′ k ∧ ¬ψ ′ , ⊤, ϕ ′ k+1 , . . . , ϕ n k 1 ¬ϕ
Proof i ranges over {0, . . . , n} and j ranges over {1, . . . , n}.

Suppose that ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n k 2 ψ ′ holds and let (M 0 , w 0 ) be a pointed L-model and (M ′ j , w ′ j ) be n pointed L ′ -models. Assume that for all i, M i , w i is defined and for all i = k, M i , w i |= ϕ i , for all j = k, M ′ j , w ′ j |= ϕ ′ j , and M ′ k , w ′ k |= ϕ ′ k ∧ ¬ψ ′ . Assume towards a contradiction that M k , w k |= ϕ k . Then, since ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n k 2 ψ ′ holds we have that M ′ k , w ′ k |= ψ ′ . This is a contradiction, so M k , w k |= ϕ k . Now suppose that ϕ 0 , . . . , ϕ ′ k ∧ ¬ψ ′ , ⊤, ϕ ′ k+1 , .
. . , ϕ n k 1 ¬ϕ k holds and let (M 0 , w 0 ) be a pointed L-model and (M ′ j , w ′ j ) be n pointed L ′ -models. Assume that for all i, M i , w i is defined and M i , w i |= ϕ i , and assume that for all j, M ′ j , w ′ j |= ϕ ′ j . Assume towards a contradiction that

M ′ k , w ′ k |= ψ ′ . Then M ′ k , w ′ k |= ¬ψ ′ , and because ϕ 0 , . . . , ϕ ′ k ∧ ¬ψ ′ , ⊤, ϕ ′ k+1 , . . . , ϕ n k 1 ¬ϕ k holds we have that M k , w k |= ¬ϕ k , which is a contradiction.
Moreover, the first relation can always be reduced to the case where information is inferred about the last situation:

Proposition 2 For all ϕ 0 , . . . , ϕ n ∈ L, ϕ ′ 1 , . . . , ϕ ′ n ∈ L ′ , k < n and ψ ∈ L, ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n k 1 ψ iff ϕ 0 , . . . , ϕ k ∧ ¬ψ, . . . , ϕ ′ n , ⊤ n 1 ¬ϕ n
Considering Propositions 1 and 2, in the rest of the paper we will only provide a tableau method for the DEL-sequent ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n n 1 ψ. In [START_REF] Aucher | Tableau method and NEXPTIME-completeness of DEL-sequents[END_REF], we defined three kinds of logical consequence relations dealing with a single event, which are special cases of the general relations defined here. Let ϕ 0 , ϕ 1 ∈ L and ϕ ′ ∈ L ′ . It holds that:

ϕ 0 , ϕ ′ ϕ 1 iff ϕ 0 , ϕ ′ , ⊤ 1 1 ϕ 1 ϕ ′ , ϕ 1 3 ϕ 0 iff ⊤, ϕ ′ , ϕ 1 0 1 ϕ 0 ϕ 0 , ϕ 1 2 ϕ ′ iff ϕ 0 , ⊤, ϕ 1 1 2 ϕ ′ 2 When i = 0 we let (M 0 , w 0 ) ⊗ (M ′ 1 , w ′ 1 ) ⊗ . . . ⊗ (M ′ i , w ′ i ) = (M 0 , w 0 ).

Inria 3 Tableau method

We consider 2n + 2 formulas, ϕ 0 , . . . , ϕ n , ψ ∈ L and ϕ ′ 1 , . . . , ϕ ′ n ∈ L ′ , and by P ⊂ Φ ′ we denote the finite set of all atomic events appearing in one of the event formulas ϕ ′ 1 , . . . , ϕ ′ n . i ranges over {0, . . . , n} and j ranges over {1, . . . , n}. We want to address the problem of deciding whether ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n n 1 ψ holds. To do so we equivalently decide whether this does not hold, i.e whether there exist a pointed L-model (M 0 , w 0 ) and n pointed L ′ -models (M ′ j , w ′ j ) such that for all i,

(M i , w i ) = (M 0 , w 0 ) ⊗ (M ′ 1 , w ′ 1 ) ⊗ . . . ⊗ (M ′ i , w ′ i ) is defined and M i , w i |= ϕ i , for all j M ′ j , w ′ j |= ϕ ′ j , and M n , w n |= ¬ψ.
In other terms, deciding whether ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n n 1 ψ holds reduces to the following problem called the satisfiability problem:

• Input: ϕ 0 , . . . , ϕ n , ψ ∈ L, ϕ ′ 1 , . . . , ϕ ′ n ∈ L ′
and Pre |P , the restriction of Pre to the domain P.

• Output: yes iff there exist a pointed L-model (M 0 , w 0 ) and n pointed L ′ -models

(M ′ j , w ′ j ) such that for all j, M ′ j , w ′ j |= ϕ ′ j , for all i, (M i , w i ) = (M 0 , w 0 ) ⊗ (M ′ 1 , w ′ 1 ) ⊗ . . . ⊗ (M ′ i , w ′ i ) is defined and M i , w i |= ϕ i , and M n , w n |= ψ.
In the rest of the paper, when the initial pointed model (M 0 , w 0 ) and the pointed event models (M ′ i , w ′ i ) are clear from the context, we shall write

M i for M 0 ⊗ M ′ 1 ⊗ . . . ⊗ M ′ i and w i for (w 0 , w ′ 1 , . . . , w ′ i ).

Tableau method description

Let Lab be a countable set of labels designed to represent worlds of the initial epistemic model. For all integers i, let Lab i be a countable set of labels designed to represent events of the i th event model. We suppose that Lab and Lab i for all i are disjoint. Our tableau method manipulates terms that we call tableau terms and they are of the following kind:

• (σ ϕ) means that M 0 , w 0 |= ϕ, where w 0 is the world of the initial epistemic model M 0 represented by σ and ϕ is a formula of L;

• (σ i ϕ ′ ) means that M ′ i , w ′ i |= ϕ ′
, where w ′ i is the event of the i th event model M ′ i represented by σ i , and ϕ ′ is a formula of L ′ ;

• (σ σ 1 . . . σ i ϕ) means that M i , (w 0 , w ′ 1 , . . . , w ′ i ) |= ϕ
, where w 0 is the world of M 0 represented by σ, w ′ k ∈ M ′ k is the event represented by σ k , and ϕ is a formula of L;

• (σ σ 1 . . . σ i 0) means that (w 0 , w ′ 1 , . . . , w ′ i ) is not in M i
, where w 0 is the world of M 0 represented by σ and w ′ k ∈ M ′ k is the event represented by σ k ; • (R a σ σ ′ ) means that the worlds w and u of M 0 represented respectively by σ and σ ′ are such that wR a u;

• (R i a σ i σ ′ i ) means that in M ′ i , the events w ′ and u ′ represented by σ i and σ ′ i are such that w ′ R ′ i a u ′ ; • ⊥ denotes an inconsistency.
We also use generic labels Σ to simplify notations: Σ can be either σ, σ i or σ σ

1 . . . σ i . (R a Σ Σ ′ ) is interpreted in the following way: if Σ = σ, Σ ′ = σ ′ then (R a Σ Σ ′ ) denotes (R a σ σ ′ ), if Σ = σ i , Σ ′ = σ ′ i then (R a Σ Σ ′ ) denotes (R i a σ i σ ′ i ), and if Σ = σ σ 1 . . . σ i , Σ ′ = σ ′ σ ′ 1 . . . σ ′ i then (R a Σ Σ ′ ) denotes (R a σ σ ′ )(R 1 a σ 1 σ 1 ) . . . (R i a σ i σ i ).
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 for a tuple (ϕ 0 , . . . , ϕ n , ϕ ′ 1 , . . . , ϕ ′ n ) of formulas is a finite tree with a set of tableau terms at each node.

The root is

Γ 0 = {(σ ϕ 0 ), (σ σ 1 ϕ 1 ), . . . , (σ σ 1 . . . σ n ϕ n ), (σ 1 ϕ ′ 1 ), . . . , (σ n ϕ ′ n )}∪ {(σ 1 p ′+ 1 ), . . . , (σ n p ′+ n )}
, where p ′+ 1 , . . . , p ′+ n are fresh new atomic events. Indeed, in our tableau method, when a new event label σ i is added to the set Γ of a node, it is assigned a fresh new atomic event p ′+ . By fresh we mean that they do not appear in any event formula ϕ ′ in Γ, and their precondition is also a fresh new atomic proposition that appears neither in any formula nor in any precondition of any atomic event p ′ of Γ. We denote it by Pre(p ′+ ) = p + . We abuse notations by writing p ′ ∈ Γ whenever p ′ occurs in a formula appearing in a tableau term in Γ. Those additional fresh atomic propositions and events are used in the tableau method to avoid the problematic case of events being built with trivial precondition.

A rule with numerator N is applicable to a node carrying a set Γ if Γ contains an instance of N . If no rule is applicable, Γ is said to be saturated. We call a node n an end node if the set of formulas Γ it carries is saturated, or if ⊥∈ Γ. The tableau 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 branch in a tableau 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 is closed if all its branches are closed, otherwise it is open. We write ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n 1 ψ if there is a closed tableau for (ϕ 0 , . . . , ϕ n-1 , ϕ n ∧ ¬ψ, ϕ ′ 1 , . . . , ϕ ′ n ).

Tableau rules

• Common rules for epistemic formulas and event formulas:

(Σ ϕ ∧ ψ) (Σ ϕ) (Σ ψ) ∧ (Σ ¬(ϕ ∧ ψ)) (Σ ¬ϕ) | (Σ ¬ψ) ¬∧ (Σ ¬¬ϕ) (Σ ϕ) ¬ (Σ p)(Σ ¬p) ⊥ ⊥ (Σ B a ϕ) (R a Σ Σ + )(Σ + ϕ)(σ + 1 p ′+ 1 ) . . . (σ + i p ′+ i ) B a (Σ B a ϕ)(R a Σ Σ ′ ) (Σ ′ ϕ) | (Σ ′ 0) B a
where p is in Φ ∪ Φ ′ , σ + 1 . . . σ + i are the σ + k in the fresh generic label Σ + (none if Σ + = σ + ) and p ′+ k are fresh new atomic events with Pre(p ′+ i ) = p + i .

• Specific rule for event formulas:

Inria (σ i p ′ )(σ i p ′′ ) ⊥ Excl
where p ′ , p ′′ are not fresh (p ′ , p ′′ ∈ Γ 0 ) and p ′ = p ′′ .

• Specific rules for epistemic formulas:

(σ σ 1 . . . σ i p) (σ p) ← 1 (σ σ 1 . . . σ i ¬p) (σ ¬p) ← 2 (σ 0) ⊥ Pre 0 (σ σ 1 . . . σ i ϕ)(σ i p ′ ) (σ σ 1 . . . σ i-1 Pre(p ′ )) Pre 1 ϕ = 0, i > 0 (σ σ 1 . . . σ i 0)(σ i p ′ ) (σ σ 1 . . . σ i-1 ¬Pre(p ′ )) | (σ σ 1 . . . σ i-1 0) Pre 2 i > 0
We explain informally the meaning of these rules. The boolean rules, rule B a and rule B a are classic. Rule Excl enforces the Exclusivity of event models. It does not apply to the fresh atomic events that we add at the creation of each event label, because a "meaningful" atomic event may be added to such a label; however these fresh events are removed from the final constructed models unless they are the only atomic event in their possible event. Rules ← 1 and ← 2 reflect the fact that for a world (w 0 , w ′ 1 , . . . , w ′ i ) in M i , by definition of the update product,

M i , (w 0 , w ′ 1 , . . . , w ′ i ) |= p if, and only if, M 0 , w 0 |= p. Rule Pre 1 says that if (w 0 , w ′ 1 , . . . , w ′ i ) is in M i and M ′ i , w ′ i |= p ′ , then (w 0 , w ′ 1 , . . . , w ′ i-1 ) is in M i-1 and M i-1 , (w 0 , w ′ 1 , . . . , w ′ i-1 ) verifies Pre(p ′ ). Rule Pre 2 says that if (w 0 , w ′ 1 , . . . , w ′ i ) is not in M i and M ′ i , w ′ i |= p ′ , either (w 0 , w ′ 1 , . . . , w ′ i-1 ) is not in M i-1 , or it is in M i-1 but M i-1 , (w 0 , w ′ 1 , . . . , w ′ i-1
) |= Pre(p ′ ). Finally, Rule Pre 0 is used to forbid the rightmost choice in Rule Pre 2 when i = 1. Indeed it would make no sense to say that the world associated to a label σ must not be in the initial model M 0 when it has been created to be in M 0 .

Proposition 3 (Tableau method soundness) For all ϕ 0 , . . . , ϕ n , ψ ∈ L, for all ϕ

′ 1 , . . . , ϕ ′ n ∈ L ′ , ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n 1 ψ implies ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n n 1 ψ.
Proof We prove it by contrapositive. Suppose that there exist a pointed L-model (M 0 , w 0 ), and n L ′ -models (M ′ j , w ′ j ) such that for all i, M i , w i is defined and M i , w i |= ϕ i , for all j, M ′ j , w ′ j |= ϕ ′ j and M n , w n |= ψ. We must prove that every tableau for (ϕ 0 , . . . , ϕ n-1 , ϕ n ∧ ¬ψ, ϕ ′ 1 , . . . , ϕ ′ n ) has an open branch (the proof of termination is in the proof of Lemma 8).

We say that a set Σ of tableau terms is interpretable with respect to a subset of relevent atomic events S ′ if there exists an L-model M 0 , n L ′ -models M ′ i , partial functions ν : Lab → W and ν i : Lab i → W ′ i (where i ranges over {1 . . . , n}) defined exactly on labels that appear in Σ such that (M, (M ′ i ) 1≤i≤n , ν, (ν i ) 1≤i≤n ) makes all the tableau terms in Σ true for the following semantics |= T :

(M 0 , (M ′ i ) 1≤i≤n , ν, (ν i ) 1≤i≤n ) |= T (σ ϕ) iff M, ν(σ) |= ϕ (M 0 , (M ′ i ) 1≤i≤n , ν, (ν i ) 1≤i≤n ) |= T (σ i ϕ ′ ) iff ϕ ′ = p ′ for some p ′ / ∈ S ′ or M ′ i , ν i (σ i ) |= ϕ ′ (M 0 , (M ′ i ) 1≤i≤n , ν, (ν i ) 1≤i≤n ) |= T (R a σ σ ′ ) iff ν(σ)R a ν(σ ′ ) (M 0 , (M ′ i ) 1≤i≤n , ν, (ν i ) 1≤i≤n ) |= T (R ′ i a σ i σ ′ i ) iff ν i (σ i )R ′ i a ν i (σ ′ i )
We prove the contrapositive. Suppose there is a tableau for (ϕ 0 , . . . , ϕ n-1 , ϕ n ∧¬ψ, ϕ ′ 1 , . . . , ϕ ′ n ) that has an open branch. We prove that there exist a pointed L-model (M 0 , w 0 ) and n pointed L ′ -models (M ′ j , w ′ j ) such that for all j, M ′ j , w ′ j |= ϕ ′ j , for all i, w i ∈ M i and M i , w i |= ϕ i , and M n , w n |= ¬ψ.

Let Γ f be the set of tableau terms carried by the end node of the open branch. We define M 0 , M ′ 1 , . . . , M ′ n as follows.

• Let M 0 = (W, R, V ) with W = {w σ | (σ ψ) ∈ Γ f }, R(a) = {(w σ , w σ ′ ) | (R a σ σ ′ ) ∈ Γ f } and V (p) = {w σ | (σ p) ∈ Γ f }. • Let M ′ i = (W ′ i , R ′ i , V ′ i ) with W ′ i = {w ′ σi | (σ i ϕ ′ ) ∈ Γ f }, R ′ i (a) = {(w ′ σi , w ′ σ ′ i ) | (R i a σ i σ ′ i ) ∈ Γ f } and V ′ i (p ′ ) = {w ′ σi | (σ i p ′ ) ∈ Γ f } if p ′ ∈ Γ 0 {w ′ σi | (σ i p ′ ) ∈ Γ f and (σ i p ′′ ) / ∈ Γ f for all p ′′ = p ′ } otherwise.
Notice that each event model M ′ i verifies the Exclusivity condition: by saturation of rule Excl, there can not be p ′ and p ′′ in Γ 0 in the same event otherwise the branch would be closed, and the fresh p ′+ assigned to an event label σ i at its creation is kept in w ′ σi only if there is no other atomic event in this event. So for every event w ′ σi , there is exactly one atomic event

p ′ such that w ′ σi ∈ V ′ i (p ′ ). Finally, for i ∈ {1, . . . , n} we define M i as M 0 ⊗ M ′ 1 ⊗ . . . ⊗ M ′ i .
Lemmas 5 and 6 below establish the completeness of our tableau method.

Lemma 5 Let ϕ ∈ L and ϕ ′ ∈ L ′ such that ϕ ′ not a fresh atomic event. If (σ ϕ) ∈ Γ f then M 0 , w σ |= ϕ, and if (σ i ϕ ′ ) ∈ Γ f , then M ′ i , w ′ σi |= ϕ ′ .
Proof We only prove it for M 0 , it is similar for M ′ i . The proof is done by induction on ϕ.

p, ¬p: by definition of M 0 , w σ ∈ V (p) if and only if (σ p) ∈ Γ f . So if (σ p) ∈ Γ f , M 0 , w σ |= p, and if (σ ¬p) ∈ Γ f , we have that (σ p) / ∈ Γ f (otherwise the branch would be closed by saturation of rule ⊥), hence M 0 , w σ |= ¬p. As for the case ϕ ∧ ψ, by saturation of rule ∧, Γ f also contains (σ ϕ) and (σ ψ). By induction hypothesis we have that M 0 , w σ |= ϕ and M 0 , w σ |= ψ, so M 0 , w σ |= ϕ ∧ ψ. The cases ¬(ϕ ∧ ψ) and ¬¬ϕ are proved similarly.

B a ϕ: By saturation of rule B a (with Σ of the form σ), there exists σ ′ such that (R a σ σ ′ ) ∈ Γ f and (σ ′ ϕ) ∈ Γ f . By induction hypothesis M 0 , w σ ′ |= ϕ, and w σ R a w σ ′ holds by construction of M 0 , so M 0 , w σ |= B a ϕ.

B a ϕ: Take some w σ ′ in W 0 such that w σ R a w σ ′ holds, we prove that M 0 , w σ ′ |= ϕ and conclude that M 0 , w σ |= B a ϕ. Since w σ R a w σ ′ holds we know by construction of M that (R a σ σ ′ ) is in Γ f . So by saturation of rule B a , (σ ′ ϕ) also belongs to Γ f , and by induction hypothesis

M 0 , w σ ′ |= ϕ. Lemma 6 Let ϕ ∈ L. For all i such that 0 ≤ i ≤ n, if (σ σ 1 . . . σ i ϕ) ∈ Γ f , then w i = (w σ , w ′ σ1 , . . . , w ′ σi ) ∈ M i and M i , w i |= ϕ. If (σ σ 1 . . . σ i 0) ∈ Γ f , then w i / ∈ M i .
Proof We prove it by double induction on i and ϕ ′ . For i = 0: if ϕ ∈ L, the result holds by Lemma 5. If ϕ = 0, (σ 0) ∈ Γ f , hence by saturation of rule Pre 0 , the branch is closed. Contradiction. Now assume that the result holds for i < n, we prove it for i + 1.

We write w i = (w σ , w ′ σ1 , . . . , w ′ σi ), w i+1 = (w σ , w ′ σ1 , . . . , w ′ σi+1 ) and we start with the case where (σ σ 1 . . . σ i+1 0) ∈ Γ f . Let p ′ be the only atomic event true in event w ′ σi+1 . We have (σ i+1 p ′ ) ∈ Γ f , and by saturation of Rule Pre 2 , we obtain two cases.

If (σ σ 1 . . . σ i ¬Pre(p ′ )) ∈ Γ f , then by induction hypothesis M i , w i |= Pre(w ′ σi+1 ), hence w i+1 is not in M i+1 . If (σ σ 1 . . . σ i 0) ∈ Γ f , by induction hypothesis, w i is not in M i , hence M i+1 , w i+1 is not defined.
Now the case where (σ σ 1 . . . σ i+1 ϕ) ∈ Γ f with ϕ = 0. We first prove that w i+1 ∈ M i+1 : by construction of M ′ i there is exactly one

p ′ ∈ Φ ′ such that w ′ σi+1 ∈ V ′ i+1 (p ′ ), and
(σ i+1 p ′ ) ∈ Γ f . By saturation of Rule Pre 1 , (σ σ 1 . . . σ i Pre(p ′ )) is in Γ f ,

and by induction hypothesis,

w i ∈ M i and M i , w i |= Pre(p ′ ). Since Pre(w ′ σi+1 ) = Pre(p ′ ), we have that M i , w i |= Pre(w ′ σi+1 ), hence w i+1 is in M i+1 .
We prove that M i+1 , w i+1 |= ϕ.

p, ¬p: By saturation of Rule ← 1 , (σ p) ∈ Γ f , and so M 0 , w σ |= p by Lemma 5. Since w i+1 ∈ M i+1 , M i+1 , w i+1 |= p by definition of the product update. The proof for ¬p is similar to the case of p. The proof of the other boolean cases ϕ ∧ ψ, ¬(ϕ ∧ ψ) and ¬¬ϕ is obtained by applying straightforwardly the Induction Hypothesis.

B a ϕ: If (σ σ 1 . . . σ i+1 B a ϕ) ∈ Γ f , then by saturation of Rule B a , (R a σ σ + ), (R 1 a σ 1 σ + 1 ), . . . , (R i a σ i+1 σ + i+1 ), (σ + σ + 1 . . . σ + i+1 ϕ) and (σ + 1 p ′+ 1 ), . . . , (σ + i+1 p ′+ i+1 ) are in Γ f . Let u i+1 = (w σ + , w ′ σ + 1 , . . . , w ′ σ + i+1
). Since

(σ + σ + 1 . . . σ + i+1 ϕ) is in Γ f , by induction hypothesis, u i+1 is in M i+1 and M i+1 , u i+1 |= ϕ. By construction of M 0 and M ′ j , for 1 ≤ j ≤ i + 1, we have w σ R a w σ + , w ′ σ1 R 1 a w ′ σ + 1 , . . . , w ′ σi+1 R i+1 a w ′ σ + i+1
, so w i+1 R i+1 a u i+1 , hence the result.

B a ϕ: If (σ σ 1 . . . σ i+1 B a ϕ) ∈ Γ f , take u i+1 = (w σ ′ , w ′ σ ′ 1 , . . . , w ′ σ ′ i+1
) in M i+1 such that w i+1 R i+1 a u i+1 , we prove that M i+1 , u i+1 |= ϕ. By definition of the product and of the models M 0 and M ′ 1 , . . . , M ′ i+1 , we have that (R a σ σ ′ ), (R 1 a σ i σ ′ i ), . . . , (R i a σ i σ ′ i ) are in Γ f . By saturation of Rule B a , whether (σ ′ σ ′ 1 . . . σ ′ i+1 ϕ) is in Γ f in which case we conclude by induction hypothesis, or (σ ′ σ ′ 1 . . . σ ′ i+1 0) is in Γ f and by induction hypothesis u i+1 is not in M i+1 , which is a contradiction.

NEXPTIME-completeness and implementation

The NEXPTIME-completeness of our simple DEL-sequents [START_REF] Aucher | Tableau method and NEXPTIME-completeness of DEL-sequents[END_REF] extends to generalized DELsequents.

Proposition 7

The satisfiability problem is NEXPTIME-complete Lemma 8 The satisfiability problem is in NEXPTIME.

Proof The tableau rules presented in Subsection 3.2 give rise to a non-deterministic algorithm running in exponential time. The algorithm starts with the following set of tableau formulas

Γ 0 = {(σ ϕ 0 ), (σ σ 0 1 ϕ 1 ), . . . , (σ σ 0 1 . . . σ 0 n ϕ n ), (σ 0 1 ϕ ′ 1 ), . . . , (σ 0 n ϕ ′ n )} ∪ {(σ 0 1 p ′+ 1 ), . . . , (σ 0 n p ′+ n )}

Inria

where the p ′+ 1 , . . . p ′+ n are fresh new atomic events. Let δ(.) be the function that gives the modal depth of a given formula. Let max pre be the maximum of δ(Pre(p ′ )) where p ′ ranges over the propositions appearing in the formulas ϕ ′ 1 , . . . , ϕ ′ n . Let (∆W i ) i∈{0,...,n} be defined as follows:

• ∆W n = δ(ϕ n ) • ∆W i = max(δ(ϕ ′ i ) + max pre , δ(ϕ i )) if 0 < i < n • ∆W 0 = max(δ(ϕ ′ i ) + max pre , δ(ϕ i ), ∆W 1 , . . . , ∆W n ).
The algorithm runs as follows. Let N = ∆W 0 . For t = 0 to N , we execute:

1. Γ t ′ := the saturation of Γ t by rules ∧, ¬∧, ¬, ⊥, Excl, ← 1 , ← 2 , Pre 1 , Pre 2 ;

2. If ⊥ ∈ Γ t ′ , we stop the current execution;

3. Γ t+1 := the set of tableau terms obtained by applying B a , B a on Γ t ′ .

Step 1 is non-deterministic and corresponds to a Boolean saturation of labels of depth i. It non-deterministically runs in linear size of Γ i . Step 2 consists in checking if rule ⊥ has been executed. In this case, the current execution halts.

Remark that the term of the modal depth of ϕ ′ in terms of the form (σ i ϕ ′ ) is strictly decreasing when we apply rule B a and B a . So when t > δ(ϕ ′ i ), the set Γ t will not contain any terms of the form (σ i ϕ ′ ).

Let us prove by induction that for all i we have the following property P (i): for all t > ∆W i , the set Γ t will not contain any term of the form (σ σ 1 . . . σ i ψ).

Let us begin with the basic case: i = n. Note that the maximal depth of formulas ψ in tableau terms corresponding to the last product model, that is, the modal depth of ψ in terms of the form (σ σ 1 . . . σ n ψ) in Γ t is strictly decreasing with t (see rule B a and B a ). So when t > ∆W n , there is no more tableau formula of the form (σ σ 1 . . . σ n ψ) in Γ t where ψ is a formula or 0. So when t > δ(ϕ), the rules Pre 2 , B a and B a will no more be applied to terms of the form (σ σ 1 . . . σ n ψ). So P (n) is true. Now suppose P (i + 1) and let us prove P (i). Suppose there exists t > ∆W i such that Γ t contains a term of the form (σ σ 1 . . . σ i ψ). As the modal depth decreases at each step, if ψ is a subformula of ϕ i , we have t ≤ δ(ϕ i ). Also by definition of ∆W i , we have δ(ϕ i ) ≤ ∆W i . This leads to a contradiction with t > ∆W i . So the formula ψ is either a subformula of a (possibility negated) precondition added from rule P re 1 or P re 2 [START_REF] Aucher | An internal version of epistemic logic[END_REF] or is a literal from ← 1 or ← 2 (2).

In the case (1), it implies that t ≤ ∆W i + 1 + max pre . There is a contradiction. In the case (2), it implies that t ≤ ∆W i for all i > 0. There is a contradiction.

That is why we have Γ N +1 = ∅ and the algorithm has applied rules until saturation, that is, the set of tableau formulas N t=0 Γ t is saturated. Now let us have a look at the time required to execute the algorithm. Let x be the size of the input, that is the sum of the sizes of ϕ 0 , . . . , ϕ n , ϕ ′ 1 , . . . , ϕ ′ n , ϕ and the function Pre.

Step 1 saturates the nodes σ, σ i and (σ σ 1 . . . σ i ) appearing in the tableau formulas in Γ t . For each of those worlds, the saturation is linear in x.

Step 3 creates new tableau terms for each B a -formula appearing in Γ t ′ : more precisely each B a -formula creates at most n-new labels σ + , σ + 1 , . . . , σ + n . So for each world in Γ t it produces at most x worlds in the initial model, x worlds in each i-th event model, x worlds in the i-th product model, that is to say it produces at most (2x) n new worlds. If we note y t the maximal number of worlds in Γ t , we have that y t+1 = (2x) n y t . So y t = (2x) nt . Now, remark

RR n°8012

that N = max(max(δ(ϕ ′ 1 ), . . . , δ(ϕ ′ n )) + max pre , δ(ϕ 0 ), . . . , δ(ϕ n )) ≤ x.The total number of created worlds is bounded by Σ N t=0 y t ≤ Σ x t=0 (2x) nt ≤ (2x) n(x+1) and this construction takes an exponential amount of time.

Lemma 9

The satisfiability problem is NEXPTIME-hard.

Proof The satisfiability problem is NEXPTIME-hard because we can encode in it the satisfiability problem of a syntactic fragment. This syntactic fragment is studied in the proof of the Proposition 4.2 in [START_REF] Aucher | Tableau method and NEXPTIME-completeness of DEL-sequents[END_REF] and we summarize here the result in the following fact.

Claim 1

The following problem

• input: ϕ 0 , ϕ 1 ∈ L and ϕ ′ 1 ∈ L such that: -there is only one agent a occurring in ϕ 0 , ϕ 1 , ϕ ′ 1 ; -ϕ 1 is of the form ψ 1 ∧ i≤δ(ϕ ′ 1 ) i=1 B i
a p ′ where ψ 1 does not contain any atomic event; -Pre(p ′ ) = ⊤.

• output: yes iff ϕ 0 , ϕ ′ 1 , ⊤ 1 1 ϕ 1 does not hold.
is NEXPTIME-hard.

An implementation of the tableau method can be found at the following webpage:

http://www.irisa.fr/prive/fschwarz/lotrecscheme/.

The tableau rules are written in LotrecScheme [START_REF] Schwarzentruber | [END_REF] which is a term rewriting system designed for implementing tableau methods. The corresponding rules can be found directly in the software by clicking 'open' and 'generalized DEL-sequents'.

The implemented rules are similar to those presented in Subsection 3.2. There are two main differences. The first one is that we tag worlds with ok and ¬ok to say respectively that the node belongs to the model or not. We use those two tags for a reason of efficiency. The second difference concerns the pattern-matching of a condition of a rule: as LotrecScheme does not enable an arbitrary number of terms to match in a condition, we adapt the method so that the numbers of terms in all rules are fixed. For instance, let us consider the rule B a . (R a Σ Σ ′ ) is a macro to denote an arbitrary number of terms whereas in the implementation (R a Σ Σ ′ ) is not a macro but a term and we have to simulate the way relations are defined in the product update:

(R a Σ Σ ′ )(R a a b)(Σ :: a ok) (R a Σ :: a Σ ′ :: b) and (R a Σ :: a Σ ′ :: b) (R a Σ Σ ′ )(R a a b)
where a, b, Σ and Σ ′ are terms, and where Σ :: a is the concatenation of Σ and a, and Σ ′ :: b is the concatenation of Σ ′ and b. Σ and Σ ′ are sequences of labels, and a and b are labels representing worlds of an event model.

Extension to other semantics

In this section, we investigate the complexity of the satisfiability problem with semantics where the accessibility relations are also assumed to be reflexive or serial (an accessibility relation R a is reflexive when for all w ∈ W , w ∈ R a (w), and serial when for all w ∈ W , there is u ∈ W such that u ∈ R a (w)).

For reflexivity, we add the following rule to the tableau method:

Inria (Σ ϕ) (R a Σ Σ) T
where Σ can be σ or σ i (reflexivity of product models stems from initial and event models being reflexive). This rule is sound and complete with respect to reflexive models.

For seriality, we add the following rule to the tableau method:

(Σ B a ϕ) (R a Σ Σ + )(Σ + ϕ) D
where Σ can be σ, σ i or σ σ 1 . . . σ i . This rule is sound and complete with respect to serial models. There is no problem of termination because we add a successor to a node if, and only if there is a modal formula in it.

Proposition 10

The satisfiability problem when the relations are reflexive or serial is NEXPTIME-complete.

For the membership, it suffices to notice that adding the rule for reflexivity of seriality to the tableau method does not modify the proof of NEXPTIME membership 8.

For the lower-bound, we reduce the satisfiability problem given in the proof of Lemma 9 to the satisfiability problems when the relations are reflexive and when the relations are serial. Given new fresh atomic propositions p 0 , p 1 , . . . , let us consider the two following translations:

tr k (p) = p tr ′ k (p ′ ) = p ′ k tr k (⊥) = ⊥ tr ′ k (⊥) = ⊥ tr k (B j ψ) = B j (p k+1 → tr k+1 (ψ))
tr ′ k (B j ψ) = B j (p ′ k+1 → tr k+1 (ψ)) where Pre(p ′ k ) = p k for all k. We define tr(ϕ) = p 0 ∧ tr 0 (ϕ) and tr ′ (ϕ ′ ) = p ′ 0 ∧ tr ′ 0 (ϕ ′ ). The three following statements are equivalent:

1. ϕ 0 , ϕ ′ , ϕ 1 is satisfiable 2. tr(ϕ 0 ), tr ′ (ϕ ′ ), tr(ϕ 1 ) is satisfiable in reflexive models 3. tr(ϕ 0 ), tr ′ (ϕ ′ ), tr(ϕ 1 ) is satisfiable in serial models.

(i) → (ii): If ϕ 0 , ϕ ′ , ϕ 1 is satisfiable, then ϕ 0 , ϕ ′ , ϕ 1 is satisfiable in models that are trees (indeed, the tableau method is sound and complete and the corresponding models are trees). So there exists a tree-model M = (W, R, V ), a world w ∈ W , and a tree event model M ′ = (W ′ , R ′ * , V ′ ) and an event w ′ ∈ W ′ such that M, w |= ϕ 0 , M ′ , w ′ |= ϕ ′ and M ⊗ M ′ , (w, w ′ ) |= ϕ 1 . We add reflexive edges at each worlds in M and M ′ . We also extend the valuations so that p k is true in a world u of M iff the depth of u in the tree-model M is equal to k. Let M * = (W * , R * , V * ) and M ′ * = (W ′ * , R ′ * , V ′ * ) be the resulting models. We have:

• R a = R a * ∩ {(u, v) | for all k, if u ∈ V (p k ) then u ∈ V (p k+1 ) } • and R ′ = R ′ * ∩ {(u ′ , v ′ ) | for all k, if u ′ ∈ V ′ (p ′ k ) then v ′ ∈ V ′ (p ′ k+1 ) }.
We have M * , w |= tr(ϕ 0 ), M ′ * , w ′ |= tr ′ (ϕ ′ ) and M * ⊗ M ′ * , (w, w ′ ) |= tr(ϕ 1 ).

(ii) → (iii): This direction is trivial. (iii) → (i): Suppose that there exist a serial epistemic model M * = (W, R * , V ), w ∈ W , a serial event model M ′ * = (W ′ , R ′ * , V ′ ) and w ′ ∈ W ′ such that M * , w |= tr(ϕ 0 ), M ′ * , w ′ |= tr ′ (ϕ ′ ), M * ⊗ M ′ * , (w, w ′ ) |= tr(ϕ 1 ) and M * ⊗ M ′ * is serial. We define the following new model M = (W, R, V ) in the following way: it ([2] deals more with synthesis), it can still be instrumental in finding out some of its necessary properties. It can also be used during the design of the epistemic plan itself to check that we are designing it in the 'right' direction.

As the title of this paper suggests, we have generalized our previous work [START_REF] Aucher | Tableau method and NEXPTIME-completeness of DEL-sequents[END_REF] to arbitrary long sequences of events, and extended it to the case of reflexive or serial models. Also we illustrate our method by encoding the coordinated attack problem. However, other generalizations still need to be done, such as the addition of a common knowledge operator in the language (as illustrated in Section 6) and the integration of ontic events.

2 .

 2 (a) If ρ has only one denominator, add the appropriate instanciation to Γ. (b) If ρ has k denominators with k > 1, create k successor nodes for n, where each successor i carries the union of Γ with an appropriate instanciation of denominator D i .

RR n°8012

In[START_REF] Dupin De Saint-Cyr | Belief extrapolation (or how to reason about observations and unpredicted change)[END_REF], Dupin de Saint-Cyr and Lang define an operator of "extrapolation". This operator takes as input a temporal formula, which corresponds to a sequence of observations under the form of propositional formulas indexed by time stamps, and yields as output another temporal formula, which corresponds semantically to the preferred sequences of states which satisfy the input temporal formula. The authors follow an internal approach. In[START_REF] Booth | Reconstructing an agent's epistemic state from observations about its beliefs and non-beliefs[END_REF], Booth and Nittka RR n°8012

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

(M 0 , (M ′ i ) 1≤i≤n , ν, (ν i ) 1≤i≤n ) |= T (σ σ 1 . . . σ i 0) iff (ν(σ), ν 1 (σ 1 ), . . . , ν i (σ i )) / ∈ M i (M 0 , (M ′ i ) 1≤i≤n , ν, (ν i ) 1≤i≤n ) |= T (σ σ 1 . . . σ i ϕ i ) iff w i ∈ M i , where w i = (ν(σ), ν 1 (σ 1 ), . . . , ν i (σ i )), and M i , w i |= ϕ i (M 0 , (M ′ i ) 1≤i≤n , ν, (ν i ) 1≤i≤n ) |= T ⊥ iff false Since ϕ 0 , ϕ ′ 1 , ϕ 1 , . . . , ϕ ′ n , ϕ n n 1 ψ, the set Γ 0 = {(σ ϕ 0 ), (σ σ 1 ϕ 1 ), . . . , (σ σ 1 . . . σ n-1 ϕ n-1 )} ∪{(σ σ 1 . . . σ n ϕ n ∧¬ψ), (σ 1 ϕ ′ 1 ), . . . , (σ n ϕ ′ n ), (σ 1 p ′+ 1 ), . . . , (σ n p ′+ n )} 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 , . . . , ϕ n-1 , ¬ϕ n , ϕ ′ 1 , . . . , ϕ ′ n ) has an open branch. We only prove it for Excl, B a and B a when Σ = σ σ 1 . . . σ i , and the specific rules for epistemic formulas, the proof for the other rules being standard. 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.

, and M ′′ j being the same as M ′ j except that its valuation maps p ′+ j to {u ′ j }, we have that

, or u i ∈ M i , and by definition of R i a we have that w i R i a u i , hence M i , u i |= ϕ and we conclude that

The case of rule ← 2 is proved similarly.

Rules Pre 1 and Pre 2 :

There are two cases: either

. Rules Pre 0 and Excl are sound since their numerator is never interpretable.

Proposition 4 (Tableau method completeness) For all ϕ 0 , . . . , ϕ n , ψ ∈ L, for all

and

Example: coordinated attack problem

In this section, we assume that there are only two agents a and b. We extend our epistemic language L with the common knowledge operator C a,b ϕ. The truth conditions of the common knowledge operator are defined as follows:

Intuitively, C a,b ϕ is an abbreviation of an infinite conjunction (see [START_REF] Fagin | Reasoning about knowledge[END_REF] for more details):

The definitions of DEL-sequents of Definition 1 can easily be adapted to this extended language with common knowledge.

The coordinated attack problem from the distributed systems folklore can be described informally as follows. Two generals need to attack their common enemy simultaneously if they want to win. However, their only way to communicate is by means of a messenger, and this messenger may be captured at any time between the two camps. If we assume that the messenger is really lucky and never gets caught on that particular night, how long will it take for the generals to coordinate an attack?

We can model this problem within our framework. Assume that general a has decided to attack at dawn. General a then sends a messenger to general b to inform him of his decision. The content of the first message sent by general a to general b is represented by the propositional letter attack standing for 'general a has decided to attack at dawn'. This message eventually reaches general b, but general a does not know it yet. This event is represented by an atomic event p ′ 1 standing for 'general b receives the decision of general a to attack at dawn'. Its precondition is Pre(p ′ 1 ) = attack. The only information we have about this event p ′ 1 is that general b knows about its occurrence:

As a result of this event, general b now knows that general a has decided to attack: B b attack. However, general a does not know it, so they still cannot coordinate a simultaneous attack. Therefore, general b sends an acknowledgement to general a. This message eventually reaches general a. This event is represented by the atomic event p ′ 2 standing for 'general a receives the first acknowledgement of general b'. The precondition of atomic event p ′ 2 is Pre(p ′ 2 ) = B b attack. This time, general b does not know that his message has been delivered. Therefore, the only information we have about this event p ′ 2 is that general a knows about its occurrence: B a p ′ 2 . As a result of this event, general a now knows that general b knows that general a has decided to attack: B a B b attack. However, there is still no common knowledge that general a has decided to attack. This informal reasoning could go on indefinitely. It shows that common knowledge that general a has decided to attack cannot be attained.

The above informal reasoning can be formalized within our framework in a natural way. To achieve this aim, we define for all k ∈ N * the atomic event p ′ k whose precondition is Pre(p

The statement that after any Inria finite number of messages exchanged, it is impossible to infer that there is common knowledge that general a has decided to attack is formalized by the fact that, for all k ∈ N * :

This result is itself due to the following fact:

Proof To prove the result of the coordinated attack problem, we define the following epistemic model M = (W, R, V ) by:

We define the following event models M ′k = (W ′k , R ′k , V ′k ) for all k ∈ N. In the DEL literature, these event models represent private announcements. If k is even, (M ′k , w ′k ) represents the private announcement to general a that B b B a B b . . . B a B b attack holds, and if k is odd, (M ′k , w ′k ) represents the private announcement to general b that B a B b . . . B a B b attack holds.

• W ′k = {w ′k , u ′k };

• R ′k a = {(w ′k , w ′k ), (u ′k , u ′k )}; R ′k b = {(w ′k , w ′k ), (w ′k , u ′k ), (u ′k , u ′k )} if k is even; • R ′k b = {(w ′k , w ′k ), (u ′k , u ′k )}; R ′k a = {(w ′k , w ′k ), (w ′k , u ′k ), (u ′k , u ′k )} if k is odd;

We illustrate our tableau method by proving this fact for k = 1 in Figure 1. Remark that E 2 a,b attack = B a (B a attack∧B b attack)∧B b (B a attack∧B b attack). Also, we only show one branch of the full tableau, the one which is open.

Conclusion

Related work

address a similar problem but with an imperfect external approach (see [START_REF] Aucher | An internal version of epistemic logic[END_REF] for more details on the different modeling approaches). They are interested in inferring what the agent believed (or will believe) at a given moment, based on a sequence of observations consisting of responses that the agent has given to a sequence of belief revision inputs. Both papers deal with situations involving a single agent. Our approach is different from both approaches, because we do not strive to "extrapolate" new information from existing observations by resorting to an argument of minimal change. Instead, we are only interested in inferring some necessary property that follows from these existing observations. Some tableau methods have been proposed for DEL, but only for public announcement logic [START_REF] Balbiani | Tableaux for public announcement logic[END_REF][START_REF] De | KE tableaux for public anouncement logic[END_REF] and hybrid public anouncement logic [START_REF] Ulrik | Terminating tableaux for dynamic epistemic logic[END_REF]. A terminating tableau method has also been proposed for the full BMS framework in [START_REF] Ulrik | Terminating tableaux for dynamic epistemic logic[END_REF] by encoding the reduction axioms as tableau rules. However, none of these tableau methods can somehow address the two problems raised in the introduction, because the BMS language of [START_REF] Baltag | Logic for epistemic programs[END_REF] does not allow for partial and incomplete descriptions of events: an event model or a formula announced publicly specifies completely how all the agents perceive the occurrence of the corresponding event. In particular, it is impossible to model the coordinated attack problem.

In [START_REF] Baltag | Algebra and sequent calculus for epistemic actions[END_REF], a sequent calculus has been developed, yet in an algebraic setting, making a systematic comparison difficult. Their sequents m 1 , . . . , q 1 , . . . , A 1 , . . . , m k , . . . , q l , . . . , A n ⊢ δ are arbitrarily long and consist of different types of formulas which can contain propositions m 1 , . . . , m k , events q 1 , . . . , q l and agents A 1 , . . . , A n , and which resolve into a single proposition or event δ. A sequent calculus has also been proposed for public announcement logic [START_REF] Maffezioli | A gentzen-style analysis of public announcement logic[END_REF] which, alike our tableau terms, refers explicitely to possible worlds and relations.

Concluding remarks

As we said in the previous subsection, our tableau method can infer necessary information which was somehow already encoded in the sequence. In fact, our method allows us to verify in a complexity-optimal way that a piece of information about a sequence of events does follow from this sequence. It also allows us to check that a given epistemic plan (viewed as a sequence of event properties) yields an epistemic goal. Even if it does not provide an algorithm to synthesize Inria