# SCP-GAN: Self-Correcting Discriminator Optimization for Training Consistency
Preserving Metric GAN on Speech Enhancement Tasks

###### Abstract

In recent years, Generative Adversarial Networks (GANs) have produced
significantly improved results in speech enhancement (SE) tasks. They are
difficult to train, however. In this work, we introduce several improvements
to the GAN training schemes, which can be applied to most GAN-based SE models.
We propose using consistency loss functions, which target the inconsistency in
time and time-frequency domains caused by Fourier and Inverse Fourier
Transforms. We also present self-correcting optimization for training a GAN
discriminator on SE tasks, which helps avoid “harmful” training directions for
parts of the discriminator loss function. We have tested our proposed methods
on several state-of-the-art GAN-based SE models and obtained consistent
improvements, including new state-of-the-art results for the Voice Bank+DEMAND
dataset.

Index Terms—  Speech Enhancement, Generative Adversarial Network, MetricGAN,
Self-Correcting Optimization, STFT Consistency, Voice Bank+DEMAND

##  1 Introduction

Speech Enhancement (SE) is a process of making deteriorated speech signals
more understandable and perceptually pleasing. The SE has been widely used for
various applications, including mobile communication, speech recognition
systems, hearing aids, etc. SE as an area of research interest has been around
for several decades. Traditional SE techniques [1, 2] often use a heuristic or
straightforward signal processing algorithm to estimate a gain function, which
is then applied to the noisy input to produce improved speech. Recent
developments in deep learning have inspired many Deep Neural Network
(DNN)-based SE techniques [3, 4, 5, 6, 7] that outperform conventional signal
processing-based methods. One particular DNN-based architecture, Generative
Adversarial Net (GAN), has garnered much interest in the SE community for the
past few years [5, 6, 8, 9]. In the applications of SE, GAN architecture is
primarily employed to generate enhanced speech. One of the earliest works
where GAN models were implemented on the SE domain is the SEGAN [5] model. It
utilizes an adversarial framework to map the noisy waveform to a corresponding
enhanced speech. Later, MetricGAN [6] introduced a metric score optimization
scheme, where an evaluated metric was introduced into adversarial loss
functions, replacing a traditional binary-classifier [5] and creating a new
branch for SE GAN-based research. There have been several improvements to the
MetricGAN model, e.g. MetricGAN+ [8], iMetricGAN [10], CMGAN [9], etc. More
recently, with a rise of Transformers [11] and Conformers [12], models such as
DB-AIAT [13], DPT-FSNet [14], SE-Conformer [15], CMGAN [9], etc. show
significant improvements on SE tasks.

Despite much work, training of GAN-based models are prone to problems such as
non-convergence, overfitting, and gradient instabilities. One common issue in
GAN’s discriminator training is potentially “harmful” gradient direction [16]
where parts of the model might train opposite to the desired direction. To
overcome this problem, we propose a new method called Self-Correcting (SC)
Discriminator Optimization. At the same time, the SE DNN-based models are
subject to problems caused by the signal-processing tools, e.g., an
inconsistency in the Short-Time Fourier Transform (STFT) and its inverse
(iSTFT) [7, 17]. Inspired by [18], we adapt and introduce the consistency loss
function as a part of Consistency Preserving (CP) Net into the GAN framework,
where loss and architecture take into account the iSTFT effects. From our
experiments, the combination of SC and CP methods improves the SE GAN-based
models even further than either single method; we call such a combination SCP-
GAN.

The remainder of this paper is laid out as follows. In section 2, we list
earlier works pertinent to our work. In section 3, we introduce our
improvements to current GAN-based SE models. We present and compare the SCP-
GAN results on Voice Bank+DEMAND dataset [19] to the current state-of-the-art
(SOTA) models in section 4. Then, in section 5, we provide an extensive
ablation study to show the advantages of the proposed methods. Finally, in
section 6, we highlight the methods’ contributions to the field.

##  2 Related Work

###  2.1 Adaptively Weighted GAN (awGAN)

The discriminator plays a very important role in training GAN-based models.
However, optimization of the discriminator loss function(s) has been a
challenge [16]. In the image generation domain, a majority of discriminator
loss functions have the following form:
$\mathcal{L}_{D}=\mathcal{L}_{r}+\mathcal{L}_{f}$, where $\mathcal{L}_{r}$ is
the part that only relies on the original dataset; [16] calls it the ‘real
part’. $\mathcal{L}_{f}$ depends on the generator network, its output, and not
the original data; [16] calls this one the ‘fake part’. However, the training
with $\mathcal{L}_{D}$ is not performed equally on the real and fake parts,
but it depends on the angle between $\nabla\mathcal{L}_{r}$ and
$\nabla\mathcal{L}_{f}$ and their magnitudes. Under such conditions, the
actual training direction $\nabla\mathcal{L}_{D}$ might end up being in the
opposite direction to either $\nabla\mathcal{L}_{r}$ or
$\nabla\mathcal{L}_{f}$, which is undesirable. To solve such issue [16]
proposed the method of adaptive weights for the discriminator loss function:
$\mathcal{L}_{D}^{aw}=w_{r}\mathcal{L}_{r}+w_{f}\mathcal{L}_{f}$, and the
algorithm for choosing these weights.

###  2.2 STFT Consistencies in SE DNN models

In audio signal processing, the short-time Fourier transform (STFT) is one of
the most fundamental and widely used methods. Most DNN-based SE models [7, 9,
17] use a complex-valued STFTs generator to suppress noise and preserve
speech. However, using STFT methods has its issues. One of those issues is the
STFT consistency. This is an issue when a loss function does not consider
iSTFT signal reconstruction. Several works have been done to resolve this
issue. [17] presented an algorithm for a phase reconstruction based on a local
approximation of the consistency constraints. Adding simple differentiable
projection layers to the enhancement DNN to solve the issue was proposed by
[7]. More recently, [18] introduced the iSTFT into back-propagation methods
for SE DNN-based models.

##  3 SCP-GAN

We propose the following two innovative learning strategies to enhance the
performance of the SE GAN-based models.

###  3.1 Self-Correcting Discriminator Optimization

We introduce the Self-Correcting (SC) Discriminator Optimization method, an
adaptation and generalization of the method from [16] to the SE domain. A
large number of existing SE GAN-based models have the discriminator loss
function consisting of either two [6, 9] or three [8] equally weighted parts:

$\displaystyle\mathcal{L}_{D}$ $\displaystyle=\mathcal{L}_{C}+\mathcal{L}_{E}$
(1) $\displaystyle\mathcal{L}_{D}$
$\displaystyle=\mathcal{L}_{C}+\mathcal{L}_{E}+\mathcal{L}_{N},$ (2)

where $\mathcal{L}_{C}$, $\mathcal{L}_{E}$, and $\mathcal{L}_{N}$ exclusively
rely on clean, enhanced, and noisy datasets, respectively; for example,
MetricGAN [6] has a two-part discriminator loss with

$\displaystyle\mathcal{L}_{C}$
$\displaystyle=\mathbb{E}_{y}\left(D(y,y)-Q(y,y)\right)^{2}$ (3)
$\displaystyle\mathcal{L}_{E}$
$\displaystyle=\mathbb{E}_{x,y}\left(D(G(x),y)-Q(G(x),y)\right)^{2},$ (4)

where $x$ is a noisy signal, $y$ is its corresponding clean version, and $D$,
$G$, and $Q$ are the discriminative model, generative model, and evaluation
metric function, respectively. However, gradient descent training with
$\nabla\mathcal{L}_{D}$ is not performed equally on clean and enhanced parts;
its effect depends on the angle between $\nabla\mathcal{L}_{C}$ and
$\nabla\mathcal{L}_{E}$ and their magnitudes. For example, if the angle
between $\nabla\mathcal{L}_{C}$ and $\nabla\mathcal{L}_{E}$ is a large obtuse
angle and
$\left\lvert\left\lvert\nabla\mathcal{L}_{C}\right\rvert\right\rvert_{2}>>\left\lvert\left\lvert\nabla\mathcal{L}_{E}\right\rvert\right\rvert_{2}$,
then $\nabla\mathcal{L}_{D}$ would make an obtuse angle with
$\nabla\mathcal{L}_{E}$ and thus training along $\nabla\mathcal{L}_{D}$ would
increase the loss $\mathcal{L}_{E}$, which would be harmful to the enhanced
part of the model. In addition, MetricGAN+ [8] uses the $\mathcal{L}_{N}$ of
the following form

$\mathcal{L}_{N}=\mathbb{E}_{x,y}\left(D(x,y)-Q(x,y)\right)^{2}.$ (5)

To address this issue, as in [16] for GAN, we introduce weights into the two-
part discriminator in (1),

$\mathcal{L}_{D}^{SC}=w_{C}\mathcal{L}_{C}+w_{E}\mathcal{L}_{E}$ (6)

and call it SC2. Moreover, we introduce weights into the three-part
discriminator in (2)

$\mathcal{L}_{D}^{SC}=w_{C}\mathcal{L}_{C}+w_{E}\mathcal{L}_{E}+w_{N}\mathcal{L}_{N}$
(7)

and call it SC3. The weights in (6) and (7) are determined by Algorithm 1
using $\nabla\mathcal{L}_{C}$, $\nabla\mathcal{L}_{E}$, or
$\nabla\mathcal{L}_{N}$, resulting in a self-correcting discriminator
gradient. The goal of Algorithm 1 is to minimize the potential harm to parts
of the model by ensuring the training gradient $\nabla\mathcal{L}_{D}^{SC}$
does not go obtuse to $\nabla\mathcal{L}_{C}$, $\nabla\mathcal{L}_{E}$, or
$\nabla\mathcal{L}_{N}$.

1Compute: $\nabla\mathcal{L}_{C}$, $\nabla\mathcal{L}_{E}$,
$\nabla\mathcal{L}_{N}$ if $\mathcal{L}_{N}$ is used

2if  _$\angle_{2}\left(\nabla\mathcal{L}_{C},\nabla\mathcal{L}_{E}\right)
<90^{\circ}$_ then

3 $w_{C}=1$ and $w_{E}=1$

4 if  _$\mathcal{L}_{N}$ is used and
$\angle_{2}\left(w_{C}\nabla\mathcal{L}_{C}+w_{E}\nabla\mathcal{L}_{E},\nabla\mathcal{L}_{N}\right)<90^{\circ}$
_ then

5 $w_{N}=1$

6 else

7
$w_{N}=-\dfrac{\left\langle\nabla\mathcal{L}_{C},\nabla\mathcal{L}_{N}\right\rangle_{2}}{\left\lvert\left\lvert\nabla\mathcal{L}_{N}\right\rvert\right\rvert_{2}^{2}}-\dfrac{\left\langle\nabla\mathcal{L}_{E},\nabla\mathcal{L}_{N}\right\rangle_{2}}{\left\lvert\left\lvert\nabla\mathcal{L}_{N}\right\rvert\right\rvert_{2}^{2}}$

8 end if

9

10else

11 $w_{C}=1$ and
$w_{E}=-\dfrac{\left\langle\nabla\mathcal{L}_{C},\nabla\mathcal{L}_{E}\right\rangle_{2}}{\left\lvert\left\lvert\nabla\mathcal{L}_{E}\right\rvert\right\rvert_{2}^{2}}$

12 if  _$\mathcal{L}_{N}$ is used and
$\angle_{2}\left(w_{C}\nabla\mathcal{L}_{C}+w_{E}\nabla\mathcal{L}_{E},\nabla\mathcal{L}_{N}\right)<90^{\circ}$
_ then

13 $w_{N}=1$

14 else

15

$w_{N}=-\dfrac{\left\langle\nabla\mathcal{L}_{C},\nabla\mathcal{L}_{N}\right\rangle_{2}}{\left\lvert\left\lvert\nabla\mathcal{L}_{N}\right\rvert\right\rvert_{2}^{2}}+\dfrac{\left\langle\nabla\mathcal{L}_{C},\nabla\mathcal{L}_{E}\right\rangle_{2}\left\langle\nabla\mathcal{L}_{E},\nabla\mathcal{L}_{N}\right\rangle_{2}}{\left\lvert\left\lvert\nabla\mathcal{L}_{E}\right\rvert\right\rvert_{2}^{2}\left\lvert\left\lvert\nabla\mathcal{L}_{N}\right\rvert\right\rvert_{2}^{2}}$

16 end if

17

18 end if

Algorithm 1 SC2/SC3 method

###  3.2 Consistency Preserving Network

(a)

(b)

Fig. 1: Traditional vs. Consistency Preserving SE GAN-based models

The majority of GAN-based SE models [6, 9, 13, 14] have a generator (G) that
accepts STFT spectrogram of a noisy waveform as input. The G’s output is an
enhanced spectrogram that later uses iSTFT to produce the enhanced waveform;
Figure 1(a) illustrates the process. The G is then updated using a combination
of various loss functions, e.g. Time Loss [20], TF-magnitude Loss [21],
Adversarial Metric Loss [6], etc. For example, the TF-magnitude Loss [21] is
computed between the enhanced and clean spectrograms, see diagram in Figure
1(a). However, such loss and architectural setup do not take into account the
effect of the iSTFT reconstruction which causes inconsistencies between
signals.

We incorporate the idea from [18] to SE GAN-based model by modifying
architecture and loss function(s) such that any input into a loss function
undergoes the same process, taking into consideration the effects of signal
reconstruction from the spectrogram; we call such process and loss function a
Consistency Preserving (CP) Network and a consistency loss, respectively.
Figure 1(b) depicts the process of computing Time and TF-magnitude losses
using the proposed CP method by ensuring that the same transforms are applied
on enhanced, clean, and noisy (if used) signals.

Note that the Clean Audio to the Clean∗ Audio process inside the CP Net
(2${}^{\text{nd}}$ row of Figure 1(b)) can be performed at the data
preprocessing stage.

##  4 Experiments

Model | # of Param. | PESQ | CSIG | CBAK | COVL | SSNR | STOI
---|---|---|---|---|---|---|---
Noisy Data | n/a | 1.97 | 3.35 | 2.44 | 2.63 | 1.68 | 0.91
SE-Conformer [15] | - | 3.13 | 4.45 | 3.55 | 3.82 | - | 0.95
MANNER [22] | - | 3.21 | 4.53 | 3.65 | 3.91 | - | -
DB-AIAT [13] | 2.81M | 3.31 | 4.61 | 3.75 | 3.96 | 10.79 | 0.96
DPT-FSNet [14] | 0.91M | 3.33 | 4.58 | 3.72 | 4.00 | - | 0.96
PCS [23] | - | 3.35 | 4.43 | - | 3.92 | - | 0.95
MetricGAN+ [8] | 2.6M | 3.15 | 4.14 | 3.16 | 3.64 | - | 0.93†
MetricGAN+ (repro.) | 2.6M | 3.08 | 4.05 | 3.01 | 3.60 | - | 0.92
SCP-MetricGAN+ (ours) | 2.6M | 3.19 | 4.20 | 3.20 | 3.65 | - | 0.93
CMGAN [9] | 1.83M | 3.41 | 4.63 | 3.94 | 4.12 | 11.10 | 0.96
CMGAN (repro.) | 1.83M | 3.39 | 4.62 | 3.93 | 4.13 | 10.61 | 0.96
SCP-CMGAN (ours) | 1.83M | 3.52 | 4.75 | 3.97 | 4.25 | 10.82 | 0.96

Table 1: Performance comparison on Voice Bank+DEMAND dataset [19]: “-” denotes
the results not provided in the original paper; $\dagger$ \- quoted from [23];
repro. - our reproduction of experiments

###  4.1 Dataset

We use the publicly accessible Voice Bank+DEMAND [19] dataset to evaluate and
compare our proposed SCP-GAN method. The training set of the Voice Bank+DEMAND
dataset consists of 11,572 individual recordings of 28 speakers from the Voice
Bank corpus [24] which are mixed with DEMAND [25] database and some artificial
background noises at the signal-to-noise ratios (SNRs) of 0, 5, 10, and 15 dB.
The test set has 824 utterances of two speakers from the Voice Bank corpus,
which are mixed with unseen DEMAND noises at the SNRs of 2.5, 7.5, 12.5, and
17.5 dB.

###  4.2 Evaluation Metrics

To assess the speech quality, we select a set of widely used metrics,
including the Perceptual Evaluation of Speech Quality (PESQ) [26] (ranging
between -0.5 and 4.5), the Mean Opinion Score (MOS) [27], prediction of the
signal distortion (CSIG), the MOS prediction of the intrusiveness of
background noise (CBAK), MOS prediction of the overall effect (COVL) (all MOS
metrics range between 1 and 5), the Segmental Signal-to-Noise Ratio (SSNR),
and the Short-Time Objective Intelligibility (STOI) [28] (with a range 0 to
1). For all metrics, higher numbers denote better performance.

###  4.3 Experimental Results

We have applied our proposed methods to two baseline models: a widely-used
MetricGAN+ [8] model and a current SOTA model - CMGAN [9]. Our SCP method
shows a consistent improvement over the compared baseline. On the MetricGAN+
model, our SCP-MetricGAN+ improved by 0.04, 0.06, 0.04, and 0.01 on the PESQ,
CSIG, CBAK, and COVL metrics, respectively. Our improvements with the SCP-
CMGAN model are 0.11, 0.12, 0.03, and 0.13 on the same scores. Moreover, we
have compared our method to other recent SOTA models which can be seen in
Table 1.

Note: Results provided in Table 1 for MetricGAN+ and CMGAN models are quoted
from the original papers; however, to verify them, we have obtained our
results: MetricGAN+ (repro.) and CMGAN (repro.). The results for the CMGAN
(repro.) model are very similar to the results from [9] with one exception -
the SSNR metric, where our result is lower: 10.61 (ours) vs. 11.10 [9].
Furthermore, the results for MetricGAN+ (repro.) model are slightly lower than
the ones provided in the original paper [8].

##  5 Ablation Study

We have conducted an ablation study to demonstrate the importance of our
methods. We have chosen the CMGAN [9] model as the base model due to its SOTA
performance at the time of this study. Table 2 shows the average results of
each model’s best performance over three randomly chosen seeds.

First, we have retrained the CMGAN [9] model to verify the results from [9].
The results obtained from our experiments are relatively close to the results
stated in [9], except for the SSNR metric where we have obtained slightly
lower results, i.e., SSNR of 10.61 (ours) vs. SSNR of 11.10 [9].

Next, we have added Noisy Data (ND) to the CMGAN model discriminator training
(‘+ ND’ in Table 2); however, such an addition had slight improvement over the
baseline. Following it, we have considered adding our SC method to the
baseline model (‘+ SC2’ in Table 2) and nothing else. With SC2, we saw some
improvements in PESQ, COVL, and SSNR metrics. Furthermore, we have analyzed
the advantages of the CP method (‘+ CP’ in Table 2) without any add-ons. The
CP shows significant improvements in PESQ, CSIG, and COVL metrics and is
comparable in the others.

Then, we combined ND and SC3 methods (‘+ ND, SC3’ in Table 2). Such a setup
further improves baseline as well as single methods, particularly in COVL and
SSNR metrics. A combination of ND and CP methods (‘+ ND, CP’ in Table 2) has
the same nature of improvements, producing better results in PESQ, CSIG, and
COVL metrics. The last combination of SC2 and CP methods (‘+ SC2, CP’ in Table
2) demonstrates that together both proposed methods achieve significant
improvements on the SE task. Moreover, this particular model achieved the
highest SSNR result of 10.91.

Finally, we have combined ND, SC3, and CP methods in the model we call SCP-
CMGAN in Table 1. Adding ND and switching from SC2 to SC3 further improves the
‘CMGAN + SC2, CP’ model, achieving new SOTA results.

Note that all of the above models were trained under the same conditions
without changing the hyperparameters and with identical software and hardware
settings: Python 3.8.13, PyTorch 1.10, and CUDA 11 on NVIDIA Tesla V100 GPUs.

Model | PESQ | CSIG | CBAK | COVL | SSNR
---|---|---|---|---|---
CMGAN (repro.)† | 3.39 | 4.62 | 3.93 | 4.13 | 10.61
\+ ND | 3.41 | 4.65 | 3.92 | 4.13 | 10.68
\+ SC2 | 3.44 | 4.65 | 3.92 | 4.17 | 10.70
\+ CP | 3.47 | 4.71 | 3.93 | 4.20 | 10.54
\+ ND, SC3 | 3.43 | 4.64 | 3.93 | 4.18 | 10.76
\+ ND, CP | 3.47 | 4.73 | 3.93 | 4.22 | 10.53
\+ SC2, CP | 3.49 | 4.72 | 3.96 | 4.24 | 10.91
\+ ND, SC3, CP | 3.52 | 4.75 | 3.97 | 4.25 | 10.82

Table 2: Ablation Study on Voice Bank + DEMAND: STOI results are equal to 0.96
for all the tests; † \- results from our tests; ND - Noisy Data, CP -
Consistency Preserving method, SC2 \- SC with $\mathcal{L}_{C}$ and
$\mathcal{L}_{E}$, SC3 \- SC with $\mathcal{L}_{C}$, $\mathcal{L}_{E}$,
$\mathcal{L}_{N}$.

##  6 Conclusion

This paper presents several improvements to SE GAN-based models. The proposed
method of Consistency Preservation reconciles the issue with Fourier and
Inverse-Fourier transforms inside the generative models. At the same time, the
Self-Correcting Discriminator Optimization method helps with training the
discriminative model by avoiding gradient directions that are potentially
harmful to the training. Our experiments and ablation study demonstrate the
advantages of using one or both of the proposed methods, including new SOTA
results for the Voice Bank+DEMAND dataset.

## References

  * [1] S. Boll,  “Suppression of acoustic noise in speech using spectral subtraction,”  IEEE TASSP, pp. 113–120, 1979.
  * [2] J. Lim and A. Oppenheim,  “All-pole modeling of degraded speech,”  IEEE TASSP, pp. 197–210, 1978.
  * [3] A. E. Bulut and K. Koishida,  “Low-latency single channel speech enhancement using u-net convolutional neural networks,”  in ICASSP, 2020, pp. 6214–6218.
  * [4] D. Tran and K. Koishida,  “Single-channel speech enhancement by subspace affinity minimization.,”  in INTERSPEECH, 2020, pp. 2447–2451.
  * [5] S. Pascual, A. Bonafonte, and J. Serrà,  “Segan: Speech enhancement generative adversarial network,” 2017.
  * [6] S.-W. Fu, C.-F. Liao, Y. Tsao, and S.-D. Lin,  “MetricGAN: Generative adversarial networks based black-box metric scores optimization for speech enhancement,”  in Proceedings of the ICML, 2019, pp. 2031–2041.
  * [7] S. Wisdom, J. Hershey, K. Wilson, J. Thorpe, M. Chinen, B. Patton, and R. Saurous,  “Differentiable consistency constraints for improved deep speech enhancement,”  ICASSP, pp. 900–904, 2019.
  * [8] S.-W. Fu, C. Yu, T.-A. Hsieh, P. Plantinga, M. Ravanelli, X. Lu, and Y. Tsao,  “Metricgan+: An improved version of metricgan for speech enhancement,”  arXiv, 2021.
  * [9] R. Cao, S. Abdulatif, and B. Yang,  “Cmgan: Conformer-based metric gan for speech enhancement,”  arXiv:2203.15149, 2022.
  * [10] H. Li, S.-W. Fu, Y. Tsao, and J. Yamagishi,  “imetricgan: Intelligibility enhancement for speech-in-noise using generative adversarial network-based metric learning,”  ArXiv, vol. abs/2004.00932, 2020.
  * [11] A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. Gomez, L. Kaiser, and I. Polosukhin,  “Attention is all you need,”  in NIPS, 2017.
  * [12] A. Gulati, J. Qin, C.-C. Chiu, N. Parmar, Y. Zhang, J. Yu, W. Han, S. Wang, Z. Zhang, Y. Wu, and R. Pang,  “Conformer: Convolution-augmented transformer for speech recognition,”  ArXiv, vol. abs/2005.08100, 2020.
  * [13] G. Yu, A. Li, C. Zheng, Y. Guo, Y. Wang, and H. Wang,  “Dual-branch attention-in-attention transformer for single-channel speech enhancement,”  in Processing of ICASSP, 2022, pp. 7847–7851.
  * [14] F. Dang, H. Chen, and P. Zhang,  “Dpt-fsnet: Dual-path transformer based full-band and sub-band fusion network for speech enhancement,”  in Processing of ICASSP, 2022, pp. 6857–6861.
  * [15] E. Kim and H. Seo,  “Se-conformer: Time-domain speech enhancement using conformer,”  in Proc. Interspeech, 2021, pp. 2736–2740.
  * [16] V. Zadorozhnyy, Q. Cheng, and Q. Ye,  “Adaptive weighted discriminator for training gans,”  in Proceedings of the CVPR Conference, 2021, pp. 4781–4790.
  * [17] J. Le Roux, H. Kameoka, N. Ono, and S. Sagayama,  “Fast signal reconstruction from magnitude stft spectrogram based on spectrogram consistency,”  in Proc. DAFx, 2010, pp. 397–403.
  * [18] S. Braun, H. Gamper, C. Reddy, and I. Tashev,  “Towards efficient models for real-time deep noise suppression,”  ICASSP, pp. 656–660, 2021.
  * [19] C. Valentini-Botinhao, X. Wang, S. Takaki, and J. Yamagishi,  “Investigating rnn-based speech enhancement methods for noise-robust text-to-speech,”  in SSW, 2016.
  * [20] S. Abdulatif, K. Armanious, Ja. Thaiparambil Sajeev, K. Guirguis, and B. Yang,  “Investigating cross-domain losses for speech enhancement,”  2021, pp. 411–415.
  * [21] S. Braun and I. Tashev,  “A consolidated view of loss functions for supervised deep learning-based speech enhancement,”  ICTSP, pp. 72–76, 2021.
  * [22] H. J. Park, B. H. Kang, W. Shin, J. S. Kim, and S. W. Han,  “Manner: Multi-view attention network for noise erasure,”  in ICASSP, 2022, pp. 7842–7846.
  * [23] R. Chao, C. Yu, S.-W. Fu, X. Lu, and Y. Tsao,  “Perceptual contrast stretching on target feature for speech enhancement,”  Proc. of INTERSPEECH, 2022.
  * [24] C. Veaux, J. Yamagishi, and S. King,  “The voice bank corpus: Design, collection and data analysis of a large regional accent speech database,”  in O-COCOSDA/CASLRE, 2013, pp. 1–4.
  * [25] J. Thiemann, N. Ito, and E. Vincent,  “The diverse environments multi-channel acoustic noise database (demand): A database of multichannel environmental noise recordings,”  POMA, p. 035081, 2013.
  * [26] A. Rix, J. Beerends, M. Hollier, and A. Hekstra,  “Perceptual evaluation of speech quality (pesq)-a new method for speech quality assessment of telephone networks and codecs,”  ICASSP, pp. 749–752, 2001.
  * [27] Y. Hu and P. Loizou,  “Evaluation of objective quality measures for speech enhancement,”  IEEE/ACM TASLP, pp. 229–238, 2008.
  * [28] C. Taal, R. Hendriks, R. Heusdens, and J. Jensen,  “A short-time objective intelligibility measure for time-frequency weighted noisy speech,”  in ICASSP, 2010, pp. 4214–4217.


Then, $\emptyset$ is $\lambda$-consistent with any step, and (b) follows from
$(\star)$.

  * •

If $\rho,i\models_{\mathcal{K}}K$ for some
$K\in\mathcal{K}_{\mathcal{B}}(\Phi)$, we may take
$(\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl},\\{K\\})\in\delta(\text{\textgravedbl}\\!{K}\\!\text{\textacutedbl})$.
As $\rho,i\models_{\mathcal{K}}K$, $\alpha_{i}$ satisfies $K(b_{i})$, so
consistency holds and we use ($\star$) for $(b)$.

  * •

If $\rho,i\models_{\mathcal{K}}\mathsf{X}\,\psi$ then $i\,{<}\,n$ and
$\rho,i{+}1\models_{\mathcal{K}}\psi$. For
$(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl},\\{\neg\lambda\\})\in\delta(\text{\textgravedbl}\\!{\mathsf{X}\,\psi}\\!\text{\textacutedbl})$,
part $(a)$ holds since $\neg\lambda\in\varsigma$ and $i\,{<}\,n$, and $(b)$
because of $\rho,i{+}1\models_{\mathcal{K}}\psi$.

  * •

Suppose $\rho,i\models_{\mathcal{K}}\mathsf{Y}\,\psi$. If $i=n$ then (a) is by
definition, and (b) by $(\star)$. If $i\,{<}\,n$ then
$\rho,i{+}1\models_{\mathcal{K}}\psi$. For
$(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl},\\{\neg\lambda\\})\in\delta(\text{\textgravedbl}\\!{\mathsf{Y}\,\psi}\\!\text{\textacutedbl})$,
part $(a)$ holds since $\neg\lambda\in\varsigma$ and $i\,{<}\,n$, and $(b)$
because of $\rho,i{+}1\models_{\mathcal{K}}\psi$.

  * •

Suppose $\psi=\psi_{1}\wedge\psi_{2}$. By assumption
$\rho,i\models_{\mathcal{K}}\psi_{1}\wedge\psi_{2}$, and hence
$\rho,i\models_{\mathcal{K}}\psi_{1}$ and
$\rho,i\models_{\mathcal{K}}\psi_{2}$. By the induction hypothesis, there are
$(\text{\textgravedbl}\\!{\psi_{1}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1})\in\delta(\text{\textgravedbl}\\!{\psi_{1}}\\!\text{\textacutedbl})$
and
$(\text{\textgravedbl}\\!{\psi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2})\in\delta(\text{\textgravedbl}\\!{\psi_{2}}\\!\text{\textacutedbl})$
such that for both $k\in\\{1,2\\}$, $(a^{\prime})$ $\varsigma_{k}$ is
consistent with step $i$ of $\rho$ and $(b^{\prime})$ either
$\rho,i{+}1\models_{\mathcal{K}}\psi_{k}^{\prime}$, or $i\,{=}\,n$ and
$\psi_{k}^{\prime}=\top$. By definition of $\delta$, we can choose
$(\text{\textgravedbl}\\!{\psi_{1}^{\prime}\wedge\psi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1}\cup\varsigma_{2})\in\delta(\text{\textgravedbl}\\!{\psi_{1}\wedge\psi_{2}}\\!\text{\textacutedbl})$.
Then $(a)$ follows from $(a^{\prime})$ and
$\varsigma=\varsigma_{1}\cup\varsigma_{2}$, and $(b)$ if $i=n$ then
$(b^{\prime})$ implies $\psi^{\prime}=\top$, and otherwise
$\rho,i{+}1\models_{\mathcal{K}}\psi_{1}^{\prime}\wedge\psi_{2}^{\prime}$.

  * •

Suppose $\psi=\psi_{1}\vee\psi_{2}$. By assumption
$\rho,i\models_{\mathcal{K}}\psi_{1}\vee\psi_{2}$, and hence
$\rho,i\models_{\mathcal{K}}\psi_{1}$ or
$\rho,i\models_{\mathcal{K}}\psi_{2}$. We assume the former. By the induction
hypothesis, there is some
$(\text{\textgravedbl}\\!{\psi_{1}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1})\in\delta(\text{\textgravedbl}\\!{\psi_{1}}\\!\text{\textacutedbl})$
such that $(a^{\prime})$ $\varsigma_{1}$ is consistent with step $i$ of
$\rho$, and $(b^{\prime})$ $\rho,i{+}1\models_{\mathcal{K}}\psi_{1}^{\prime}$,
or $i\,{=}\,n$ and $\psi_{1}^{\prime}=\top$. As $\delta$ is total (Lem. 7),
there must be some
$(\text{\textgravedbl}\\!{\psi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2})\in\delta(\text{\textgravedbl}\\!{\psi_{2}}\\!\text{\textacutedbl})$
such that $\varsigma_{2}$ is $\lambda$-consistent with step $i$ of $\rho$. By
definition of $\delta$, we can choose
$(\text{\textgravedbl}\\!{\psi^{\prime}}\\!\text{\textacutedbl},\varsigma)$ as
$(\text{\textgravedbl}\\!{\psi_{1}^{\prime}\vee\psi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1}\cup\varsigma_{2})\in\delta(\text{\textgravedbl}\\!{\psi_{1}\vee\psi_{2}}\\!\text{\textacutedbl})$.
Then $(a)$ follows from $(a^{\prime})$ and $\varsigma_{2}$ being
$\lambda$-consistent with step $i$ of $\rho$, and $(b)$ if $i\,{=}\,n$ then
$(b^{\prime})$ implies $\psi_{1}^{\prime}\,{=}\,\top$, hence
$\psi^{\prime}\,{=}\,\top$; otherwise
$\rho,i{+}1\models_{\mathcal{K}}\psi_{1}^{\prime}\vee\psi_{2}^{\prime}$.

  * •

Suppose $\rho,i\models_{\mathcal{K}}\mathsf{G}\,\psi$, so
$\rho,i\models_{\mathcal{K}}\psi$ and either (1) $i=n$, or (2)
$\rho,i{+}1\models_{\mathcal{K}}\mathsf{G}\,\psi$. We have
$\delta(\text{\textgravedbl}\\!{\mathsf{G}\,\psi}\\!\text{\textacutedbl})=\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})\wedge(\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\mathsf{G}\,\psi}\\!\text{\textacutedbl})\vee\delta_{\lambda})=(\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})\wedge\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\mathsf{G}\,\psi}\\!\text{\textacutedbl}))\vee(\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})\wedge\delta_{\lambda})$.
In either case, by the induction hypothesis there is some
$(\text{\textgravedbl}\\!{\psi^{\prime}}\\!\text{\textacutedbl},\varsigma^{\prime})\in\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})$
such that $(a^{\prime})$ $\varsigma^{\prime}$ is $\lambda$-consistent with
step $i$ of $\rho$, and $(b^{\prime})$
$\rho,i{+}1\models_{\mathcal{K}}\psi^{\prime}$, or $i\,{=}\,n$ and
$\psi^{\prime}=\top$.

(1) Let
$(\text{\textgravedbl}\\!{\psi_{1}}\\!\text{\textacutedbl},\varsigma_{1})$ be
$(\text{\textgravedbl}\\!{\psi^{\prime}\wedge\top}\\!\text{\textacutedbl},\varsigma^{\prime}\cup\\{\lambda\\})\in\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})\wedge\delta_{\lambda}$.
We have $(a_{1})$ $\varsigma_{1}$ is $\lambda$-consistent with step $i$ of
$\rho$ because of $(a^{\prime})$ and $i\,{=}\,n$, and $(b_{1})$
$\rho,i{+}1\models_{\mathcal{K}}\psi_{1}=\top$ by $(b^{\prime})$.

(2) Let
$(\text{\textgravedbl}\\!{\psi_{2}}\\!\text{\textacutedbl},\varsigma_{2})$ be
$(\text{\textgravedbl}\\!{\psi^{\prime}\wedge\mathsf{G}\,\psi}\\!\text{\textacutedbl},\varsigma^{\prime}\cup\\{\neg\lambda\\})\in\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})\wedge\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\mathsf{G}\,\psi}\\!\text{\textacutedbl})$.
Then $(a_{2})$ $\varsigma_{2}$ is $\lambda$-consistent with step $i$ of $\rho$
by $(a^{\prime})$ and $i<n$, and $(b_{2})$
$\rho,i{+}1\models_{\mathcal{K}}\psi_{2}=\psi^{\prime}\wedge\mathsf{G}\,\psi$,
using $(b^{\prime})$ and $\rho,i{+}1\models_{\mathcal{K}}\mathsf{G}\,\psi$.
Thus the two cases can be combined as in the case for disjunction, using
$(a_{1})$, $(b_{1})$ and $(a_{2})$, $(b_{2})$.

  * •

The case for the $\mathrel{\mathsf{U}}$ operator is similar.

($\Longleftarrow$) Note that the assumptions exclude $\psi^{\prime}=\bot$. We
apply induction on $\psi$, and use the definition of $\delta$ for each case.

  * •

If $\psi=\top$ then
$(\text{\textgravedbl}\\!{\psi^{\prime}}\\!\text{\textacutedbl},\varsigma)\in\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})$
implies $\psi^{\prime}=\top$, and $\rho,i\models_{\mathcal{K}}\top$ holds.

  * •

If $\psi\,{=}\,K\in\mathcal{K}_{\mathcal{B}}(\Phi)$, we must have
$\psi^{\prime}=\top$ and $\varsigma=\\{K\\}$. As $\alpha_{i}\models K(b_{i})$
by $\lambda$-consistency, $\rho,i\models_{\mathcal{K}}K$.

  * •

Let $\psi=\mathsf{X}\,\chi$. As $\psi^{\prime}=\bot$ or
$\rho,i{+}1\models_{\mathcal{K}}\psi^{\prime}$, by definition of $\delta$ the
only possibility is
$\psi^{\prime}=\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl}$ and
$\varsigma=\\{\neg\lambda\\}$. As $\varsigma$ is consistent with step $i$ of
$\rho$ and $\neg\lambda\in\varsigma$, we must have $i\,{<}\,n$, so
$\rho,i{+}1\models_{\mathcal{K}}\psi^{\prime}$ and hence
$\rho,i\models_{\mathcal{K}}\psi$ by Def. 9.

  * •

Suppose $\psi=\mathsf{Y}\,\chi$. If $\psi^{\prime}=\top$ then $i=n$ and
$\rho,i\models_{\mathcal{K}}\psi$ holds by definition. Otherwise, we can
reason as in the case above.

  * •

If $\psi=\psi_{1}\wedge\psi_{2}$ then by
$(\text{\textgravedbl}\\!{\psi^{\prime}}\\!\text{\textacutedbl},\varsigma)\in\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})$
and the definition of $\delta$ there are $\psi_{1}^{\prime}$ and
$\psi_{2}^{\prime}$ such that
$(\text{\textgravedbl}\\!{\psi_{1}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1}^{\prime})\in\delta(\text{\textgravedbl}\\!{\psi_{1}}\\!\text{\textacutedbl})$
and
$(\text{\textgravedbl}\\!{\psi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2}^{\prime})\in\delta(\text{\textgravedbl}\\!{\psi_{2}}\\!\text{\textacutedbl})$,
and $\psi^{\prime}=\psi_{1}^{\prime}\wedge\psi_{2}^{\prime}$ and
$\varsigma=\varsigma_{1}^{\prime}\cup\varsigma_{2}^{\prime}$. Therefore,
either $i=n$ and $\psi^{\prime}=\psi_{1}^{\prime}=\psi_{2}^{\prime}=\top$, or
$i<n$ and $\rho,i{+}1\models_{\mathcal{K}}\psi^{\prime}$, which implies
$\rho,i{+}1\models_{\mathcal{K}}\psi_{1}^{\prime}$ and
$\rho,i{+}1\models_{\mathcal{K}}\psi_{2}^{\prime}$. In either case,
$\rho,i\models_{\mathcal{K}}\psi_{1}$ and
$\rho,i\models_{\mathcal{K}}\psi_{2}$ hold by the induction hypothesis, so
$\rho,i\models_{\mathcal{K}}\psi_{1}\wedge\psi_{2}$.

  * •

Similarly, if $\psi=\psi_{1}\vee\psi_{2}$ then there are $\psi_{1}^{\prime}$
and $\psi_{2}^{\prime}$ such that
$(\text{\textgravedbl}\\!{\psi_{1}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1}^{\prime})\in\delta(\text{\textgravedbl}\\!{\psi_{1}}\\!\text{\textacutedbl})$
and
$(\text{\textgravedbl}\\!{\psi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2}^{\prime})\in\delta(\text{\textgravedbl}\\!{\psi_{2}}\\!\text{\textacutedbl})$,
$\psi^{\prime}=\psi_{1}^{\prime}\vee\psi_{2}^{\prime}$ and
$\varsigma=\varsigma_{1}^{\prime}\cup\varsigma_{2}^{\prime}$. If $i=n$ and
$\psi^{\prime}=\top$, then $\psi_{1}^{\prime}=\top$ or
$\psi_{2}^{\prime}=\top$. If otherwise $i<n$ then
$\rho,i{+}1\models_{\mathcal{K}}\psi^{\prime}$ implies
$\rho,i{+}1\models_{\mathcal{K}}\psi_{1}^{\prime}$ or
$\rho,i{+}1\models_{\mathcal{K}}\psi_{2}^{\prime}$. From the induction
hypothesis we obtain in either case $\rho,i\models_{\mathcal{K}}\psi_{1}$ or
$\rho,i\models_{\mathcal{K}}\psi_{2}$, so
$\rho,i\models_{\mathcal{K}}\psi_{1}\vee\psi_{2}$.

  * •

If $\psi=\mathsf{G}\,\chi$ then we can distinguish two cases:

(1) There are $\psi_{1}$ and $\psi_{2}$ such that
$(\text{\textgravedbl}\\!{\psi_{1}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1})\in\delta(\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl})$,
$(\text{\textgravedbl}\\!{\psi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2})\in\delta_{\lambda}$,
$\psi^{\prime}=\psi_{1}^{\prime}\wedge\psi_{2}^{\prime}$ and
$\varsigma=\varsigma_{1}\cup\varsigma_{2}$. As
$(\text{\textgravedbl}\\!{\psi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2})\in\delta_{\lambda}$,
we must have $\psi_{2}^{\prime}=\top$ and $\varsigma_{2}=\\{\lambda\\}$
(otherwise, we would have $\psi^{\prime}=\bot$). By consistency,
$\lambda\in\varsigma$ implies $i=n$, so $\psi^{\prime}=\top$ by assumption and
therefore we must have $\psi_{1}^{\prime}=\top$. From the induction hypothesis
and
$(\text{\textgravedbl}\\!{\psi_{1}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1})\in\delta(\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl})$
we conclude $\rho,i\models_{\mathcal{K}}\chi$, so by Def. 9
$\rho,i\models_{\mathcal{K}}\mathsf{G}\,\chi$.

(2) There are $\psi_{1}^{\prime}$ and $\psi_{2}^{\prime}$ such that
$(\text{\textgravedbl}\\!{\psi_{1}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1})\in\delta(\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl})$,
$(\text{\textgravedbl}\\!{\psi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2})\in\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\mathsf{G}\,\chi}\\!\text{\textacutedbl})$,
$\psi^{\prime}=\psi_{1}^{\prime}\wedge\psi_{2}^{\prime}$ and
$\varsigma=\varsigma_{1}\cup\varsigma_{2}$. We have
$\neg\lambda\in\varsigma_{2}$, so by consistency $i<n$. As
$\rho,i{+}1\models_{\mathcal{K}}\psi^{\prime}=\psi_{1}^{\prime}\wedge\psi_{2}^{\prime}$,
by Def. 9 $\rho,i{+}1\models_{\mathcal{K}}\psi_{1}^{\prime}$ and
$\rho,i{+}1\models_{\mathcal{K}}\psi_{2}^{\prime}$. By the induction
hypothesis,
$(\text{\textgravedbl}\\!{\psi_{1}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1})\in\delta(\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl})$
and $\rho,i{+}1\models_{\mathcal{K}}\psi_{1}^{\prime}$ imply
$\rho,i\models_{\mathcal{K}}\chi$. Moreover,
$(\text{\textgravedbl}\\!{\psi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2})\in\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\mathsf{G}\,\chi}\\!\text{\textacutedbl})$
and $\rho,i{+}1\models_{\mathcal{K}}\psi_{2}^{\prime}$ imply
$\psi_{2}^{\prime}=\mathsf{G}\,\chi$ by Def. 9, so we have
$\rho,i\models_{\mathcal{K}}\langle\cdot\rangle\mathsf{G}\,\chi$. Thus
$\rho,i\models_{\mathcal{K}}\mathsf{G}\,\chi$.

  * •

The case for $\mathrel{\mathsf{U}}$ is similar. ∎

Let a word $\varsigma_{0}\varsigma_{1}\cdots\varsigma_{n}\in\Sigma^{\prime*}$
be _well-formed_ if $\lambda\not\in\varsigma_{i}$ for all
$0\,{\leq}\,i\,{\leq}\,n$, and $\neg\lambda\,{\not\in}\,\varsigma_{n}$.

###### Lemma 9

A well-formed word $w\in\Sigma^{\prime*}$ that is consistent with a run $\rho$
satisfies
$\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}\in\delta^{*}(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl},w)$
iff $\rho,0\models_{\mathcal{K}}\psi$.

###### Proof

($\Longrightarrow$) Let $w=\varsigma_{0}\varsigma_{1}\cdots\varsigma_{n}$ and
$\chi_{0},\chi_{1},\dots,\chi_{n+1}$ be the sequence of formulas witnessing
$\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}\in\delta^{*}(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl},w)$,
so that $\chi_{0}=\psi$, $\chi_{n+1}=\top$, and
$(\text{\textgravedbl}\\!{\chi_{i{+}1}}\\!\text{\textacutedbl},\varsigma_{i})\in\delta(\text{\textgravedbl}\\!{\chi_{i}}\\!\text{\textacutedbl})$
for all $i$, $0\leq i\leq n$. As $w$ is well-formed and consistent with
$\rho$, by definition $\varsigma_{i}$ is $\lambda$-consistent with $\rho$ at
$i$ for all $i$, $0\leq i\leq n$. In order to show that
$\rho,0\models_{\mathcal{K}}\psi$ holds, we verify that
$\rho,i\models_{\mathcal{K}}\chi_{i}$ for all $i$, $0\,{\leq}\,i\,{\leq}\,n$,
by induction on $n-i$. In the base case $i\,{=}\,n$. We have $\chi_{n+1}=\top$
and
$(\text{\textgravedbl}\\!{\chi_{n{+}1}}\\!\text{\textacutedbl},\varsigma_{n})\in\delta(\text{\textgravedbl}\\!{\chi_{n}}\\!\text{\textacutedbl})$,
and from Lem. 8 ($\Longrightarrow$) it follows that
$\rho,n\models_{\mathcal{K}}\chi_{n}$. If $i<n$, we assume by the induction
hypothesis that $\rho,i{+}1\models_{\mathcal{K}}\chi_{i{+}1}$. We have
$(\text{\textgravedbl}\\!{\chi_{i{+}1}}\\!\text{\textacutedbl},\varsigma_{i})\in\delta(\text{\textgravedbl}\\!{\chi_{i}}\\!\text{\textacutedbl})$,
so $\rho,i\models_{\mathcal{K}}\chi_{i}$ follows again from Lem. 8
($\Longrightarrow$), which concludes the induction step. Finally, the claim
follows for the case $i\,{=}\,0$ because $\chi_{0}=\psi$.

($\Longleftarrow$) Let $\rho$ be of the form (2). We show that for all $i$,
$0\leq i\leq n$, and every formula $\chi$, if
$\rho,i\models_{\mathcal{K}}\chi$ then there is a word
$w_{i}=\varsigma_{i}\varsigma_{i+1}\cdots\varsigma_{n}$ of length $n-i+1$ such
that
$\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}\in\delta^{*}(\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl},w_{i})$,
and $\varsigma_{j}$ is $\lambda$-consistent with step $j$ of $\rho$ for all
$j$, $i\leq j\leq n$. The proof of is by induction on $n-i$.

In the base case where $i=n$, we assume that
$\rho,n\models_{\mathcal{K}}\chi$. By Lem. 8 ($\Longleftarrow$) there is some
$\varsigma_{n}$ such that
$(\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl},\varsigma_{n})\in\delta(\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl})$,
and $\varsigma_{n}$ is $\lambda$-consistent with step $n$ of $\rho$. For the
induction step, assume $i\,{<}\,n$ and $\rho,i\models_{\mathcal{K}}\chi$. By
Lem. 8 ($\Longleftarrow$) there is some
$(\text{\textgravedbl}\\!{\chi^{\prime}}\\!\text{\textacutedbl},\varsigma_{i})\in\delta(\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl})$
such that $\rho,i{+}1\models_{\mathcal{K}}\chi^{\prime}$, and moreover
$\varsigma_{i}$ is $\lambda$-consistent with $\rho$ at step $i$. By the
induction hypothesis, there is a word
$w_{i+1}=\varsigma_{i+1}\cdots\varsigma_{n}$ such that
$\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}\in\delta^{*}(\text{\textgravedbl}\\!{\chi^{\prime}}\\!\text{\textacutedbl},w_{i+1})$,
and $\varsigma_{j}$ is $\lambda$-consistent with $\rho$ at instant $j$ for all
$j$, $i\,{<}\,j\,{\leq}\,n$. We can define
$w_{i}=\varsigma_{i}\varsigma_{i+1}\cdots\varsigma_{n}$, which satisfies
$\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}\in\delta^{*}(\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl},w_{i})$
and $\varsigma_{j}$ is $\lambda$-consistent with $\rho$ at $j$ for all $j$,
$i\,{\leq}\,j\,{\leq}\,n$, so the induction step works.

By assumption, $\rho,0\models_{\mathcal{K}}\psi$ holds. From the case $i=0$ of
the above statement, we obtain a word $w=w_{0}$ such that
$\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}\in\delta^{*}(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl},w)$
and $w$ is $\lambda$-consistent with all steps of $\rho$, i.e., $w$ is well-
formed and consistent with $\rho$. ∎

We next show some simple properties that will be useful to show correctness of
the automaton without $\lambda$.

###### Lemma 10

Let $\psi\in\smash{\textup{LTL}_{f}^{\mathcal{B}}}$ and
$(\chi,\varsigma)\in\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})$.
(1) If $\lambda\,{\in}\,\varsigma$ and $\neg\lambda\not\in\varsigma$ then
$\chi\,{=}\,\top$ or $\chi=\bot$.  (2) Suppose
$\neg\lambda\,{\in}\,\varsigma$, $\lambda\not\in\varsigma$, and
$\chi\,{=}\,\top$, and $\varsigma$ is consistent with step $i$ of run $\rho$.
Then there is some
$(\top,\varsigma^{\prime})\in\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})$
such that $\neg\lambda\not\in\varsigma^{\prime}$ and $\varsigma^{\prime}$ is
consistent with step $i$ of $\rho$ as well.  (3) If $\chi$ is not $\top$ or
$\bot$ then $\varsigma$ has $\lambda$ or $\neg\lambda$.

###### Proof

All three statements are shown simultaneously by induction on $\psi$.

  * •

If $\psi$ is $\top$, $\bot$, or an atom $K$ then $\chi$ is $\top$ or $\bot$,
so (1) and (3) hold, and $\neg\lambda\not\in\varsigma$, so also (2) is
satisfied.

  * •

If $\psi=\mathsf{X}\,\psi^{\prime}$ then
$\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})=\\{(\text{\textgravedbl}\\!{\psi^{\prime}}\\!\text{\textacutedbl},\\{\neg\lambda\\}),(\text{\textgravedbl}\\!{\bot}\\!\text{\textacutedbl},\\{\lambda\\})\\}$.
(1) is satisfied by
$(\text{\textgravedbl}\\!{\bot}\\!\text{\textacutedbl},\\{\lambda\\})$, (2)
holds because $\psi^{\prime}$ cannot be $\top$ since $\top$ does not occur in
$\smash{\textup{LTL}_{f}^{\mathcal{B}}}$, and (3) is satisfied anyway.

  * •

If $\psi=\mathsf{Y}\,\psi^{\prime}$ then
$\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})=\\{(\text{\textgravedbl}\\!{\psi^{\prime}}\\!\text{\textacutedbl},\\{\neg\lambda\\}),(\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl},\\{\lambda\\})\\}$.
(1) is satisfied by
$(\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl},\\{\lambda\\})$, (2)
holds because $\psi^{\prime}$ cannot be $\top$ since $\top$ does not occur in
$\smash{\textup{LTL}_{f}^{\mathcal{B}}}$, and (3) is satisfied anyway.

  * •

If $\psi=\psi_{1}\vee\psi_{2}$ then we must have $\chi=\chi_{1}\vee\chi_{2}$
such that
$(\chi_{i},\varsigma_{i})\in\delta(\text{\textgravedbl}\\!{\psi_{i}}\\!\text{\textacutedbl})$
for both $i\in\\{1,2\\}$, and $\varsigma=\varsigma_{1}\cup\varsigma_{2}$.

(1) Suppose $\lambda\,{\in}\,\varsigma$ and $\neg\lambda\not\in\varsigma$.
First, assume $\lambda\in\varsigma_{1}$, $\neg\lambda\not\in\varsigma_{1}$,
and $\neg\lambda\not\in\varsigma_{2}$. By the induction hypothesis (1),
$\chi_{1}$ is either $\top$ or $\bot$. In the former case, $\chi=\top$, so the
claim holds. Otherwise, $\chi=\chi_{2}$. Then, if $\lambda\in\varsigma_{2}$ we
can again use the induction hypothesis to conclude that $\chi=\chi_{2}$ is
$\top$ or $\bot$. Otherwise, we have $\lambda\not\in\varsigma_{2}$ and
$\neg\lambda\not\in\varsigma_{2}$, so $\chi_{2}$ must be $\top$ or $\bot$ by
the induction hypothesis (3).

(2) Suppose $\neg\lambda\,{\in}\,\varsigma$, $\lambda\not\in\varsigma$, and
$\chi=\top$, and $\varsigma$ is consistent with step $i$ of $\rho$. W.l.o.g.,
we can assume $\neg\lambda\in\varsigma_{1}$, $\lambda\not\in\varsigma_{1}$,
$\lambda\not\in\varsigma_{2}$, and $\chi_{1}=\top$. By the induction
hypothesis (2) applied to $\chi_{1}$, there is some
$(\top,\varsigma_{1}^{\prime})\in\delta(\text{\textgravedbl}\\!{\psi_{1}}\\!\text{\textacutedbl})$
such that $\neg\lambda\not\in\varsigma_{1}^{\prime}$ and
$\varsigma_{1}^{\prime}$ is consistent with step $i$ of $\rho$. By Lem. 7,
there is some
$(\chi_{2}^{\prime},\varsigma_{2}^{\prime})\in\delta(\text{\textgravedbl}\\!{\psi_{2}}\\!\text{\textacutedbl})$
such that $\varsigma_{2}^{\prime}$ is consistent with step $i$ of $\rho$, and
such that $\neg\lambda\not\in\varsigma_{2}^{\prime}$. Thus
$(\top,\varsigma^{\prime})\in\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})$
with $\varsigma^{\prime}=\varsigma_{1}^{\prime}\cup\varsigma_{2}^{\prime}$
satisfies the claim.

(3) If $\chi$ is not $\top$ or $\bot$ then at least one of $\chi_{1}$ or
$\chi_{2}$ is not $\top$ or $\bot$, so by the induction hypothesis (3),
$\varsigma_{1}$ or $\varsigma_{2}$ contains $\lambda$ or $\neg\lambda$, hence
so does $\varsigma$.

  * •

If $\psi=\psi_{1}\wedge\psi_{2}$ then we must have
$\chi=\chi_{1}\wedge\chi_{2}$ such that
$(\chi_{i},\varsigma_{i})\in\delta(\text{\textgravedbl}\\!{\psi_{i}}\\!\text{\textacutedbl})$
for both $i\in\\{1,2\\}$.

(1) Suppose $\lambda\in\varsigma$ and $\neg\lambda\not\in\varsigma$. W.l.o.g.,
we can assume $\lambda\in\varsigma_{1}$, $\neg\lambda\not\in\varsigma_{1}$,
and $\neg\lambda\not\in\varsigma_{2}$. By the induction hypothesis (1),
$\chi_{1}$ is either $\top$ or $\bot$. In the latter case, $\chi=\bot$, so the
claim holds. Otherwise, $\chi=\chi_{2}$, and as by assumption
$\neg\lambda\not\in\varsigma_{2}$, by the induction hypothesis (3), $\chi_{2}$
must be $\top$ or $\bot$.

(2) Suppose $\neg\lambda\in\varsigma$, $\lambda\not\in\varsigma$, and
$\chi=\top$, and $\varsigma$ is consistent with step $i$ of $\rho$. We can
assume $\lambda\not\in\varsigma_{1}$, $\lambda\not\in\varsigma_{2}$ and
$\chi_{1}=\chi_{2}=\top$. We must have $\lambda\in\varsigma_{1}$,
$\lambda\in\varsigma_{2}$, or both. However, for each $i\in\\{1,2\\}$ such
that $\lambda\in\varsigma_{i}$, by the induction hypothesis (2) there is some
$(\top,\varsigma_{i}^{\prime})\in\delta(\text{\textgravedbl}\\!{\psi_{i}}\\!\text{\textacutedbl})$
such that $\lambda\not\in\varsigma_{i}^{\prime}$ and $\varsigma_{i}^{\prime}$
is consistent with step $i$ of $\rho$. If $\lambda\not\in\varsigma_{i}$, set
$\varsigma_{i}^{\prime}=\varsigma_{i}$. Hence
$(\top,\varsigma_{1}^{\prime}\cup\varsigma_{2}^{\prime})\in\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})$
such that $\varsigma_{1}^{\prime}\cup\varsigma_{2}^{\prime}$ is consistent
with step $i$ of $\rho$ and
$\neg\lambda\not\in\varsigma_{1}^{\prime}\cup\varsigma_{2}^{\prime}$.

(3) If $\chi$ is not $\top$ or $\bot$ then at least one of $\chi_{1}$ or
$\chi_{2}$ is not $\top$ or $\bot$, so by the induction hypothesis (3),
$\varsigma_{1}$ or $\varsigma_{2}$ contains $\lambda$ or $\neg\lambda$, hence
so does $\varsigma$.

  * •

For $\psi=\mathsf{G}\,\psi^{\prime}$, note that
$\delta_{\lambda}=\\{(\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl},\\{\lambda\\}),(\text{\textgravedbl}\\!{\bot}\\!\text{\textacutedbl},\\{\neg\lambda\\})\\}$
satisfies the properties. The result then follows from the cases for $\vee$
and $\wedge$.

  * •

All other cases follow from the cases for $\vee$ and $\wedge$. ∎

###### Lemma 2

${\mathcal{N}}_{\psi}$ accepts a word that is consistent with a run $\rho$ iff
$\rho,0\models_{\mathcal{K}}\psi$.

###### Proof

($\Longrightarrow$) Let $w=\varsigma_{0}\varsigma_{1}\cdots\varsigma_{n}$ be
accepted, and
$q_{0}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\varsigma_{0}}$}}q_{1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\varsigma_{1}}$}}\dots\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\varsigma_{n}}$}}q_{n+1}$
be the respective accepting run of ${\mathcal{N}}_{\psi}$. By Def. 12, there
are $\varsigma_{i}^{\prime}$, such that
$\varsigma_{i}=\varsigma_{i}^{\prime}\setminus\\{\lambda,\neg\lambda\\}$ and
$\\{\lambda,\neg\lambda\\}\not\subseteq\varsigma_{i}^{\prime}$ for all $i$,
$0\leq i\leq n$. Let $w^{\prime}$ be the word
$w^{\prime}=\varsigma_{0}^{\prime}\varsigma_{1}^{\prime}\cdots\varsigma_{n}^{\prime}$.
Then $w^{\prime}$ is consistent with $\rho$ because so is $w$. Moreover, by
Lem. 10 (2) we can choose $\varsigma_{n}^{\prime}$ such that
$\neg\lambda\not\in\varsigma_{n}^{\prime}$, and $\varsigma_{n}^{\prime}$ is
consistent with $\rho$ at $n$. Then $w^{\prime}$ is well-formed: indeed, since
edges to $\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}$ labeled
$\lambda$ are redirected to $q_{e}$ and
$\text{\textgravedbl}\\!{\bot}\\!\text{\textacutedbl}$ cannot occur in the
accepting sequence, by Lem. 10 (1) we have
$\lambda\not\in\varsigma_{i}^{\prime}$ for $i<n$. Thus by Def. 12 we have
$\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}\in\delta^{*}(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl},w^{\prime})$.
According to Lem. 9, $\rho\models_{\mathcal{K}}\psi$.

($\Longleftarrow$) If $\rho\models_{\mathcal{K}}\psi$ then by Lem. 9 there is
a well-formed word $w=\varsigma_{0}\varsigma_{1}\cdots\varsigma_{n}$ that is
consistent with $\rho$ such that
$\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}\in\delta^{*}(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl},w)$.
As $w$ is well-formed, no $\varsigma_{i}$ has both $\lambda$ and
$\neg\lambda$. Hence all $\delta$-steps are reflected by transitions in
${\mathcal{N}}_{\psi}$. As
$\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl}$ is the initial state,
by Def. 12, there is an accepting run in ${\mathcal{N}}_{\psi}$ to
$\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}$ or $q_{e}$. ∎