15112 LABEL:LastPageNov. 29, 2017Feb. 13, 2019

††Extended version of results presented at POPL 2013 [19].

# Efficient reduction of nondeterministic automata
with application to language inclusion testing

Lorenzo Clementea  aUniversity of Warsaw, Faculty of Mathematics, Informatics
and Mechanics, Banacha 2, 02-097 Warszawa, Poland  and  Richard Mayrb
bUniversity of Edinburgh, School of Informatics, LFCS, 10 Crichton Street,
Edinburgh EH89AB, UK

###### Abstract.

We present efficient algorithms to reduce the size of nondeterministic Büchi
word automata (NBA) and nondeterministic finite word automata (NFA), while
retaining their languages. Additionally, we describe methods to solve PSPACE-
complete automata problems like language universality, equivalence, and
inclusion for much larger instances than was previously possible ($\geq 1000$
states instead of 10-100). This can be used to scale up applications of
automata in formal verification tools and decision procedures for logical
theories.

The algorithms are based on new techniques for removing transitions (pruning)
and adding transitions (saturation), as well as extensions of classic
quotienting of the state space. These techniques use criteria based on
combinations of backward and forward trace inclusions and simulation
relations. Since trace inclusion relations are themselves PSPACE-complete, we
introduce _lookahead simulations_ as good polynomial time computable
approximations thereof.

Extensive experiments show that the average-case time complexity of our
algorithms scales slightly above quadratically. (The space complexity is
worst-case quadratic.) The size reduction of the automata depends very much on
the class of instances, but our algorithm consistently reduces the size far
more than all previous techniques. We tested our algorithms on NBA derived
from LTL-formulae, NBA derived from mutual exclusion protocols and many
classes of random NBA and NFA, and compared their performance to the well-
known automata tool GOAL [68].

###### Key words and phrases:

Automata reduction; Inclusion testing; Simulation

###### 1991 Mathematics Subject Classification:

F.1.1; D.2.4

##  1\. Introduction

Nondeterministic Büchi automata (NBA) are a fundamental data structure to
represent and manipulate $\omega$-regular languages [67]. They appear in many
automata-based formal software verification methods, as well as in decision
procedures for logical theories. For example, in LTL software model checking
[40, 25], temporal logic specifications are converted into NBA. In other
cases, different versions of a program (obtained by abstraction or refinement
of the original) are translated into automata whose languages are then
compared. Testing the conformance of an implementation with its requirements
specification thus reduces to a language inclusion problem. Another
application of NBA in software engineering is program termination analysis by
the size-change termination method [51, 28]. Via an abstraction of the effect
of program operations on data, the termination problem can often be reduced to
a language inclusion problem between two derived NBA.

Our goal is to improve the efficiency and scalability of automata-based formal
software verification methods. Our contribution is threefold: We describe a
very effective _automata reduction_ algorithm, which is based on novel,
efficiently computable _lookahead simulations_ , and we conduct an extensive
_experimental evaluation_ of our reduction algorithm.

This paper is partly based on results presented at POPL’13 [19], but contains
several large parts that have not appeared previously. While [19] only
considered nondeterministic Büchi automata (NBA), we additionally present
corresponding results on nondeterministic finite automata (NFA). We also
present more extensive empirical results for both NBA and NFA (cf. Sec. 9).
Moreover, we added a section on the new saturation technique (cf. Sec. 10).
Finally, we added some notes on the implementation (cf. Sec. 11).

###  1.1. Automata reduction.

We propose a novel, efficient, practical, and very effective algorithm to
reduce the size of automata, in terms of both states and transitions. It is
well-known that, in general, there are several non-isomorphic nondeterministic
automata of minimal size recognizing a given language, and even testing the
minimality of the number of states of a given automaton is PSPACE-complete
[45]. Instead, our algorithm produces a smaller automaton recognizing the same
language, though not necessarily one with the absolute minimal possible number
of states, thus avoiding the complexity bottleneck. The reason to perform
reduction is that smaller automata are in general more efficient to handle in
a subsequent computation. Thus, there is an algorithmic tradeoff between the
effort for the reduction and the complexity of the problem later considered
for this automaton. If only computationally easy algorithmic problems are
considered, like reachability or emptiness (which are solvable in NLOGSPACE),
then extensive reduction does not pay off since in these cases it is faster to
solve the initial problem directly. Instead, the main applications are the
following.

  1. (1)

PSPACE-complete automata problems like language universality, equivalence, and
inclusion [49]. Since exact algorithms are exponential for these problems, one
should first reduce the automata as much as possible before applying them.

  2. (2)

LTL model checking [40], where one searches for loops in a graph that is the
product of a large system specification with an NBA derived from an LTL-
formula. Smaller automata often make this easier, though in practice it also
depends on the degree of nondeterminism [63]. Our reduction algorithm, based
on transition pruning techniques, yields automata that are not only smaller,
but also sparser (fewer transitions per state, on average), and thus contain
less nondeterministic branching.

  3. (3)

Procedures that combine and modify automata repeatedly. Model checking
algorithms and automata-based decision procedures for logical theories (cf.
the TaPAS tool [53]) compute automata products, unions, complements,
projections, etc., and thus the sizes of automata grow rapidly. Another
example is in the use of automata for the reachability analysis of safe Petri
nets [61]. Thus, it is important to intermittently reduce the automata to keep
their size manageable.

Our reduction algorithm combines the following techniques:

  * •

The removal of dead states. These are states that trivially do not contribute
to the language of the automaton, either because they cannot be reached from
any initial state or because no accepting loop in the NBA (resp. no accepting
state in the NFA) is reachable from them.

  * •

Quotienting. Here one finds a suitable equivalence relation on the set of
states and quotients w.r.t. it, i.e., one merges each equivalence class into a
single state.

  * •

_Transition pruning_ (i.e., removing transitions) and _transition saturation_
(i.e., adding transitions), using suitable criteria such that the language of
the automaton is preserved.

The first technique is trivial and the second one is well-understood [26, 16].
Here, we investigate thoroughly transition pruning and transition saturation.

For pruning, the idea is that certain transitions can be removed, because
other ‘better’ transitions remain. The ‘better’ criterion compares the source
and target states of transitions w.r.t. certain semantic preorders, e.g.,
forward and backward simulations and trace inclusions. We provide a complete
picture of which combinations of relations are correct to use for pruning.
Pruning transitions reduces not only the number of transitions, but also,
indirectly, the number of states. By removing transitions, some states may
become dead, and can thus be removed from the automaton without changing its
language. The reduced automata are generally much sparser than the originals
(i.e., use fewer transitions per state and less nondeterministic branching),
which yields additional performance advantages in subsequent computations.

Dually, for saturation, the idea is that certain transitions can be added,
because other ‘better’ transitions are already present. Again, the ‘better’
criterion relies on comparing the source/target states of the transitions
w.r.t. semantic preorders like forward and backward simulations and trace
inclusions. We provide a complete picture of which combinations of relations
are correct to use for saturation. Adding transitions does not change the
number of states, but it may pave the way for further quotienting that does.
Moreover, adding some transitions might allow the subsequent pruning of other
transitions, and the final result might even have fewer transitions than
before. It often happens, however, that there is a tradeoff between the
numbers of states and transitions.

$p_{0}$$p_{1}$$p_{2}$$\cdots$$p_{n}$$p$$a,b$$a$$a,b$$a,b$$a,b$$\$$$\$$ Figure
1. Family of NBA accepting languages
$L_{n}=\\{a,b\\}^{*}a\\{a,b\\}^{n-1}\$^{\omega}$ for which the minimal WDBA
has size $\Omega(2^{n})$.

Finally, it is worth mentioning that the minimization problem can sometimes be
solved efficiently if one considers minimization _within_ a restricted class
of languages. For instance, for the class of _weak deterministic Büchi
languages_ (a strict subclass of the $\omega$-regular languages) it is well-
known that given a weak deterministic Büchi automaton (WDBA) one can find in
time $O(n\log n)$ a minimal equivalent automaton in the same class [54]
(essentially by applying Hopcroft’s DFA minimization algorithm [41]). However,
it is possible that a weak deterministic language admits only large WDBA, but
succinct NBA; cf. Fig. 1 (this is similar to what happens for DFA vs. NFA over
finite words). Thus, minimizing a WDBA in the class of WDBA and minimizing a
WDBA in the larger class of NBA are two distinct problems. Since in this paper
we consider size reduction of NBA (and thus WDBA) in the larger class of all
NBA, our method and the one of [54] are incomparable.

###  1.2. Lookahead simulations

Simulation preorders play a central role in automata reduction via pruning,
saturation and quotienting, because they provide PTIME-computable under-
approximations of the PSPACE-hard trace inclusions. However, the quality of
the approximation is insufficient in many practical examples. Multipebble
simulations [24] yield better under-approximations of trace inclusions; while
theoretically they can be computed in PTIME for a fixed number of pebbles, in
practice they are not easily computed.

We introduce _lookahead simulations_ as an efficient and practical method to
compute good under-approximations of trace inclusions and multipebble
simulations. For a fixed lookahead, lookahead simulations are computable in
PTIME, and it is correct to use them instead of the more expensive trace
inclusions and multipebble simulations. Lookahead itself is a classic concept,
which has been used in parsing and many other areas of computer science, like
in the uniformization problem of regular relations [42], in the composition of
e-services (under the name of lookahead delegators [34, 62, 13, 55]), and in
infinite games [39, 30, 47, 48]. However, lookahead can be defined in many
different variants. Our contribution is to identify and formally describe the
lookahead-variant for simulation preorders that gives the optimal compromise
between efficient computability and maximizing the sizes of the relations; cf.
Sec. 6. From a practical point of view, we use degrees of lookahead ranging
from 4 to 25 steps, depending on the size and shape of the automata. Our
experiments show that even a moderate lookahead often yields much larger
approximations of trace-inclusions and multipebble simulations than normal
simulation preorder. Notions very similar to the ones we introduce are
discussed in [43] under the name of _multi-letter simulations_ and _buffered
simulations_ [44]; cf. Remark 6.6 for a comparison of multi-letter and
buffered simulations w.r.t. lookahead simulations.

###  1.3. Experimental results

We performed an extensive experimental evaluation of our techniques based on
lookahead simulations on tasks of automata reduction and language
universality/inclusion testing. (The raw data of the experiments is stored
together with the arXiv version of this paper [20].)

#### Automata reduction.

We applied our reduction algorithm on automata of up-to $20000$ states. These
included 1) random automata according to the Tabakov-Vardi model [66], 2)
automata obtained from LTL formulae, and 3) real-world mutual exclusion
protocols. The empirically determined average-case time complexity on random
automata is slightly above quadratic, while the (never observed) worst-case
complexity is $O(n^{4})$. The worst-case space complexity is quadratic. Our
algorithm reduces the size of automata much more strongly, on average, than
previously available practical methods as implemented in the popular GOAL
automata tool [68]. However, the exact advantage varies, depending on the type
of instances; cf. Sec. 9. For example, consider random automata with 100–1000
states, binary alphabet and varying transition density ${\it td}$. Random
automata with ${\it td}=1.4$ cannot be reduced much by any method. The only
substantial effect is achieved by the trivial removal of dead states which, on
average, yields automata of $78\%$ of the original size. On the other hand,
for ${\it td}=1.8,\dots,2.2$, the best previous reduction methods yielded
automata of $85\%$–$90\%$ of the original size on average, while our algorithm
yielded automata of $3\%$–$15\%$ of the original size on average.

#### Language universality/inclusion.

Language universality and inclusion of NBA/NFA are PSPACE-complete problems
[49], but many practically efficient methods have been developed [22, 23, 60,
4, 28, 29, 2, 3]. Still, these all have exponential worst-case time complexity
and do not scale well. Typically they are applied to automata with 15–100
states (unless the automaton has a particularly simple structure), and
therefore one should first reduce the automata before applying these exact
exponential-time methods.

Even better, already the polynomial time reduction algorithm alone can solve
many instances of the PSPACE-complete universality, equivalence, and inclusion
problems. E.g., an automaton might be reduced to the trivial universal
automaton, thus witnessing language universality, or when one checks inclusion
of two automata, it may compute a small (polynomial size) certificate for
language inclusion in the form of a (lookahead-)simulation. Thus, the complete
exponential time methods above need only be invoked in a minority of the
cases, and on much smaller instances. This allows to scale language inclusion
testing to much larger instances (e.g., automata with $\geq 1000$ states)
which are beyond previous methods.

###  1.4. Nondeterministic finite automata.

We present our methods mostly in the framework of nondeterministic Büchi
automata (NBA), but they directly carry over to the simpler case of
nondeterministic finite-word automata (NFA). The main differences are the
following:

  * •

Since NFA accept finite words, it matters in exactly which step an accepting
state is reached (unlike for NBA where the acceptance criterion is to visit
accepting states infinitely often). Therefore, lookahead-simulations for NFA
need to treat accepting states in a way which is more restrictive than for
NBA. Thus, in NFA, one is limited to a smaller range of semantic
preorders/equivalences, namely direct and backward simulations (and the
corresponding multipebble simulations, lookahead simulations and trace
inclusions), while more relaxed notions (like delayed and fair simulations)
can be used for NBA.

  * •

On the other hand, unlike NBA, an NFA can always be transformed into an
equivalent NFA with just one accepting state without any outgoing transitions
(unless the language contains the empty word). This special form makes it much
easier to compute good approximations of direct and backward trace inclusion,
which greatly helps in the NFA reduction algorithm.

relations on NBA | complexity | quotienting | inclusion |  pruning$\mbox{}^{(1)}$
---|---|---|---|---
direct simulation $\sqsubseteq^{\mathsf{di}}$ | PTIME | $\checkmark$ | [65, 25] | $\checkmark$ | [22] | $\checkmark$ |  [14], Thm. 5.6
delayed simulation $\sqsubseteq^{\mathsf{de}}$ | PTIME | $\checkmark$ | [26] | $\checkmark$ | [26] | $\times$ |  Fig. 5(a)
fair simulation $\sqsubseteq^{\mathsf{f}}$ | PTIME | $\times$ | [26] | $\checkmark$ | [37] | $\times$ |  Fig. 5(a)
backward direct sim. $\sqsubseteq^{\mathsf{bw\textrm{-}di}}$ | PTIME | $\checkmark$ | [65] | $\checkmark$ |  Thm. 4.3 | $\checkmark$ |  Thm. 5.5
direct trace inclusion $\subseteq^{\mathsf{di}}$ | PSPACE | $\checkmark$ | [24] | $\checkmark$ | obvious | $\checkmark$ |  Thm. 5.3, 5.5
delayed trace inclusion $\subseteq^{\mathsf{de}}$ | PSPACE | $\times$ |  Fig. 2 [16] | $\checkmark$ | obvious | $\times$ |  cf. Thm. 5.7
fair trace inclusion $\subseteq^{\mathsf{f}}$ | PSPACE | $\times$ |  Fig. 2 [16] | $\checkmark$ | obvious | $\times$ |  cf. Thm. 5.7
direct fixed-word sim. $\sqsubseteq^{\mathsf{fx\textrm{-}di}}$ | PSPACE | $\checkmark$ |  Lem. 3.4[16] | $\checkmark$ | obvious | $\checkmark$ |  by $\subseteq^{\mathsf{di}}$
delayed fixed-word sim. $\sqsubseteq^{\mathsf{fx\textrm{-}de}}$ | PSPACE | $\checkmark$ |  Lem. 3.4[16] | $\checkmark$ | obvious | $\times$ | by delayed sim.
fair fixed-word sim. $\sqsubseteq^{\mathsf{fx\textrm{-}f}}$ | PSPACE | $\times$ |  by $\subseteq^{\mathsf{f}}$ | $\checkmark$ | obvious | $\times$ | by delayed sim.
bwd. direct trace incl. $\subseteq^{\mathsf{bw\textrm{-}di}}$ | PSPACE | $\checkmark$ |  Thm. 3.3 | $\checkmark$ |  Thm. 4.3 | $\checkmark$ |  Thm. 5.4, 5.6
direct lookahead sim. $\preceq^{k\textrm{-}\mathsf{di}}$ |  PTIME$\mbox{}^{(2)}$ | $\checkmark$ |  Lemma 6.3 | $\checkmark$ |  Lemma 6.3 | $\checkmark$ |  Sec. 7.1
delayed lookahead sim. $\preceq^{k\textrm{-}\mathsf{de}}$ |  PTIME$\mbox{}^{(2)}$ | $\checkmark$ |  Lemma 6.3 | $\checkmark$ |  Lemma 6.3 | $\checkmark$ |  Sec. 7.1
fair lookahead sim. $\preceq^{k\textrm{-}\mathsf{f}}$ |  PTIME$\mbox{}^{(2)}$ | $\times$ | by fair sim. | $\checkmark$ |  Lemma 6.3 | $\times$ |  Sec. 7.1
bwd. di. lookahead sim. $\preceq^{k\textrm{-}\mathsf{bw\textrm{-}di}}$ |  PTIME$\mbox{}^{(2)}$ | $\checkmark$ |  by $\subseteq^{\mathsf{bw\textrm{-}di}}$ | $\checkmark$ |  by $\subseteq^{\mathsf{bw\textrm{-}di}}$ | $\checkmark$ |  by $\subseteq^{\mathsf{bw\textrm{-}di}}$
relations on NFA |  |  |  |  |  |  |
forward direct sim. $\sqsubseteq^{\mathsf{di}}$ | PTIME | $\checkmark$ |  Thm. 3.4 | $\checkmark$ |  Thm. 4.4 | $\checkmark$ |  Thm. 5.10, 5.11
bwd. finite-word sim. $\sqsubseteq^{\mathsf{bw}}$ | PTIME | $\checkmark$ |  Thm. 3.4 | $\checkmark$ |  Thm. 4.4 | $\checkmark$ |  Thm. 5.10, 5.11
fwd. finite trace incl. $\subseteq^{\mathsf{fw}}$ | PSPACE | $\checkmark$ |  Thm. 3.4 | $\checkmark$ |  Thm. 4.4 | $\checkmark$ |  Thm. 5.8–5.11
bwd. finite trace incl. $\subseteq^{\mathsf{bw}}$ | PSPACE | $\checkmark$ |  Thm. 3.4 | $\checkmark$ |  Thm. 4.4 | $\checkmark$ |  Thm. 5.8–5.11
fwd. di. lookahead sim. $\preceq^{k\textrm{-}\mathsf{di}}$ |  PTIME$\mbox{}^{(2)}$ | $\checkmark$ |  Sec. 7.2 | $\checkmark$ |  Sec. 7.2 | $\checkmark$ |  Sec. 7.2
bwd. lookahead sim. $\preceq^{k\textrm{-}\mathsf{bw}}$ |  PTIME$\mbox{}^{(2)}$ | $\checkmark$ |  Sec. 7.2 | $\checkmark$ |  Sec. 7.2 | $\checkmark$ |  Sec. 7.2
Table 1.  Summary of old and new results for simulation-like relations on NBA
and NFA. $(1)$ For pruning, cf. also Table 2 in Sec. 5.1 for NBA, and Sec. 5.2
for NFA. $(2)$ PTIME for fixed lookahead.

### Outline of the paper.

A summary of old and new results about simulation-like preorders as used in
inclusion checking, quotienting, and pruning transitions can be found in Table
1.

The rest of the paper is organized as follows. In Sec. 2, we define basic
notation for automata and languages. Sec. 3 introduces basic semantic
preorders and equivalences between states of automata and considers
quotienting methods, while Sec. 4 shows which preorders witness language
inclusion. In Sec. 5, we present the main results on transition pruning.
Lookahead simulations are introduced in Sec. 6 and used in the algorithms for
automata reduction and language inclusion testing in Sections 7 and 8,
respectively. These algorithms are empirically evaluated in Sec. 9. In Sec. 10
we describe and evaluate an extended reduction algorithm that additionally
uses transition saturation methods. Sec. 11 describes some algorithmic
optimizations in the implementation, and Sec. 12 contains a summary and
directions for future work.

##  2\. Preliminaries

A _preorder_ $R$ is a reflexive and transitive relation, a _partial order_ is
a preorder which is antisymmetric ($xRy\wedge yRx\Rightarrow x=y$), and a
_strict partial order_ is an irreflexive ($\neg xRx$), asymmetric
($xRy\Rightarrow\neg yRx$), and transitive relation. We often denote preorders
by $\sqsubseteq$, and when we do so, with $\sqsubset$ we denote its strict
version, i.e., $x\sqsubset y$ if $x\sqsubseteq y$ and $y\not\sqsubseteq x$; we
follow a similar convention for $\subseteq$.

A _nondeterministic Büchi automaton (NBA)_ $\mathcal{A}$ is a tuple
$(\Sigma,Q,I,F,\delta)$ where $\Sigma$ is a finite alphabet, $Q$ is a finite
set of states, $I\subseteq Q$ is the set of _initial_ states, $F\subseteq Q$
is the set of _accepting_ states, and $\delta\subseteq Q\times\Sigma\times Q$
is the transition relation. We write
$p\stackrel{{\scriptstyle\sigma}}{{\longrightarrow}}q$ for
$(p,\sigma,q)\in\delta$. A state of a Büchi automaton is _dead_ if either it
is not reachable from any initial state, or it cannot reach any accepting loop
(i.e., a loop that contains at least one accepting state). In our
simplification techniques, we always remove dead states, since this does not
affect the language of the automaton. To simplify the presentation, we assume
that automata are _forward and backward complete_ , i.e., for any state $p\in
Q$ and symbol $\sigma\in\Sigma$, there exist states $q_{0},q_{1}\in Q$ s.t.
$q_{0}\stackrel{{\scriptstyle\sigma}}{{\longrightarrow}}p\stackrel{{\scriptstyle\sigma}}{{\longrightarrow}}q_{1}$.
Every automaton can be converted into an equivalent complete one by adding at
most two states and at most $2\cdot(|Q|+2)\cdot|\Sigma|$ transitions.111 For
efficiency reasons, our implementation works directly on incomplete automata.
Completeness is only assumed to simplify the technical development. A Büchi
automaton $\mathcal{A}$ describes a set of infinite words (its language),
i.e., a subset of $\Sigma^{\omega}$. An _infinite trace_ of $\mathcal{A}$ on
an infinite word $w=\sigma_{0}\sigma_{1}\cdots\in\Sigma^{\omega}$ (or _$w$
-trace_) _starting_ in a state $q_{0}\in Q$ is an infinite sequence of
transitions
$\pi=q_{0}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$.
Similarly, a _finite trace_ on a finite word
$w=\sigma_{0}\sigma_{1}\cdots\sigma_{m-1}\in\Sigma^{*}$ (or _$w$ -trace_)
starting in a state $q_{0}\in Q$ and _ending_ in a state $q_{m}\in Q$ is a
finite sequence of transitions
$\pi=q_{0}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle\sigma_{m-1}}}{{\longrightarrow}}q_{m}$.
By convention, a finite trace over the empty word $\varepsilon$ is just a
single state $\pi=q$ (where the trace both starts and ends). For an infinite
trace $\pi$ and index $i\geq 0$, we denote by $\pi i$ the finite prefix trace
$\pi
i=q_{0}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle\sigma_{i-1}}}{{\longrightarrow}}q_{i}$,
and by $\pi i$ the infinite suffix trace $\pi
i=q_{i}\stackrel{{\scriptstyle\sigma_{i}}}{{\longrightarrow}}q_{i+1}\stackrel{{\scriptstyle\sigma_{i+1}}}{{\longrightarrow}}\cdots$.
A finite or infinite trace is _initial_ if it starts in an initial state
$q_{0}\in I$, and a finite trace is _final_ if it ends in an accepting state
$q_{m}\in F$. A trace is _fair_ if it is infinite and $q_{i}\in F$ for
infinitely many $i$’s. A transition is _transient_ if it appears at most once
in any trace of the automaton. The _language of an NBA $\mathcal{A}$_ is
$\mathcal{L}(\mathcal{A})=\\{w\in\Sigma^{\omega}\mid\mbox{$\mathcal{A}$ has an
initial and fair trace on $w$}\\}$.

A _nondeterministic finite automaton (NFA)_
$\mathcal{A}=(\Sigma,Q,I,F,\delta)$ has the same syntax as an NBA, and all
definitions from the previous paragraph carry over to NFA. (Sometimes,
accepting states in NBA are called _final_ in the context of NFA.) However,
since NFA recognize languages of finite words, their semantics is different.
The language of an NFA $\mathcal{A}$ is thus defined as
$\mathcal{L}(\mathcal{A})=\\{w\in\Sigma^{*}\mid\mbox{$\mathcal{A}$ has an
initial and final trace on $w$}\\}$.

When the distinction between NBA and NFA is not important, we just call
$\mathcal{A}$ an automaton. Given two automata $\mathcal{A}$ and $\mathcal{B}$
we write $\mathcal{A}\subseteq\mathcal{B}$ if
$\mathcal{L}(\mathcal{A})\subseteq\mathcal{L}(\mathcal{B})$ and
$\mathcal{A}\approx\mathcal{B}$ if
$\mathcal{L}(\mathcal{A})=\mathcal{L}(\mathcal{B})$.

##  3\. Quotienting reduction techniques

An interesting problem is how to simplify an automaton while preserving its
semantics, i.e., its language. Generally, one tries to reduce the number of
states/transitions. This is useful because the complexity of decision
procedures usually depends on the size of the input automata. A classical
operation for reducing the number of states of an automaton is that of
quotienting, where states of the automaton are identified according to a given
equivalence, and transitions are projected accordingly. Since in practice we
obtain quotienting equivalences from suitable preorders, we directly define
quotienting w.r.t. a preorder. In the rest of the section, fix an automaton
$\mathcal{A}=(\Sigma,Q,I,F,\delta)$, and let $\sqsubseteq$ be a preorder on
$Q$, with induced equivalence
$\approx\;\coloneqq\;(\sqsubseteq\cap\sqsupseteq)$. Given a state $q\in Q$, we
denote by $[q]$ its equivalence class w.r.t. $\approx$ (which is left implicit
for simplicity), and, for a set of states $P\subseteq Q$, $[P]$ is the set of
equivalence classes $[P]=\\{[p]\;|\;p\in P\\}$.

######  Definition 3.1.

The _quotient_ of $\mathcal{A}$ by $\sqsubseteq$ is
$\mathcal{A}/\\!\sqsubseteq=(\Sigma,[Q],[I],[F],\delta^{\prime})$, where
transitions are induced element-wise as
$\delta^{\prime}=\\{([q_{1}],\sigma,[q_{2}])\;|\;\exists
q_{1}^{\prime}\in[q_{1}],q_{2}^{\prime}\in[q_{2}]\cdot(q_{1}^{\prime},\sigma,q_{2}^{\prime})\in\delta\\}$.

Clearly, every trace
$q_{0}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$
in $\mathcal{A}$ immediately induces a corresponding trace
$[q_{0}]\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}[q_{1}]\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$
in $\mathcal{A}/\\!\sqsubseteq$, which is fair/initial/final if the former is
fair/initial/final, respectively. Consequently,
$\mathcal{A}\;\subseteq\;(\mathcal{A}/\\!\sqsubseteq)$ for _any_ preorder
$\sqsubseteq$. If, additionally,
$(\mathcal{A}/\\!\sqsubseteq)\;\subseteq\;\mathcal{A}$, then we say that the
preorder $\sqsubseteq$ is _good for quotienting_ (GFQ).

######  Definition 3.2.

A preorder $\sqsubseteq$ is _good for quotienting_ (GFQ) if
$\mathcal{A}\approx\mathcal{A}/\\!\sqsubseteq$.

GFQ preorders are downward closed (since a smaller preorder induces a smaller
equivalence, which quotients ‘less’). We are interested in finding coarse and
efficiently computable GFQ preorders for NBA and NFA. Classical examples are
given by forward simulation relations (Sec. 3.1) and forward trace inclusions
(Sec. 3.3), which are well known GFQ preorders for NBA. A less known GFQ
preorder for NBA is given by their respective backward variants (Sec. 3.5).
For completeness, we also consider suitable simulations and trace inclusions
for NFA (Sec. 3.6). In Sec. 4, the previous preorders are applied to language
inclusion for both NBA and NFA. In Sec. 5, we present novel language-
preserving transition pruning techniques based on simulations and trace
inclusions. While simulations are efficiently computable, e.g., in PTIME,
trace inclusions are PSPACE-complete. In Sec. 6, we present _lookahead
simulations_ , which are novel efficiently computable GFQ relations coarser
than simulations.

###  3.1. Forward simulation relations

Forward simulation [59, 57] is a binary relation on the states of
$\mathcal{A}$; it relates states whose behaviors are step-wise related, which
allows one to reason about the internal structure of automaton
$\mathcal{A}$—i.e., _how_ a word is accepted, and not just _whether_ it is
accepted. Formally, simulation between two states $p_{0}$ and $q_{0}$ can be
described in terms of a game between two players, Spoiler (he) and Duplicator
(she), where the latter wants to prove that $q_{0}$ can step-wise mimic any
behavior of $p_{0}$, and the former wants to disprove it. The game starts in
the initial configuration $(p_{0},q_{0})$. Inductively, given a game
configuration $(p_{i},q_{i})$ at the $i$-th round of the game, Spoiler chooses
a symbol $\sigma_{i}\in\Sigma$ and a transition
${p_{i}}\stackrel{{\scriptstyle\sigma_{i}}}{{\longrightarrow}}{p_{i+1}}$.
Then, Duplicator responds by choosing a matching transition
${q_{i}}\stackrel{{\scriptstyle\sigma_{i}}}{{\longrightarrow}}{q_{i+1}}$, and
the next configuration is $(p_{i+1},q_{i+1})$. Since the automaton is assumed
to be complete, the game goes on forever, and the two players build two
infinite traces
$\pi_{0}=p_{0}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}p_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$
and
$\pi_{1}=q_{0}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$.
The winning condition for Duplicator is a predicate on the two traces
$\pi_{0},\pi_{1}$, and it depends on the type of simulation. For our purposes,
we consider _direct_ [22], _delayed_ [26] and _fair simulation_ [37]. Let
$x\in\\{\mathrm{di,de,f}\\}$. Duplicator wins the play if
$\mathcal{C}^{x}(\pi_{0},\pi_{1})$ holds, where

$\displaystyle\mathcal{C}^{\mathrm{di}}(\pi_{0},\pi_{1})$
$\displaystyle\quad\iff\quad\forall(i\geq 0)\cdot p_{i}\in F\implies q_{i}\in
F$ $\displaystyle\mathcal{C}^{\mathrm{de}}(\pi_{0},\pi_{1})$
$\displaystyle\quad\iff\quad\forall(i\geq 0)\cdot p_{i}\in
F\implies\exists(j\geq i)\cdot q_{j}\in F$
$\displaystyle\mathcal{C}^{\mathrm{f}}(\pi_{0},\pi_{1})$
$\displaystyle\quad\iff\quad\textrm{ if $\pi_{0}$ is fair, then $\pi_{1}$ is
fair }$

Intuitively, direct simulation requires that accepting states are matched
immediately (the strongest condition), while in delayed simulation Duplicator
is allowed to accept only after a finite delay. In fair simulation (the
weakest condition), Duplicator must visit accepting states infinitely often
only if Spoiler does so. Thus, the three conditions are presented in
increasing degree of coarseness. We define $x$-simulation relation
$\sqsubseteq^{x}\subseteq Q\times Q$, for $x\in\\{\mathrm{di,de,f}\\}$, by
stipulating that $p_{0}\sqsubseteq^{x}q_{0}$ holds if Duplicator has a winning
strategy in the $x$-simulation game, starting from configuration
$(p_{0},q_{0})$. Thus,
$\sqsubseteq^{\mathsf{di}}\,\subseteq\,\sqsubseteq^{\mathsf{de}}\,\subseteq\,\sqsubseteq^{\mathsf{f}}$.
Simulation between states in different automata $\mathcal{A}$ and
$\mathcal{B}$ can be computed as a simulation on their disjoint union. [[22,
36, 37, 26]] For $x\in\\{\mathrm{di,de,f}\\}$, $x$-simulation
$\sqsubseteq^{x}$ is a PTIME computable preorder. For
$y\in\\{\mathrm{di,de}\\}$, $\sqsubseteq^{y}$ is GFQ on NBA. Notice that fair
simulation $\sqsubseteq^{\mathsf{f}}$ is not GFQ. A simple counterexample can
be found in [26] (even for fair _bi_ simulation); cf. also the automaton from
Fig. 2, where all states are fair bisimulation equivalent, and thus the
quotient automaton would recognize $\Sigma^{\omega}$. However, the interest in
fair simulation stems from the fact that it is a PTIME computable under-
approximation of fair trace inclusion (introduced in the next Sec. 3.3). Trace
inclusions between certain states can be used to establish language inclusion
between automata, as discussed in Sec. 4; this is a part of our inclusion
testing presented in Sec. 8.

###  3.2. Multipebble simulations

While simulations are efficiently computable, their use is often limited by
their size, which can be much smaller than other GFQ preorders. _Multipebble
simulations_ [24] offer a generalization of simulations where Duplicator is
given several pebbles that she can use to hedge her bets and delay the
resolution of nondeterminism. This increased power of Duplicator yields
coarser GFQ preorders.

[[24]] Multipebble direct and delayed simulations are GFQ preorders on NBA
coarser than direct and delayed simulations, respectively. They are PTIME
computable for a fixed number of pebbles.

However, computing multipebble simulations is PSPACE-hard in general [17], and
in practice it is exponential in the number of pebbles. For this reason, we
study (cf. Sec. 6) lookahead simulations, which are efficiently computable
under-approximations of multipebble simulations, and, more generally, of trace
inclusions, which we introduce next.

###  3.3. Forward trace inclusions

There are other generalizations of simulations (and their multipebble
extensions) that are GFQ. One such example of coarser GFQ preorders is given
by _trace inclusions_ , which are obtained through the following modification
of the simulation game. In a simulation game, the players build two paths
$\pi_{0},\pi_{1}$ by choosing single transitions in an alternating fashion.
That is, Duplicator moves by a single transition by knowing only the next
single transition chosen by Spoiler. We can obtain coarser relations by
allowing Duplicator a certain amount of _lookahead_ on Spoiler’s chosen
transitions. In the extremal case of infinite lookahead, i.e., where Spoiler
has to reveal his entire path in advance, we obtain trace inclusions.
Analogously to simulations, we define direct, delayed, and fair trace
inclusion, as binary relations on $Q$. Formally, for
$x\in\\{\mathrm{di,de,f}\\}$, _$x$ -trace inclusion_ holds between $p$ and
$q$, written $p\subseteq^{x}q$ if, for every word
$w=\sigma_{0}\sigma_{1}\cdots\in\Sigma^{\omega}$, and for every infinite
$w$-trace
$\pi_{0}=p_{0}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}p_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$
starting at $p_{0}=p$, there exists an infinite $w$-trace
$\pi_{1}=q_{0}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$
starting at $q_{0}=q$, s.t. $\mathcal{C}^{x}(\pi_{0},\pi_{1})$ holds. (Recall
the definition of $\mathcal{C}^{x}(\pi_{0},\pi_{1})$ from Sec. 3.1).

Like simulations, trace inclusions are preorders. Clearly, direct trace
inclusion $\subseteq^{\mathsf{di}}$ is a subset of delayed trace inclusion
$\subseteq^{\mathsf{de}}$, which, in turn, is a subset of fair trace inclusion
$\subseteq^{\mathsf{f}}$. Moreover, since Duplicator has more power in the
trace inclusion game than in the corresponding simulation game, trace
inclusions subsume the corresponding simulation (and even the corresponding
multipebble simulation222It turns out that multipebble direct simulation with
the maximal number of pebbles in fact _coincides_ with direct trace inclusion,
while the other inclusions are strict for the delayed and fair variants
[17].). In particular, fair trace inclusion $\subseteq^{\mathsf{f}}$ is not
GFQ, since it subsumes fair simulation $\sqsubseteq^{\mathsf{f}}$ which we
have already observed not to be GFQ in Sec. 3.1.

$p$$q$$r$$s$$a$$a$$a$$a$$a$ |  | $\subseteq^{\mathsf{de}}$ | $p$ | $q$ | $r$ | $s$
---|---|---|---|---
$p$ | $\checkmark$ | $\checkmark$ | $\times$ | $\times$
$q$ | $\checkmark$ | $\checkmark$ | $\times$ | $\times$
$r$ | $\checkmark$ | $\checkmark$ | $\checkmark$ | $\times$
$s$ | $\checkmark$ | $\checkmark$ | $\checkmark$ | $\checkmark$
$[p]$$[r]$$[s]$$a$$a$$a$$a$
The original automaton $\mathcal{A}$ |  Delayed trace inclusion | The quotient automaton $\mathcal{A}/\\!\subseteq^{\mathsf{de}}$
Figure 2. Delayed trace inclusion $\subseteq^{\mathsf{de}}$ is not GFQ.

We further observe that even the finer delayed trace inclusion
$\subseteq^{\mathsf{de}}$ is not GFQ. Consider the automaton $\mathcal{A}$ on
the left in Fig. 2 (taken from [16]). The states $p$ and $q$ are equivalent
w.r.t. delayed trace inclusion (and are the only two equivalent states), and
thus $[p]=[q]$, but merging them induces the quotient automaton
$\mathcal{A}/\\!\subseteq^{\mathsf{de}}$ on the right in the figure, which
accepts the new word $a^{\omega}$ that was not previously accepted.

It thus remains to decide whether direct trace inclusion
$\subseteq^{\mathsf{di}}$ is GFQ. This is the case, since
$\subseteq^{\mathsf{di}}$ in fact coincides with multipebble direct
simulation, which is GFQ by Lemma 3.2.

[[24, 16]] Forward trace inclusions are PSPACE computable preorders. Moreover,
direct trace inclusion $\subseteq^{\mathsf{di}}$ is GFQ for NBA, while delayed
$\subseteq^{\mathsf{de}}$ and fair $\subseteq^{\mathsf{f}}$ trace inclusions
are not.

The fact that direct trace inclusion $\subseteq^{\mathsf{di}}$ is GFQ also
follows from a more general result presented in the next section, where we
consider a different way to give lookahead to Duplicator.

###  3.4. Fixed-word simulations

_Fixed-word simulation_ [16] is a variant of simulation where Duplicator has
infinite lookahead only on the input word $w$, but _not_ on Spoiler’s actual
$w$-trace $\pi_{0}$. Formally, for $x\in\\{\mathrm{di,de,f}\\}$, one considers
the family of preorders indexed by infinite words
${\\{\sqsubseteq^{\mathsf{fx\textrm{-}}x}_{w}\\}_{w\in\Sigma^{\omega}}}$,
where $\sqsubseteq^{\mathsf{fx\textrm{-}}x}_{w}$ for a fixed infinite word $w$
is like $x$-simulation, but Spoiler is forced to play the word $w$. Then,
$x$-fixed-word simulation $\sqsubseteq^{\mathsf{fx\textrm{-}}x}$ is defined by
requiring that Duplicator wins for every infinite word $w$, that is,
$\sqsubseteq^{\mathsf{fx\textrm{-}}x}=\bigcap_{w\in\Sigma^{\omega}}\sqsubseteq^{\mathsf{fx\textrm{-}}x}_{w}$.
Thus, $x$-fixed-word simulation, by definition, falls between $x$-simulation
and $x$-trace inclusion. What is surprising is that delayed fixed-word
simulation $\sqsubseteq^{\mathsf{fx\textrm{-}de}}$ is _coarser_ than
multipebble delayed simulation (and thus direct trace inclusion
$\subseteq^{\mathsf{di}}$, since this one turns out to coincide with direct
multipebble simulation $\sqsubseteq^{\mathsf{di}}_{n}$, which is included in
$\sqsubseteq^{\mathsf{de}}_{n}$ by definition), and not incomparable as one
could have assumed; this fact is non-trivial [16]. Since delayed fixed-word
simulation is GFQ for NBA, this completes the classification of GFQ preorders
for NBA and makes $\sqsubseteq^{\mathsf{fx\textrm{-}de}}$ the coarsest
simulation-like GFQ preorder known to date. The reader is referred to [16] for
a more exhaustive discussion of the results depicted in Fig. 3. [[16]]
Direct/delayed fixed-word simulations
$\sqsubseteq^{\mathsf{fx\textrm{-}di}},\sqsubseteq^{\mathsf{fx\textrm{-}de}}$
are PSPACE-complete GFQ preorders.

The simulations and trace inclusions considered so far explore the state space
of the automaton in a forward manner. Their relationship and GFQ status are
summarized in Fig. 3, where an arrow means inclusion and a double arrow means
equality. Notice that there is a backward arrow from fixed-word direct
simulation to multipebble direct simulation, and not the other way around as
one might expect [16]. In a dual fashion, one can exploit the backward
behavior of the automaton to recognize structural relationships allowing for
quotienting states, which is the topic of the next section.

$\sqsubseteq^{\mathsf{di}}$$\sqsubseteq^{\mathsf{de}}$$\sqsubseteq^{\mathsf{f}}$$\sqsubseteq^{\mathsf{di}}_{n}$$\sqsubseteq^{\mathsf{de}}_{n}$$\sqsubseteq^{\mathsf{f}}_{n}$$\sqsubseteq^{\mathsf{fx\textrm{-}di}}$$\sqsubseteq^{\mathsf{fx\textrm{-}de}}$$\sqsubseteq^{\mathsf{fx\textrm{-}f}}$$\subseteq^{\mathsf{di}}$$\subseteq^{\mathsf{de}}$$\subseteq^{\mathsf{f}}$$\begin{array}[]{c}\textrm{forward}\\\
\textrm{simulations}\end{array}$$\begin{array}[]{c}\textrm{multipebble}\\\
\textrm{simulations}\end{array}$$\begin{array}[]{c}\textrm{fixed-word}\\\
\textrm{simulations}\end{array}$$\begin{array}[]{c}\textrm{trace}\\\
\textrm{inclusions}\end{array}$GFQnot GFQ Figure 3. Forward-like preorders on
NBA

###  3.5. Backward direct simulation and backward direct trace inclusion

Another way of obtaining GFQ preorders is to consider variants of
simulation/trace inclusion which go backwards w.r.t. transitions. _Backward
direct simulation_ $\sqsubseteq^{\mathsf{bw\textrm{-}di}}$ (called _reverse
simulation_ in [65]) is defined like ordinary simulation, except that
transitions are taken backwards: From configuration $(p_{i},q_{i})$, Spoiler
selects a transition
${p_{i+1}}\stackrel{{\scriptstyle\sigma_{i}}}{{\longrightarrow}}{p_{i}}$,
Duplicator replies with a transition
${q_{i+1}}\stackrel{{\scriptstyle\sigma_{i}}}{{\longrightarrow}}{q_{i}}$, and
the next configuration is $(p_{i+1},q_{i+1})$. Let
$\pi_{0}=\cdots\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}p_{1}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}p_{0}$
and
$\pi_{1}=\cdots\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}q_{1}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{0}$
be the two infinite backward traces built in this way. The corresponding
winning condition $\mathcal{C}^{\mathrm{bw}}_{I,F}$ requires Duplicator to
match _both_ accepting and initial states:

$\mathcal{C}^{\mathrm{bw}}_{I,F}(\pi_{0},\pi_{1})\quad\iff\quad\forall(i\geq
0)\cdot p_{i}\in F\implies q_{i}\in F\textrm{ and }p_{i}\in I\implies q_{i}\in
I$

Then, $p\sqsubseteq^{\mathsf{bw\textrm{-}di}}q$ holds if Duplicator has a
winning strategy in the backward simulation game starting from $(p,q)$ with
winning condition $C^{\mathrm{bw}}_{I,F}$. Backward simulation
$\sqsubseteq^{\mathsf{bw\textrm{-}di}}$ is an efficiently computable GFQ
preorder [65] on NBA incomparable with forward simulations. [[65]] Backward
simulation $\sqsubseteq^{\mathsf{bw\textrm{-}di}}$ is a PTIME computable GFQ
preorder on NBA. The corresponding notion of _backward direct trace inclusion_
$\subseteq^{\mathsf{bw\textrm{-}di}}$ is defined as follows:
$p\subseteq^{\mathsf{bw\textrm{-}di}}q$ if, for every finite word
$w=\sigma_{0}\sigma_{1}\cdots\sigma_{m-1}\in\Sigma^{*}$, and for every
initial, finite $w$-trace
$\pi_{0}=p_{0}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}p_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle\sigma_{m-1}}}{{\longrightarrow}}p_{m}$
ending in $p_{m}=p$, there exists an initial, finite $w$-trace
$\pi_{1}=q_{0}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle\sigma_{m-1}}}{{\longrightarrow}}q_{m}$
ending in $q_{m}=q$, s.t. $C^{\mathrm{bw}}_{F}(\pi_{0},\pi_{1})$ holds, where

$\mathcal{C}^{\mathrm{bw}}_{F}(\pi_{0},\pi_{1})\quad\iff\quad\forall(0\leq
i\leq m)\cdot p_{i}\in F\implies q_{i}\in F$

Note that backward direct trace inclusion deals with _finite traces_ (unlike
forward trace inclusions), which is due to the asymmetry between past and
future in $\omega$-automata.

As for their forward counterparts, backward direct simulation
$\sqsubseteq^{\mathsf{bw\textrm{-}di}}$ is included in backward direct trace
inclusion $\subseteq^{\mathsf{bw\textrm{-}di}}$. Notice that there is a slight
mismatch between the two notions, since the winning condition of the former is
defined over infinite traces, while the latter is on finite ones. In any case,
inclusion holds thanks to the automaton being backward complete. Indeed,
assume $p\sqsubseteq^{\mathsf{bw\textrm{-}di}}q$, and let $\pi_{0}$ be an
initial, finite $w$-trace starting in some $p_{0}\in I$ and ending in $p$. We
play the backward direct simulation game from $(p,q)$ by letting Spoiler take
transitions according to $\pi_{0}$ until configuration $(p_{0},q_{0})$ is
reached for some state $q_{0}$, and from there we let Spoiler play for ever
according to any strategy (which is possible since the automaton is backward
complete). We obtain a backward infinite path $\pi^{\prime}_{0}$ with suffix
$\pi_{0}$ for Spoiler, and a corresponding $\pi^{\prime}_{1}$ with suffix
$\pi_{1}$ for Duplicator s.t.
$\mathcal{C}^{\mathrm{bw}}_{I,F}(\pi^{\prime}_{0},\pi^{\prime}_{1})$. Since
$p_{0}\in I$, we obtain $q_{0}\in I$. Similarly, accepting states are matched
all along, as required in the winning condition for backward direct trace
inclusion. Thus, $p\subseteq^{\mathsf{bw\textrm{-}di}}q$.

In Lemma 3.5 we recalled that backward direct simulation
$\sqsubseteq^{\mathsf{bw\textrm{-}di}}$ is GFQ on NBA. We now prove that even
backward direct trace inclusion $\subseteq^{\mathsf{bw\textrm{-}di}}$ is GFQ
on NBA, thus generalizing the previous result.

######  Theorem 3.3.

Backward direct trace inclusion $\subseteq^{\mathsf{bw\textrm{-}di}}$ is a
PSPACE-complete GFQ preorder on NBA.

###### Proof.

We first show that $\subseteq^{\mathsf{bw\textrm{-}di}}$ is GFQ. Let
$w=\sigma_{0}\sigma_{1}\cdots\in\mathcal{L}(\mathcal{A}/\\!\subseteq^{\mathsf{bw\textrm{-}di}})$,
and we show $w\in\mathcal{L}(\mathcal{A})$. There exists an initial and fair
$w$-trace
$\pi=[q_{0}]\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}[q_{1}]\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$.
For $i\geq-1$, let $w_{i}=\sigma_{0}\sigma_{1}\cdots\sigma_{i}$ (with
$w_{-1}=\varepsilon$), and, for $i\geq 0$, let $\pi[0..i]$ be the
$w_{i-1}$-trace prefix of $\pi$ ending in $[q_{i}]$.

For any $i\geq 0$, we build by induction an initial and finite $w_{i-1}$-trace
$\pi_{i}$ of $\mathcal{A}$ ending in $q_{i}$ and visiting at least as many
accepting states as $\pi[0..i]$ (and at the same time as $\pi[0..i]$ does).
For $i=0$, just take the empty $\varepsilon$-trace $\pi_{0}=q_{0}$. For $i>0$,
assume that an initial $w_{i-2}$-trace $\pi_{i-1}$ of $\mathcal{A}$ ending in
$q_{i-1}$ has already been built. We have the transition
${[q_{i-1}]}\stackrel{{\scriptstyle\sigma_{i-1}}}{{\longrightarrow}}{[q_{i}]}$
in $\mathcal{A}/\\!\subseteq^{\mathsf{bw\textrm{-}di}}$. There exist
$\hat{q}\in[q_{i-1}]$ and $\hat{q}^{\prime}\in[q_{i}]$ s.t. we have a
transition
${\hat{q}}\stackrel{{\scriptstyle\sigma_{i-1}}}{{\longrightarrow}}{\hat{q}^{\prime}}$
in $\mathcal{A}$. W.l.o.g. we can assume that $\hat{q}^{\prime}=q_{i}$, since
$[\hat{q}^{\prime}]=[q_{i}]$. By
$q_{i-1}\subseteq^{\mathsf{bw\textrm{-}di}}\hat{q}$, there exists an initial
and finite $w_{i-1}$-trace $\pi^{\prime}$ of $\mathcal{A}$ ending in
$\hat{q}$. By the definition of backward direct trace inclusion,
$\pi^{\prime}$ visits at least as many accepting states as $\pi_{i-1}$, which,
by inductive hypothesis, visits at least as many accepting states as
$\pi[0..i-1]$. Therefore,
$\pi_{i}:=\pi^{\prime}\stackrel{{\scriptstyle\sigma_{i-1}}}{{\longrightarrow}}q_{i}$
is an initial and finite $w_{i-1}$-trace of $\mathcal{A}$ ending in $q_{i}$.
Moreover, if $[q_{i}]\in F^{\prime}=[F]$, then, since backward direct trace
inclusion respects accepting states, $[q_{i}]\subseteq F$, hence $q_{i}\in F$,
and, consequently, $\pi_{i}$ visits at least as many accepting states as
$\pi[0..i]$.

Since $\pi$ is fair, we have thus built a sequence of finite and initial
traces $\pi_{0},\pi_{1},\cdots$ visiting unboundedly many accepting states.
Since $\mathcal{A}$ is finitely branching, by König’s Lemma there exists an
initial and fair (infinite) $w$-trace $\pi_{\omega}$. Therefore,
$w\in\mathcal{L}(\mathcal{A})$.

Regarding complexity, PSPACE-hardness follows from an immediate reduction from
language inclusion of NFA, and membership in PSPACE can be shown by reducing
to a reachability problem in a finite graph $G$ of exponential size. Since
reachability in graphs is in NLOGSPACE, we get the desired complexity. The
finite graph $G=(V,\to)$ is obtained by a product construction combined with a
backward determinization construction: Vertices are those in

$\displaystyle V=\\{(p,\hat{p})\in Q\times 2^{Q}\;|\;p\in
F\implies\hat{p}\subseteq F\\}$

and there is an edge $(q,\hat{q})\to(p,\hat{p})$ if there exists a symbol
$\sigma\in\Sigma$ s.t. $p\stackrel{{\scriptstyle\sigma}}{{\longrightarrow}}q$
and for every $s\in\hat{q}$ there exists $r\in\hat{p}$ s.t.
$r\stackrel{{\scriptstyle\sigma}}{{\longrightarrow}}s$. Consider the target
set of vertices

$T=I\times\\{\hat{p}\subseteq Q\;|\;\hat{p}\cap I=\emptyset\\}.$

We clearly have $p\not\subseteq^{\mathsf{bw\textrm{-}di}}q$ iff from vertex
$(p,\\{q\\})$ we can reach $T$. ∎

The results on backward-like simulations established in this section are
summarized in Fig. 4, where the arrow indicates inclusion. Notice that
backward relations are in general incomparable with the corresponding forward
notions from Fig. 3. In the next section we explore suitable GFQ relations for
NFA.

$\sqsubseteq^{\mathsf{bw\textrm{-}di}}$$\subseteq^{\mathsf{bw\textrm{-}di}}$$\begin{array}[]{c}\textrm{backward
direct}\\\ \textrm{simulation}\end{array}$$\begin{array}[]{c}\textrm{backward
direct}\\\ \textrm{trace inclusion}\end{array}$GFQ Figure 4. Backward-like
preorders on NBA

###  3.6. Simulations and trace inclusions for NFA

The preorders presented so far were designed for NBA (i.e., infinite words).
For NFA (i.e., finite words), the picture is much simpler. Both forward and
backward direct simulations
$\sqsubseteq^{\mathsf{di}},\sqsubseteq^{\mathsf{bw\textrm{-}di}}$ are GFQ also
on NFA. However, over finite words one can consider a backward simulation
coarser than $\sqsubseteq^{\mathsf{bw\textrm{-}di}}$ where only initial states
have to be matched (but not necessarily final ones). In _backward finite-word
simulation_ $\sqsubseteq^{\mathsf{bw}}$ the two players play as in backward
direct simulation, except that Duplicator wins the game when the following
coarser condition is satisfied

$\displaystyle\mathcal{C}^{\mathrm{bw}}_{I}(\pi_{0},\pi_{1})$
$\displaystyle\quad\iff\quad\forall(i\geq 0)\cdot p_{i}\in I\implies q_{i}\in
I$

The corresponding trace inclusions are as follows. In _forward finite trace
inclusion_ $\subseteq^{\mathsf{fw}}$ Spoiler plays a finite, final trace, and
Duplicator has to match it with a final trace. Dually, in _backward finite
trace inclusion_ $\subseteq^{\mathsf{bw}}$, moves are backward and initial
traces must be matched. Clearly, direct simulation $\sqsubseteq^{\mathsf{di}}$
is included in $\subseteq^{\mathsf{fw}}$, and similarly for
$\sqsubseteq^{\mathsf{bw}}$ and $\subseteq^{\mathsf{bw}}$. While
$\subseteq^{\mathsf{fw}},\sqsubseteq^{\mathsf{bw}},\subseteq^{\mathsf{bw}}$
are not GFQ for NBA (they are not designed to consider the infinitary
acceptance condition of NBA, which can be shown with trivial examples) they
are for NFA. The following theorem can be considered as folklore and its proof
is just an adaptation of similar proofs for NBA in the simpler setting of NFA.
The PSPACE-completeness is an immediate consequence of the fact that language
inclusion for NFA is also PSPACE-complete [56].

######  Theorem 3.4.

Forward direct simulation $\sqsubseteq^{\mathsf{di}}$ and backward finite-word
simulation $\sqsubseteq^{\mathsf{bw}}$ are PTIME GFQ preorders on NFA. Forward
$\subseteq^{\mathsf{fw}}$ and backward $\subseteq^{\mathsf{bw}}$ finite trace
inclusions are PSPACE-complete GFQ preorders on NFA.

##  4\. Language inclusion

When automata are viewed as finite representations of languages, it is natural
to ask whether two different automata represent the same language, or, more
generally, to compare these languages for inclusion. Recall that, for two
automata $\mathcal{A}$ and $\mathcal{B}$ over the same alphabet $\Sigma$, we
write $\mathcal{A}\subseteq\mathcal{B}$ iff
$\mathcal{L}(\mathcal{A})\subseteq\mathcal{L}(\mathcal{B})$, and
$\mathcal{A}\approx\mathcal{B}$ iff
$\mathcal{L}(\mathcal{A})=\mathcal{L}(\mathcal{B})$. The _language
inclusion/equivalence problem_ consists in determining whether
$\mathcal{A}\subseteq\mathcal{B}$ or $\mathcal{A}\approx\mathcal{B}$ holds,
respectively. For nondeterministic finite and Büchi automata, language
inclusion and equivalence are PSPACE-complete [56, 49]. This entails that,
under standard complexity theoretic assumptions, there exists no efficient
deterministic algorithm for deciding the inclusion/equivalence problem.
Therefore, we consider suitable under-approximations thereof.

######  Remark 4.1.

A partial approach to NBA language inclusion testing has been described by
Kurshan in [50]. Given an NBA $\mathcal{B}$ with $n$ states, Kurshan’s
construction builds an NBA $\mathcal{B}^{\prime}$ with $2n$ states such that
$\overline{\mathcal{L}(\mathcal{B})}\subseteq\mathcal{L}(\mathcal{B}^{\prime})$,
i.e., $\mathcal{B}^{\prime}$ over-approximates the complement of
$\mathcal{B}$. Moreover, if $\mathcal{B}$ is deterministic then
$\overline{\mathcal{L}(\mathcal{B})}=\mathcal{L}(\mathcal{B}^{\prime})$.

This yields a sufficient test for inclusion, since
$\mathcal{L}(\mathcal{A})\cap\mathcal{L}(\mathcal{B}^{\prime})=\emptyset$
implies $\mathcal{L}(\mathcal{A})\subseteq\mathcal{L}(\mathcal{B})$ (though
generally not vice-versa). This condition can be checked in polynomial time.

Of course, for general NBA, this sufficient inclusion test cannot replace a
complete test. Depending on the input automaton $\mathcal{B}$, the over-
approximation
$\overline{\mathcal{L}(\mathcal{B})}\subseteq\mathcal{L}(\mathcal{B}^{\prime})$
could be rather coarse.

The following definition captures in which sense a preorder on states can be
used as a sufficient inclusion test.

######  Definition 4.2.

Let
$\mathcal{A}=(\Sigma,Q_{\mathcal{A}},I_{\mathcal{A}},F_{\mathcal{A}},\delta_{\mathcal{A}})$
and
$\mathcal{B}=(\Sigma,Q_{\mathcal{B}},I_{\mathcal{B}},F_{\mathcal{B}},\delta_{\mathcal{B}})$
be two automata. A preorder $\sqsubseteq$ on $Q_{\mathcal{A}}\times
Q_{\mathcal{B}}$ is _good for inclusion_ (GFI) if either one of the following
two conditions holds:

$\displaystyle 1.\textrm{ whenever }\forall p\in I_{\mathcal{A}}\cdot\exists
q\in I_{\mathcal{B}}\cdot p\sqsubseteq q\textrm{, then
}\mathcal{A}\subseteq\mathcal{B},\textrm{ or }$ $\displaystyle 2.\textrm{
whenever }\forall p\in F_{\mathcal{A}}\cdot\exists q\in F_{\mathcal{B}}\cdot
p\sqsubseteq q\textrm{, then }\mathcal{A}\subseteq\mathcal{B}.$

In other words, GFI preorders give a sufficient condition for inclusion, by
either matching initial states of $\mathcal{A}$ with initial states of
$\mathcal{B}$ (case 1), or by matching accepting states of $\mathcal{A}$ with
accepting states of $\mathcal{B}$ (case 2). However, a GFI preorder is not
necessary for inclusion in general333In the presence of multiple initial
$\mathcal{B}$ states it might be the case that inclusion holds but the
language of $\mathcal{A}$ is not included in the language of any of the
initial states of $\mathcal{B}$, only in their “union”.. Usually, forward-like
simulations are GFI for case 1, and backward-like simulations are GFI for case
2. Moreover, if computing a GFI preorder is efficient, then this leads to a
sufficient test for inclusion. Finally, if a preorder is GFI, then all smaller
preorders are GFI too, i.e., GFI is $\subseteq$-downward closed.

It is obvious that fair trace inclusion is GFI for NBAs (by matching initial
states of $\mathcal{A}$ with initial states of $\mathcal{B}$). Therefore, all
variants of direct, delayed, and fair simulation from Sec. 3.1, and the
corresponding trace inclusions from Sec. 3.3, are GFI. We notice here that
backward direct trace inclusion $\subseteq^{\mathsf{bw\textrm{-}di}}$ is GFI
for NBA (by matching accepting states of $\mathcal{A}$ with accepting states
of $\mathcal{B}$), which entails that the finer backward direct simulation is
GFI as well.

######  Theorem 4.3.

Backward direct simulation $\sqsubseteq^{\mathsf{bw\textrm{-}di}}$ and
backward direct trace inclusion $\subseteq^{\mathsf{bw\textrm{-}di}}$ are GFI
preorders for NBA.

###### Proof.

Every accepting state in $\mathcal{A}$ is in relation with an accepting state
in $\mathcal{B}$. Let
$w=\sigma_{0}\sigma_{1}\cdots\in\mathcal{L}(\mathcal{A})$, and let
$\pi_{0}=p_{0}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}p_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$
be an initial and fair $w$-path in $\mathcal{A}$. Since $\pi_{0}$ visits
infinitely many accepting states, and since each such state is
$\subseteq^{\mathsf{bw\textrm{-}di}}$-related to an accepting state in
$\mathcal{B}$, by using the definition of
$\subseteq^{\mathsf{bw\textrm{-}di}}$ it is possible to build in $\mathcal{B}$
longer and longer finite, initial traces in $\mathcal{B}$ visiting unboundedly
many accepting states. Since $\mathcal{B}$ is finitely branching, by König’s
Lemma there exists an initial and fair (infinite) $w$-trace $\pi_{\omega}$ in
$\mathcal{B}$. Thus, $w\in\mathcal{L}(\mathcal{B})$. ∎

For NFA, we observe that forward finite trace inclusion
$\subseteq^{\mathsf{fw}}$ is GFI by matching initial states, and backward
finite trace inclusion $\subseteq^{\mathsf{bw}}$ is GFI by matching accepting
states. The proof of the following theorem is immediate.

######  Theorem 4.4.

Forward $\subseteq^{\mathsf{fw}}$ and backward $\subseteq^{\mathsf{bw}}$
finite trace inclusions are GFI preorders on NFA.

##  5\. Transition pruning reduction techniques

While quotienting-based reduction techniques reduce the number of states by
merging them, we explore an alternative method which prunes (i.e., removes)
transitions. The intuition is that certain transitions can be removed from an
automaton without changing its language when other ‘better’ transitions
remain.

######  Definition 5.1.

Let $\mathcal{A}=(\Sigma,Q,I,F,\delta)$ be an automaton, let
$P\subseteq\delta\times\delta$ be a relation on $\delta$, and let $\max P$ be
the set of maximal elements of $P$, i.e.,

$\displaystyle\max
P=\\{(p,\sigma,r)\in\delta\;|\;\nexists(p^{\prime},\sigma^{\prime},r^{\prime})\in\delta\cdot((p,\sigma,r),(p^{\prime},\sigma^{\prime},r^{\prime}))\in
P\\}$

The _pruned automaton_ is defined as ${\it
Prune}({\mathcal{A}},{P})\;\coloneqq\;(\Sigma,Q,I,F,\delta^{\prime})$, where
$\delta^{\prime}=\max P$.

In most practical cases, $P$ will be a strict partial order, but this
condition is not absolutely required.

While the computation of $P$ depends on $\delta$ in general, _all subsumed
transitions are removed ‘in parallel’_ , and thus $P$ is not re-computed even
if the removal of a single transition changes $\delta$, and thus $P$ itself.
This is important for computational reasons. Computing $P$ may be expensive,
and thus it is beneficial to remove at once all transitions that can be
witnessed with the $P$ at hand. E.g., one might remove thousands of
transitions in a single step without re-computing $P$. On the other hand,
removing transitions in parallel makes arguing about correctness much more
difficult due to potential mutual dependencies between the involved
transitions.

Regarding correctness, note that removing transitions cannot introduce new
words in the language, thus ${\it
Prune}({\mathcal{A}},{P})\subseteq\mathcal{A}$. When also the converse
inclusion holds (so the language is preserved), we say that $P$ is good for
pruning (GFP).

######  Definition 5.2.

A relation $P\subseteq\delta\times\delta$ is _good for pruning_ (GFP) if ${\it
Prune}({\mathcal{A}},{P})\approx\mathcal{A}$.

Like GFQ, also GFP is $\subseteq$-downward closed in the space of relations.
We study specific GFP relations obtained by comparing the endpoints of
transitions over the same input symbol. Formally, given two binary state
relations $\mathrel{R_{b}},\mathrel{R_{\\!f}}\,\subseteq Q\times Q$ for the
source and target endpoints, respectively, we define

$\displaystyle\mathrel{P({\mathrel{R_{b}}},{\mathrel{R_{\\!f}}})}=\\{((p,\sigma,r),(p^{\prime},\sigma,r^{\prime}))\in\delta\times\delta\;|\;p\mathrel{R_{b}}p^{\prime}\textrm{
and }r\mathrel{R_{\\!f}}r^{\prime}\\}.$ (1)

$\mathrel{P({\cdot},{\cdot})}$ is monotone in both arguments.

In the following section, we explore which state relations
$\mathrel{R_{b}},\mathrel{R_{\\!f}}$ induce GFP relations
$\mathrel{P({\mathrel{R_{b}}},{\mathrel{R_{\\!f}}})}$ for NBA. In Sec. 5.2, we
present similar GFP relations for NFA.

###  5.1. Pruning NBA

$\mathrel{R_{b}}\backslash\mathrel{R_{\\!f}}$ | ${\it id}$ | $\sqsubset^{\mathsf{di}}$ | $\sqsubseteq^{\mathsf{di}}$ | $\subset^{\mathsf{di}}$ | $\subseteq^{\mathsf{di}}$ | $\sqsubset^{\mathsf{de}}$ | $\sqsubset^{\mathsf{f}}$ | $\subset^{\mathsf{f}}$
---|---|---|---|---|---|---|---|---
${\it id}$ | $-$ | $\checkmark$ | $-$ | $\checkmark$ | $-$ | $\times$ | $\times$ | $\times$
$\sqsubset^{\mathsf{bw\textrm{-}di}}$ | $\checkmark$ | $\checkmark$ | $\checkmark$ | $\checkmark$ | $\checkmark$ | $\times$ | $\times$ | $\times$
$\sqsubseteq^{\mathsf{bw\textrm{-}di}}$ | $-$ | $\checkmark$ | $-$ | $\times$ | $-$ | $\times$ | $\times$ | $\times$
$\subset^{\mathsf{bw\textrm{-}di}}$ | $\checkmark$ | $\checkmark$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$
$\subseteq^{\mathsf{bw\textrm{-}di}}$ | $-$ | $\checkmark$ | $-$ | $\times$ | $-$ | $\times$ | $\times$ | $\times$
Table 2. GFP relations $\mathrel{P({\mathrel{R_{b}}},{\mathrel{R_{\\!f}}})}$
for NBA. $\checkmark$ denotes yes, $\times$ denotes no, and $-$ denotes the
case where GFP does not hold for the trivial reason that the relation is not
irreflexive.

Our results are summarized in Table 2. It has long been known that
$\mathrel{P({{\it id}},{\sqsubset^{\mathsf{di}}})}$ and
$\mathrel{P({\sqsubset^{\mathsf{bw\textrm{-}di}}},{{\it id}})}$ are GFP (see
[14], where the removed transitions are called ‘little brothers’). However,
already slightly relaxing direct simulation to delayed simulation is
incorrect, i.e., $\mathrel{P({{\it id}},{\sqsubset^{\mathsf{de}}})}$ is not
GFP. This is shown in the counterexample in Fig. 5(a), where
$q\sqsubset^{\mathsf{de}}p$, but removing the dashed transition
$p\stackrel{{\scriptstyle a}}{{\longrightarrow}}q$ (due to
$p\stackrel{{\scriptstyle a}}{{\longrightarrow}}p$) makes the language empty.
The essential problem is that $q\sqsubset^{\mathsf{de}}p$ holds precisely
thanks to the presence of transition $p\stackrel{{\scriptstyle
a}}{{\longrightarrow}}q$, without which we would have
$q\not\sqsubset^{\mathsf{de}}p$, thus creating a cyclical dependency.
Consequently, $\mathrel{P({{\it id}},{\sqsubset^{\mathsf{f}}})}$ and
$\mathrel{P({{\it id}},{\subset^{\mathsf{f}}})}$ are not GFP either.

$p$$q$$a$$\sqsupset^{\mathsf{de}}$$a,b$$a$ (a) $\mathrel{P({{\it
id}},{\sqsubset^{\mathsf{de}}})}$ is not GFP.

$p$$q$$r$$s$$a$$a$$b$$a$$b$$a$$c$

$\sqsubset^{\mathsf{bw\textrm{-}di}}$

$\sqsubset^{\mathsf{di}}$

(b) $\mathrel{P({{\it
id}},{\sqsubset^{\mathsf{di}}})}\cup\mathrel{P({\sqsubset^{\mathsf{bw\textrm{-}di}}},{{\it
id}})}$ is not GFP.

Figure 5. Two pruning counterexamples.

Moreover, while $\mathrel{P({{\it id}},{\sqsubset^{\mathsf{di}}})}$ and
$\mathrel{P({\sqsubset^{\mathsf{bw\textrm{-}di}}},{{\it id}})}$ are GFP, their
union $\mathrel{P({{\it
id}},{\sqsubset^{\mathsf{di}}})}\cup\mathrel{P({\sqsubset^{\mathsf{bw\textrm{-}di}}},{{\it
id}})}$ (or the transitive closure thereof) is not. A counterexample is shown
in Fig. 5(b), where pruning would remove both the transitions
$p\stackrel{{\scriptstyle a}}{{\longrightarrow}}r$ (subsumed by
$p\stackrel{{\scriptstyle a}}{{\longrightarrow}}q$ with
$r\sqsubset^{\mathsf{di}}q$) and $q\stackrel{{\scriptstyle
a}}{{\longrightarrow}}s$ (subsumed by $r\stackrel{{\scriptstyle
a}}{{\longrightarrow}}s$ with $q\sqsubset^{\mathsf{bw\textrm{-}di}}r$), and
$aac^{\omega}$ would no longer be accepted. Again, the essential issue is a
cyclical dependency: $r\sqsubset^{\mathsf{di}}q$ holds only if
$q\stackrel{{\scriptstyle a}}{{\longrightarrow}}s$ is not pruned, and
symmetrically $q\sqsubset^{\mathsf{bw\textrm{-}di}}r$ holds only if
$p\stackrel{{\scriptstyle a}}{{\longrightarrow}}r$ is not pruned. Therefore,
removing any single one of these two transitions is sound, but not removing
both.

However, it is possible to relax simulation in $\mathrel{P({{\it
id}},{\sqsubset^{\mathsf{di}}})}$ and
$\mathrel{P({\sqsubset^{\mathsf{bw\textrm{-}di}}},{{\it id}})}$ to direct
trace inclusion $\subset^{\mathsf{di}}$, resp., backward trace inclusion
$\subset^{\mathsf{bw\textrm{-}di}}$, and prove that $\mathrel{P({{\it
id}},{\subset^{\mathsf{di}}})}$ and
$\mathrel{P({\subset^{\mathsf{bw\textrm{-}di}}},{{\it id}})}$ are GFP. This is
shown below in Theorems 5.3 and 5.4.

######  Theorem 5.3.

For every strict partial order $R\subseteq\subseteq^{\mathsf{di}}$,
$\mathrel{P({{\it id}},{R})}$ is GFP on NBA. In particular, $\mathrel{P({{\it
id}},{\subset^{\mathsf{di}}})}$ is GFP.

###### Proof.

Let $\mathcal{B}={\it Prune}({\mathcal{A}},{\mathrel{P({{\it id}},{R})}})$. We
show $\mathcal{A}\subseteq\mathcal{B}$. If
$w=\sigma_{0}\sigma_{1}\cdots\in\mathcal{L}(\mathcal{A})$ then there exists an
infinite fair initial trace $\hat{\pi}$ on $w$ in $\mathcal{A}$. We show
$w\in\mathcal{L}(\mathcal{B})$.

We call a trace
$\pi=q_{0}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$
on $w$ in $\mathcal{A}$ $i$-good if it does not contain any transition
$q_{j}\stackrel{{\scriptstyle\sigma_{j}}}{{\longrightarrow}}q_{j+1}$ for $j<i$
s.t. there exists an $\mathcal{A}$ transition
$q_{j}\stackrel{{\scriptstyle\sigma_{j}}}{{\longrightarrow}}q_{j+1}^{\prime}$
with $q_{j+1}\mathrel{R}q_{j+1}^{\prime}$ (i.e., no such transition is used
within the first $i$ steps). Since $\mathcal{A}$ is finitely branching, for
every state and symbol there exists at least one $R$-maximal successor that is
still present in $\mathcal{B}$, because $R$ is asymmetric and transitive.
Thus, for every $i$-good trace $\pi$ on $w$ there exists an $(i+1)$-good trace
$\pi^{\prime}$ on $w$ s.t. $\pi$ and $\pi^{\prime}$ are identical on the first
$i$ steps and $\mathcal{C}^{\mathrm{di}}(\pi,\pi^{\prime})$, because
$R\subseteq\subseteq^{\mathsf{di}}$. Since $\hat{\pi}$ is an infinite fair
initial trace on $w$ (which is trivially $0$-good), there exists an infinite
initial trace $\tilde{\pi}$ on $w$ that is $i$-good for every $i$ and
$\mathcal{C}^{\mathrm{di}}(\hat{\pi},\tilde{\pi})$. Moreover, $\tilde{\pi}$ is
a trace in $\mathcal{B}$. Since $\hat{\pi}$ is fair and
$\mathcal{C}^{\mathrm{di}}(\hat{\pi},\tilde{\pi})$, $\tilde{\pi}$ is an
infinite fair initial trace on $w$ that is $i$-good for every $i$. Therefore
$\tilde{\pi}$ is a fair initial trace on $w$ in $\mathcal{B}$ and thus
$w\in\mathcal{L}(\mathcal{B})$. ∎

######  Theorem 5.4.

For every strict partial order
$R\subseteq\subseteq^{\mathsf{bw\textrm{-}di}}$, $\mathrel{P({R},{{\it id}})}$
is GFP on NBA. In particular,
$\mathrel{P({\subset^{\mathsf{bw\textrm{-}di}}},{{\it id}})}$ is GFP.

###### Proof.

Let $\mathcal{B}={\it Prune}({\mathcal{A}},{\mathrel{P({R},{{\it id}})}})$. We
show $\mathcal{A}\subseteq\mathcal{B}$. If
$w=\sigma_{0}\sigma_{1}\cdots\in\mathcal{L}(\mathcal{A})$ then there exists an
infinite fair initial trace $\hat{\pi}$ on $w$ in $\mathcal{A}$. We show
$w\in\mathcal{L}(\mathcal{B})$.

We call a trace
$\pi=q_{0}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$
on $w$ in $\mathcal{A}$ $i$-good if it does not contain any transition
$q_{j}\stackrel{{\scriptstyle\sigma_{j}}}{{\longrightarrow}}q_{j+1}$ for $j<i$
s.t. there exists an $\mathcal{A}$ transition
$q_{j}^{\prime}\stackrel{{\scriptstyle\sigma_{j}}}{{\longrightarrow}}q_{j+1}$
with $q_{j}\mathrel{R}q_{j}^{\prime}$ (i.e., no such transition is used within
the first $i$ steps). We show, by induction on $i$, the following property
(P): For every $i$ and every initial trace $\pi$ on $w$ in $\mathcal{A}$ there
exists an initial $i$-good trace $\pi^{\prime}$ on $w$ in $\mathcal{A}$ s.t.
$\pi$ and $\pi^{\prime}$ have identical suffixes from step $i$ onwards and
$\mathcal{C}^{\mathrm{di}}(\pi,\pi^{\prime})$. The base case $i=0$ is trivial
with $\pi^{\prime}=\pi$. For the induction step there are two cases. If $\pi$
is $(i+1)$-good then we can take $\pi^{\prime}=\pi$. Otherwise there exists a
transition
$q_{i}^{\prime}\stackrel{{\scriptstyle\sigma_{i}}}{{\longrightarrow}}q_{i+1}$
with $q_{i}\mathrel{R}q_{i}^{\prime}$. Without restriction (since
$\mathcal{A}$ is finite and $R$ is asymmetric and transitive) we assume that
$q_{i}^{\prime}$ is $R$-maximal among the $\sigma_{i}$-predecessors of
$q_{i+1}$. In particular, the transition
$q_{i}^{\prime}\stackrel{{\scriptstyle\sigma_{i}}}{{\longrightarrow}}q_{i+1}$
is present in $\mathcal{B}$. Since
$R\subseteq\subseteq^{\mathsf{bw\textrm{-}di}}$, there exists an initial trace
$\pi^{\prime\prime}$ on $w$ that has suffix
$q_{i}^{\prime}\stackrel{{\scriptstyle\sigma_{i}}}{{\longrightarrow}}q_{i+1}\stackrel{{\scriptstyle\sigma_{i+1}}}{{\longrightarrow}}q_{i+2}\dots$
and $\mathcal{C}^{\mathrm{di}}(\pi,\pi^{\prime\prime})$. Then, by induction
hypothesis, there exists an initial $i$-good trace $\pi^{\prime}$ on $w$ that
has suffix
$q_{i}^{\prime}\stackrel{{\scriptstyle\sigma_{i}}}{{\longrightarrow}}q_{i+1}\stackrel{{\scriptstyle\sigma_{i+1}}}{{\longrightarrow}}q_{i+2}\dots$
and $\mathcal{C}^{\mathrm{di}}(\pi^{\prime\prime},\pi^{\prime})$. Since
$q_{i}^{\prime}$ is $R$-maximal among the $\sigma_{i}$-predecessors of
$q_{i+1}$, we obtain that $\pi^{\prime}$ is also $(i+1)$-good. Moreover,
$\pi^{\prime}$ and $\pi$ have identical suffixes from step $i+1$ onwards.
Finally, by $\mathcal{C}^{\mathrm{di}}(\pi,\pi^{\prime\prime})$ and
$\mathcal{C}^{\mathrm{di}}(\pi^{\prime\prime},\pi^{\prime})$, we obtain
$\mathcal{C}^{\mathrm{di}}(\pi,\pi^{\prime})$.

Given the infinite fair initial trace $\hat{\pi}$ on $w$ in $\mathcal{A}$, it
follows from property (P) and König’s Lemma that there exists an infinite
initial trace $\tilde{\pi}$ on $w$ that is $i$-good for every $i$ and
$\mathcal{C}^{\mathrm{di}}(\hat{\pi},\tilde{\pi})$. Therefore $\tilde{\pi}$ is
an infinite fair initial trace on $w$ in $\mathcal{B}$ and thus
$w\in\mathcal{L}(\mathcal{B})$. ∎

One can also compare both endpoints of transitions, i.e., using relations
larger than the identity as in the previous cases. The following Theorems 5.5
and 5.6 prove that
$\mathrel{P({\sqsubset^{\mathsf{bw\textrm{-}di}}},{\subseteq^{\mathsf{di}}})}$,
resp.,
$\mathrel{P({\subseteq^{\mathsf{bw\textrm{-}di}}},{\sqsubset^{\mathsf{di}}})}$
are GFP. Consequently,
$\mathrel{P({\sqsubset^{\mathsf{bw\textrm{-}di}}},{\sqsubset^{\mathsf{di}}})}$
is also GFP. This is already a non-trivial fact. To witness this, notice that
while pruning w.r.t. $\mathrel{P({{\it
id}},{\sqsubset^{\mathsf{di}}})}$/$\mathrel{P({\sqsubset^{\mathsf{bw\textrm{-}di}}},{{\it
id}})}$ preserves forward/backward simulation, respectively, pruning w.r.t.
$\mathrel{P({{\it id}},{\sqsubset^{\mathsf{di}}})}$ disrupts backward
simulation, and pruning w.r.t.
$\mathrel{P({\sqsubset^{\mathsf{bw\textrm{-}di}}},{{\it id}})}$ disrupts
forward simulation. Therefore, when pruning simultaneously w.r.t. the coarser
$\mathrel{P({\sqsubset^{\mathsf{bw\textrm{-}di}}},{\sqsubset^{\mathsf{di}}})}$
both simulations are disrupted and the structure of the automaton can change
radically.

Let us also notice that, while
$\mathrel{P({\sqsubset^{\mathsf{bw\textrm{-}di}}},{\subseteq^{\mathsf{di}}})}$
and
$\mathrel{P({\subseteq^{\mathsf{bw\textrm{-}di}}},{\sqsubset^{\mathsf{di}}})}$
are GFP on NBA, neither
$\mathrel{P({\subset^{\mathsf{bw\textrm{-}di}}},{\subseteq^{\mathsf{di}}})}$
subsuming the first one, nor
$\mathrel{P({\subseteq^{\mathsf{bw\textrm{-}di}}},{\subset^{\mathsf{di}}})}$
subsuming the second one, are GFP on NBA. Indeed,
$\mathrel{P({\subset^{\mathsf{bw\textrm{-}di}}},{\subset^{\mathsf{di}}})}$ is
already not GFP. A counter-example is shown in Fig. 6, where removing the
dashed transitions $p_{0}\stackrel{{\scriptstyle a}}{{\longrightarrow}}q_{0}$
(due to $p_{1}\stackrel{{\scriptstyle a}}{{\longrightarrow}}q_{1}$) and
$r_{1}\stackrel{{\scriptstyle a}}{{\longrightarrow}}s_{1}$ (due to
$r_{0}\stackrel{{\scriptstyle a}}{{\longrightarrow}}s_{0}$) causes the word
$a^{5}e^{\omega}$ to be no longer accepted; the extra transitions going up
from the initial state to the unnamed state and to $r_{0}$, and the extra
transitions going down from $q_{1}$ to the unnamed state and to the accepting
state are used in order to ensure that the trace inclusions are strict, which
shows that the two transitions $p_{0}\stackrel{{\scriptstyle
a}}{{\longrightarrow}}q_{0}$ and $r_{1}\stackrel{{\scriptstyle
a}}{{\longrightarrow}}s_{1}$ are even strictly subsumed, and yet they cannot
both be removed, lest the language be altered. Thus, one cannot use trace
inclusions on both endpoints, i.e., at least one endpoint must be a
simulation.

$p_{0}$$q_{0}$$r_{0}$$s_{0}$$p_{1}$$q_{1}$$r_{1}$$s_{1}$$a$$c$$b$$a$$a$$a$$a,d$$a$$a$$a,c$$a$$b$$a$$a$$a$$a$$a$$d$$e$

$\subset^{\mathsf{bw\textrm{-}di}}$

$\subset^{\mathsf{di}}$

$\subset^{\mathsf{bw\textrm{-}di}}$

$\subset^{\mathsf{di}}$

Figure 6.
$\mathrel{P({\subset^{\mathsf{bw\textrm{-}di}}},{\subset^{\mathsf{di}}})}$ is
not GFP.
$p_{0}$$q_{0}$$r_{0}$$s_{0}$$q_{1}$$r_{1}$$s_{1}$$b,c$$a$$a$$a$$a$$a$$a,b$$a$$a$$a$$a$

$\subset^{\mathsf{bw\textrm{-}di}}$

$\sqsubseteq^{\mathsf{di}}$

$\subset^{\mathsf{bw\textrm{-}di}}$

$\sqsubseteq^{\mathsf{di}}$

Figure 7.
$\mathrel{P({\subset^{\mathsf{bw\textrm{-}di}}},{\sqsubseteq^{\mathsf{di}}})}$
is not GFP.

Moreover, the endpoint using simulation must actually use strict simulation,
and not just simulation. In fact, while
$\mathrel{P({\sqsubset^{\mathsf{bw\textrm{-}di}}},{\subseteq^{\mathsf{di}}})}$
and
$\mathrel{P({\subseteq^{\mathsf{bw\textrm{-}di}}},{\sqsubset^{\mathsf{di}}})}$
are GFP on NBA, neither
$\mathrel{P({\sqsubseteq^{\mathsf{bw\textrm{-}di}}},{\subset^{\mathsf{di}}})}$
nor
$\mathrel{P({\subset^{\mathsf{bw\textrm{-}di}}},{\sqsubseteq^{\mathsf{di}}})}$
is GFP. A counter-example for the second case is shown in Fig. 7 (the first
case is symmetric). If both dashed transitions are removed, the automaton
stops recognizing $a^{\omega}$.

######  Theorem 5.5.

The relation
$\mathrel{P({\sqsubset^{\mathsf{bw\textrm{-}di}}},{\subseteq^{\mathsf{di}}})}$
is GFP on NBA.

###### Proof.

Let $\mathcal{B}={\it
Prune}({\mathcal{A}},{\mathrel{P({\sqsubset^{\mathsf{bw\textrm{-}di}}},{\subseteq^{\mathsf{di}}})}})$.
We show $\mathcal{A}\subseteq\mathcal{B}$. Let
$w=\sigma_{0}\sigma_{1}\cdots\in\mathcal{L}(\mathcal{A})$. There exists an
infinite fair initial trace $\hat{\pi}$ on $w$ in $\mathcal{A}$. We show
$w\in\mathcal{L}(\mathcal{B})$.

Let $i\geq 0$. We call a trace
$\pi=q_{0}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$
in $\mathcal{A}$ on $w$ $i$-good if there is no $j\leq i$ s.t. there exists a
state $q_{j}^{\prime}$ with
$q_{j}\sqsubset^{\mathsf{bw\textrm{-}di}}q_{j}^{\prime}$ and there exists an
infinite trace $\pi^{\prime}j$ from $q_{j}^{\prime}$ on the word
$\sigma_{j}\sigma_{j+1}\cdots$ with $\mathcal{C}^{\mathrm{di}}(\pi
j,\pi^{\prime}j)$. First, we show that, for every $i\geq 0$, there are
$i$-good traces in $\mathcal{A}$. For the base case, it suffices to choose the
state $q_{0}$ to be $\sqsubset^{\mathsf{bw\textrm{-}di}}$-maximal amongst the
starting points of all infinite initial traces $\pi$ on $w$ s.t.
$\mathcal{C}^{\mathrm{di}}(\pi,\hat{\pi})$. (This set is non-empty since it
contains $\hat{\pi}$.) For the inductive step, let $i\geq 1$ and let $\pi$ be
an infinite $(i-1)$-good trace on $w$. If $\pi$ is also $i$-good, then we are
done. Otherwise, $\pi$ is not $i$-good, and there exist a state
$q_{i}^{\prime}$ and an infinite path $\pi^{\prime}i$ from $q_{i}^{\prime}$
s.t. $q_{i}\sqsubset^{\mathsf{bw\textrm{-}di}}q_{i}^{\prime}$ and
$C^{\mathrm{di}}(\pi i,\pi^{\prime}i)$. We further choose $q_{i}^{\prime}$ to
be $\sqsubset^{\mathsf{bw\textrm{-}di}}$-maximal with the former property. By
the definition of $q_{i}\sqsubset^{\mathsf{bw\textrm{-}di}}q_{i}^{\prime}$,
there exists an initial path
$\pi^{\prime}i=q_{0}^{\prime}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}^{\prime}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle\sigma_{i-1}}}{{\longrightarrow}}q_{i}^{\prime}$
ending in $q_{i}^{\prime}$ s.t., for every $j\leq i$,
$q_{j}\sqsubseteq^{\mathsf{bw\textrm{-}di}}q_{j}^{\prime}$. (This last
property uses the fact that $\sqsubseteq^{\mathsf{bw\textrm{-}di}}$ propagates
backward. Backward direct trace inclusion
$\subseteq^{\mathsf{bw\textrm{-}di}}$ does not suffice.) Thus,
$\pi^{\prime}=q_{0}^{\prime}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}^{\prime}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$
is an initial, infinite, and fair trace on $w$. Moreover, it is $i$-good: By
contradiction, let $q^{\prime\prime}_{j}$ be s.t.
$q^{\prime}_{j}\sqsubset^{\mathsf{bw\textrm{-}di}}q^{\prime\prime}_{j}$ with
$j\leq i$. It cannot be the case that $j=i$ by the maximality of
$q_{i}^{\prime}$. Since
$q_{j}\sqsubseteq^{\mathsf{bw\textrm{-}di}}q^{\prime}_{j}$, it also cannot be
the case that $j<i$ since $\pi$ is $(i-1)$-good. Thus, $\pi^{\prime}$ is
$i$-good.

Second, by König’s Lemma it follows that there exists an initial, infinite,
trace
$\tilde{\pi}=q_{0}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$
on $w$ that is $i$-good for every $i$ and
$\mathcal{C}^{\mathrm{di}}(\hat{\pi},\tilde{\pi})$. In particular, this
implies that $\tilde{\pi}$ is fair. We show that such a $\tilde{\pi}$ is also
possible in $\mathcal{B}$ by assuming the opposite and deriving a
contradiction. Suppose that $\tilde{\pi}$ contains a transition
$q_{j}\stackrel{{\scriptstyle\sigma_{j}}}{{\longrightarrow}}q_{j+1}$ that is
not present in $\mathcal{B}$. Then there exists a transition
$q_{j}^{\prime}\stackrel{{\scriptstyle\sigma_{j}}}{{\longrightarrow}}q_{j+1}^{\prime}$
in $\mathcal{B}$ s.t. $q_{j}\sqsubset^{\mathsf{bw\textrm{-}di}}q_{j}^{\prime}$
and $q_{j+1}\subseteq^{\mathsf{di}}q_{j+1}^{\prime}$. Since
$q_{j}^{\prime}\stackrel{{\scriptstyle\sigma_{j}}}{{\longrightarrow}}q_{j+1}^{\prime}$
and $q_{j+1}\subseteq^{\mathsf{di}}q_{j+1}^{\prime}$, there exists an
infinite, fair, trace $\pi^{\prime}j$ from $q_{j}^{\prime}$ with
$\mathcal{C}^{\mathrm{di}}(\pi j,\pi^{\prime}j)$. Since
$q_{j}\sqsubset^{\mathsf{bw\textrm{-}di}}q_{j}^{\prime}$, this contradicts the
fact that $\tilde{\pi}$ is $j$-good. Therefore $\tilde{\pi}$ is a fair initial
trace on $w$ in $\mathcal{B}$, and thus $w\in\mathcal{L}(\mathcal{B})$. ∎

######  Theorem 5.6.

The relation
$\mathrel{P({\subseteq^{\mathsf{bw\textrm{-}di}}},{\sqsubset^{\mathsf{di}}})}$
is GFP on NBA.

###### Proof.

Let $\mathcal{B}={\it
Prune}({\mathcal{A}},{\mathrel{P({\subseteq^{\mathsf{bw\textrm{-}di}}},{\sqsubset^{\mathsf{di}}})}})$.
We show $\mathcal{A}\subseteq\mathcal{B}$. Let
$w=\sigma_{0}\sigma_{1}\cdots\in\mathcal{L}(\mathcal{A})$. There exists an
infinite fair initial trace $\hat{\pi}$ on $w$ in $\mathcal{A}$. We show
$w\in\mathcal{L}(\mathcal{B})$.

For an index $i\geq 0$, we define the following preorder $\preceq_{i}$ on
infinite initial traces on $w$: Given two infinite initial traces
$\pi,\pi^{\prime}$ on $w$, with
$\pi=q_{0}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$
and
$\pi^{\prime}=q_{0}^{\prime}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}^{\prime}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$,
we write $\pi\preceq_{i}\pi^{\prime}$ whenever the following condition is
satisfied:

$\displaystyle\pi\preceq_{i}\pi^{\prime}\quad\iff\quad\mathcal{C}^{\mathrm{di}}(\pi,\pi^{\prime})\textrm{
and }\forall j\geq i\cdot q_{j}\sqsubseteq^{\mathsf{di}}q_{j}^{\prime},$

and we write $\pi\prec_{i}\pi^{\prime}$ when, additionally,
$q_{i}\sqsubset^{\mathsf{di}}q_{i}^{\prime}$. Moreover, we say that $\pi$ is
_$i$ -good_ whenever its first $i$ transitions are also possible in
$\mathcal{B}$. We show, by induction on $i$, the following property (PP): For
every infinite initial trace $\pi$ on $w$ and every $i\geq 0$, there exists an
infinite initial trace $\pi^{\prime}$ on $w$ s.t. $\pi\preceq_{i}\pi^{\prime}$
and $\pi^{\prime}$ is $i$-good. The base case $i=0$ is trivially true with
$\pi^{\prime}=\pi$. For the induction step, consider an infinite initial trace
$\pi$ on $w$. By induction hypothesis, there exists an infinite initial trace
$\pi^{1}=q_{0}^{1}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}^{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$
on $w$ s.t. $\pi\preceq_{i}\pi^{1}$ and $\pi^{1}$ is $i$-good. Consequently,
$\pi\preceq_{i+1}\pi^{1}$ holds, and we may additionally assume that $\pi^{1}$
is _maximal_ in the sense that there is no other $\pi^{\prime}$ which is
$i$-good and $\pi^{1}\prec_{i+1}\pi^{\prime}$. We argue that such a maximal
$\pi^{1}$ is necessarily $(i+1)$-good. By contradiction, assume that the
transition
$q_{i}^{1}\stackrel{{\scriptstyle\sigma_{i}}}{{\longrightarrow}}q_{i+1}^{1}$
is not in $\mathcal{B}$. Then there exists a transition
$q_{i}^{2}\stackrel{{\scriptstyle\sigma_{i}}}{{\longrightarrow}}q_{i+1}^{2}$
in $\mathcal{B}$ s.t. $q_{i}^{1}\subseteq^{\mathsf{bw\textrm{-}di}}q_{i}^{2}$
and $q_{i+1}^{1}\sqsubset^{\mathsf{di}}q_{i+1}^{2}$. From the definitions of
$\subseteq^{\mathsf{bw\textrm{-}di}}$ and $\sqsubseteq^{\mathsf{di}}$ it
follows that there exists an infinite initial trace
$\pi^{2}=q_{0}^{2}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}^{2}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$
on $w$ s.t. $\pi^{1}\prec_{i+1}\pi^{2}$. (This last property uses the fact
that $\sqsubseteq^{\mathsf{di}}$ propagates forward. Direct trace inclusion
$\subseteq^{\mathsf{di}}$ does not suffice.) By induction hypothesis, there
exists an infinite initial trace
$\pi^{3}=q_{0}^{3}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}^{3}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$
on $w$ s.t. $\pi^{2}\preceq_{i}\pi^{3}$ (and thus
$\pi^{2}\preceq_{i+1}\pi^{3}$) and $\pi^{3}$ is $i$-good. Thus,
$\pi^{1}\prec_{i+1}\pi^{3}$, which contradicts the maximality of $\pi^{1}$.
Therefore, $\pi^{1}$ is $(i+1)$-good.

Given the infinite fair initial trace $\hat{\pi}$ on $w$ in $\mathcal{A}$, it
follows from property (PP) and König’s Lemma that there exists an infinite
initial trace $\tilde{\pi}$ on $w$ that is $i$-good for every $i$ and
$\mathcal{C}^{\mathrm{di}}(\hat{\pi},\tilde{\pi})$. Therefore $\tilde{\pi}$ is
an infinite fair initial trace on $w$ in $\mathcal{B}$, and thus
$w\in\mathcal{L}(\mathcal{B})$. ∎

Notice that Theorems 5.3 (about $\mathrel{P({{\it
id}},{\subset^{\mathsf{di}}})}$) and 5.5 (about
$\mathrel{P({\sqsubset^{\mathsf{bw\textrm{-}di}}},{\subseteq^{\mathsf{di}}})}$)
are incomparable: In the former, we require the source endpoints to be the
same (which is forbidden by the latter), and in the latter we allow the
destination endpoints to be the same (which is forbidden by the former), and
it is not clear whether one can find a common GFP generalization. For the same
reason, Theorems 5.4 (about
$\mathrel{P({\subset^{\mathsf{bw\textrm{-}di}}},{{\it id}})}$) and 5.6 (about
$\mathrel{P({\subseteq^{\mathsf{bw\textrm{-}di}}},{\sqsubset^{\mathsf{di}}})}$)
are also incomparable.

#### Pruning w.r.t. transient transitions.

Recall that a transition is _transient_ when it appears at most once on every
path of the automaton. (Analogously, one can define transient states. E.g.,
[65] consider variants of direct/backward simulations that do not care about
the accepting status of transient states.) While at the beginning of the
section we observed that $\mathrel{P({{\it id}},{\subset^{\mathsf{f}}})}$ is
not GFP, it is correct to remove a transition w.r.t. $\mathrel{P({{\it
id}},{\subset^{\mathsf{f}}})}$ when it is subsumed by a transient one [65,
Theorem 3].

This motivates us to define the following transient variant of
$\mathrel{P({\mathrel{R_{b}}},{\mathrel{R_{\\!f}}})}$, for
$\mathrel{R_{b}},\mathrel{R_{\\!f}}\subseteq Q\times Q$:

$\displaystyle\mathrel{P_{t}({\mathrel{R_{b}}},{\mathrel{R_{\\!f}}})}=\\{((p,\sigma,r),(p^{\prime},\sigma,r^{\prime}))\in\delta\times\delta\;|\;p\mathrel{R_{b}}p^{\prime},r\mathrel{R_{\\!f}}r^{\prime},\textrm{
and }(p^{\prime},\sigma,r^{\prime})\textrm{ is transient}\\}.$

The relation $\mathrel{P_{t}({{\it id}},{\subset^{\mathsf{f}}})}$ using the
very coarse fair trace inclusion $\subset^{\mathsf{f}}$ is GFP for NBA [65].
We note that one cannot relax the source endpoint to go beyond the identity.
In fact,
$\mathrel{P_{t}({\sqsubset^{\mathsf{bw\textrm{-}di}}},{\subset^{\mathsf{f}}})}$
—and even
$\mathrel{P_{t}({\sqsubset^{\mathsf{bw\textrm{-}di}}},{\sqsubset^{\mathsf{de}}})}$—is
already not GFP. A counterexample is shown in Fig. 8: Both transitions
$p\stackrel{{\scriptstyle a}}{{\longrightarrow}}q$ and
$q\stackrel{{\scriptstyle a}}{{\longrightarrow}}r$ are transient, and
$(q,a,r)\mathrel{P_{t}({\sqsubset^{\mathsf{bw\textrm{-}di}}},{\sqsubset^{\mathsf{de}}})}(p,a,q)$.
However, removing the smaller transition $q\stackrel{{\scriptstyle
a}}{{\longrightarrow}}r$ changes the language, since $a^{\omega}$ is no longer
accepted.

However, one can combine pruning w.r.t. transient transitions using the coarse
fair trace inclusion, and _simultaneously_ pruning w.r.t. all transitions
using direct trace inclusion. Let $R_{t}\subseteq\delta\times\delta$ be the
relation on transitions defined as $R_{t}=\mathrel{P({{\it
id}},{\subset^{\mathsf{di}}})}\cup\mathrel{P_{t}({{\it
id}},{\subset^{\mathsf{f}}})}$.

We will use the fact that $R_{t}$ is GFP when describing our automata
reduction algorithm in Sec. 7. The following result thus generalizes Theorem
5.3.

######  Theorem 5.7.

The relation $R_{t}$ is GFP on NBA.

###### Proof.

Even though the relation $R_{t}$ is not transitive in general, it is acyclic
since $R_{t}\subseteq\mathrel{P({{\it id}},{\subset^{\mathsf{f}}})}$. Let
$\mathcal{B}={\it Prune}({\mathcal{A}},{R_{t}})$. To show
$\mathcal{A}\subseteq\mathcal{B}$, let
$w=\sigma_{0}\sigma_{1}\cdots\in\mathcal{L}(\mathcal{A})$, and let $\hat{\pi}$
be any infinite fair initial trace on $w$ in $\mathcal{A}$. We call a trace
$\pi=q_{0}\stackrel{{\scriptstyle\sigma_{0}}}{{\longrightarrow}}q_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\longrightarrow}}\cdots$
on $w$ in $\mathcal{A}$ $i$-maximal if it does not contain any transition
$q_{j}\stackrel{{\scriptstyle\sigma_{j}}}{{\longrightarrow}}q_{j+1}$ for $j<i$
s.t. there exists an $\mathcal{A}$ transition
$q_{j}\stackrel{{\scriptstyle\sigma_{j}}}{{\longrightarrow}}q_{j+1}^{\prime}$
with $(q_{j},\sigma_{j},q_{j+1})R_{t}(q_{j},\sigma_{j},q_{j+1}^{\prime})$.
Moreover, let ${\it tt}_{i}(\pi)$ be the number of transient transitions
occurring in the first $i$ steps of $\pi$.

Since $\mathcal{A}$ is finitely branching and $R_{t}$ is acyclic, for every
state and symbol there exists at least one $R_{t}$-maximal successor that is
still present in $\mathcal{B}$. Thus, for every $i$-maximal fair trace $\pi$
on $w$ there exists an $(i+1)$-maximal fair trace $\pi^{\prime}$ on $w$ s.t.
$\pi$ and $\pi^{\prime}$ are identical on the first $i$ steps.

Since $\hat{\pi}$ is an infinite fair initial trace on $w$ (which is trivially
$0$-maximal), for every $i$ there exists an infinite fair initial trace
$\tilde{\pi}_{i}$ which is $i$-maximal and agrees with $\tilde{\pi}_{i-1}$ on
the first $i-1$ steps. Consider the sequence of these traces $\tilde{\pi}_{i}$
for increasing $i$. We have ${\it tt}_{i-1}(\tilde{\pi}_{i-1})={\it
tt}_{i-1}(\tilde{\pi}_{i})\leq{\it tt}_{i}(\tilde{\pi}_{i})$.

Since no transient transition can repeat twice in a run, the limit
$\lim_{i\rightarrow\infty}{\it tt}_{i}(\tilde{\pi}_{i})$ is bounded from above
by the finite number of transient transitions in $\mathcal{B}$. Thus there
exists a finite number $N=\lim_{i\rightarrow\infty}{\it
tt}_{i}(\tilde{\pi}_{i})$. Let $N^{\prime}$ be the smallest number where the
limit is reached, i.e., $N^{\prime}:=\min\\{i\ |\ {\it
tt}_{i}(\tilde{\pi}_{i})=N\\}$. In particular, $N^{\prime}\geq N$. Since, for
every $i\geq N^{\prime}$, the trace $\tilde{\pi}_{i}$ agrees with
$\tilde{\pi}_{N^{\prime}}$ on the first $N^{\prime}$ steps, it follows that
$\tilde{\pi}_{i}[N^{\prime}..]$ does not contain any transient transition.
Thus for every $N^{\prime}\leq i\leq j$,
$\mathcal{C}^{\mathrm{di}}(\tilde{\pi}_{i}[N^{\prime}..],\tilde{\pi}_{j}[N^{\prime}..])$.
I.e., after $N^{\prime}$ steps we are effectively pruning w.r.t.
$\mathrel{P({{\it id}},{\subset^{\mathsf{di}}})}$ (and not
$\mathrel{P_{t}({{\it id}},{\subset^{\mathsf{f}}})}$), and
$\subseteq^{\mathsf{di}}$ preserves the position of accepting states. By
arranging the $\tilde{\pi}_{i}$’s in a finitely-branching tree, by König’s
lemma there exists a infinite fair initial trace $\tilde{\pi}_{\infty}$ which
is $i$-maximal for every $i$. Therefore, $\tilde{\pi}_{\infty}$ is a trace in
$\mathcal{B}$ (by maximality), and thus $w\in\mathcal{L}(\mathcal{B})$. ∎

$p$$q$$r$$a$$a$$b$$a,b$$a$ Figure 8.
$\mathrel{P_{t}({\sqsubset^{\mathsf{bw\textrm{-}di}}},{\sqsubset^{\mathsf{de}}})}$
is not GFP.

###  5.2. Pruning NFA

The proofs of the following theorems are entirely similar to their equivalents
for NBA from the previous section— except for the fact that a simple induction
on the length of the word suffices (and thus König’s Lemma is not needed), and
thus they will not be repeated here. The difference is that forward trace
inclusion $\subseteq^{\mathsf{fw}}$ needs only to match accepting states at
the end of the computation (and not throughout the computation as in NBA),
and, symmetrically, backward trace inclusion $\subseteq^{\mathsf{bw}}$ needs
only to match initial states at the beginning of the computation (and not also
accepting states throughout as in NBA). An analogue of pruning transient
transitions for NBA as in Theorem 5.7 is missing for NFA, since pruning w.r.t.
coarser acceptance conditions like in delayed or fair trace inclusion does not
apply to finite words.

######  Theorem 5.8.

For every strict partial order $R\mathrel{\subseteq}\subseteq^{\mathsf{fw}}$,
$\mathrel{P({{\it id}},{R})}$ is GFP on NFA. In particular, $\mathrel{P({{\it
id}},{\subset^{\mathsf{fw}}})}$ is GFP.

######  Theorem 5.9.

For every strict partial order $R\mathrel{\subseteq}\subseteq^{\mathsf{bw}}$,
$\mathrel{P({R},{{\it id}})}$ is GFP on NFA. In particular,
$\mathrel{P({\subset^{\mathsf{bw}}},{{\it id}})}$ is GFP.

######  Theorem 5.10.

The relation
$\mathrel{P({\sqsubset^{\mathsf{bw}}},{\subseteq^{\mathsf{fw}}})}$ is GFP on
NFA.

######  Theorem 5.11.

The relation
$\mathrel{P({\subseteq^{\mathsf{bw}}},{\sqsubset^{\mathsf{di}}})}$ is GFP on
NFA.

##  6\. Lookahead Simulation

While trace inclusions are theoretically appealing as GFQ/GFI/GFP preorders
coarser than simulations, it is not feasible to use them in practice, because
they are too hard to compute (even their membership problem is PSPACE-complete
[56, 49]). Multipebble simulations ([24]; cf. Sec. 3.2) constitute sound
under-approximations to trace inclusions, and by varying the number of pebbles
one can achieve a better tradeoff between complexity and size than just
computing the full trace inclusion. However, computing multipebble simulations
with $k>0$ pebbles requires solving a game of size $n\cdot n^{k}$ (where $n$
is the number of states of the automaton), which is not feasible in practice,
even for modest values for $k$. (Even for $k=2$ one has a cubic best-case
complexity, which severely limits the size of $n$ that can be handled.) For
this reason, we consider a different way to extend Duplicator’s power, i.e.,
by using _lookahead_ on the moves of Spoiler. While lookahead itself is a
classic concept, it can be defined in several ways in the context of
adversarial games, like simulation. We compare different variants for
computational efficiency and approximation quality: _multistep simulation_
(Sec. 6.1), _continuous simulation_ (Sec. 6.2), culminating in _lookahead
simulation_ (6.3), which offers the best compromise, and it is the main object
of study of this section. We will use lookahead simulation in our automata
reduction (Sec. 7) and inclusion testing algorithms (Sec. 8). In the
following, we let $n$ be the number of the states of the automaton.

###  6.1. Multistep simulation.

In _$k$ -step simulation_ the players select sequences of transitions of
length $k>0$ instead of single transitions. This gives Duplicator more
information, and thus yields a larger simulation relation. In general,
$k$-step simulation and $k$-pebble simulation are incomparable, but $k$-step
simulation is strictly contained in $n$-pebble simulation. However, the rigid
use of lookahead in big-steps causes at least two issues: First, for an NBA
with maximal out-degree $d$, in every round we have to explore up-to $d^{k}$
different moves for each player, which is too large in practice (e.g., $d=4$,
$k=12$). Second, Duplicator’s lookahead varies between $1$ and $k$, depending
where she is in her response to Spoiler’s long move. Thus, Duplicator might
lack lookahead where it is most needed, while having a large lookahead in
other situations where it is not useful. In the next notion, we attempt at
ameliorating this.

###  6.2. Continuous simulation.

In _$k$ -continuous simulation_, Duplicator is continuously kept informed
about Spoiler’s next $k>0$ moves, i.e., she always has lookahead $k$.
Initially, Spoiler makes $k$ moves, and from this point on they alternate
making one move each (and matching the corresponding input symbols). Thus,
$k$-continuous simulation is coarser than $k$-step simulation. In general, it
is incomparable with $k$-pebble simulation for $k<n$, but it is always
contained in $k$-pebble simulation for $k=n$, and there are examples where the
containment is strict. Note that here the configuration of the game consists
not only of the current states of Spoiler and Duplicator, but also of the
announced $k$ next moves of Spoiler. While this is arguably the strongest way
of giving lookahead to Duplicator, it requires storing $n^{2}\cdot d^{k-1}$
configurations (for branching degree $d$), which is infeasible for non-trivial
$n$ and $k$ (e.g., $n=10000$, $d=4$, $k=12$).

###  6.3. Lookahead simulation.

We introduce $k$-lookahead simulation as an optimal compromise between the
finer $k$-step and the coarser $k$-continuous simulation. Intuitively, we put
the lookahead under Duplicator’s control, who can choose _at each round_ and
_depending on Spoiler’s move_ how much lookahead she needs (up to $k$).
Formally, configurations are pairs $(p_{i},q_{i})$ of states. From
configuration $(p_{i},q_{i})$, one round of the game is played as follows.

  * •

Spoiler chooses a sequence of $k$ consecutive transitions
$p_{i}\stackrel{{\scriptstyle\sigma_{i}}}{{\longrightarrow}}{p_{i+1}}\stackrel{{\scriptstyle\sigma_{i+1}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle\sigma_{i+k-1}}}{{\longrightarrow}}p_{i+k}$.

  * •

Duplicator chooses a degree of lookahead $m$ such that $1\leq m\leq k$.

  * •

Duplicator responds with a sequence of $m$ transitions
$q_{i}\stackrel{{\scriptstyle\sigma_{i}}}{{\longrightarrow}}{q_{i+1}}\stackrel{{\scriptstyle\sigma_{i+1}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle\sigma_{i+m-1}}}{{\longrightarrow}}q_{i+m}$.

The remaining $k-m$ moves of Spoiler
$p_{i+m}\stackrel{{\scriptstyle\sigma_{i+m}}}{{\longrightarrow}}{p_{i+m+1}}\stackrel{{\scriptstyle\sigma_{i+m+1}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle\sigma_{i+k-1}}}{{\longrightarrow}}p_{i+k}$
_are forgotten_ , and the next configuration is $(p_{i+m},q_{i+m})$; in
particular, in the next round Spoiler can chose a different attack from
$p_{i+m}$. In this way, the players build as usual two infinite traces
$\pi_{0}$ from $p_{0}$ and $\pi_{1}$ from $q_{0}$. Backward simulation is
defined similarly with backward transitions. For any acceptance condition
$x\in\\{\mathrm{di,de,f}\\}$, Duplicator wins this play if
$\mathcal{C}^{x}(\pi_{0},\pi_{1})$ holds, for $x=\mathrm{bw\textrm{-}di}$ we
require $\mathcal{C}^{\mathrm{bw}}_{I,F}(\pi_{0},\pi_{1})$ (cf. Sec. 3.5), and
for $x=\mathrm{bw}$ we require
$\mathcal{C}^{\mathrm{bw}}_{I}(\pi_{0},\pi_{1})$ (cf. Sec. 3.6).

######  Definition 6.1.

Two states $(p_{0},q_{0})$ are in _$k$ -lookahead $x$-simulation_, written
$p_{0}\sqsubseteq^{k\textrm{-}x}q_{0}$, iff Duplicator has a winning strategy
in the above game.

In general, greater lookahead yields coarser lookahead relations, i.e.,
$\sqsubseteq^{h\textrm{-}x}\subseteq\sqsubseteq^{k\textrm{-}x}$ whenever
$h\leq k$, and moreover it is not difficult to find examples where the
inclusion is actually strict when $h<k$. A simple such example (not depending
on the choice of $x$) for the case $h=1$ and $k=2$ can be found in Fig. 9
(which is also used below to show non-transitivity): First, we have
$p_{0}\not\sqsubseteq^{1}q_{0}$, since Duplicator must choose whether to go to
$q_{1}$ (and then Spoiler wins by playing $b$) or to $q_{2}$ (and then Spoiler
wins by playing $a$). Moreover, $p_{0}\sqsubseteq^{2}q_{0}$ holds, since now
with lookahead $k=2$ we let Duplicator take the transition via $q_{1}$ or
$q_{2}$ depending on whether Spoiler plays the word $(a+b)a$ or $(a+b)b$,
respectively.

$p_{0}$$q_{0}$$q_{1}$$q_{2}$$r_{0}$$r_{1}$$r_{2}$$a,b$$a,b$$a,b$$a$$b$$a,b$$a,b$$a$$a$$b$$b$$\sqsubseteq^{2}$$\sqsubseteq^{2}$
Figure 9. A lookeahead simulation example.

######  Remark 6.2.

$k$-lookahead simulation is not transitive for $k\geq 2$. Consider again the
example in Fig. 9. We have $p_{0}\sqsubseteq^{k}q_{0}\sqsubseteq^{k}r_{0}$
(and $k=2$ suffices), but $p_{0}\not\sqsubseteq^{k}r_{0}$ for any $k>0$. We
have already seen above that $p_{0}\sqsubseteq^{k}q_{0}$ holds for $k=2$.
Moreover, $q_{0}\sqsubseteq^{k}r_{0}$ holds by the following reasoning, with
$k=2$: If Spoiler goes to $q_{1}$ or $q_{2}$, then Duplicator goes to $r_{1}$
or $r_{2}$, respectively. Then, it can be shown that
$q_{1}\sqsubseteq^{k}r_{1}$ holds as follows (the case
$q_{2}\sqsubseteq^{k}r_{2}$ is similar). If Spoiler takes transitions
$q_{1}\stackrel{{\scriptstyle
a}}{{\longrightarrow}}q_{0}\stackrel{{\scriptstyle
a}}{{\longrightarrow}}q_{1}$, then Duplicator does
$r_{1}\stackrel{{\scriptstyle
a}}{{\longrightarrow}}r_{1}\stackrel{{\scriptstyle
a}}{{\longrightarrow}}r_{1}$, and if Spoiler does
$q_{1}\stackrel{{\scriptstyle
a}}{{\longrightarrow}}q_{0}\stackrel{{\scriptstyle
b}}{{\longrightarrow}}q_{1}$, then Duplicator does
$r_{1}\stackrel{{\scriptstyle
a}}{{\longrightarrow}}r_{2}\stackrel{{\scriptstyle
b}}{{\longrightarrow}}r_{1}$. The other cases are similar. Finally,
$p_{0}\not\sqsubseteq^{k}r_{0}$, for any $k>0$: From $r_{0}$, Duplicator can
play a trace for any word $w$ of length $k>0$, but in order to extend it to a
trace of length $k+1$ for any $w^{\prime}=wa$ or $wb$, she needs to know
whether the last $(k+1)$-th symbol is $a$ or $b$. Thus, no finite lookahead
suffices for Duplicator.

Non-transitivity of lookahead simulation $\sqsubseteq^{k\textrm{-}x}$ (unless
$k=1$) is not an obstacle to its applications. Since we use it to under-
approximate suitable preorders, we consider its transitive closure instead
(which is a preorder), which we denote by $\preceq^{k\textrm{-}x}$. Moreover,
we denote its asymmetric restriction by
$\prec^{k\textrm{-}x}=\preceq^{k\textrm{-}x}\setminus(\preceq^{k\textrm{-}x})^{-1}$.

######  Lemma 6.3.

For $k>0$ and $x\in\\{\mathrm{di,de,f,bw\textrm{-}di}\\}$, the transitive
closure of $k$-lookahead $x$-simulation $\preceq^{k\textrm{-}x}$ is GFI.
Moreover, it is GFQ for $x\neq\mathrm{f}$.

###### Proof.

Being GFQ/GFI follows from the fact that the transitive closure of lookahead
simulation is included in the corresponding trace inclusion/multipebble
simulation. Moreover direct/delayed multipebble simulations are included in
delayed fixed-word simulation; cf. Figure 3. These are is GFI (cf. Sec. 4, and
in particular Theorem 4.3 for backward trace inclusion), and GFQ for
$x\in\\{\mathrm{di,de}\\}$ by Lemma 3.4, and for $x=\mathrm{bw\textrm{-}di}$
by Theorem 3.3. ∎

$p_{0}$$q_{0}$$q_{1}$$q_{2}$$r_{0}$$r_{1}$$r_{2}$$q$$r$$a,b$$a,b$$a,b$$a$$b$$a,b$$a,b$$a$$a$$b$$b$$a$$a$$a$$\approx^{2}$$\approx^{2}$
(a) The original automaton $\mathcal{A}$
$\\{q,r\\}$$\\{p_{0},q_{0},r_{0}\\}$$\\{q_{1},r_{1}\\}$$\\{q_{2},r_{2}\\}$$a$$a,b$$a,b$$a$$a$$a$$b$$b$$b$$a,b$
(b) The quotient automaton $\mathcal{A}/\\!\preceq^{2}$

Figure 10. Lookeahead simulation is not preserved under quotienting.

######  Remark 6.4.

Let $\preceq^{k}$ be the transitive closure of $k$-lookahead simulation
$\sqsubseteq^{k}$. While quotienting w.r.t. ordinary simulation (i.e.,
lookahead $k=1$) preserves ordinary simulation itself in the sense that a
quotient class $[p]$ in the quotient automaton $\mathcal{A}/\\!\preceq^{k}$ is
simulation equivalent to $p$, this is not the case when considering larger
lookahead $k>1$. This is a consequence of lack of transitivity; cf. Fig. 10,
which builds on the previous non-transitivity example of Fig. 9. Here and in
the following we define $\approx^{k}$ as $\preceq^{k}\cap\succeq^{k}$, i.e.,
the largest equivalence included in $\preceq^{k}$. (Notice that
$\mathcal{A}/\\!\preceq^{k}$ is the same as $\mathcal{A}/\\!\approx^{k}$ by
definition of quotienting.) We have that
$p_{0}\approx^{2}q_{0}\approx^{2}r_{0}$, $q_{1}\approx^{2}r_{1}$,
$q_{2}\approx^{2}r_{2}$, and $q\approx^{2}r$ (which follows from the
discussion in Remark 6.2), and thus we obtain the quotient automaton
$\mathcal{A}/\\!\preceq^{2}$ on the right. However,
$\\{q,r\\}\not\sqsubseteq^{2}r$, since Spoiler can play
$\\{q,r\\}\stackrel{{\scriptstyle
a}}{{\longrightarrow}}\\{p_{0},q_{0},r_{0}\\}\stackrel{{\scriptstyle
a}}{{\longrightarrow}}\\{p_{0},q_{0},r_{0}\\}$ and Duplicator replies with
either (1) $r\stackrel{{\scriptstyle a}}{{\longrightarrow}}r_{0}$, but this is
losing since $\\{p_{0},q_{0},r_{0}\\}\not\sqsubseteq^{2}r_{0}$ (cf. the
discussion of $p_{0}\not\sqsubseteq^{2}r_{0}$ in Remark 6.2), or (2)
$r\stackrel{{\scriptstyle a}}{{\longrightarrow}}r_{0}\stackrel{{\scriptstyle
a}}{{\longrightarrow}}r_{1}$, but this is losing since Spoiler can then play a
$b$ letter (which is not available from $r_{1}$), or symmetrically (3)
$r\stackrel{{\scriptstyle a}}{{\longrightarrow}}r_{0}\stackrel{{\scriptstyle
a}}{{\longrightarrow}}r_{2}$, but this is losing too since Spoiler plays $a$
in this case.

While lookahead simulation is not preserved under quotienting, the lemma above
shows that the recognized language is nonetheless preserved, which is all that
we care about for correctness.

Lookahead simulation offers better reduction under quotienting than ordinary
(i.e., $k=1$) simulation. We will define a family of automata
$\mathcal{A}_{n}$ of size $O(n^{2})$ which is not compressible w.r.t. ordinary
simulation, but which is compressed to size $O(n)$ w.r.t. simulation with
lookahead $k=2$. Therefore, quotienting w.r.t. lookahead simulation performs
better than w.r.t. ordinary simulation by a linear factor at least. The
construction of $\mathcal{A}_{n}$ is as follows. The alphabet is
$\Sigma=\\{a,b_{1},\dots,b_{n}\\}$. There is a state $p_{\\{i,j\\}}$ for every
unordered pair $\\{i,j\\}\subseteq\\{1,\dots,n\\}$, there is a state $q_{i}$
for every $i\in\\{1,\dots,n\\}$, and finally we have a state $r$. Transitions
are as follows: $p_{\\{i,j\\}}\stackrel{{\scriptstyle
a}}{{\longrightarrow}}q_{i}$, $p_{\\{i,j\\}}\stackrel{{\scriptstyle
a}}{{\longrightarrow}}q_{j}$, and
$q_{i}\stackrel{{\scriptstyle\Sigma\setminus\\{b_{i}\\}}}{{\longrightarrow}}r$
for every unordered pair $\\{i,j\\}\subseteq\\{1,\dots,n\\}$. This automaton
is incompressible w.r.t. ordinary simulation since each two distinct
$p_{\\{i,j\\}},p_{\\{k,h\\}}$ are $\sqsubseteq^{1}$-incomparable: For
instance, assume w.l.o.g. that $i\not\in\\{k,h\\}$. Spoiler takes transition
$p_{\\{i,j\\}}\stackrel{{\scriptstyle a}}{{\longrightarrow}}q_{i}$, and now
Duplicator takes either transition $p_{\\{k,h\\}}\stackrel{{\scriptstyle
a}}{{\longrightarrow}}q_{k}$, which is losing since Spoiler plays $b_{k}$ in
this case, or transition $p_{\\{k,h\\}}\stackrel{{\scriptstyle
a}}{{\longrightarrow}}q_{h}$, which is also losing since Spoiler plays $b_{h}$
in this case. On the other hand, with lookahead $k=2$ we can readily see that
$p_{\\{i,j\\}}\approx^{2}p_{\\{h,k\\}}$ (thus falling in the same quotient
class), since now Duplicator can always match Spoiler’s choice in the second
round because
$\Sigma\setminus\\{b_{h}\\}\cup\Sigma\setminus\\{b_{k}\\}=\Sigma$.

Lookahead simulation offers the optimal tradeoff between $k$-step and
$k$-continuous simulation. Since the lookahead is discarded at each round,
$k$-lookahead simulation is (strictly) included in $k$-continuous simulation
(where the lookahead is never discarded). However, this has the benefit of
only requiring to store $n^{2}$ configurations, which makes computing
lookahead simulation space-efficient. On the other hand, when Duplicator
always chooses a maximal reply $m=k$ we recover $k$-step simulation, which is
thus included in $k$-lookahead simulation. Moreover, thanks to the fact that
Duplicator controls the lookahead, most rounds of the game can be solved
without ever reaching the maximal lookahead $k$: [label=0)]

for a fixed attack by Spoiler, we only consider Duplicator’s responses for
small $m=1,2,\dots,k$ until we find a winning one, and

also Spoiler’s attacks can be built incrementally since, if he loses for some
lookahead, then he also loses for any larger one. In practice, this greatly
speeds up the computation, and allows us to use lookaheads in the range
$4$-$25$, depending on the size and structure of the automata; see Sec. 9 for
the experimental evaluation and benchmark against the GOAL tool [68].

######  Remark 6.5.

$k$-lookahead simulation can also be expressed as a restriction of $n$-pebble
simulation, where Duplicator is allowed to split pebbles maximally (thus
$n$-pebbles), but after a number $m\leq k$ rounds (where $m$ is chosen
dynamically by Duplicator) he has to discard all but one pebble. Then
Duplicator is allowed to split pebbles maximally again, etc. Thus,
$k$-lookahead simulation is contained in $n$-pebble simulation, though it is
generally incomparable with $k$-pebble simulation.

######  Remark 6.6.

In [43, 44] very similar lookahead-like simulations are presented. In
particular, [43] defines two variants of what they call _multi-letter
simulations_. The _static_ variant is the same as multistep simulation from
Sec. 6.1, and the _dynamic_ variant corresponds to the case where Duplicator
chooses the amount of lookahead at each round, _independently of Spoiler’s
attack_ ; thus, dynamic multi-letter simulation is included in lookahead
simulation, since in the latter, Duplicator chooses the amount of lookahead
actually used (i.e., the length of the response) depending on Spoiler’s
attack. Moreover, [44] introduces what they call _buffered simulations_ ,
which extend multi-letter simulations by considering unbounded lookahead. In
particular, what they call _look-ahead buffered simulations_ correspond to
lookahead simulations as presented in Sec. 6.3 without a uniform bound on the
maximal amount of lookahead that Duplicator can choose at each round, and they
prove that they are PSPACE-complete to compute. Similarly, the more liberal
variant that they call _continuous look-ahead buffered simulations_
corresponds to continuous simulations as presented in Sec. 6.2, and they show
that they are EXPTIME-complete to compute. While in principle it might seem
that buffered simulations subsume lookahead/continuous simulations, in fact
from the results of [47] it can be established that an exponential amount of
lookahead suffices in both cases, and thus buffered simulations coincide with
lookahead/continuous simulations from this section for sufficiently large (but
fixed in advance) lookahead.

###  6.4. Fixpoint logic characterization.

We conclude this section by giving a characterization of lookahead simulation
in the modal $\mu$-calculus. While this characterization could be used as the
basis of an algorithm to compute lookahead simulations symbolically by using
fixpoint iteration, it is more efficient to consider lookahead simulations as
a special case of multipebble simulations, as described in Remark 6.5. See
Section 11 for details on efficient implementations.

The $\mu$-calculus characterization follows from the following preservation
property enjoyed by lookahead simulation: Let
$x\in\\{\mathrm{di,de,f,bw\textrm{-}di}\\}$ and $k>0$. When Duplicator plays
according to a winning strategy, in any configuration $(p_{i},q_{i})$ of the
resulting play, $p_{i}\sqsubseteq^{k\textrm{-}x}q_{i}$ holds. Thus,
$k$-lookahead simulation (without acceptance condition) can be characterized
as the largest $X\subseteq Q\times Q$ which is closed under a certain monotone
predecessor operator. For convenience, we take the point of view of Spoiler,
and compute the complement relation $W^{x}=(Q\times
Q)\setminus\sqsubseteq^{k\textrm{-}x}$ instead. This is particularly useful
for delayed simulation, since we can avoid recording the obligation bit (see
[26]) by using the technique of [46].

####  6.4.1. Direct and backward simulation.

Consider the following monotone (w.r.t. $\subseteq$) predecessor operator
$\mathsf{CPre}^{\mathrm{di}}(X)$, for any set $X\subseteq Q\times Q$:

$\displaystyle\mathsf{CPre}^{\mathrm{di}}(X)$
$\displaystyle=\\{(p_{0},q_{0})\;|\;\exists(p_{0}\stackrel{{\scriptstyle
a_{0}}}{{\longrightarrow}}p_{1}\stackrel{{\scriptstyle
a_{1}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle
a_{k-1}}}{{\longrightarrow}}p_{k})$
$\displaystyle\forall(q_{0}\stackrel{{\scriptstyle
a_{0}}}{{\longrightarrow}}q_{1}\stackrel{{\scriptstyle
a_{1}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle
a_{m-1}}}{{\longrightarrow}}q_{m})\textrm{ with }0<m\leq k,$ either
$\displaystyle\exists(0\leq j\leq m)\cdot p_{j}\in F\textrm{ and }q_{j}\not\in
F,$ or $\displaystyle(p_{m},q_{m})\in X\\}.$

Intuitively, $(p,q)\in\mathsf{CPre}^{\mathrm{di}}(X)$ iff, from position
$(p,q)$, in one round of the game Spoiler can either force the game in $X$, or
win immediately by violating the winning condition for direct simulation. For
backward simulation, $\mathsf{CPre}^{\mathrm{bw\textrm{-}di}}(X)$ is defined
analogously, except that transitions are reversed and also initial states are
taken into account:

$\displaystyle\mathsf{CPre}^{\mathrm{bw\textrm{-}di}}(X)$
$\displaystyle=\\{(p_{0},q_{0})\;|\;\exists(p_{0}\stackrel{{\scriptstyle
a_{0}}}{{\longleftarrow}}p_{1}\stackrel{{\scriptstyle
a_{1}}}{{\longleftarrow}}\cdots\stackrel{{\scriptstyle
a_{k-1}}}{{\longleftarrow}}p_{k})$
$\displaystyle\forall(q_{0}\stackrel{{\scriptstyle
a_{0}}}{{\longleftarrow}}q_{1}\stackrel{{\scriptstyle
a_{1}}}{{\longleftarrow}}\cdots\stackrel{{\scriptstyle
a_{m-1}}}{{\longleftarrow}}q_{m})\textrm{ with }0<m\leq k,$ either
$\displaystyle\exists(0\leq j\leq m)\cdot p_{j}\in F\textrm{ and }q_{j}\not\in
F,$ or $\displaystyle\exists(0\leq j\leq m)\cdot p_{j}\in I\textrm{ and
}q_{j}\not\in I,$ or $\displaystyle(p_{m},q_{m})\in X\\}.$

######  Remark 6.7.

The definition of $\mathsf{CPre}^{x}(X)$ requires that the automaton has no
deadlocks; otherwise, Spoiler would incorrectly lose if he can only perform at
most $k^{\prime}<k$ transitions. We assume that the automaton is complete to
keep the definition simple, but our implementation works with general
automata.

For $X=\emptyset$, $\mathsf{CPre}^{x}(X)$ is the set of states from which
Spoiler wins in at most one step. Thus, Spoiler wins iff he can eventually
reach $\mathsf{CPre}^{x}(\emptyset)$. Formally, for
$x\in\\{\mathrm{di,bw\textrm{-}di}\\}$,

$W^{x}=\mu W\cdot\mathsf{CPre}^{x}(W).$

####  6.4.2. Delayed and fair simulation.

We introduce a more elaborate three-arguments predecessor operator
$\mathsf{CPre}(X,Y,Z)$. Intuitively, a configuration belongs to
$\mathsf{CPre}(X,Y,Z)$ iff Spoiler can make a move s.t., for any Duplicator’s
reply, at least one of the following conditions holds:

  1. (1)

Spoiler visits an accepting state, while Duplicator never does so; then, the
game goes to $X$.

  2. (2)

Duplicator never visits an accepting state; the game goes to $Y$.

  3. (3)

The game goes to $Z$ (without any further condition).

$\displaystyle\mathsf{CPre}(X,Y,Z)$
$\displaystyle=\\{(p_{0},q_{0})\;|\;\exists(p_{0}\stackrel{{\scriptstyle
a_{0}}}{{\longrightarrow}}p_{1}\stackrel{{\scriptstyle
a_{1}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle
a_{k-1}}}{{\longrightarrow}}p_{k})$
$\displaystyle\forall(q_{0}\stackrel{{\scriptstyle
a_{0}}}{{\longrightarrow}}q_{1}\stackrel{{\scriptstyle
a_{1}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle
a_{m-1}}}{{\longrightarrow}}q_{m})\textrm{ with }0<m\leq k,$ either
$\displaystyle\exists(0\leq i\leq m)\cdot p_{i}\in F,\forall(i\leq j\leq
m)\cdot q_{j}\not\in F,(p_{m},q_{m})\in X,$ or $\displaystyle\forall(0\leq
j\leq m)\cdot q_{j}\not\in F,(p_{m},q_{m})\in Y,$ or
$\displaystyle(p_{m},q_{m})\in Z\\}.$

For fair simulation, Spoiler wins iff, except for finitely many rounds (least
fixpoint $\mu Z$), he visits accepting states infinitely often while
Duplicator does not visit any accepting state at all (greatest and least
fixpoints $\nu X\mu Y$):

$W^{\mathrm{f}}=\mu Z\cdot\nu X\cdot\mu Y\cdot\mathsf{CPre}(X,Y,Z).$

Indeed, for fixed $X$ and $Z$, a configuration belongs to $\mu
Y\cdot\mathsf{CPre}(X,Y,Z)$ if Spoiler can force the game in a finite number
of steps to either visit an accepting state and go to $X$ (while Duplicator
never visits an accepting state), or go to $Z$ (with the possibility that
Duplicator visits an accepting state). Thus, for fixed $Z$, a configuration
belongs to $\nu X\cdot\mu Y\cdot\mathsf{CPre}(X,Y,Z)$ if Spoiler can visit
accepting states infinitely often while Duplicator never visits an accepting
state, or go to $Z$. Finally, a configuration belongs to $W^{\mathrm{f}}$ if
Spoiler can force the game in a finite number of steps to a configuration from
where he can visit infinitely many accepting states while Duplicator never
visits an accepting state, as required by the fair winning condition for
Spoiler.

For delayed simulation, Spoiler wins if, after finitely many rounds,

  1. (1)

he can visit an accepting state, and from this moment on

  2. (2)

he can prevent Duplicator from visiting accepting states in the future.

For condition 1), let $\mathsf{CPre}^{1}(X,Y):=\mathsf{CPre}(X,\emptyset,Y)$,
and, for 2), $\mathsf{CPre}^{2}(X,Y):=\mathsf{CPre}(\emptyset,X,Y)$. From the
definition, a configuration belongs to $\mathsf{CPre}^{1}(X,Y)$ if Spoiler can
in one step either visit an accepting state (while Duplicator does not do so)
and go to $X$, or go to $Y$. Similarly, a configuration belongs to
$\mathsf{CPre}^{2}(X,Y)$ if Spoiler can in one step either force the game to
$X$ while Duplicator does not visit an accepting state, or force the game to
$Y$. Then,

$W^{\mathrm{de}}=\mu W\cdot\mathsf{CPre}^{1}(\nu
X\cdot\mathsf{CPre}^{2}(X,W),W).$

Indeed, for any fixed $X$, $\mu W\cdot\mathsf{CPre}^{1}(X,W)$ is the set of
configurations from which Spoiler can force a visit to an accepting state in a
finite number of steps (and Duplicator does not visit an accepting state after
Spoiler has done so) and go to $X$, and for any fixed $W$, $\nu
X\cdot\mathsf{CPre}^{2}(X,W)$ is the largest set of configurations from where
Spoiler can prevent Duplicator from visiting accepting states, or go to $W$.
Therefore a configuration is in $W^{\mathrm{de}}$ if Spoiler can force a visit
to an accepting state in a finite number of steps, after which he can prevent
Duplicator from visiting accepting states ever after, as required by the
delayed winning condition for Spoiler.

##  7\. The Automata Reduction Algorithm

###  7.1. Nondeterministic Büchi Automata

We reduce nondeterministic Büchi automata by the quotienting and transition
pruning techniques from Sections 3 and 5. While trace inclusions would be an
ideal basis for such techniques, they (i.e., their membership problems) are
PSPACE-complete. Instead, we use the lookahead simulations from Sec. 6 as
efficiently computable under-approximations; in particular, we use

  * •

direct lookahead simulation $\preceq^{k\textrm{-}\mathsf{di}}$ in place of
direct trace inclusion $\subseteq^{\mathsf{di}}$,

  * •

delayed lookahead simulation $\preceq^{k\textrm{-}\mathsf{de}}$ in place of
delayed fixed-word simulation $\sqsubseteq^{\mathsf{fx\textrm{-}de}}$,

  * •

fair lookahead simulation $\preceq^{k\textrm{-}\mathsf{f}}$ in place of fair
trace inclusion $\subseteq^{\mathsf{f}}$, and

  * •

backward direct lookahead simulation
$\preceq^{k\textrm{-}\mathsf{bw\textrm{-}di}}$ in place of backward direct
trace inclusion $\subseteq^{\mathsf{bw\textrm{-}di}}$.

For quotienting, we employ delayed $\preceq^{k\textrm{-}\mathsf{de}}$, and
backward $k$-lookahead $\preceq^{k\textrm{-}\mathsf{bw\textrm{-}di}}$
simulations, which are GFQ by Lemma 6.3. For pruning, we apply the results of
Sec. 5 and the substitutions above to obtain the following incomparable GFP
relations:

  * •

$\mathrel{P({{\it id}},{\prec^{k\textrm{-}\mathsf{di}}})}$ (by Theorem 5.3),

  * •

$\mathrel{P({\prec^{k\textrm{-}\mathsf{bw\textrm{-}di}}},{{\it id}})}$ (by
Theorem 5.4),

  * •

$\mathrel{P({\sqsubset^{\mathsf{bw\textrm{-}di}}},{\preceq^{k\textrm{-}\mathsf{di}}})}$
(by Theorem 5.5),

  * •

$\mathrel{P({\preceq^{k\textrm{-}\mathsf{bw\textrm{-}di}}},{\sqsubset^{\mathsf{di}}})}$
(by Theorem 5.6), and

  * •

$\mathrel{P_{t}({{\it id}},{\prec^{k\textrm{-}\mathsf{f}}})}$ (by Theorem
5.7).

Below we describe two possible ways to combine our simplification techniques:
_Heavy- $k$_ and _Light- $k$_ (which are parameterized by the lookahead value
$k$).

####  7.1.1. Heavy-$k$.

We advocate the following reduction procedure, which repeatedly applies all
the techniques described in this paper until the automaton cannot be further
modified:

  * •

Remove dead states.

  * •

Prune transitions w.r.t. the GFP relations above (using lookahead $k$).

  * •

Quotient w.r.t. $\preceq^{k\textrm{-}\mathsf{de}}$ and
$\preceq^{k\textrm{-}\mathsf{bw\textrm{-}di}}$.

The resulting simplified automaton cannot be further reduced by any of these
techniques. In this sense, it is a local minimum in the space of automata
(w.r.t. this set of reduction techniques). Many different variants are
possible where the techniques above are applied in different orders. In
particular, applying the techniques in a different order might produce a
different local minimum. In general, there does not exist an optimal order
that works best in every instance. One reason for this is that one needs to
decide whether to first quotient w.r.t. backward simulation and then to
quotient w.r.t. forward simulation or vice-versa; cf. Fig. 11.

| $p$$q$$r$$s$$t$$u$$a$$a$$b$$c$$a$$b$$a,b$$a$
---
The original NFA $\mathcal{A}$
| $p$$\\{q,r\\}$$s$$t$$u$$a$$b$$c$$a,b$$a,b$$a$ | $p$$\\{q,r,s\\}$$t$$u$$a,b\ $$c$$a,b$$a$
---|---
$\mathcal{A}/\\!\sqsubseteq^{\mathsf{bw}}$ | $(\mathcal{A}/\\!\sqsubseteq^{\mathsf{bw}})/\\!\sqsubseteq^{\mathsf{fw}}$
|
$p$$\\{q,t\\}$$r$$s$$u$$a,c\ $$a$$b$$a$$b$$a,b$ | $p$$\\{q,t\\}$$r$$s$$u$$a,c\ $$a$$b$$a$$b$$a,b$
$\mathcal{A}/\\!\sqsubseteq^{\mathsf{fw}}$ | $(\mathcal{A}/\\!\sqsubseteq^{\mathsf{fw}})/\\!\sqsubseteq^{\mathsf{bw}}=\mathcal{A}/\\!\sqsubseteq^{\mathsf{fw}}$
Figure 11. There is no universally optimal order of applying quotienting
operations. In this example, it is best to first quotient the NFA
$\mathcal{A}$ w.r.t. backward simulation and then to quotient it w.r.t.
forward simulation. Thus one obtains an irrecucible NFA with $4$ states (first
row above), while the reverse order yields an irrecucible NFA with $5$ states
(second row above). To obtain a dual example where it is best to first
quotient w.r.t. forward simulation, just reverse the direction of all
transitions in the original automaton $\mathcal{A}$ and make state $u$ initial
instead of $p$. To obtain a similar example for Büchi automata, just add a
self-loop with action $d$ at state $u$ (resp. at state $p$ for the dual
example).

In practice, the order is determined by efficiency considerations and easily
computable operations are used first. More exactly, our implementation uses a
nested loop, where the inner loop uses only lookahead $1$ (until a fixpoint is
reached), while the outer loop uses lookahead $k$. In other words, the
algorithm uses expensive operations only when cheap operations have no more
effect. For details about the precise order of the techniques in our
implementation, the reader is referred to [15] (algorithms/Minimization.java).

######  Remark 7.1.

Quotienting w.r.t. simulation is idempotent, since quotienting itself
preserves simulation. However, in general this is not true for lookahead
simulations, because these relations are not preserved under quotienting.
Moreover, quotienting w.r.t. forward simulations does not preserve backward
simulations, and vice-versa. Our experiments showed that repeatedly and
alternatingly quotienting w.r.t. $\preceq^{k\textrm{-}\mathsf{de}}$ and
$\preceq^{k\textrm{-}\mathsf{bw\textrm{-}di}}$ (in addition to our pruning
techniques) yields the best reduction effect.

The Heavy-$k$ procedure strictly subsumes all simulation-based automata
reduction methods described in the literature (removing dead states,
quotienting, pruning of ‘little brother’ transitions, mediated preorder (see
Sec. 7.3)), except for the following two:

  1. (1)

The _fair simulation reduction_ of [35] is implemented in GOAL [68], and works
by tentatively merging fair simulation equivalent states and then checking if
this operation preserved the language. (In general, fair simulation is not
GFQ.) It potentially subsumes quotienting with $\sqsubseteq^{\mathsf{de}}$,
provided that the chosen merged states are not only fair simulation
equivalent, but also delayed simulation equivalent. However, it does not
subsume quotienting with $\preceq^{k\textrm{-}\mathsf{de}}$. We benchmarked
our methods against it and found Heavy-$k$ to be much better in both effect
and efficiency; cf. Sec. 9.

  2. (2)

The GFQ _jumping-safe preorders_ of [16, 17] are incomparable to the
techniques described in this paper. If applied in addition to Heavy-$k$ (for
quotienting only, since they are GFQ but not GFP), they yield a modest extra
reduction effect. In our experiments in Sec. 9 we also benchmarked an extended
version of Heavy-$k$, called _Heavy- $k$-jump_, that additionally uses the
jumping-safe preorders of [16, 17] for quotienting.

####  7.1.2. Light-$k$.

This reduction procedure is defined purely for comparison reasons. It
demonstrates the effect of the lookahead $k$ in a single quotienting operation
and works as follows: Remove all dead states and then quotient w.r.t.
$\preceq^{k\textrm{-}\mathsf{de}}$. Although Light-$k$ achieves much less than
Heavy-$k$, it is not necessarily faster. This is because it uses the more
expensive to compute relation $\preceq^{k\textrm{-}\mathsf{de}}$ directly,
while Heavy-$k$ applies other cheaper (pruning) operations first and only then
computes $\preceq^{k\textrm{-}\mathsf{de}}$ on the resulting smaller
automaton.

###  7.2. Nondeterministic Finite Automata

Most of the techniques from Sec. 7.1 carry over to NFA, except for the
following differences.

  * •

Delayed and fair simulation do not apply to NFA. Thus, pruning w.r.t.
$\mathrel{P_{t}({{\it id}},{\prec^{k\textrm{-}\mathsf{f}}})}$ is omitted.
Moreover, instead of quotienting with the transitive closures of lookahead
delayed simulation $\preceq^{k\textrm{-}\mathsf{de}}$ and lookahead backward
direct simulation $\preceq^{k\textrm{-}\mathsf{bw\textrm{-}di}}$, we quotient
NFA with the transitive closures of lookahead forward direct simulation
$\preceq^{k\textrm{-}\mathsf{di}}$ and lookahead backward simulation
$\preceq^{k\textrm{-}\mathsf{bw}}$. Those are included in forward
$\subseteq^{\mathsf{fw}}$ and backward $\subseteq^{\mathsf{bw}}$ finite trace
inclusion, respectively, and thus they are GFQ on NFA by Theorem 3.4.

  * •

The transition pruning techniques use $\preceq^{k\textrm{-}\mathsf{bw}}$
instead of $\preceq^{k\textrm{-}\mathsf{bw\textrm{-}di}}$ and
$\prec^{k\textrm{-}\mathsf{bw}}$ instead of
$\prec^{k\textrm{-}\mathsf{bw\textrm{-}di}}$. The correctness for NFA follows
from the theorems in Sec. 5.2.

  * •

Unlike NBA, every NFA can be transformed into an equivalent one with just a
single accepting state without any outgoing transitions (unless the language
contains the empty word; this case can be handled separately), as follows:
[label=0)]

  * •

Add a new accepting state ${\it acc}$.

  * •

For every transition $p\stackrel{{\scriptstyle a}}{{\longrightarrow}}q$ where
$q$ is accepting and $q\neq{\it acc}$, add a transition
$p\stackrel{{\scriptstyle a}}{{\longrightarrow}}{\it acc}$.

  * •

Make ${\it acc}$ the only accepting state. This transformation adds just one
state, but possibly many transitions. In this new form, the direct forward and
backward (lookahead) simulations are significantly larger, because the
acceptance conditions are easier to satisfy. This greatly increases the effect
of the remaining quotienting and pruning reduction methods, and partly offsets
the negative effect caused by the loss of the delayed and fair simulation
based methods.

  * •

A variant of the GFQ _jumping-safe preorders_ of [16, 17] can also be applied
to NFA. Unlike the version for NBA, it does not make use of (jumping) delayed
simulation, but uses (jumping) direct forward and backward simulations. It is
implemented only in the extended Heavy-$k$-jump version of the NFA reduction
algorithm; cf. Sec. 9.

###  7.3. Quotienting w.r.t. mediated simulation

We show that the quotienting and transition pruning techniques described above
subsume quotienting w.r.t. mediated preorder [5, 6] (but not vice-versa), in
the sense that after applying our reduction algorithm, quotienting w.r.t.
mediated preorder provably does not yield any further reduction. Mediated
preorder was originally defined for alternating Büchi automata as an attempt
at combining backward and forward simulations for automata reduction. Here, we
consider its restriction to nondeterministic Büchi automata (and the arguments
carry over directly to NFA).

######  Definition 7.2 ([5, 6]).

A relation $M\subseteq Q\times Q$ is a _mediated simulation_ 555For two
relations $A,B\subseteq Q\times Q$, we write $A\circ B$ for the relation
$A\circ B\subseteq Q\times Q$ s.t. $(x,y)\in A\circ B$ iff there exists $z$
s.t. $(x,z)\in A$ and $(z,y)\in B$. if

  1. (1)

$M\mathrel{\subseteq}(\sqsubseteq^{\mathsf{di}}\circ\sqsupseteq^{\mathsf{bw\textrm{-}di}})$,
and

  2. (2)

$(M\circ\sqsubseteq^{\mathsf{di}})\mathrel{\subseteq}M$.