# Continuous speech separation using speaker inventory for long multi-talker
recording

###### Abstract

Leveraging additional speaker information to facilitate speech separation has
received increasing attention in recent years. Recent research includes
extracting target speech by using the target speaker’s voice snippet and
jointly separating all participating speakers by using a pool of additional
speaker signals, which is known as speech separation using speaker inventory
(SSUSI). However, all these systems ideally assume that the pre-enrolled
speaker signals are available and are only evaluated on simple data
configurations. In realistic multi-talker conversations, the speech signal
contains a large proportion of non-overlapped regions, where we can derive
robust speaker embedding of individual talkers. In this work, we adopt the
SSUSI model in long recordings and propose a self-informed, clustering-based
inventory forming scheme for long recording, where the speaker inventory is
fully built from the input signal without the need for external speaker
signals. Experiment results on simulated noisy reverberant long recording
datasets show that the proposed method can significantly improve the
separation performance across various conditions.

Index Terms—  Speech separation, continuous speech separation, speaker
inventory, embedding clustering

##  1 Introduction

Single-channel speech separation has been a challenging speech signal
processing problem, and deep learning has provided advanced methods toward
solving this problem [1, 2, 3, 4, 5, 6, 7]. In recent years, research that
leverages additional speaker information has received increasing attention [8,
9, 10, 11, 12, 13, 14]. We can categorize them into two main categories. The
first category is informed speech extraction, which exploits an additional
voice snippet of the target speaker to distinguish his/her speech from the
mixture. SpeakerBeam [8, 9] derives a speaker embedding from an utterance of
the target speaker by using a sequence summary network [15] and uses the
embedding to guide an extraction network to extract the speaker of interest.
VoiceFilter [10] concatenates spectral features of the mixture with the
d-vector [16] of a voice snippet to extract the target speaker. Xiao et al.
[11] uses an attention mechanism to generate context-dependent biases for
target speech extraction. Informed speech extraction naturally solves the
permutation problem and unknown number of speakers. However, it has two
limitations. Firstly, the computation cost is proportional to the number of
speakers to be extracted, so in a multi-speaker conversation, the system needs
to run multiple times to extract each speaker one by one. Most importantly,
the extraction usually fails when the target speaker’s biased information is
not strong enough [9].

The second category is speech separation using speaker inventory (SSUSI) [14].
The method employs a pool of additional enrollment utterances from a list of
candidate speakers, from which profiles of relevant speakers involved in the
mixture are first selected. Then the method fuses the selected profiles and
the mixed speech to separate all speakers simultaneously. As multiple profiles
are provided during separation, more substantial speaker discrimination can be
expected, which yields better speech separation. The method can also employ
permutation invariant training (PIT) [2] to compensate for weak biased
information and wrong selection.

Though with promising results reported in prior arts, both categories suffer
from two issues. Firstly, as the separation performance heavily relies on the
profile quality, when there is a severe acoustic mismatch between the mixed
signal and the enrolled utterances, the effectiveness of speaker information
could be largely degraded. Secondly, methods in both categories assume
additional speaker information is available ahead of extraction or separation,
which may be impractical in real scenarios. Wavesplit [17] uses clustering to
infer source embeddings from the mixed signal and then uses them to guide
speaker separation. However, the number of source embeddings must be fixed and
identical to the speakers to be separated, limiting its application in a long
recording with various speakers. Also, all the methods mentioned above mostly
prove their successes on relative simple datasets, e.g., LibriMix [18] that
contains only anechoic speech, or WSJ0-2mix [1] and its variants that contain
pre-segmented speech utterances that are usually fully overlapped. These
further blur the practicality of these methods as overlap in real conversation
usually possess very different characteristics [19, 20, 21, 22].

In this paper, we address these problems on the continuous speech separation
(CSS) task [23, 24]. CSS focuses on separating long recordings where the
overall overlap ratio is low and the speaker activations are sparse. A large
proportion of non-overlapped regions in the recording enables the derivation
of robust features for the participants. We adopt the SSUSI in the CSS task
and propose continuous SSUSI (CSSUSI), which constructs the speaker inventory
from the mixed signal itself, instead of external speaker enrollments, by
using speaker clustering methods. CSSUSI informs the separation network with
relevant speaker profiles dynamically selected from the inventory to
facilitate source separation at local regions. The outputs from local regions
are then concatenated such that the output audio streams are continuous speech
that do not contain any overlap. We create a more realistic dataset that
simulates natural multi-talker conversations in conference rooms to test
CSSUSI on the CSS task. Experimental results show that CSSUSI can successfully
build a speaker inventory from the long speech mixture using the clustering-
based method and take advantage of the global information to improve
separation performance significantly.

The rest of the paper is organized as follows. We introduce the SSUSI
framework in Section 2, describe the CSSUSI system for long recording in
Section 3, present the experiment configurations in Section 4, analyze the
experiment results in Section 5, and conclude the paper in Section 6.

##  2 SSUSI using pre-enrolled utterance

We first overview the original SSUSI system [14], which requires pre-enrolled
speaker signals. A SSUSI system contains three modules: a speaker
identification module, a speaker profile selection module, and a biased speech
separation module. The speaker identification module is responsible for
embedding extraction from both the speaker enrollments and input mixture.
Embeddings of speaker enrollments are used for speaker inventory construction.
The speaker profile selection module selects from the inventory the best-
matched speaker profiles with the mixture embeddings. The selected profiles
are then fed into the biased separation module to separate speakers in the
mixture.

Since each speech segment is short (4s in this paper) and typically contains
at most two speakers, we focus on two-speaker separation for each speech
segment, and the model always generates two outputs. Moreover, we make several
modifications to the original SSUSI architecture [14] for better performance.

###  2.1 Speaker identification module

The speaker identification module is used to construct the speaker inventory
first. The inventory is a pool of $K$-dimensional speaker embeddings
$\left\\{\bm{\mathrm{e}}^{j}\right\\}_{j=1}^{M},\bm{\mathrm{e}}^{j}\in\mathbb{R}^{K}$,
which are extracted from a collection of time-domain enrollment speech
$\left\\{\bm{\mathrm{a}}^{j}\right\\}_{j=1}^{M},\bm{\mathrm{a}}^{j}\in\mathbb{R}^{L_{a_{j}}}$,
where $L_{a_{j}}$ is the temporal dimension of speech signal
$\bm{\mathrm{a}}^{j}$. $M$ is typically larger than the maximum number of
speakers in the mixture to be separated. We also assume that each speaker only
has one enrollment sentence. A speaker identification network, referred to as
the SNet, is applied for embedding extraction:

$\displaystyle\bm{\mathrm{E}}^{j}=\rm{SNet}(\bm{\mathrm{a}}^{j})$ (1)

where $\bm{\mathrm{E}}^{j}\in\mathbb{R}^{T_{j}\times K}$ and $T_{j}$ is the
temporal dimension of the embedding sequence. Here we simply use mean-pooling
across the $T_{j}$ frames of $\bm{\mathrm{E}}^{j}$ to obtain the single vector
$\bm{\mathrm{e}}^{j}\in\mathbb{R}^{K}$.

The mixture embeddings are directly extracted from the input mixture
$\bm{\mathrm{y}}\in\mathbb{R}^{T}$ with the temporal dimension T:

$\displaystyle\bm{\mathrm{E}}^{y}=\rm{SNet}(\bm{\mathrm{y}})$ (2)

where $\bm{\mathrm{E}}^{y}\in\mathbb{R}^{T_{y}\times K}$ and $T_{y}$ is the
temporal dimension of the mixture embeddings.

###  2.2 Speaker profile selection module

The speaker profile selection module selects the relevant speaker profiles
from the inventory that are best matched with the mixture embeddings
$\bm{\mathrm{E}}^{y}$ in equation 2. The selection is performed by calculating
the similarity between the mixture embeddings and items in the inventory, and
two items with the highest similarity are selected. The similarity are
calculated by applying the Softmax function on the dot-product between the
mixture and inventory embeddings:

$\displaystyle\begin{split}\bm{\mathrm{d}}_{s}^{y,j}&=\bm{\mathrm{e}}_{s}^{y}\cdot\bm{\mathrm{e}}^{j}\\\
\bm{\mathrm{w}}_{s}^{y,j}&=\frac{\rm
exp(\bm{\mathrm{d}}_{s}^{y,j})}{\sum_{p=1}^{M}\rm
exp(\bm{\mathrm{d}}_{s}^{y,p})}\end{split}$ (3)

where $\bm{\mathrm{e}}_{s}^{y}$ denotes $\bm{\mathrm{E}}^{y}$ at temporal
index $s$. We then calculate the average score $\bm{\mathrm{w}}^{y,j}$ across
the $T_{y}$ frames:

$\displaystyle\bm{\mathrm{w}}^{y,j}$
$\displaystyle=\frac{\sum_{s=1}^{T_{y}}\bm{\mathrm{w}}_{s}^{y,j}}{T_{y}}$ (4)

Two inventory items $\bm{\mathrm{e}}^{p_{1}}$ and $\bm{\mathrm{e}}^{p_{2}}$
are then selected according to the two highest scores in
$\left\\{\bm{\mathrm{w}}^{y,j}\right\\}_{j=1}^{M}$.

Fig. 1: (A) The architecture of the proposed continuous speech separation
using speaker inventory. The Speaker inventory construction module forms the
speaker inventory from the long mixture by using Kmeans clustering; the long
mixture is split into small segments, and the speaker profile selection module
selects two relevant profiles from the inventory for each segment; the speech
separation module fuses the selected speaker profiles into the system for
source separation. (B) Multiplicative adaptation of the selected profiles
$\bm{\mathrm{e}}^{p_{1}}$ and $\bm{\mathrm{e}}^{p_{2}}$. (C) Stitching
procedure of adjacent segment outputs in a long recording.

###  2.3 Biased speech separation module

The biased speech separation module is adapted to the speech characteristics
of the speakers selected from the inventory for biased source separation. The
module contains three layers, a feature extraction layer, a profile adaptation
layer, and a separation layer. Both feature extraction and separation layers
are 2-layer BLSTM in this paper. Previous research [8] has shown that a
multiplicative adaptation layer, i.e., multiplying the speaker embedding with
the output of one of the middle layers of the network, is a simple yet
effective way to realize adaptation, so we use the same method here. Given the
two selected speaker profiles $\bm{\mathrm{e}}^{p_{1}}$ and
$\bm{\mathrm{e}}^{p_{2}}$, two target-biased adaptation features are
calculated by frame-level element-wise multiplication between the profiles and
the output of the feature extraction layer:

$\displaystyle\bm{\mathrm{a}}_{l}^{p_{1}}$
$\displaystyle=\bm{\mathrm{b}}_{l}\odot\bm{\mathrm{e}}^{p_{1}}$ (5)
$\displaystyle\bm{\mathrm{a}}_{l}^{p_{2}}$
$\displaystyle=\bm{\mathrm{b}}_{l}\odot\bm{\mathrm{e}}^{p_{2}}$ (6)

where $\bm{\mathrm{b}}_{l}\in\mathbb{R}^{K}$ denotes the output of the feature
layer, $l$ denotes the frame index, and $\odot$ denotes the element-wise
multiplication. The two target-biased features are then concatenated:

$\displaystyle\bm{\mathrm{A}}=\rm
concat([\bm{\mathrm{A}}^{p_{1}},\bm{\mathrm{A}}^{p_{2}}])$ (7)

where
$\bm{\mathrm{A}}^{p_{1}}=[\bm{\mathrm{a}}_{1}^{p_{1}},\ldots,\bm{\mathrm{a}}_{L}^{p_{1}}]\in\mathbb{R}^{L\times
K}$,
$\bm{\mathrm{A}}^{p_{2}}=[\bm{\mathrm{a}}_{1}^{p_{2}},\ldots,\bm{\mathrm{a}}_{L}^{p_{2}}]\in\mathbb{R}^{L\times
K}$, and $\bm{\mathrm{A}}\in\mathbb{R}^{L\times 2K}$. The separation layer
takes $\bm{\mathrm{A}}$ as the input and estimates two time-frequency (T-F)
masks $\bm{\mathrm{M}}^{1},\bm{\mathrm{M}}^{2}\in\mathbb{R}^{L\times F}$.

##  3 Continuous SSUSI using self-informed mechanism for inventory
construction

SSUSI assumes that pre-recorded utterances of all speakers are available for
the speaker inventory construction. However, such an assumption may not be
realistic, especially for unseen speakers or meeting scenarios where the
collection of pre-recorded speech from the participants is not feasible.

Continuous speech separation (CSS) aims at estimating the individual target
signals from a continuous mixed signal which is usually a hours long signal
and contains both overlapped and non-overlap speech, but the overlap ratio is
low. So, single-speaker regions can be exploited to derive robust acoustic
characteristics of participating speakers without the need for external
utterances, which makes the self-informed speaker inventory construction
possible. This section introduces how we adopt SSUSI in the CSS task and
eliminate the need for pre-recorded speech by using a clustering method.

Figure 1 (A) shows the overall flowchart of the continuous SSUSI (CSSUSI)
framework. The main difference between CSSUSI and the original SSUSI is the
construction of the speaker inventory. Original SSUSI applies the speaker
identification module on extra enrollment utterances, whereas CSSUSI first
splits the mixture recording $\bm{\mathrm{y}}$ into $B$ small chunks, and
directly extracts the mixture embeddings
$\left\\{\bm{\mathrm{e}}_{b}^{y}\right\\}_{b=1}^{B}$, where
$\bm{\mathrm{e}}_{b}^{y}\in\mathbb{R}^{K}$ denotes the embedding vector in
chunk b. Then, CSSUSI applies Kmeans clustering on
$\left\\{\bm{\mathrm{e}}_{b}^{y}\right\\}_{b=1}^{B}$ to form $M$ clusters, and
the cluster centroids form the speaker inventory. In Section 5 we will show
that the separation performance is insensitive to the choice of $M$ as long as
$M$ is no smaller than the actual number of active speakers in the recording.

CSUSSI uniformly segments the mixture recording and exploits the inventory to
facilitate source separation in each segment. Except for the self-informed
speaker inventory, CSSUSI uses the same speaker profile selection and biased
speech separation methods as introduced in Section 2.2 and Section 2.3,
respectively. To stitch the outputs from different segments to form output
streams where each stream only contains non-overlapped speakers, the
similarity between the overlapped regions in adjacent blocks determines the
pair of segments to be stitched. Figure 1 (C) shows the stitching procedure of
adjacent segment outputs.

##  4 Experimental settings

Table 1: SNR (dB) on eight-speaker long recordings (segment-wise evaluation).
The performance on different overlap ratios is reported.
---
Method |  Speaker enrollment |  Overlap ratio in $\%$
0 | 0-25 | 25-50 | 50-75 | 75-100 | Average
Unprocessed | - | 8.6 | -9.7 | -1.2 | -0.9 | -0.7 | -0.1
BLSTM | - | 15.5 | 8.0 | 8.6 | 7.5 | 6.9 | 10.6
SSUSI | Two wrong profiles | 15.2 | 7.1 | 8.4 | 7.8 | 7.1 | 10.3
One correct and one wrong profiles | 15.4 | 7.8 | 9.0 | 8.2 | 7.6 | 10.7
Two correct profiles | 15.9 | 9.5 | 10.6 | 9.4 | 8.7 | 11.9
| Selected profiles | 15.7 | 8.8 | 10.0 | 9.0 | 8.3 | 11.5

###  4.1 Dataset

In our training set, we randomly generate 3000 rooms. The length and width of
the rooms are randomly sampled between 5 and 12 meters, and the height is
randomly sampled between 2.5 and 4.5 meters. A microphone is randomly placed
in the room, and its location is constrained to be within 2 meters of the room
center. The height of the microphone is randomly sampled between 0.4 and 1.2
meters. We randomly sample 10 speakers from the LibriSpeech corpus [25] for
each room. All the speakers are at least 0.5 meters away from the room walls
and the height of the speakers are between 1 and 2 meters. The reverberation
time is uniformly sampled between 0.1 and 0.5 seconds. We randomly choose 2
speakers as relevant speakers and arrange them according to one of the four
following patterns:

  1. 1.

Inclusive: one speaker talks a short period while the other one is talking.

  2. 2.

Sequential: one talks after the other one finishes talking.

  3. 3.

Fully-overlapped: two speakers always talk simultaneously.

  4. 4.

Partially-overlapped: two speakers talk together only in a certain period.

The frequencies for the four patterns are 10%, 20%, 35%, and 35%,
respectively. The minimal length of the overlapped periods in inclusive and
partially-overlapped patterns is set to 1 second. The maximal length of the
silent periods between the two speakers in the sequential pattern is 0.5
second. Moreover, to generate single-speaker utterances, there is a 0.1
probability that one of the speakers is muted in each pattern. We use the
remaining 8 speakers as the irrelevant speakers that will not appear in the
mixture. Each of the room configurations is used for 8 times. The mixture
length is 4 seconds. So, the total training time is $3000\times 8\times
4s=26.7\ \text{hours}$. For both the relevant and irrelevant speakers, a
10-second utterance is sampled to form the speaker inventory. All speech
signals are single-channel and sampled at 16 kHz. Gaussian noise with SNR
randomly chosen between 0 and 20 dB is added into the mixture.

In our testing set, we set three configurations: $60$-second mixture
containing 2 speakers, $150$-second mixture containing 5 speakers, and
$240$-second mixture containing 8 speakers. We generate 300 recordings for
each configuration. The overall overlap ratio of each recording is 30$\%$
complying with natural conversion [26].

###  4.2 Implementation details

All models contain 4 bidirectional LSTM (BLSTM) layers with 600 hidden units
in each direction. In the CSSUSI models, the speaker identification module
adopts the similar design in [27], and the module is pretrained on the
VoxCeleb2 dataset [28] and achieves 2.04$\%$ equal error rate on the VoxCeleb1
test set [29]. The module extracts 128-dimensional speaker embeddings for
every 1.2-second (30-frame) segment. We use SNR as training objective [30] and
Adam [31] as the optimizer with initial learning rate of 0.001. The learning
rate is decayed by 0.98 for every two epochs.

##  5 Results and discussions

Table 2: SNR (dB) on long recordings with different configurations (segment-
wise evaluation).
---
Speaker number | Method | External utterances | Clusters | Avg.
2 speakers | Unprocessed | - | - | 1.6
BLSTM | - | - | 11.2
SSUSI | 2 | No | 12.2
CSSUSI |  No | 2 | 12.1
3 | 11.9
4 | 11.9
5 speakers | Unprocessed | - | - | 0
BLSTM | - | - | 10.6
SSUSI | 5 | No | 11.5
CSSUSI |  No | 3 | 10.9
5 | 11.3
8 | 11.2
10 | 11.2
8 speakers | Unprocessed | - | - | -0.1
BLSTM | - | - | 10.6
SSUSI | 8 | No | 11.5
CSSUSI |  No | 5 | 11.0
8 | 11.3
12 | 11.3
16 | 11.2

Table 1 compares different models on 4-second segments of eight-speaker
recordings. The inventory contains eight speakers’ profiles that are derived
from eight external utterances. SSUSI achieves leading performance on all
levels of overlap ratios when two correct speaker profiles are used; however,
the performance of SSUSI drops greatly with two wrong speaker profiles
randomly chosen from the 8 irrelevant speakers, which indicates that
performance gain obtained by SSUSI mainly comes from leveraging the target
speaker information. We also notice that the performance of SSUSI with two
wrong profiles is only slightly worse than the baseline BLSTM, and when only
one correct speaker profile is enrolled, SSUSI can still outperform the
baseline model, which proves that PIT can compensate for wrong selection and
the separation module is robust to adaptation features. When the speaker
profiles are selected by the profile selection module, the SSUSI model
performs slightly better on the non-overlapped mixtures (overlap ratio is 0)
but much better on the overlapped mixtures at all overlap ratios. This
confirms the effectiveness of the SSUSI framework on improving separation
performance across various settings, which is consistent with the observations
in [14] that conducted experiments on Librispeech although the model
architectures are different.

Table 2 compares CSSUSI with different clusters on recordings with different
number of speakers. Since the number of participating speakers in a meeting
may be unknown, we intend to do over-clustering, i.e., setting the number of
clusters greater than the number of speakers in a meeting. Table 2 compares
CSSUSI with different clustering settings. The performance of CSSUSI is almost
identical once the number of clusters is not fewer than the number of
speakers. Over-clustering has very little impact on the performance as it
ensures each speaker possesses at least one cluster center. Some extra
clusters may represent acoustic characteristics of overlapped regions, which
will be regarded as irrelevant profiles during profile selection. We can see
that CSSUSI outperforms the baseline model BLSTM on all configurations. As we
conclude from Table 1, the performance gain is achieved via leveraging
relevant speakers’ information. So the performance gain from CSUSSI suggests
the successful construction of the speaker inventory from the mixture itself
and effective utilization of speaker information. Furthermore, we compare
CSSUSI with SSUSI that derives speaker profiles from external utterances that
contain only a single speaker in each utterance. CSSUSI sacrifices very little
performance but does not require external utterances, which shows CSSUSI is a
better model than SSUSI for long recording speech separation.

Table 3 compares utterance-wise separation performance. After segments are
stitched, each complete utterance is extracted from the output streams by
using ground-truth segmentation information, i.e., onset and offset of each
utterance. We find that CSSUSI surpasses the baseline in all configurations by
a large margin, which further proves the strength of CSSUSI in the long
recordings.

Table 3: Utterance-level evaluation. SI-SDR(dB) is reported.
---
Method | Need external utterances? | 2 spk | 5 spk | 8spk
Unprocessed | - | 6.0 | 4.5 | 4.3
BLSTM | No | 11.7 | 10.8 | 10.6
SSUSI | Yes | 13.2 | 12.0 | 11.7
CSSUSI | No | 13.1 | 11.9 | 11.7

##  6 Conclusion

In this paper, we investigated continuous speech separation using speaker
inventory for long multi-talker recordings. In the CSS task, we made use of
the fact that long recording, in general, contains a large proportion of non-
overlapped regions and proposed continuous SSUSI (CSSUSI) that extracted
speaker embeddings from the long recordings and performed “over-clustering” on
the embeddings to construct the self-informed speaker inventory. CSSUSI
overcomes the limitation of the original SSUSI that required external
enrollments. Experiments on a simulated noisy reverberant dataset showed that
CSSUSI significantly outperformed the baseline models across various
conditions. Future works include extending the CSSUSI system into real-world
recordings, designing a block-online system instead of an offline system, and
investigate better model architectures.

##  7 Acknowledgement

The work reported here was started at JSALT 2020 at JHU, with support from
Microsoft, Amazon and Google.

## References

  * [1] J. R. Hershey, Z. Chen, J. Le Roux, and S. Watanabe, “Deep clustering: Discriminative embeddings for segmentation and separation,” in _2016 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_. IEEE, 2016, pp. 31–35.
  * [2] D. Yu, M. Kolbæk, Z.-H. Tan, and J. Jensen, “Permutation invariant training of deep models for speaker-independent multi-talker speech separation,” in _2017 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_. IEEE, 2017, pp. 241–245.
  * [3] Y. Luo, Z. Chen, and N. Mesgarani, “Speaker-independent speech separation with deep attractor network,” _IEEE/ACM Transactions on Audio, Speech, and Language Processing_ , vol. 26, no. 4, pp. 787–796, 2018.
  * [4] C. Han, Y. Luo, and N. Mesgarani, “Online deep attractor network for real-time single-channel speech separation,” in _2019 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_. IEEE, 2019, pp. 361–365.
  * [5] Y. Luo and N. Mesgarani, “Conv-tasnet: Surpassing ideal time–frequency magnitude masking for speech separation,” _IEEE/ACM transactions on audio, speech, and language processing_ , vol. 27, no. 8, pp. 1256–1266, 2019\.
  * [6] S. Wisdom, E. Tzinis, H. Erdogan, R. J. Weiss, K. Wilson, and J. R. Hershey, “Unsupervised sound separation using mixtures of mixtures,” in _Advances in Neural Information Processing Systems (NeurIPS)_ , 2020.
  * [7] T. Jenrungrot, V. Jayaram, S. Seitz, and I. Kemelmacher-Shlizerman, “The cone of silence: speech separation by localization,” in _Advances in Neural Information Processing Systems (NeurIPS)_ , vol. 33, 2020.
  * [8] K. Žmolíková, M. Delcroix, K. Kinoshita, T. Ochiai, T. Nakatani, L. Burget, and J. Černockỳ, “Speakerbeam: Speaker aware neural network for target speaker extraction in speech mixtures,” _IEEE Journal of Selected Topics in Signal Processing_ , vol. 13, no. 4, pp. 800–814, 2019.
  * [9] M. Delcroix, T. Ochiai, K. Zmolikova, K. Kinoshita, N. Tawara, T. Nakatani, and S. Araki, “Improving speaker discrimination of target speech extraction with time-domain speakerbeam,” in _2020 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_. IEEE, 2020, pp. 691–695.
  * [10] Q. Wang, H. Muckenhirn, K. Wilson, P. Sridhar, Z. Wu, J. Hershey, R. A. Saurous, R. J. Weiss, Y. Jia, and I. L. Moreno, “Voicefilter: Targeted voice separation by speaker-conditioned spectrogram masking,” _arXiv preprint arXiv:1810.04826_ , 2018.
  * [11] X. Xiao, Z. Chen, T. Yoshioka, H. Erdogan, C. Liu, D. Dimitriadis, J. Droppo, and Y. Gong, “Single-channel speech extraction using speaker inventory and attention network,” in _2019 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_. IEEE, 2019, pp. 86–90.
  * [12] J. Wang, J. Chen, D. Su, L. Chen, M. Yu, Y. Qian, and D. Yu, “Deep extractor network for target speaker recovery from single channel speech mixtures,” _arXiv preprint arXiv:1807.08974_ , 2018.
  * [13] T. Ochiai, M. Delcroix, K. Kinoshita, A. Ogawa, and T. Nakatani, “A unified framework for neural speech separation and extraction,” in _2019 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_. IEEE, 2019, pp. 6975–6979.
  * [14] P. Wang, Z. Chen, X. Xiao, Z. Meng, T. Yoshioka, T. Zhou, L. Lu, and J. Li, “Speech separation using speaker inventory,” in _2019 IEEE Automatic Speech Recognition and Understanding Workshop (ASRU)_. IEEE, 2019, pp. 230–236.
  * [15] K. Veselỳ, S. Watanabe, K. Žmolíková, M. Karafiát, L. Burget, and J. H. Černockỳ, “Sequence summarizing neural network for speaker adaptation,” in _2016 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_. IEEE, 2016, pp. 5315–5319.
  * [16] E. Variani, X. Lei, E. McDermott, I. L. Moreno, and J. Gonzalez-Dominguez, “Deep neural networks for small footprint text-dependent speaker verification,” in _2014 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_. IEEE, 2014, pp. 4052–4056.
  * [17] N. Zeghidour and D. Grangier, “Wavesplit: End-to-end speech separation by speaker clustering,” _arXiv preprint arXiv:2002.08933_ , 2020.
  * [18] J. Cosentino, M. Pariente, S. Cornell, A. Deleforge, and E. Vincent, “Librimix: An open-source dataset for generalizable speech separation,” _arXiv preprint arXiv:2005.11262_ , 2020.
  * [19] A. Janin, D. Baron, J. Edwards, D. Ellis, D. Gelbart, N. Morgan, B. Peskin, T. Pfau, E. Shriberg, A. Stolcke _et al._ , “The icsi meeting corpus,” in _2003 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_ , vol. 1. IEEE, 2003, pp. I–I.
  * [20] J. Carletta, S. Ashby, S. Bourban, M. Flynn, M. Guillemot, T. Hain, J. Kadlec, V. Karaiskos, W. Kraaij, M. Kronenthal _et al._ , “The ami meeting corpus: A pre-announcement,” in _International Workshop on Machine Learning for Multimodal Interaction_. Springer, 2005, pp. 28–39.
  * [21] T. Yoshioka, I. Abramovski, C. Aksoylar, Z. Chen, M. David, D. Dimitriadis, Y. Gong, I. Gurvich, X. Huang, Y. Huang _et al._ , “Advances in online audio-visual meeting transcription,” in _2019 IEEE Automatic Speech Recognition and Understanding Workshop (ASRU)_. IEEE, 2019, pp. 276–283.
  * [22] J. Barker, S. Watanabe, E. Vincent, and J. Trmal, “The fifth’chime’speech separation and recognition challenge: Dataset, task and baselines,” in _INTERSPEECH_ , 2018, pp. 1561–1565.
  * [23] T. Yoshioka, H. Erdogan, Z. Chen, and F. Alleva, “Multi-microphone neural speech separation for far-field multi-talker speech recognition,” in _2018 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_. IEEE, 2018, pp. 5739–5743.
  * [24] Z. Chen, T. Yoshioka, L. Lu, T. Zhou, Z. Meng, Y. Luo, J. Wu, X. Xiao, and J. Li, “Continuous speech separation: Dataset and analysis,” in _2020 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_. IEEE, 2020, pp. 7284–7288.
  * [25] V. Panayotov, G. Chen, D. Povey, and S. Khudanpur, “Librispeech: an asr corpus based on public domain audio books,” in _2015 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_. IEEE, 2015, pp. 5206–5210.
  * [26] Ö. Çetin and E. Shriberg, “Analysis of overlaps in meetings by dialog factors, hot spots, speakers, and collection site: Insights for automatic speech recognition,” in _9th International Conference on Spoken Language Processing_ , 2006.
  * [27] T. Zhou, Y. Zhao, J. Li, Y. Gong, and J. Wu, “CNN with Phonetic Attention for Text-Independent Speaker Verification,” in _2019 IEEE Automatic Speech Recognition and Understanding Workshop (ASRU)_. IEEE, 2019, pp. 718–725.
  * [28] J. S. Chung, A. Nagrani, and A. Zisserman, “Voxceleb2: Deep speaker recognition,” in _INTERSPEECH_ , 2018, pp. 1086–1090.
  * [29] A. Nagrani, J. S. Chung, and A. Zisserman, “Voxceleb: A large-scale speaker identification dataset,” in _INTERSPEECH_ , 2017, pp. 2616–2620.
  * [30] C. Han, Y. Luo, and N. Mesgarani, “Real-time binaural speech separation with preserved spatial cues,” in _2020 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_. IEEE, 2020, pp. 6404–6408.
  * [31] D. P. Kingma and J. Ba, “Adam: A method for stochastic optimization,” _arXiv preprint arXiv:1412.6980_ , 2014.


# Undecidability of a Very Simple Modal Logic with Binding

Guillaume Hoffmann
Consejo Nacional de Investigaciones Científicas y Técnicas (CONICET)
Universidad Blas Pascal
Universidad Nacional de Córdoba
<EMAIL_ADDRESS>
(2015-08-14)

###### Abstract

We show undecidability of the satisfiability problem of what is arguably the
simplest non-sub-Boolean modal logic with an implicit notion of binding. This
work enriches the series of existing results of undecidability of modal logics
with binders, which started with Hybrid Logics and continued with Memory
Logics.

##  1 Modal Logics, Names and Binders

Modal Logics are languages that are able to describe graphs from an internal
perspective. When they are enriched with _nominals_ , that is, propositional
symbols that are true at only one state of the graph, they are called _Hybrid
Logics_ [4]. A nominal can unequivocally name a particular state. It was soon
discovered that the ability to dynamically name states could lead to the
ability to describe more interesting graphs. Goranko ([6]) introduced the
_down-arrow binder_ , with the syntax ${\downarrow}x.\varphi$ meaning “after
naming the current state $x$, $\varphi$ holds”. For instance,
$\square{\downarrow}x.\lozenge x$ means “all accessible states are reflexive”.

Hybrid Logics with binders are robustly undecidable, from the full
$\mathcal{H}(@,{\downarrow})$ language [5], to $\mathcal{H}({\downarrow})$
with only one relation and no propositional symbol beyond nominals [2]. Also,
$\mathcal{H}({\downarrow})$ with propositional symbols, a single nominal and a
single relation has the same fate [8].

Attempts have been made to find interesting decidable fragments of hybrid
logics with binder. Some successful approaches involve restricting the class
of models on which the satisfiability problem is specified: models of finite
width [10], or models with a single relation and certain frame properties (S5,
transitive, complete) [9].

On the other hand, a few syntactical restrictions have been successful.
$\mathcal{H}(@,{\downarrow})\setminus\square{\downarrow}\square$, the language
obtained by removing formulas that contain a nesting of $\square$,
${\downarrow}$ and $\square$, is decidable [10]. Also, only allowing one
nominal, and restricting the depth between the binder and the nominal to 2
yields decidability [7].

##  2 Memory Logics

_Memory logics_ [1, 3] are a distinct take on the binder. They are modal
logics with the ability to _store_ the current state of evaluation into some
memory, and to consult whether the current state belongs to it. The two
operators associated to these actions are $ⓡ$ and $ⓚ$. $ⓡ\varphi$ means
“remember the current state and evaluate $\varphi$” and $ⓚ$ means “this state
is known”.

Given a model $\mathcal{M}=\langle W,R,V\rangle$, a state $s$ and a memory $S$
(which is a subset of $W$), the semantics of these operators is given by:

$\begin{array}[]{rcl}\mathcal{M},S,s\models ⓡ\varphi&\mbox{ iff
}&\mathcal{M},S\cup\\{s\\},s\models\varphi\\\ \mathcal{M},S,s\models ⓚ&\mbox{
iff }&s\in S.\end{array}$

Let us take two pointed models that are bisimilar for the basic modal logic:

$\mathcal{M}$$\mathcal{M}^{\prime}$

Assuming an empty initial memory, the formula $ⓡ\lozenge ⓚ$ is false on the
left and true on the right. Whereas with hybrid logics we would have used an
explicit name (e.g., with the formula ${\downarrow}a.\lozenge a$), memory
logics do not involve any explicit binding process.

The satisfiability problem for the basic modal logic extended with $ⓡ$ and $ⓚ$
with initial empty memory is undecidable [3]. Another proposal is a memory
logic without $\lozenge$ and $ⓡ$, but with a remember-and-move operator
$\langle r\rangle$ equivalent to $ⓡ\lozenge\varphi$. In this language, the
operator $ⓚ$ identifies whether the current world has already been explored
during the evaluation of the formula. It can be seen as an “I’ve already been
here” operator. Again, satisfiability with an empty initial memory is
undecidable in this simplified language.

Undecidability proofs for the aforementioned logics regularly involve encoding
the tiling problem into the language of satisfiable formula [11]. Since sets
of tiles are represented by propositional symbols, we propose to study a
language that lacks them.

##  3 The $\mathcal{B}(\langle r\rangle,ⓚ)$ fragment

We consider the language $\mathcal{B}(\langle r\rangle,ⓚ)$. $\mathcal{B}$
refers to the Boolean connectors, and $\langle r\rangle$ and $ⓚ$ are the only
non-Boolean logical symbols. For readability sake, let us write $\lozenge$
instead of $\langle r\rangle$. The syntax of $\mathcal{B}(\langle r\rangle,ⓚ)$
is:

$F~{}:=~{}\neg F~{}\mid~{}F_{1}\wedge F_{2}~{}\mid~{}\lozenge F~{}\mid~{}ⓚ$

We interpret formulas on Kripke frames $\mathcal{M}=\langle W,R\rangle$ made
of a set of states $W$ and a binary relation $R$ on $W$, with some current
evaluation state $s$ and a set $S\subseteq W$ of visited states:

$\begin{array}[]{rlcl}\mathcal{M},S,s&\models\neg\varphi&\mbox{iff}&\mathcal{M},S,s\not\models\varphi\\\
\mathcal{M},S,s&\models\varphi\wedge\psi&\mbox{iff}&\mathcal{M},S,s\models\varphi\mbox{
and }\mathcal{M},S,s\models\psi\\\
\mathcal{M},S,s&\models\lozenge\varphi&\mbox{iff}&\mbox{there exists }t\in
W\mbox{ such that}\\\ &&&Rst\mbox{ and
}\mathcal{M},S\cup\\{s\\},t\models\varphi\\\ \mathcal{M},S,s&\models
ⓚ&\mbox{iff}&s\in S\\\ \end{array}$

We define the notations $\vee$, $\rightarrow$ and $\square$ as usual, and
$\bot\equiv ⓚ\wedge\neg ⓚ$ and $\top\equiv ⓚ\vee\neg ⓚ$.

We will use the following notion of satisfiability:

######  Definition 1.

A formula $\varphi$ of $\mathcal{B}(\langle r\rangle,ⓚ)$ is satisfiable, or is
in $\mathcal{B}(\langle r\rangle,ⓚ)$-sat, if there exists a model
$\mathcal{M}=\langle W,R\rangle$ and $s\in W$ such that
$\mathcal{M},\emptyset,s\models\varphi$.

As a warm-up, let us see that we can define a formula satisfiable only in
infinite models. Consider the formula $Inf$ made of the following conjuncts:

>   1. 1.
>
> $s$
>
>   2. 2.
>
> $\square\neg s$
>
>   3. 3.
>
> $\square\square(ⓚ\rightarrow s)$
>
>   4. 4.
>
> $\lozenge\lozenge ⓚ$
>
>   5. 5.
>
> $\square(\lozenge\top\rightarrow\lozenge(\neg ⓚ\wedge\neg s))$
>
>   6. 6.
>
> $\square\square(\neg s\rightarrow\lozenge(ⓚ\wedge
> s\wedge\lozenge(ⓚ\wedge\square(ⓚ\rightarrow s))))$
>
>   7. 7.
>
> $\square\square(\neg s\rightarrow\square(\neg s\rightarrow\lozenge(ⓚ\wedge
> s\wedge\square(\mbox{a-or-b}\rightarrow\lozenge c))))$
>
>

Which use the macros:

$\begin{array}[]{lll}s&\equiv&\lozenge\square\bot\\\
\mbox{a-or-b}&\equiv&ⓚ\wedge\lozenge(ⓚ\wedge\neg s)\\\
c&\equiv&ⓚ\wedge\square(ⓚ\rightarrow s)\\\ \end{array}$

We call “spy” the evaluation state and review the conjuncts one by one, each
time assuming all previous conjuncts also hold:

  1. 1.

spy sees a dead-end

  2. 2.

spy’s successors see no dead-ends, also implying spy is irreflexive

  3. 3.

successors of spy are irreflexive

  4. 4.

spy has a successor that has spy as a succesor

  5. 5.

if a successor of spy is not a dead-end, then it has a successor that is
different from itself

  6. 6.

all states of the chain are linked to spy in both directions, and the relation
between chain states is asymetric

  7. 7.

relation between chain states is transitive (a-or-b and $c$ are macros that
help referring to successive states of the infinite chain)

As we require that the relation on chain states be serial (5), asymetric (6),
irreflexive (3) and transitive (7), we get an infinite chain of states
(transitive links are not represented):

…$\mathit{spy}$

######  Theorem 1.

If there is a frame $\mathcal{M}=\langle W,R\rangle$ and $s\in W$ such that
$\mathcal{M},\emptyset,s\models Inf$ then $W$ is infinite.

Hence $\mathcal{B}(\langle r\rangle,ⓚ)$ lacks the finite model property. This
does not necessarily imply that this logic is undecidable, but we are going to
see that it is actually the case.

##  4 Undecidability of $\mathcal{B}(\langle r\rangle,ⓚ)$-sat

We adapt the proof of [8], where the tiling problem [11] is encoded into a
description logic with the down-arrow binder, one nominal, and one relation.

We build a formula that is satisfiable only in models with the following
components (see Figure 1):

  * •

the _spy state_ is where the formula is evaluated.

  * •

_grid states_ are direct successors of the spy state. A grid state is
connected to other grid states, but also to switch and propositional states.

  * •

_switch states_ are in one-to-one correspondence with grid states, and help
building the structure by simulating an explicit binding operator. A switch
state sees the grid state that sees it.

  * •

_propositional states_ encode propositional symbols at every grid state, using
chains of determined length. A grid state can see several propositional
states, but a propositional state does not see its origin grid state.

  * •

The spy, switch and propositional states see at least one dead-end state,
while grid states do not.

grid…………$\mathit{spy}$$\square\bot$$\mathit{switch}$$\square\bot$ Figure 1:
Model of a formula encoding some tiling problem, with details for the first
grid state

Let us enumerate the conjuncts of the formula that encodes a given instance of
the tiling problem.

The first formulas specify that the spy state sees a dead-end, is irreflexive,
that all its successors are also irreflexive, that all grid states see the spy
state, and that the relation between grid states is symmetric:

  1. 1.

$s$

  2. 2.

$\square\neg s$

  3. 3.

$\square\square(ⓚ~{}\rightarrow~{}s)$

  4. 4.

$\square(\lozenge\top~{}\rightarrow~{}\lozenge ⓚ)$

  5. 5.

$\square\square(\neg s\rightarrow\lozenge(ⓚ\wedge\neg s))$

The following two formulas implement switch states for grid states accessible
in one and two steps from spy:

  1. 6.

$\square(\lozenge\top\rightarrow\lozenge sw)$

  2. 7.

$\square\square(\neg s\rightarrow\lozenge sw)$

With the macro:

$\begin{array}[]{lll}sw&\equiv&\neg ⓚ\wedge s\\\ &\wedge&\lozenge(ⓚ\wedge\neg
s)\\\ &\wedge&\square(\lozenge\top~{}\rightarrow(ⓚ\wedge\neg
s\wedge\square((s\wedge\lozenge ⓚ)\rightarrow ⓚ)))\end{array}$

Each grid state sees to its own switch state, which sees a dead-end and sees
the grid state that sees it. Switch states help us simulate the $ⓡ$ operator:
to “remember” a particular grid state, we visit its associated switch state
and come back. Note that formula $(7)$ depends on formula $(6)$ to implement
switches on grid states distants from two steps from spy.

We use the following macro to “remember’ the current grid state:

$\begin{array}[]{lll}ⓡ^{\prime}\varphi&\equiv&\square(\neg ⓚ\wedge
s~{}\rightarrow\square(ⓚ~{}\rightarrow\varphi))\\\ \end{array}$

And to check that a grid state has been remembered:

$\begin{array}[]{lll}ⓚ^{\prime}&\equiv&ⓚ\wedge\square((s\wedge\lozenge
ⓚ)\rightarrow ⓚ)\\\ \end{array}$

Now the following formula makes the spy state see every grid state:

  1. 8.

$\square\square(\neg s\rightarrow ⓡ^{\prime}\square\square(ⓚ\wedge
s~{}\rightarrow\lozenge ⓚ^{\prime}))$

We encode the tiling problem with only one relation, by combining a symmetric
relation with “propositional macros” to represent two “meta-relations” _up_
and _right_ , as shown in Figure 2. In what follows, we use the notations $i$,
$s(i)$ and $p(i)$, with:

$\begin{array}[]{lll}i&\in&\\{0,1,2\\}\\\ s(i)&=&(i+1)\mbox{ mod }3\\\
p(i)&=&(i+2)\mbox{ mod }3\\\ \end{array}$

021102210rrrrrruuuuuu Figure 2: Organization of the grid

Every grid state has an “up”- and a “right”-successor:

  1. 9.

$\bigwedge_{i\in\\{0,1,2\\}}\square(\lozenge\top\wedge
i\rightarrow\lozenge(\neg s\wedge u\wedge\lozenge(\neg s\wedge s(i))))$

  2. 10.

$\bigwedge_{i\in\\{0,1,2\\}}\square(\lozenge\top\wedge
i\rightarrow\lozenge(\neg s\wedge r\wedge\lozenge(\neg s\wedge p(i))))$

“Up” and “right” are irreflexive and functional:

  1. 11.

$\bigwedge_{i\in\\{0,1,2\\}}\square(\lozenge\top\wedge s(i)\rightarrow
ⓡ^{\prime}\square(\neg s\wedge u\rightarrow\square(\neg s\wedge
i\rightarrow\neg ⓚ\wedge\square(\neg s\wedge u\rightarrow\square(\neg s\wedge
s(i)\rightarrow ⓚ^{\prime})))))$

  2. 12.

$\bigwedge_{i\in\\{0,1,2\\}}\square(\lozenge\top\wedge p(i)\rightarrow
ⓡ^{\prime}\square(\neg s\wedge r\rightarrow\square(\neg s\wedge
i\rightarrow\neg ⓚ\wedge\square(\neg s\wedge r\rightarrow\square(\neg s\wedge
p(i)\rightarrow ⓚ^{\prime})))))$

We finish with the confluence property as shown in Figure 3:

  1. 13.

$\bigwedge_{i\in\\{0,1,2\\}}\square(\lozenge\top\wedge s(i)\rightarrow
ⓡ^{\prime}\square(\neg s\wedge u\rightarrow\square(\neg s\wedge
i\rightarrow\square(\neg s\wedge r\rightarrow\square(\neg s\wedge
p(i)\rightarrow\lozenge(\neg s\wedge u\wedge\lozenge(\neg s\wedge
i\wedge\lozenge(\neg s\wedge r\wedge\lozenge(\neg s\wedge s(i)\wedge
ⓚ^{\prime})))))))))$

$i$$p(i)$$s(i)$$i$rruu Figure 3: Confluence property

Now, we encode the actual tiling problem. Given $T={T_{1},\ldots,T_{k}}$ a set
of tile types, we represent each type $T_{i}$ as a macro $t_{i}$. At every
point of the grid, one and only one tile holds:

  1. 14.

$\bigwedge_{i\in\\{0,1,2\\}}\square(\lozenge\top\wedge
i\rightarrow(\bigvee_{1\leq n\leq k}t_{n})\wedge(\bigwedge_{1\leq n<m\leq
k}\neg(t_{n}\wedge t_{m})))$

Then, tile matching:

  1. 15.

$\bigwedge_{i\in\\{0,1,2\\},1\leq n\leq k}\square(\lozenge\top\wedge i\wedge
t_{n}\rightarrow\square(\neg s\wedge u\rightarrow\square(\neg s\wedge
s(i)\rightarrow\bigvee\\{t_{m}\mid top(T_{n})=bottom(T_{m})\\})))$

  2. 16.

$\bigwedge_{i\in\\{0,1,2\\},1\leq n\leq k}\square(\lozenge\top\wedge i\wedge
t_{n}\rightarrow\square(\neg s\wedge r\rightarrow\square(\neg s\wedge
p(i)\rightarrow\bigvee\\{t_{m}\mid right(T_{n})=left(T_{m})\\})))$

We initialize the grid with a first state:

  1. 17.

$\lozenge(\lozenge\top\wedge 0)$

Finally, we assign a distinct natural number $p$ to every propositional macro
that appear in formulas 9–17, and rewrite it to:

$\begin{array}[]{lll}p&\equiv&\lozenge(s\wedge\neg ⓚ\wedge\square\neg
ⓚ\wedge\overbrace{\lozenge\lozenge\ldots\lozenge}^{p~{}times}\square\bot)\end{array}$

We call “propositional states” the states accessible from grid states where
$s\wedge\neg ⓚ\wedge\square\neg ⓚ$ holds. Hence, propositional states do not
see the grid point that see them. Each “propositional symbol” that should be
true at a grid state is represented by a propositional state that sees a dead-
end, does not see the grid point where it came from, and sees the beginning of
a chain of determined length. Propositional states and their corresponding
chains are not seen by the spy state (see formula $(8)$). One can check that
negating such a macro does not interfere with the structure of the grid:

$\begin{array}[]{lll}\neg p&\equiv&\square(s\wedge\neg ⓚ\wedge\square\neg
ⓚ~{}\rightarrow\overbrace{\lozenge\lozenge\ldots\lozenge}^{p~{}times}\square\bot)\end{array}$

######  Lemma 1.

Given a tiling problem $T=T_{1}\ldots T_{k}$, let $Grid(T)$ be the conjunction
of formulas 1–17 rewritten with the propositional encoding previously shown.

$T$ tiles the grid if, and only if, $Grid(T)\in$ $\mathcal{B}(\langle
r\rangle,ⓚ)$-sat.

######  Theorem 2.

$\mathcal{B}(\langle r\rangle,ⓚ)$-sat is undecidable.

##  5 Closing Remarks

We showed that $\mathcal{B}(\langle r\rangle,ⓚ)$, arguably the simplest non-
sub-Boolean modal logic with binding, has an undecidable satisfiability
problem. This result can be reused to show undecidability of the
satisfiability problem of most memory logics and hybrid logics with binders,
by means of simple satisfiability-preserving translations. For instance the
following translation from $\mathcal{B}(\langle r\rangle,ⓚ)$-sat to
$\mathcal{H}({\downarrow})$-sat [3]:

$\begin{array}[]{lll}{\sf Tr}_{N}(\neg\varphi)&=&\neg{\sf Tr}_{N}(\varphi)\\\
{\sf Tr}_{N}(\varphi\wedge\psi)&=&{\sf Tr}_{N}(\varphi)\wedge{\sf
Tr}_{N}(\psi)\\\ {\sf Tr}_{N}(\lozenge\varphi)&=&{\downarrow}i.{\sf
Tr}_{N\cup\\{i\\}}(\varphi)~{}\mbox{with $i\notin N$}\\\ {\sf
Tr}_{N}(ⓚ)&=&\bigvee_{i\in N}i\end{array}$

where $N$ is a subset of the set of nominals, initially empty.

Taking as a starting point the basic hybrid logic with binder
$\mathcal{H}(@,{\downarrow})$, the undecidability results for modal logics
with binding have progressed in two directions. First, by maintaining the
ability to bind an arbitrary number of states, while decreasing the expressive
power of the language. This is how we went from $\mathcal{H}(@,{\downarrow})$,
to $\mathcal{H}({\downarrow})$ without non-nominal propositional symbols [2],
to memory logics with $ⓡ$ and $ⓚ$ [3], to memory logics with $\langle
r\rangle$ instead of $ⓡ$ and $\lozenge$, and finally, to the memory logic
presented in this article.

The second direction has been to restrict the number of bindable states to
only one [8]. This approach actually removes the differences between hybrid
and memory logics (the latter of which were not yet invented at the time of
the result).

It is not clear how to transpose this last approach to the logic presented
here. One way would be to restrict the memory to the last $n$ visited states.
But this involves giving up on the simplicity of the very definition of the
problem. Hence it seems probable that the quest for pushing the undecidable
frontier will continue within a different setting.

## References

  * [1] C. Areces.  Hybrid logics: The old and the new.  In X. Arrazola and J. Larrazabal, editors, Proceedings of LogKCA-07, pages 15–29, San Sebastian, Spain, 2007.
  * [2] C. Areces, P. Blackburn, and M. Marx.  A road-map on complexity for hybrid logics.  In J. Flum and M. Rodríguez-Artalejo, editors, Computer Science Logic, number 1683 in LNCS, pages 307–321, Madrid, Spain, 1999. Springer.  Proceedings of the 8th Annual Conference of the EACSL, Madrid, September 1999.
  * [3] C. Areces, D. Figueira, S. Figueira, and S. Mera.  The expressive power of memory logics.  Review of Symbolic Logic, 4(2):290–318, 2011.
  * [4] C. Areces and B. ten Cate.  Hybrid logics.  In P. Blackburn, F. Wolter, and J. van Benthem, editors, Handbook of Modal Logics, pages 821–868. Elsevier, 2006.
  * [5] P. Blackburn and J. Seligman.  Hybrid languages.  Journal of Logic, Language and Information, 4:251–272, 1995.
  * [6] V. Goranko.  Temporal logic with reference pointers.  In Temporal logic, volume 827 of LNCS, pages 133–148. Berlin: Springer, 1994.
  * [7] Daniel Gorín and Lutz Schröder.  Narcissists are easy, stepmothers are hard.  In Lars Birkedal, editor, Foundations of Software Science and Computational Structures, volume 7213 of Lecture Notes in Computer Science, pages 240–254. Springer Berlin Heidelberg, 2012.
  * [8] Maarten Marx.  Narcissists, stepmothers and spies.  In In Proc. of DL’02, volume 53. CEUR, 2002.
  * [9] T. Schneider.  The Complexity of Hybrid Logics over Restricted Frame Classes.  PhD thesis, University of Jena, 2007.
  * [10] B. ten Cate and M. Franceschet.  On the complexity of hybrid logics with binders.  In L. Ong, editor, Proceedings of Computer Science Logic 2005, volume 3634 of Lecture Notes in Computer Science, pages 339–354. Springer Verlag, 2005.
  * [11] Peter Van Emde Boas.  The convenience of tilings.  In Complexity, Logic, and Recursion Theory, pages 331–363. Marcel Dekker Inc, 1997.