11institutetext: Department of Computer Science, University of Oxford

# Image-Binary Automata

Stefan Kiefer  Cas Widdershoven

###### Abstract

We introduce a certain restriction of weighted automata over the rationals,
called _image-binary automata_. We show that such automata accept the regular
languages, can be exponentially more succinct than corresponding NFAs, and
allow for polynomial complementation, union, and intersection. This compares
favourably with unambiguous automata whose complementation requires a
superpolynomial state blowup. We also study an infinite-word version, _image-
binary Büchi automata_. We show that such automata are amenable to
probabilistic model checking, similarly to unambiguous Büchi automata. We
provide algorithms to translate $k$-ambiguous Büchi automata to image-binary
Büchi automata, leading to model-checking algorithms with optimal
computational complexity.

##  1 Introduction

A weighted automaton assigns weights to words; i.e., it defines mappings of
the form $f:\Sigma^{*}\to D$, where $D$ is some domain of weights. Weighted
automata are well-studied. Many variations have been discussed, such as max-
plus automata [8] and probabilistic automata [25, 24], both over finite words
and over infinite words, in the latter case often combined with
$\omega$-valuation monoids [9]. However, it has been shown that many natural
questions are undecidable for many kinds of weighted automata [10, 1],
including inclusion and equivalence. These problems become decidable for
finitely ambiguous weighted automata [11].

In this paper we consider only numerical weights, where $D$ is a subfield of
the reals. A _language_ $L\subseteq\Sigma^{*}$ can be identified with its
characteristic function $\chi_{L}:\Sigma^{*}\to\\{0,1\\}$. We explore weighted
automata that encode characteristic functions of languages, i.e., weighted
automata that map each word either to $0$ or to $1$. We call such automata
_image-binary finite automata (IFAs)_ and view them as acceptors of languages
$L\subseteq\Sigma^{*}$. We do not require, however, that individual
transitions have weight $0$ or $1$. This makes IFAs a “semantic” class: it may
not be obvious from the transition weights whether a given weighted automaton
over, say, the rationals is image-binary. However, we will see that it can be
checked efficiently whether a given $\mathbb{Q}$-weighted automaton is an IFA
(Theorem 2.3).

An immediate question is on the expressive power of IFAs. Deterministic finite
automata (DFAs) can be viewed as IFAs. On the other hand, in Section 2.2 we
show that all languages accepted by IFAs are regular. It follows that IFAs
accept exactly the regular languages. Moreover, IFAs are efficiently closed
under Boolean operations; i.e., given two IFAs that accept $L_{1},L_{2}$,
respectively, one can compute in polynomial time IFAs accepting $L_{1}\cup
L_{2}$, $L_{1}\cap L_{2}$, and $\Sigma^{*}\setminus L_{1}$.

The latter feature, efficient closure under complement, might be viewed as a
key advantage of IFAs over unambiguous finite automata (UFAs). UFAs are
nondeterministic finite automata (NFAs) such that every word has either zero
or one accepting runs. UFAs can be viewed as a special case of IFAs. Whereas
we show that IFAs can be complemented in polynomial time, UFAs are known to be
not polynomially closed under complement [26].

The next question is then on the succinctness of IFAs, and on the complexity
of converting other types of finite automata to IFAs and vice versa. We study
such questions in Section 2.4. In Section 2.5, we also study the relationship
of IFAs to _mod-2 multiplicity automata_ , which are weighted automata over
$\mathit{GF}(2)$, the field $\\{0,1\\}$ where $1+1=0$. Such automata [2] share
various features with IFAs, in particular efficient closure under complement.

In the second part of the paper we put IFAs “to work”. Specifically, we
consider an infinite-word version, which we call _image-binary Büchi automata
(IBAs)_. Following the theme that image-binary automata naturally generalise
and relax unambiguous automata, we show that IBAs can be used for model
checking Markov chains in essentially the same way as _unambiguous Büchi
automata (UBAs)_ [3]. Specifically, we show in Section 4 that given an IBA and
a Markov chain, one can compute in NC (hence in polynomial time) the
probability that a random word produced by the Markov chain is accepted by the
IBA.

It was shown in [22] that a nondeterministic Büchi automaton (NBA) with $n$
states can be converted to an NBA with at most $3^{n}$ states whose ambiguity
is bounded by $n$. Known conversions from NBAs to UBAs have a state blowup of
roughly $n^{n}$, see, e.g., [17]. We show in Section 3.2 that NBAs with
logarithmic ambiguity (as produced by the construction from [22]) can be
converted to IBAs in polylogarithmic space. This suggests that in order to
translate NBAs into an automaton model suitable for probabilistic model
checking (such as IBAs), it is reasonable to first employ the partial
disambiguation procedure from [22] (which does most of the work). More
specifically, by combining the partial disambiguation procedure from [22] with
our translation to an IBA, we obtain a PSPACE transducer (i.e., a Turing
machine whose work tape is polynomially bounded) that translates an NBA into
an IBA. For example, combining that with the mentioned probabilistic model
checking procedure for IBAs we obtain an (optimal) PSPACE procedure for model
checking Markov chains against NBA specifications.

##  2 Image-Binary Finite Automata

###  2.1 Definitions

Let $\mathbb{F}$ be one of the fields $\mathbb{Q}$ or $\mathbb{R}$ (with
ordinary addition and multiplication). An _$\mathbb{F}$ -weighted automaton_
$\mathcal{A}=(Q,\Sigma,M,\alpha,\eta)$ consists of a set of states $Q$, a
finite alphabet $\Sigma$, a map $M:\Sigma\to\mathbb{F}^{Q\times Q}$, an
initial (row) vector $\alpha\in\mathbb{F}^{Q}$, and a final (column) vector
$\eta\in\mathbb{F}^{Q}$. Extend $M$ to $\Sigma^{*}$ by setting $M(a_{1}\cdots
a_{k})\stackrel{{\scriptstyle\text{def}}}{{=}}M(a_{1})\cdots M(a_{k})$. The
_language_ $L_{\mathcal{A}}$ of an automaton $\mathcal{A}$ is the map
$L_{\mathcal{A}}:\Sigma^{*}\to\mathbb{F}$ with $L_{\mathcal{A}}(w)=\alpha
M(w)\eta$. Automata $\mathcal{A},\mathcal{B}$ over the same alphabet $\Sigma$
are said to be _equivalent_ if $L_{\mathcal{A}}=L_{\mathcal{B}}$.

Let $\mathcal{A}=(Q,\Sigma,M,\alpha,\eta)$ be a $\mathbb{Q}$-weighted
automaton. We call $\mathcal{A}$ an _image-binary (weighted) finite automaton
(IFA)_ if $L_{\mathcal{A}}(\Sigma^{*})\subseteq\\{0,1\\}$, i.e.,
$L_{\mathcal{A}}(w)\in\\{0,1\\}$ holds for all $w\in\Sigma^{*}$. An
$\mathbb{R}$-IFA is defined like an IFA, but with $\mathbb{Q}$ replaced by
$\mathbb{R}$. An ($\mathbb{R}$)-IFA $\mathcal{A}$ defines a language
$L(\mathcal{A}):=\\{w\in\Sigma^{*}\mid L_{\mathcal{A}}(w)=1\\}$. Note that we
call both $L_{\mathcal{A}}$ and $L(\mathcal{A})$ the language of $A$; strictly
speaking, the former is the characteristic function of the latter.

If an IFA $\mathcal{A}=(Q,\Sigma,M,\alpha,\eta)$ is such that
$\alpha\in\\{0,1\\}^{Q}$ and $\eta\in\\{0,1\\}^{Q}$ and
$M(a)\in\\{0,1\\}^{Q\times Q}$ for all $a\in\Sigma$, then $\mathcal{A}$ is
called an _unambiguous finite automaton (UFA)_. Note that this definition of a
UFA is essentially equivalent to the classical one, which says that a UFA is
an NFA (nondeterministic finite automaton) where each word has at most $1$
accepting run. Similarly, a _deterministic finite automaton (DFA)_ is
essentially a special case of a UFA, and hence of an IFA.

###### Example 1

Figure 1 shows an IFA and a UFA in a graphical notation. Formally, the IFA on
the left is
$\mathcal{A}=(Q_{\mathcal{A}},\Sigma,M_{\mathcal{A}},\alpha_{\mathcal{A}},\eta_{\mathcal{A}})$
with $Q=\\{1,2,3\\}$ and $\Sigma=\\{a,b\\}$ and

$M_{\mathcal{A}}(a)\ =\ \begin{pmatrix}-1&1&0\\\ 0&0&1\\\
0&0&1\end{pmatrix}\quad\text{and}\quad M_{\mathcal{A}}(b)\ =\
\begin{pmatrix}0&0&0\\\ 0&0&0\\\ 0&0&1\end{pmatrix}$

and $\alpha_{\mathcal{A}}=\begin{pmatrix}1&0&0\end{pmatrix}$ and
$\eta_{\mathcal{A}}=\begin{pmatrix}0&0&1\end{pmatrix}^{T}$. Both automata
recognise the language of words that start in an even (positive) number of
$a$s.

$1$$2$$3$$-1a$$a$$a$$a,b$(a)$1$$2$$3$$a$$a$$a$$b$$b$$b$(b)

Figure 1: The IFA in (a) is a forward conjugate of, and hence equivalent to,
the UFA in (b). Unless indicated otherwise, edges in (a) have weight 1.

Let $\mathcal{A}=(Q,\Sigma,M,\alpha,\eta)$ be an $\mathbb{R}$-weighted
automaton. We call
$\overrightarrow{\mathcal{A}}:=(\overrightarrow{Q},\Sigma,\overrightarrow{M},\overrightarrow{\alpha},F\eta)$
a _forward conjugate_ of $\mathcal{A}$ with base $F$ if
$F\in\mathbb{R}^{\overrightarrow{Q}\times Q}$ and
$FM(a)=\overrightarrow{M}(a)F$ for all $a\in\Sigma$ and
$\alpha=\overrightarrow{\alpha}F$. Such $\mathcal{A}$ and
$\overrightarrow{\mathcal{A}}$ are equivalent: indeed, let $w\in\Sigma^{*}$;
by induction we have $FM(w)=\overrightarrow{M}(w)F$ and hence

$L_{\mathcal{A}}(w)\ =\ \alpha M(w)\eta\ =\ \overrightarrow{\alpha}FM(w)\eta\
=\ \overrightarrow{\alpha}\overrightarrow{M}(w)F\eta\ =\
L_{\overrightarrow{\mathcal{A}}}(w)\,.$

A backward conjugate can be defined analogously.

###### Example 2

The IFA $\mathcal{A}$ on the left of Figure 1 is a forward conjugate of the
UFA on the right with base

$F\ =\ \begin{pmatrix}1&0&0\\\ 1&1&0\\\ 1&1&1\end{pmatrix}\,.$

Indeed, we have
$\begin{pmatrix}1&0&0\end{pmatrix}F=\begin{pmatrix}1&0&0\end{pmatrix}$ and
$\begin{pmatrix}0&0&1\end{pmatrix}^{T}=F\begin{pmatrix}0&0&1\end{pmatrix}^{T}$,
where $\vec{v}^{T}$ denotes the transpose of a vector $\vec{v}$, and

$F\begin{pmatrix}0&1&0\\\ 1&0&1\\\
0&0&0\end{pmatrix}\,=\,\begin{pmatrix}0&1&0\\\ 1&1&1\\\
1&1&1\end{pmatrix}\,=\,\begin{pmatrix}-1&1&0\\\ 0&0&1\\\
0&0&1\end{pmatrix}F\quad\text{and}\quad F\begin{pmatrix}0&0&0\\\ 0&0&0\\\
1&1&1\end{pmatrix}\,=\,\begin{pmatrix}0&0&0\\\ 0&0&0\\\ 0&0&1\end{pmatrix}F.$

For some proofs we need the following definition. Let
$L:\Sigma^{*}\to\mathbb{F}$, where $\mathbb{F}$ is any field. Then the _Hankel
matrix_ of $L$ is the infinite matrix
$H_{L}\in\mathbb{F}^{\Sigma^{*}\times\Sigma^{*}}$ with $H_{L}[x,y]=L(xy)$. It
was shown by Carlyle and Paz [6] and Fliess [12] that the rank of $H_{L}$ is
equal to the number of states of the minimal (in number of states)
$\mathbb{F}$-weighted automaton $\mathcal{A}$ with $L_{\mathcal{A}}=L$.

######  Proposition 1 ([6, 12])

Let $L$ be an $\mathbb{F}$-weighted regular language, i.e. a function
$L:\Sigma^{*}\to\mathbb{F}$ that can be represented by an
$\mathbb{F}$-weighted automaton. Let $\mathcal{A}=(Q,\Sigma,M,\alpha,\eta)$ be
a minimal $\mathbb{F}$-weighted automaton such that $L_{\mathcal{A}}=L$. Then
$\operatorname{rank}H_{L}=|Q|$.

###  2.2 Regularity

Since a DFA is an IFA, for each regular language there is an IFA that defines
it. Conversely, we show that the language of an IFA is regular:

###### Theorem 2.1

Let $\mathcal{A}=(Q,\Sigma,M,\alpha,\eta)$ be an $\mathbb{R}$-IFA. Then
$L(\mathcal{A})$ is regular, and there is a DFA $\mathcal{B}$ with at most
$2^{|Q|}$ states and $L(\mathcal{A})=L(\mathcal{B})$.

In order to do so, we will need some auxiliary lemmas. View
$\mathbb{Z}_{2}=\\{0,1\\}$ as the field with two elements. In the proof of
Theorem 2.1 we consider vector spaces _over_ $\mathbb{Z}_{2}$, i.e., where the
scalars are from $\mathbb{Z}_{2}$. In particular, we will argue with the
vector space $\mathbb{Z}_{2}^{\mathbb{N}}\cong\mathbb{Z}_{2}^{\Sigma^{*}}$
over $\mathbb{Z}_{2}$. We first show:

###### Lemma 1

Let $V$ be a set of $n$ vectors. Consider the vector space $\langle V\rangle$
spanned by $V$ over $\mathbb{Z}_{2}$. Then $|\langle V\rangle|\leq 2^{n}$.

###### Proof

Let $V=\\{v_{1},\ldots,v_{n}\\}$. Then $\langle
V\rangle=\\{\sum_{i=1}^{n}\lambda_{i}v_{i}\mid\lambda_{i}\in\mathbb{Z}_{2}\\}$.
∎

###### Corollary 1

Let $\mathsf{V}$ be a vector space over $\mathbb{Z}_{2}$. For any
$n\in\mathbb{N}$, if $\dim\mathsf{V}\leq n$ then $|\mathsf{V}|\leq 2^{n}$.

The following two lemmas show that if an $\mathbb{R}$-weighted automaton is
image-binary, then the rank over $\mathbb{R}$ of its Hankel matrix $H$ is at
least the rank of $H$ over $\mathbb{Z}_{2}$.

###### Lemma 2

Let $V\subseteq\\{0,1\\}^{\mathbb{N}}$ be a set of vectors. If $V$ is linearly
dependent over $\mathbb{R}$ then $V$ is linearly dependent over $\mathbb{Q}$.
Hence $\dim\langle V\rangle_{\mathbb{Q}}\leq\dim\langle
V\rangle_{\mathbb{R}}$.

###### Proof

Let $V$ be linearly dependent (over $\mathbb{R}$), and let $n=\dim\langle
V\rangle$. Then there are $v_{0},v_{1},\ldots,v_{n}\in V$ such that
$V^{\prime}:=\\{v_{1},\ldots,v_{n}\\}$ is linearly independent and
$v_{0}\not\in V^{\prime}$ but $v_{0}\in\langle V^{\prime}\rangle$. So there
are unique $\lambda_{1},\ldots,\lambda_{n}\in\mathbb{R}$ with
$v_{0}=\sum_{i=1}^{n}\lambda_{i}v_{i}$. It suffices to show that
$\lambda_{1},\ldots,\lambda_{n}\in\mathbb{Q}$. Since $V^{\prime}$ is linearly
independent, there exists $J\subseteq\mathbb{N}$ with $|J|=n$ such that
$\\{v_{1}[J],\ldots,v_{n}[J]\\}$ is linearly independent, where
$v_{i}[J]\in\\{0,1\\}^{n}$ is the restriction of $v_{i}$ to the entries
indexed by $J$. Hence the $\lambda_{i}$ are the unique solution of a linear
system of equations

$\displaystyle v_{0}[j]\ $ $\displaystyle=\
\sum_{i=1}^{n}\lambda_{i}v_{i}[j]\qquad\text{ for all $j\in J$.}$

Linear systems of equations with rational coefficients and constants have
rational solutions. Hence $\lambda_{1},\ldots,\lambda_{n}\in\mathbb{Q}$. ∎

###### Lemma 3

Let $V\subseteq\\{0,1\\}^{\mathbb{N}}$ be a set of vectors. If $V$ is linearly
dependent over $\mathbb{Q}$ then $V$ is linearly dependent over
$\mathbb{Z}_{2}$. Hence $\dim\langle V\rangle_{\mathbb{Z}_{2}}\leq\dim\langle
V\rangle_{\mathbb{Q}}$.

###### Proof

Let $V=\\{v_{1},\ldots,v_{n}\\}$ and $\sum_{i=1}^{n}\lambda_{i}v_{i}=\vec{0}$,
where $\lambda_{i}\in\mathbb{Q}$ are not all zero. By multiplying all
$\lambda_{i}$ with a common denominator, we can assume without loss of
generality that $\lambda_{i}\in\mathbb{Z}$ where $\lambda_{i}$ are not all
zero. By dividing all $\lambda_{i}$ with the largest power of $2$ that divides
all $\lambda_{i}$, we can assume without loss of generality that the
$\lambda_{i}$ are not all even. In the equation
$\sum_{i=1}^{n}\lambda_{i}v_{i}=\vec{0}$, by regarding every $\lambda_{i}$ and
every entry of every $v_{i}$ modulo $2$, we have
$\sum_{i=1}^{n}\lambda_{i}v_{i}=\vec{0}$ over $\mathbb{Z}_{2}$, i.e., $V$ is
linearly dependent over $\mathbb{Z}_{2}$. ∎

Hence we can prove Theorem 2.1:

######  Proof (of Theorem 2.1)

Write $n=|Q|$. Let $H$ be the Hankel matrix of $L_{\mathcal{A}}$. We have
$H\in\\{0,1\\}^{\Sigma^{*}\times\Sigma^{*}}$. By proposition 1 we have
$\operatorname{rank}H\leq n$, where the rank is over $\mathbb{R}$. By lemmas 2
and 3 it follows that $\operatorname{rank}H\leq n$, where the rank is over
$\mathbb{Z}_{2}$. By corollary 1 it follows that $H$ has at most $2^{n}$
different rows, say $H[w_{1},\cdot],\ldots,H[w_{\ell},\cdot]$ with $\ell\leq
2^{n}$. So every word is Myhill-Nerode equivalent to a word in
$\\{w_{1},\ldots,w_{\ell}\\}$. Thus, there is an equivalent DFA with $\ell$
states.

Explicitly, the following DFA $\mathcal{B}=(Q^{\prime},\Sigma,\delta,q_{0},F)$
is equivalent to $\mathcal{A}$:

$\displaystyle Q^{\prime}\ $ $\displaystyle=\
\\{H[w_{1},\cdot],\ldots,H[w_{\ell},\cdot]\\}$
$\displaystyle\delta(H[w_{i},\cdot],a)\ $ $\displaystyle=\ H[w_{i}a,\cdot]$
$\displaystyle q_{0}\ $ $\displaystyle=\ H[\varepsilon,\cdot]$ $\displaystyle
F\ $ $\displaystyle=\ \\{H[w_{i},\cdot]\mid 1\leq i\leq\ell,\
H[w_{i},\varepsilon]=1\\}\,.$ ∎

###  2.3 Boolean Operations and Checking Image-Binariness

IFAs are _polynomially closed_ under all boolean operations, by which we mean:

###### Theorem 2.2

Let $\mathcal{A}_{1},\mathcal{A}_{2}$ be IFAs over $\Sigma$. One can compute
in polynomial time IFAs
$\mathcal{B}_{\neg},\mathcal{B}_{\cap},\mathcal{B}_{\cup}$ with
$L(\mathcal{B}_{\neg})=\Sigma^{*}\setminus L(\mathcal{A}_{1})$ and
$L(\mathcal{B}_{\cap})=L(\mathcal{A}_{1})\cap L(\mathcal{A}_{2})$ and
$L(\mathcal{B}_{\cup})=L(\mathcal{A}_{1})\cup L(\mathcal{A}_{2})$.

By De Morgan’s laws it suffices to construct $\mathcal{B}_{\neg}$ and
$\mathcal{B}_{\cap}$. Since $\mathcal{B}_{\neg}$ and $\mathcal{B}_{\cap}$ need
to satisfy only $L_{\mathcal{B}_{\neg}}=1+(-L_{\mathcal{A}_{1}})$ (where
$1:\Sigma^{*}\to\\{1\\}$ denotes the constant $1$ function) and
$L_{\mathcal{B}_{\cap}}=L_{\mathcal{A}_{1}}\cdot L_{\mathcal{A}_{2}}$, it
suffices to know that $\mathbb{Q}$-weighted automata are polynomially closed
under negation and pointwise addition and multiplication:

######  Proposition 2 (see, e.g., [5, Chapter 1])

Let $\mathcal{A}_{1},\mathcal{A}_{2}$ be $\mathbb{Q}$-weighted automata. One
can compute in polynomial time $\mathbb{Q}$-weighted automata
$\mathcal{B}_{-},\mathcal{B}_{+},\mathcal{B}_{\times}$ with
$L_{\mathcal{B}_{-}}=-L_{\mathcal{A}_{1}}$ and
$L_{\mathcal{B}_{+}}=L_{\mathcal{A}_{1}}+L_{\mathcal{A}_{2}}$ and
$L_{\mathcal{B}_{\times}}=L_{\mathcal{A}_{1}}\cdot L_{\mathcal{A}_{2}}$.

###### Proof

For $i\in\\{1,2\\}$ let
$\mathcal{A}_{i}=(Q_{i},\Sigma,M_{i},\alpha_{i},\eta_{i})$. For
$\mathcal{B}_{-}$, replace $\alpha_{1}$ by $-\alpha_{1}$. For
$\mathcal{B}_{+}$, assume $Q_{1}\cap Q_{2}=\emptyset$, take $Q=Q_{1}\cup
Q_{2}$, and $M(a)=\begin{pmatrix}M_{1}(a)&0\\\ 0&M_{2}(a)\end{pmatrix}$ for
all $a\in\Sigma$, and
$\alpha=\begin{pmatrix}\alpha_{1}&\alpha_{2}\end{pmatrix}$, and
$\eta=\begin{pmatrix}\eta_{1}\\\ \eta_{2}\end{pmatrix}$. For
$\mathcal{B}_{\times}$, take $Q=Q_{1}\times Q_{2}$, and $M(a)=M_{1}(a)\otimes
M_{2}(a)$ for all $a\in\Sigma$, and $\alpha=\alpha_{1}\otimes\alpha_{2}$, and
$\eta=\eta_{1}\otimes\eta_{2}$, where $\mathord{\otimes}$ stands for the
Kronecker product. It follows from the mixed-product property of
$\mathord{\otimes}$ (i.e., $(A\otimes B)(C\otimes D)=(AC)\otimes(BD)$) that
indeed $L_{\mathcal{B}_{\times}}=L_{\mathcal{A}_{1}}\cdot
L_{\mathcal{A}_{2}}$. ∎

While DFAs are also polynomially closed under complement (switch accepting and
non-accepting states), NFAs and UFAs are not. For NFAs, it was shown in [14]
that the (worst-case) blowup in the number $n$ of states is $\Theta(2^{n})$.
For UFAs, it was shown recently:

######  Proposition 3 ([26])

For any $n\in\mathbb{N}$ there exists a unary (i.e., on an alphabet $\Sigma$
with $|\Sigma|=1$) UFA $\mathcal{A}_{n}$ with $n$ states such that any NFA for
the complement language has at least $n^{(\log\log\log n)^{\Theta(1)}}$
states.

This super-polynomial blowup (even for unary alphabet and even if the output
automaton is allowed to be ambiguous) refuted a conjecture that it may be
possible to complement UFAs with a polynomial blowup [7]. An upper bound (for
general alphabets and requiring the output to be a UFA) of $O(2^{0.79n})$ was
shown in [16]; see also [15] for an (unpublished) improvement.

The authors believe Proposition 3 shows the strength of Theorem 2.2: while
UFAs cannot be complemented efficiently, the more general IFAs are
polynomially closed under all boolean operations.

Proposition 2 can be used to show:

###### Theorem 2.3

Given a $\mathbb{Q}$-weighted automaton, one can check in polynomial time if
it is an IFA.

###### Proof

Let $\mathcal{A}$ be a $\mathbb{Q}$-weighted automaton. By Proposition 2 one
can compute in polynomial time a $\mathbb{Q}$-weighted automaton $\mathcal{B}$
with $L_{\mathcal{B}}=L_{\mathcal{A}}\cdot L_{\mathcal{A}}$ (pointwise
multiplication). Then $\mathcal{A}$ is an IFA if and only if $\mathcal{A}$ and
$\mathcal{B}$ are equivalent. Equivalence of $\mathbb{Q}$-weighted automata
can be checked in polynomial time, see [29, 30]. ∎

###  2.4 Succinctness

It is known that UFAs can be exponentially more succinct than DFAs: for each
$n\in\mathbb{N}$ with $n\geq 3$ there is a UFA with $n$ states such that the
smallest equivalent DFA has $2^{n}$ states, see [21, Theorem 1]. Since UFAs
are IFAs, Theorem 2.1 is optimal:

###### Corollary 2

For converting IFAs to DFAs, a state blowup of $2^{n}$ is sufficient and
necessary.

It is also known from [21] that converting NFAs to UFAs can require $2^{n}-1$
states. The argument carries over to IFAs:

###### Proposition 4

For converting NFAs to IFAs, a state blowup of $\Theta(2^{n})$ is sufficient
and necessary.

###### Proof

Sufficiency is clear via the subset construction. For necessity, Leung [21,
Theorem 3] considers for each $n\geq 3$ an NFA (even an MDFA, which is a DFA
with multiple initial states) such that its Hankel matrix has rank $2^{n}-1$,
which he proved in [20]. He then invokes an analogue of Proposition 1, due to
Schmidt [28], to show that any equivalent UFA needs at least $2^{n}-1$ states.
But by Proposition 1 this holds also for IFAs. ∎

It follows from Theorem 2.2 and Proposition 3 that IFAs cannot be converted to
NFAs in polynomial time:

###### Proposition 5

Converting IFAs to NFAs requires a super-polynomial state blowup.

###### Proof

Let $n\in\mathbb{N}$, and let $\mathcal{A}_{n}$ be the UFA from proposition 3.
By theorem 2.2 there is a polynomial-size IFA, say $\mathcal{B}_{n}$, for the
complement of $L(\mathcal{A}_{n})$. If converting IFAs to NFAs required only a
polynomial state blowup, there would exist an NFA, say
$\mathcal{B}_{n}^{\prime}$, with
$L(\mathcal{B}_{n}^{\prime})=L(\mathcal{B}_{n})=\Sigma^{*}\setminus
L(\mathcal{A}_{n})$, of size polynomial in $\mathcal{A}_{n}$, contradicting
proposition 3. ∎

###  2.5 Mod-2-Multiplicity Automata

We compare IFAs with the mod-2-multiplicity automata (mod-2-MAs) as introduced
in [2], which are weighted automata over the field $\mathbb{Z}_{2}$. Given a
mod-2-MA $\mathcal{A}$ and a word $w$, $w$ is accepted iff $\mathcal{A}(w)=1$.
Like with IFAs, mod-2-MAs are exponentially more succinct than DFAs [2, Lemma
6]. Converting NFAs to mod-2-MAs requires a super-polynomial state blowup [2,
Lemma 10] while (under the assumption that there are infinitely many Mersenne
primes) converting mod-2-MAs to NFAs requires an exponential blowup [2, Lemma
11].

We can convert IFAs to mod-2-MAs without incurring a blowup:

###### Proposition 6

For any IFA $\mathcal{A}$ with $n$ states there exists a mod-2-MA
$\mathcal{A}^{\prime}$ of at most $n$ states with
$L_{\mathcal{A}}=L_{\mathcal{A}^{\prime}}$.

###### Proof

Let $H$ be the Hankel matrix of $L_{\mathcal{A}}$. By Proposition 1,
$\operatorname{rank}H\leq n$, where the rank is taken over $\mathbb{R}$.
Invoking Lemma 2 and Lemma 3 then shows that $\operatorname{rank}H\leq n$ also
when the rank is taken over $\mathbb{Z}_{2}$. Then by Proposition 1 there
exists a mod-2-MA with $\operatorname{rank}H\leq n$ (over $\mathbb{Z}_{2}$)
states that accepts the same language as $\mathcal{A}$. ∎

However, the converse requires an exponential blowup. Inspired by Angluin et
al.’s [2] proof that mod-2 automata can be exponentially more succinct than
NFAs, this proof makes use of shift register sequences. However, note that
this proof does not require the assumption that there are infinitely many
Mersenne primes. For further information on shift register sequences, see
[13]. A _shift register sequence_ of dimension $d$ is an infinite periodic
sequence $\\{a_{n}\\}$ of bits defined by initial conditions $a_{i}=b_{i}$ for
$i=0,\ldots,d-1$ and $b_{i}\in\\{0,1\\}$, and a linear recurrence

$a_{n}=c_{1}a_{n-1}+c_{2}a_{n-2}+\ldots+c_{d}a_{n-d},$

for all $n\geq d$, where each $c_{i}\in\\{0,1\\}$ and addition is done modulo
2. The _minimum period_ of a periodic sequence $\\{a_{n}\\}$ is the lowest
$p\in\mathbb{N}$ such that $a_{n}=a_{n\bmod{p}}$ for every $n$. The maximum
possible minimum period of a shift register sequence is $2^{d}-1$, and it is
known that for each positive integer $d$ there are shift register sequences of
maximum period. These are known as _maximal length_ or _pseudo-noise_
sequences [13].

Given $d>0$, let $a_{n}=c_{1}a_{n-1}+c_{2}a_{n-2}+\ldots+c_{d}a_{n-d}$ define
a maximum period shift register sequence. Let $L_{d}$ be the language over a
unary alphabet $\\{\\#\\}$ defined by $\\#^{n}\in L_{d}$ if and only if
$a_{n}=1$. We have the following:

###### Proposition 7

The language $L_{d}$ is accepted by a mod-2-MA with $d$ states, but not by any
IFA with fewer than $2^{d}-1$ states.

###### Proof

The existence of a mod-2-MA with $d$ states accepting $L_{d}$ is shown in [2,
Lemma 11].

Consider the Hankel matrix over $\mathbb{R}$ of $L_{d}$. Since $\\{a_{n}\\}$
is $2^{d}-1$ periodic, we have that the $i$’th row of the Hankel matrix is
equal to the $i+2^{d}-1$’st row for any $i$, and similar for the columns.
Hence, the rank (over $\mathbb{R}$) of the Hankel matrix is equal to the rank
of the submatrix of size $(2^{d}-1)\times(2^{d}-1)$ in the top left corner. We
will call this matrix $H$. Notice that $H_{i,j}=a_{i+j}$. The _auto-
correlation_ of $\\{a_{n}\\}$ is defined as

$C(\tau)=\sum_{k=1}^{2^{d}-1}a_{k}a_{k+\tau},$

for $\tau\geq 0$. By Equation 10 on page 82 in [13], we have that
$C(\tau)=2^{d-1}$ if $\tau=0$ and $C(\tau)=2^{d-2}$ otherwise. Consider
$H^{2}$. If $H^{2}$ has full rank, then so does $H$. We have that

$\displaystyle(H^{2})_{i,j}$ $\displaystyle=$
$\displaystyle\sum_{k=1}^{2^{d}-1}H_{i,k}H_{k,j}$ $\displaystyle=$
$\displaystyle\sum_{k=1}^{2^{d}-1}a_{i+k}a_{k+j}$ $\displaystyle=$
$\displaystyle\sum_{k=1}^{2^{d}-1}a_{k}a_{k+|j-i|}=C(|j-i|),$

where the indices are taken modulo $2^{d}-1$. Hence, $H^{2}$ is the matrix
with $2^{d-1}$ on the diagonal and $2^{d-2}$ elsewhere. We show that the
matrix with $2^{-d+2}-2^{-2d+2}$ on the diagonal and $-2^{-2d+2}$ elsewhere is
an inverse of $H^{2}$. Let
$H^{\prime}\in\mathbb{R}^{(2^{d}-1)\times(2^{d}-1)}$ as follows:

$H^{\prime}_{i,j}=\left\\{\begin{array}[]{ll}2^{-d+2}-2^{-2d+2}&\textrm{if
$i=j$}\\\ 2^{-2d+2}&\textrm{otherwise}\end{array}\right.$

Now we have that $(H^{2}H^{\prime})_{i,j}=1$ if $i=j$:

$\displaystyle(H^{2}H^{\prime})_{i,i}$ $\displaystyle=$
$\displaystyle\sum_{k=1}^{2^{d}-1}H^{2}_{i,k}H^{\prime}_{k,i}$
$\displaystyle=$ $\displaystyle
2^{d-1}(2^{-d+2}-2^{-2d+2})+(2^{d}-2)(2^{d-2}(-2^{-2d+2})$ $\displaystyle=$
$\displaystyle 2^{1}-2^{-d+1}-2^{0}+2^{-d+1}$ $\displaystyle=$ $\displaystyle
1$

We also have $(H^{2}H^{\prime})_{i,j}=0$ if $i\neq j$:

$\displaystyle(H^{2}H^{\prime})_{i,j}$ $\displaystyle=$
$\displaystyle\sum_{k=1}^{2^{d}-1}H^{2}_{i,k}H^{\prime}_{k,j}$
$\displaystyle=$ $\displaystyle
2^{d-1}(-2^{-2d+2})+2^{d-2}(2^{-d+2}-2^{-2d+2})+(2^{d}-3)(2^{d-2}(-2^{-2d+2}))$
$\displaystyle=$ $\displaystyle-2^{-d+1}+2^{0}-2^{-d}-2^{0}+3*2^{-d}$
$\displaystyle=$ $\displaystyle 0$

Thus, $H^{\prime}$ is an inverse of $H^{2}$. Hence, $H^{2}$ and $H$ have full
rank and thus the Hankel matrix of $L_{d}$ has rank $2^{d}-1$. This means that
the smallest IFA accepting $L_{d}$ has $2^{d}-1$ states. ∎

##  3 Image-binary Büchi Automata

###  3.1 Definitions

Let $\mathcal{A}=(Q,\Sigma,M,\alpha)$ be like in a weighted automaton over a
field $\mathbb{F}$ and let $F$ be a set of final states. We call $\mathcal{A}$
_ultimately stable_ if for any $q,q^{\prime}\in Q$ and $a\in\Sigma$ such that
there exists a word $w$ with $M(w)_{q^{\prime},q}\neq 0$ (i.e., there is a
path from $q^{\prime}$ to $q$ over some word $w$), $M(a)_{q,q^{\prime}}=0$ or
$M(a)_{q,q^{\prime}}=1$, meaning that any edges in a loop have weight 1. For
any infinite word $w=w_{0}w_{1}\ldots$ we call $q_{0}q_{1}\ldots\in
Q^{\omega}$ a _path_ over $w$ if $\alpha(q_{0})\neq 0$ and for all $i$,
$M(w_{i})_{q_{i},q_{i+1}}\neq 0$. We call $q_{0}q_{1}\ldots$ a _final path_ if
$\mathit{infinite}(q_{0}q_{1}\ldots)\cap F\neq\emptyset$, where
$\mathit{infinite}(q_{0}q_{1}\ldots)$ denotes the set of states in $Q$ that
occur infinitely often in the path. We will write
$\mathit{FinalPaths}_{\mathcal{A}}(w)$ to denote the set of final paths of an
automaton $\mathcal{A}$ over a word $w$.

It is clear that for any path $q_{0}q_{1}\ldots$ over a word
$w=w_{0}w_{1}\ldots$ there exists an $i$ such that for any $j\geq i$, $q_{j}$
lies on a loop, and therefore we can define the weight of the path
$q_{0}q_{1}\ldots$ over $w$ to be $\lim_{i\to\infty}\prod_{n\leq
i}M(w_{n})_{q_{n},q_{n+1}}$, denoted by $\mathit{weight}(q_{0}q_{1}\ldots,w)$.
If $w$ is clear from context, we may simply write
$\mathit{weight}(q_{0}q_{1}\ldots)$. For any word $w$ with finitely many final
paths, we define the weight of $w$ to be the sum of the weights of the final
paths over $w$, denoted by $L_{\mathcal{A}}(w)$. We call
$\mathcal{A}=(Q,\Sigma,M,\alpha,F)$ an _image-binary (weighted) Büchi
automaton (IBA)_ if it is ultimately stable, there exists a bound
$N\in\mathbb{N}$ such that $|\mathit{FinalPaths}_{\mathcal{A}}(w)|\leq N$ for
any word $w$, and $L_{\mathcal{A}}(\Sigma^{\omega})\subseteq\\{0,1\\}$, i.e.
for all $w\in\Sigma^{\omega}$, $L_{\mathcal{A}}(w)\in\\{0,1\\}$.

If an IBA $\mathcal{A}$ is such that $\alpha\in\\{0,1\\}^{Q}$ and
$M(a)\in\\{0,1\\}^{Q\times Q}$ for all $a\in\Sigma$, then $\mathcal{A}$ is
called an _unambiguous Büchi automaton (UBA)_. Similarly to the finite word
case, we note that this definition of a UBA is essentially equivalent to the
classical one, which says that a UBA is an NBA (nondeterministic Büchi
automaton) where each word has at most 1 final path. We also see that a
_deterministic Büchi automaton (DBA)_ essentially is a special case of a UBA,
and hence of an IBA.

We will use the following notation: given a finite sequence
$a=a_{1}a_{2}\ldots a_{n}$, we will write $\mathord{last}(a)$ to denote
$a_{n}$. Given a (possibly finite) sequence $a=a_{1}a_{2}\ldots$ and a
character $a_{0}$ we will write $a_{0}\cdot a$ to denote the concatenation
$a_{0}a_{1}a_{2}\ldots$. We will write $\mathbb{B}$ to denote the two element
set $\\{\bot,\top\\}$ and for any set $S$ we will write $\mathcal{P}^{\leq
k}(S)$ to denote the set $\\{S^{\prime}\subseteq S\;\mid\;|S^{\prime}|\leq
k\\}$. For ease of notation we will treat $\mathbb{B}$ as the set of true
($\top$) and false ($\bot$) predicates, on which the standard Boolean
operations apply.

###  3.2 IBAs and $k$-Ambiguous NBAs

In this section we introduce $k$-ambiguous NBAs ($k$-ABAs) and show that they
can be exponentially more concise than IBAs. We give a procedure to translate
a $k$-ABA into an equivalent IBA using a PSPACE transducer.

A non-deterministic Büchi automaton (NBA) is a tuple
$(Q,\Sigma,\delta,Q_{0},F)$ where $Q$ is a state set, $\Sigma$ is an alphabet,
$\delta:Q\times\Sigma\rightarrow Q$ is a transition relation, $Q_{0}\subseteq
Q$ is a set of initial states, and $F$ is a set of final states. For any
infinite word $w=w_{0}w_{1}\ldots$ we call $q_{0}q_{1}\ldots\in Q^{\omega}$ a
_path_ over $w$ if $q_{0}\in Q_{0}$ and for all $i$,
$q_{i+1}\in\delta(q_{i},w_{i})$. We call $q_{0}q_{1}\ldots$ a _final path_ if
$\mathit{infinite}(q_{0}q_{1}\ldots)\cap F\neq\emptyset$, where
$\mathit{infinite}(q_{0}q_{1}\ldots)$ denotes the set of states in $Q$ that
occur infinitely often in the path. We will write
$\mathit{FinalPaths}_{\mathcal{A}}(w)$ to denote the set of final paths of an
automaton $\mathcal{A}$ over a word $w$. The _language_ of an NBA is the set
of those words $w$ such that
$\mathit{FinalPaths}_{\mathcal{A}}(w)\neq\emptyset$. A $k$-ABA is an NBA such
that for every word $w$, $|\mathit{FinalPaths}_{\mathcal{A}}(w)|\leq k$. For
the rest of the section, fix a $k$-ambiguous NBA
$\mathcal{A}_{k}=(Q,\Sigma,\delta,Q_{0},F)$.

We have that $k$-ABAs can be exponentially more succinct than equivalent IBAs:

###### Lemma 4

Let $\mathcal{A}$ be a $k$-ABA with $n$ states. The minimal IBA accepting the
same language as $\mathcal{A}$ may require at least $2^{n}$ states, even if
$k=n$.

###### Proof

By Proposition 4, there exists a family of $n$-ambiguous NFAs with
exponentially fewer states than the minimal IFAs accepting the same languages.
Let $\mathcal{A}$ be such an NFA on $n$ states, and let $L\subseteq\Sigma^{*}$
be its language. Consider the language $(L)_{\$}$ given by $w\in(L)_{\$}$ if
and only if $w$ can be decomposed as $u\$v$, where $\$$ does not occur in
$\Sigma$ and $u\in L$. We can create an $n$-ABA that accepts this language
with $n+1$ states by adding a $\$$-labeled arrow from the final states of
$\mathcal{A}$ to an accepting sink state. However, let $\mathcal{A}^{\prime}$
be any IBA accepting $(L)_{\$}$. Let $\$w$ be any infinite word starting in
$\$$, and let $\eta_{q}=L_{\mathcal{A^{\prime}}[q]}(\$w)$. Let
$\mathcal{A^{\prime\prime}}$ be IFA defined as follows: the state set of
$\mathcal{A^{\prime\prime}}$ is equal to the state set of
$\mathcal{A^{\prime}}$, the alphabet is the alphabet of $\mathcal{A}$ (i.e.
the alphabet of $\mathcal{A^{\prime}}$ without $\$$), there exists an $a$-edge
between two states $q,q^{\prime}$ if and only if there exists an $a$-edge
between $q$ and $q^{\prime}$ in $\mathcal{A^{\prime}}$, and the final vector
is given by $\eta$. We claim that $\mathcal{A^{\prime\prime}}$ accepts $L$.
Indeed, we have
$L_{\mathcal{A^{\prime\prime}}}(u)=L_{\mathcal{A^{\prime}}}(u\$w)$. Hence,
$\mathcal{A^{\prime}}$ has at least $2^{n}$ states, because otherwise
$\mathcal{A^{\prime\prime}}$ would be an IFA with fewer than $2^{n}$ states
accepting $L$. ∎

The rest of this section will be dedicated to converting $k$-ABAs to
equivalent IBAs, resulting in an IBA with at most a singly exponential state
set size blowup.

By the binomial theorem, $(1+x)^{n}=\sum_{i=0}^{n}{n\choose i}x^{i}$, and
hence, setting $x=-1$, $1=1-\sum_{i=0}^{n}(-1)^{i}{n\choose
i}=1-(-1)^{0}{n\choose 0}-\sum_{i=1}^{n}(-1)^{i}{n\choose
i}=\sum_{i=1}^{n}(-1)^{i-1}{n\choose i}$. Hence, for any set $S$,
$\sum_{S^{\prime}\in\mathcal{P}(S)\setminus\\{\emptyset\\}}(-1)^{|S^{\prime}|-1}=\sum_{i=1}^{|S|}(-1)^{i-1}{|S|\choose
i}=1$. Let $R$ be the set of final paths of $\mathcal{A}_{k}$ over a word $w$.
We can design an (infinite state) IBA
$\mathcal{A}_{k}^{\prime}=(Q^{\prime},\Sigma,\Delta^{\prime},\alpha,F^{\prime})$
where final paths correspond to subsets of $R$, and where for each
$R^{\prime}\subseteq R$, the final path corresponding to $R^{\prime}$ has
weight $(-1)^{|R^{\prime}|-1}$. This IBA is given as follows:

  * •

$Q^{\prime}=\mathcal{P}^{\leq
k}(Q^{*}\times\mathbb{B})\setminus\\{\emptyset\\}$,

  * •

$\alpha_{P}=(-1)^{|P|-1}$ for each
$P\in\mathcal{P}(Q_{0}\times\\{\bot\\})\setminus\\{\emptyset\\}$ and
$\alpha_{P}=0$ otherwise,

  * •

$F^{\prime}=\mathcal{P}(Q^{*}\times\\{\top\\})$, and

  * •

for any $P\in Q^{\prime}$, let $b^{\prime\prime}=\bot$ if for all $(r,b)\in
P$, $b=\top$, and let $b^{\prime\prime}=\top$ otherwise. Let $P^{\prime}$ be
such that:

    * –

For any $(r,b)\in P$, there exists $(r^{\prime},b^{\prime})\in P^{\prime}$ and
$q\in\delta(\mathord{last}(r),a)$ such that $r^{\prime}=r\cdot q$ and
$b^{\prime}=((\mathord{last}(r)\in F)\vee b)\wedge b^{\prime\prime}$, and

    * –

For any $(r^{\prime},b^{\prime})\in P^{\prime}$, there exists $(r,b)\in P$ and
$q\in\delta(\mathord{last}(r),a)$ such that $r^{\prime}=r\cdot q$ and
$b^{\prime}=((\mathord{last}(r)\in F)\vee b)\wedge b^{\prime\prime}$.

Then $\Delta(a)_{P,P^{\prime}}=(-1)^{|P^{\prime}|-|P|}$. For any other
$P^{\prime}$, $\Delta(a)_{P,P^{\prime}}=0$.

Intuitively, the bit $b$ in a $(r,b)$-tuple flips to true every time $r$
reaches a final state, and back to false every time all the prefixes have
reached a final state. This ensures that every sequence of prefixes in a final
path of $\mathcal{A}_{k}^{\prime}$ visits final states infinitely often. This
technique mirrors for instance Safra’s construction [27].

$q_{1}$start$q_{2}$start$q_{3}$$q_{4}$$q_{5}$$\\{(q_{1},\bot)\\}$start$\\{(q_{1}q_{3},\bot)\\}$$\\{(q_{1}q_{3}q_{4},\bot)\\}$$\\{(q_{1}q_{3}q_{5},\bot)\\}$$\\{(q_{0}q_{3}q_{4},\bot)$$(q_{0}q_{3}q_{5},\bot)\\}$$\\{(q_{0}q_{3}q_{4}q_{4},\top)\\}$$\\{(q_{0}q_{3}q_{5}q_{5},\top)\\}$$\\{(q_{0}q_{3}q_{4}q_{4},\top)$$(q_{0}q_{3}q_{5}q_{5},\top)\\}$$\\{(q_{2},\bot)\\}$start$\\{(q_{2}q_{3},\bot)\\}$$\\{(q_{2}q_{3}q_{4},\bot)\\}$$\\{(q_{2}q_{3}q_{5},\bot)\\}$$\\{(q_{2}q_{3}q_{4},\bot)$$(q_{2}q_{3}q_{5},\bot)\\}$$\\{(q_{2}q_{3}q_{4}q_{4},\top)\\}$$\\{(q_{2}q_{3}q_{5}q_{5},\top)\\}$$\\{(q_{2}q_{3}q_{4}q_{4},\top)$$(q_{2}q_{3}q_{5}q_{5},\top)\\}$$\\{(q_{1},\bot)$$(q_{2},\bot)\\}$start-1$\\{(q_{1}q_{3},\bot),$$(q_{2}q_{3},\bot)\\}$$\\{(q_{1}q_{3}q_{4},\bot),$$(q_{2}q_{3}q_{4},\bot)\\}$$\\{(q_{1}q_{3}q_{4},\bot),$$(q_{2}q_{3}q_{5},\bot)\\}$$\\{(q_{1}q_{3}q_{4},\bot),$$(q_{2}q_{3}q_{4},\bot)$$(q_{2}q_{3}q_{5},\bot)\\}$$\\{(q_{1}q_{3}q_{5},\bot),$$(q_{2}q_{3}q_{4},\bot)\\}$$\\{(q_{1}q_{3}q_{5},\bot),$$(q_{2}q_{3}q_{5},\bot)\\}$$\\{(q_{1}q_{3}q_{5},\bot),$$(q_{2}q_{3}q_{4},\bot)$$(q_{2}q_{3}q_{5},\bot)\\}$$\\{(q_{1}q_{3}q_{4},\bot),$$(q_{1}q_{3}q_{5},\bot),$$(q_{2}q_{3}q_{4},\bot)\\}$$\\{(q_{1}q_{3}q_{4},\bot),$$(q_{1}q_{3}q_{5},\bot),$$(q_{2}q_{3}q_{5},\bot)\\}$$\\{(q_{1}q_{3}q_{4},\bot),$$(q_{1}q_{3}q_{5},\bot),$$(q_{2}q_{3}q_{4},\bot),$$(q_{2}q_{3}q_{5},\bot)\\}$$\\{(q_{1}q_{3}q_{4}q_{4},\top),$$(q_{2}q_{3}q_{4}q_{4},\top)\\}$$\\{(q_{1}q_{3}q_{4}q_{4},\top),$$(q_{2}q_{3}q_{5}q_{5},\top)\\}$$\\{(q_{1}q_{3}q_{4}q_{4},\top),$$(q_{2}q_{3}q_{4}q_{4},\top)$$(q_{2}q_{3}q_{5}q_{5},\top)\\}$$\\{(q_{1}q_{3}q_{5}q_{5},\top),$$(q_{2}q_{3}q_{4}q_{4},\top)\\}$$\\{(q_{1}q_{3}q_{5}q_{5},\top),$$(q_{2}q_{3}q_{5}q_{5},\top)\\}$$\\{(q_{1}q_{3}q_{5}q_{5},\top),$$(q_{2}q_{3}q_{4}q_{4},\top)$$(q_{2}q_{3}q_{5}q_{5},\top)\\}$$\\{(q_{1}q_{3}q_{4}q_{4},\top),$$(q_{1}q_{3}q_{5}q_{5},\top),$$(q_{2}q_{3}q_{4}q_{4},\top)\\}$$\\{(q_{1}q_{3}q_{4}q_{4},\top),$$(q_{1}q_{3}q_{5}q_{5},\top),$$(q_{2}q_{3}q_{5}q_{5},\top)\\}$$\\{(q_{1}q_{3}q_{4}q_{4},\top),$$(q_{1}q_{3}q_{5}q_{5},\top),$$(q_{2}q_{3}q_{4}q_{4},\top),$$(q_{2}q_{3}q_{5}q_{5},\top)\\}$………………………………………-1-1-1-1-1-1
Figure 2: An example $4$-ambiguous automaton (above) and its infinite IBA
counterpart (below). In the IBA, the weights of the unlabeled edges are 1.

In Figure 2 we give an example of a 4-ambiguous automaton over a unary
alphabet, together with the corresponding infinite $\mathcal{A}_{k}^{\prime}$.

###### Lemma 5

$\mathcal{A}_{k}^{\prime}$ is an infinite-state IBA equivalent to
$\mathcal{A}_{k}$.

###### Proof

For $\mathcal{A}_{k}^{\prime}$ to be an IBA equivalent to $\mathcal{A}_{k}$,
it needs to satisfy three properties - the edges of $\mathcal{A}_{k}^{\prime}$
over loops have weight 1, any word $w$ has at most $N$ final paths for some
global bound $N$, and the sum of the weights of final paths over $w$ is 1 if
$w$ is accepted by $\mathcal{A}_{k}$ and 0 otherwise. Since states in a path
of $\mathcal{A}_{k}^{\prime}$ consist of sets of prefixes of increasing
length, we see that $\mathcal{A}_{k}^{\prime}$ does not have any loops and
hence the first property is trivially true. For the second and third
properties, let $w$ be any fixed word.

Suppose $w$ is not accepted by $\mathcal{A}_{k}$, then by König’s lemma there
exists a bound $m$ such that any path of $\mathcal{A}_{k}$ over $w$ has at
most $m$ occurences of final states. Let $\rho_{1}\rho_{2}\ldots\rho_{i}$ be
any prefix of a path of $\mathcal{A}_{k}^{\prime}$ over $w$. Since for any
$(r,b)\in\rho_{i}$, $r$ has at most $m$ occurrences of final states, and all
the bits are flipped to false any time every prefix in
$\rho_{1}\rho_{2}\ldots\rho_{i}$ has visited a final state, we see that
$\rho_{1}\rho_{2}\ldots\rho_{i}$ also visits final states at most $m$ times.
Therefore, $\mathcal{A}_{k}^{\prime}$ has no final paths (and hence the sum of
the weights is 0) and the second and third properties are true.

Suppose, then, that $w$ is accepted by $\mathcal{A}_{k}$. Let
$\rho_{1}\rho_{2}\ldots$ be a path of $\mathcal{A}_{k}^{\prime}$ over $w$.
Suppose that for some $i$ there exists $(r,b)\in\rho_{i}$ such that $r$ is not
a prefix of a final path of $\mathcal{A}_{k}$ over $w$. Let $r$ be the
shortest such prefix. Then for large enough $m$ and any $m^{\prime}>m$ there
exists $(r^{\prime},\bot)\in\rho_{m^{\prime}}$ where $r$ is a prefix of
$r^{\prime}$. Hence, $\rho_{m^{\prime}}\not\in F^{\prime}$ and
$\rho_{1}\rho_{2}\ldots$ is not a final path.

Finally, let $\rho_{1}\rho_{2}\ldots$ be a path of $\mathcal{A}_{k}^{\prime}$
over $w$ such that for every $i$ and every $(r,b)\in\rho_{i}$, $r$ is a prefix
of a final path of $\mathcal{A}_{k}$ over $w$. Let $R$ be the set of those
paths $\rho^{\prime}$ of $\mathcal{A}_{k}$ over $w$ such that for all $i$
there exists a tuple $(r,b)\in\rho_{i}$ where $r$ is a prefix of
$\rho^{\prime}$. We have that for any $i$ and any $(r,b)\in\rho_{i}$ there
exists $(r^{\prime},b^{\prime})\in\rho_{i+1}$ such that $r^{\prime}=r\cdot q$
with $q\in\delta(\mathord{last}(r),w_{i})$ and for any
$(r^{\prime},b^{\prime})\in\rho_{i+1}$ there exists $(r,b)\in\rho_{i}$ such
that $r^{\prime}=r\cdot q$ with $q\in\delta(\mathord{last}(r),w_{i})$.
Therefore $R$ is nonempty and $\rho_{i}$ is precisely the set of prefixes of
length $i$ of paths in $R$ (paired with some boolean $b$). Hence, paths
$\rho_{1}\rho_{2}\ldots$ in $\mathcal{A}_{k}^{\prime}$ over $w$ correspond
uniquely to sets of paths of $\mathcal{A}_{k}$ over $w$.

We claim that $R$ is a set of final paths, and that the weight of
$\rho_{1}\rho_{2}\ldots$ is $(-1)^{|R|-1}$. Indeed, suppose
$\rho^{\prime}_{1}\rho^{\prime}_{2}\ldots\in R$ is not a final path. Since for
any $i$, $\rho^{\prime}_{1}\rho^{\prime}_{2}\ldots\rho^{\prime}_{i}$ prefixes
a final path, there exists $j>i$ such that
$\rho^{\prime}_{1}\rho^{\prime}_{2}\ldots\rho^{\prime}_{i}$ is a prefix of a
final path $\rho^{\prime\prime}_{1}\rho^{\prime\prime}_{2}\ldots$, and
$\rho^{\prime\prime}_{j}\neq\rho^{\prime}_{j}$. Hence $\mathcal{A}_{k}$ has
infinitely many final paths over $w$, which contradicts its $k$-ambiguity.
Moreover, the weight of any prefix of length $i$ of $\rho_{1}\rho_{2}\ldots$
is
$(-1)^{|\rho_{1}|-1}\prod_{j}(-1)^{|\rho_{j+1}|-|\rho_{j}|}=(-1)^{|\rho_{i}|-1}$.
Since the size of $\rho_{i}$ is non-decreasing and bounded from above by $k$,
and for any $i$, $\rho_{i}$ contains prefixes of length $i$ of paths in $R$,
for large enough $i$ we have that $|\rho_{i}|=|R|$, and hence the weight of
$\rho_{1}\rho_{2}\ldots$ is $(-1)^{|R|-1}$.

Thus, final paths in $\mathcal{A}_{k}^{\prime}$ over $w$ correspond uniquely
to sets of final paths in $\mathcal{A}_{k}$ over $w$, and hence there are at
most $2^{k}$ final paths in $\mathcal{A}_{k}^{\prime}$ over $w$. Moreover,
since by the binomial theorem we have $\sum_{i=1}^{|S|}(-1)^{i-1}{|S|\choose
i}=1$ for any set $S$, and any path in $\mathcal{A}_{k}^{\prime}$
corresponding to a set $R$ of final paths in $\mathcal{A}_{k}$ has weight
$(-1)^{|R|-1}$, we see that the sum of the weights of final paths of
$\mathcal{A}_{k}^{\prime}$ over $w$ is precisely equal to 1 if and only if
$\mathcal{A}_{k}$ has an accepting path over $w$. ∎

We will construct a finite IBA called the $k$-disambiguation of
$\mathcal{A}_{k}$ based on $\mathcal{A}_{k}^{\prime}$ that accepts the same
language as $\mathcal{A}_{k}$.

Let $\pi_{\mathord{last}}:Q^{\prime}\rightarrow[k]^{Q\times\mathbb{B}}$ be
defined as $\pi_{\mathord{last}}(P)_{q,b}=|\\{(r,b)\in
P\mid\mathord{last}(r)=q\\}|$. We extend $\pi_{\mathord{last}}$ over finite
and infinite sequences of elements of $Q^{\prime}$ in the natural way:
$\pi_{\mathord{last}}(P_{1}P_{2}\ldots)=\pi_{\mathord{last}}(P_{1})\cdot\pi_{\mathord{last}}(P_{2}\ldots)$.

###### Lemma 6

Let $\rho=\rho_{1}\rho_{2}\ldots\in(Q^{\prime})^{\omega}$ be a path of
$\mathcal{A}_{k}^{\prime}$ over a word $w$ and let
$\rho^{\prime}_{1}\rho^{\prime}_{2}\ldots=\pi_{\mathord{last}}(\rho)$. Then
$\rho_{1}\rho_{2}\ldots$ is final if and only if for infinitely $i$,
$(\rho^{\prime}_{i})_{q,\bot}=0$ for all $q\in Q$.

###### Proof

Trivial. ∎

Paths in our $k$-disambiguation will be sequences in
$([k]^{Q\times\mathbb{B}})^{\omega}$ such that there exist paths in
$\mathcal{A}_{k}^{\prime}$ that map to that sequence. However, there is not a
one-to-one correspondence between sequences over $[k]^{Q\times\mathbb{B}}$ and
paths in $\mathcal{A}_{k}^{\prime}$: in Figure 2, for instance, both
$\\{(q_{1},\bot),(q_{2},\bot)\\}$ $\\{(q_{1}q_{3},\bot),(q_{2}q_{3},\bot)\\}$
$\\{(q_{1}q_{3}q_{4},\bot),(q_{2}q_{3}q_{5},\bot)\\}$
$\\{(q_{1}q_{3}q_{4}q_{4},\top),(q_{2}q_{3}q_{5}q_{5},\top)\\}\ldots$ and
$\\{(q_{1},\bot),(q_{2},\bot)\\}$ $\\{(q_{1}q_{3},\bot),(q_{2}q_{3},\bot)\\}$
$\\{(q_{1}q_{3}q_{5},\bot),(q_{2}q_{3}q_{4},\bot)\\}$
$\\{(q_{1}q_{3}q_{5}q_{5},\top),(q_{2}q_{3}q_{4}q_{4},\top)\\}\ldots$ map to
the sequence $(1,1,0,0,0,0,0,0,0,0)^{\top}$ $(0,0,2,0,0,0,0,0,0,0)^{\top}$
$((0,0,0,1,1,0,0,0,0,0)^{\top}$ $(0,0,0,0,0,0,0,0,1,1)^{\top})^{\omega}$,
where the order of the vector components is given by
$((q_{1},\bot),(q_{2},\bot),(q_{3},\bot),(q_{4},\bot),(q_{5},\bot),(q_{1},\top),(q_{2},\top),(q_{3},\top),(q_{4},\top),(q_{5},\top))$.

Fix any $\vec{r},\vec{r^{\prime}}\in[k]^{Q\times\mathbb{B}}$ and $a\in\Sigma$.
Let $P$ be any state in $Q^{\prime}$ such that
$\pi_{\mathord{last}}(P)=\vec{r}$. As it turns out, the number of states
$P^{\prime}$ with $\pi_{\mathord{last}}(P^{\prime})=\vec{r^{\prime}}$ where
$P^{\prime}$ is an $a$-successor of $P$ only depends on $\vec{r}$, $a$, and
$\vec{r^{\prime}}$. We call this number $w(\vec{r},a,\vec{r^{\prime}})$.

###### Lemma 7

The number $w(\vec{r},a,\vec{r^{\prime}})$ is unique and at most exponential
in $k$.

###### Proof

Given $\vec{r},\vec{r^{\prime}}\in[k]^{Q\times\mathcal{B}}$ and $a\in\Sigma$,
let

$\displaystyle
C=\\{f:Q\times\mathcal{B}\times[k]\rightarrow\mathcal{P}(Q)\mid$
$\displaystyle\forall(q,b,i)\in Q\times\mathcal{B}\times[k]:$
$\displaystyle((i>\vec{r}_{q,b})\rightarrow f(q,b,i)=\emptyset)\land$
$\displaystyle((i\leq\vec{r}_{q,b})\rightarrow
f(q,b,i)\in\mathcal{P}(\delta(q,a))\setminus\\{\emptyset\\})\\}.$

Intuitively, functions in $C$ map the final states of prefixes in a state $P$
with $\pi_{\mathord{last}}(P)=\vec{r}$ to nonempty sets of successor states.
Let $b^{\prime\prime}=\bot$ if $b=\top$ for all $(r,b)\in P$, and let
$b^{\prime\prime}=\top$ otherwise. Let $C^{\prime}$ be the set of those $f\in
C$ such that for any $(q^{\prime},b^{\prime})\in Q\times\mathcal{B}$,
$|\\{(q,b,i)\in Q\times\mathcal{B}\times[k]\mid(b^{\prime}=(q\in F\lor b)\land
b^{\prime\prime})\land q^{\prime}\in
f(q,b,i)\\}|=\vec{r^{\prime}}_{q^{\prime},b^{\prime}}$. We claim that
$w(\vec{r},a,\vec{r^{\prime}})=|C^{\prime}|$.

Fix an ordering on $Q^{*}$. Since $\pi_{\mathord{last}}(P)=\vec{r}$, we see
that for any $q\in Q,b\in\mathcal{B}$ there are $\vec{r}_{q,b}$ tuples $(s,b)$
in $P$ where $\mathord{last}(s)=q$. Let $s_{q,b,i}$ denote the $i$’th (under
the ordering on $Q^{*}$) path in $P$ that is paired with bit $b$ and ends in
state $q$. Then for any $f\in C$, $f(q,b,i)$ is a nonempty set of
$a$-successors of $q$. Let $b^{\prime\prime}=\bot$ if $b^{\prime}=\top$ for
every $(s^{\prime},b^{\prime})\in P$ and let $b^{\prime\prime}=\bot$
otherwise. If $q\in F$, let $b^{\prime}=\top\land b^{\prime\prime}$, and
otherwise let $b^{\prime}=b\land b^{\prime\prime}$. Hence, for any $f\in C$
the following is an $a$-successor of $P$ in $\mathcal{A}_{k}^{\prime}$:

$P^{\prime}=\left\\{(s_{q,b,i}\cdot q^{\prime},b^{\prime})\mid(s_{q,b,i},b)\in
P\land q^{\prime}\in f(q,b,i)\right\\}.$

If $f\in C^{\prime}$, then by definition of $C^{\prime}$, for any
$q^{\prime},b^{\prime}$,
$\pi_{\mathord{last}}(P^{\prime})_{q^{\prime},b^{\prime}}=\vec{r^{\prime}}_{q^{\prime},b^{\prime}}$,
and hence $\pi_{\mathord{last}}(P^{\prime})=\vec{r^{\prime}}$. Since each
$f\in C$ gives rise to a unique successor, this means $P$ has $|C^{\prime}|$
$a$-successors $P^{\prime}$ with
$\pi_{\mathord{last}}(P^{\prime})=\vec{r^{\prime}}$. Moreover,
$|C^{\prime}|\leq|C|\leq 2^{2k|Q|^{2}}$. ∎

For a state $\vec{r}\in Q^{\prime\prime}$ we will write
$\mathord{size}(\vec{r})=\sum_{(q,b)}\vec{r}_{q,b}$ to denote the size of
$\vec{r}$. We define the IBA
$\operatorname{\mathnormal{k}-dis}^{\prime}(\mathcal{A}_{k})=(Q^{\prime\prime},\Sigma,\Delta^{\prime\prime},\alpha^{\prime},F^{\prime\prime})$
where:

  * •

$Q^{\prime\prime}=([k]^{Q\times\mathbb{B}})\setminus\\{\vec{0}\\}$,

  * •

$\Delta^{\prime\prime}(a)_{\vec{r},\vec{r^{\prime}}}=(-1)^{\mathord{size}(\vec{r^{\prime}})-\mathord{size}(\vec{r})}w(\vec{r},a,\vec{r^{\prime}})$

  * •

$\alpha^{\prime}_{\vec{r}}=(-1)^{\mathord{size}(\vec{r})-1}$ for every
$\vec{r}$ with:

    * –

$\vec{r}_{q,b}=0$ if $q\not\in Q_{0}$ or $b=\top$, and

    * –

$\vec{r}_{q,b}\leq 1$ otherwise.

$\alpha^{\prime}_{\vec{r}}=0$ otherwise.

  * •

$F^{\prime\prime}=\\{\vec{r}\in Q^{\prime\prime}\mid\forall(q,\bot)\in
Q^{\prime\prime}:\vec{r}_{q,\bot}=0\\}$.

$\\{(q_{1},\bot)\\}$start$\\{(q_{2},\bot)\\}$start$\\{q_{3},\bot)\\}$$\\{(q_{4},\bot)\\}$$\\{(q_{4},\top)\\}$$\\{(q_{5},\bot)\\}$$\\{(q_{5},\top)\\}$$\\{(q_{4},\bot),(q_{5},\bot)\\}$$\\{(q_{4},\top),(q_{5},\top)\\}$-1$\\{(q_{1},\bot),(q_{2},\bot)\\}$start-1$\\{(q_{3},\bot),(q_{3},\bot)\\}$$\\{q_{5},\bot),(q_{5},\bot)\\}$$\\{(q_{5},\top),(q_{5},\top)\\}$$\\{(q_{4},\bot),(q_{5},\bot)\\}$$\\{(q_{4},\top),(q_{5},\top)\\}$$\\{(q_{4},\bot),(q_{5},\bot)$$(q_{5},\bot)\\}$$\\{(q_{4},\top),(q_{5},\top)$$(q_{5},\top)\\}$$\\{(q_{4},\bot),(q_{4},\bot)\\}$$\\{(q_{4},\top),(q_{4},\top)\\}$$\\{(q_{4},\bot),(q_{4},\bot)$$(q_{5},\bot)\\}$$\\{(q_{4},\top),(q_{4},\top)$$(q_{5},\top)\\}$$\\{(q_{4},\bot),(q_{4},\bot)$$(q_{5},\bot),(q_{5},\bot)\\}$$\\{(q_{4},\top),(q_{4},\top)$$(q_{5},\top),(q_{5},\top)\\}$2-2-2
Figure 3: The $k$-disambiguation of the automaton in Figure 2. The elements of
$[k]^{Q\times\mathbb{B}}$ are represented by multisets. Unlabeled edges have
weight 1.

The IBA $\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ (the
$k$-disambiguation of $\mathcal{A}_{k}$) is then defined as
$\operatorname{\mathnormal{k}-dis}^{\prime}(\mathcal{A}_{k})$ restricted to
those reachable states in $Q^{\prime\prime}$ that can reach a loop over a
final state. This trimness condition helps the proofs later on, but could be
omitted. In Figure 3 we see the $k$-disambiguation of the automaton in Figure
2.

The weights in $\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ count the
number of equivalent paths in $\mathcal{A}_{k}^{\prime}$, where two paths
$\rho,\rho^{\prime}\in(Q^{\prime})^{\omega}$ are equivalent if
$\pi_{\mathord{last}}(\rho)=\pi_{\mathord{last}}(\rho^{\prime})$:

###### Lemma 8

Let $\rho\in(Q^{\prime\prime})^{\omega}$ be a path in
$\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ over a word $w$. Let $R$
be the set of those paths $\rho^{\prime}$ in $\mathcal{A}_{k}^{\prime}$ over
$w$ such that $\pi_{\mathord{last}}(\rho^{\prime})=\rho$, and let
$n=\max_{i}\mathord{size}(\rho_{i})$. Then
$\mathord{weight}(\rho)=(-1)^{n-1}|R|$.

###### Proof

Let $R_{i}$ be the set of prefixes of length $i$ of paths in $R$. Let
$\rho^{\prime}_{i}$ be any path in $R_{i}$. By Lemma 7, $\rho^{\prime}_{i}$
has $w(\rho_{i},w_{i},\rho_{i+1})$ $w_{i}$-successors that map to $\rho_{i+1}$
under $\pi_{\mathord{last}}$. Hence,
$|R_{i+1}|=w(\rho_{i},w_{i},\rho_{i+1})|R_{i}|$ and in particular,
$|R|=\lim_{n\to\infty}\prod_{i=1}^{n}w(\rho_{i},w_{i},\rho_{i+1})$. Moreover,
$\lim_{n\to\infty}(-1)^{\mathord{size}(\rho_{1})-1}\prod_{i=1}^{n}(-1)^{\mathord{size}(\rho_{i+1})-\mathord{size}(\rho_{i})}=(-1)^{n-1}$,
and hence
$\mathord{weight}(\rho)=\lim_{n\to\infty}(-1)^{\mathord{size}(\rho_{1})-1}\prod_{i=1}^{n}(-1)^{\mathord{size}(\rho_{i+1})-\mathord{size}(\rho_{i})}w(\rho_{i},w_{i},\rho_{i+1})=(-1)^{n-1}|R|$.
∎

Since by Lemma 6, a path $\rho$ in
$\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ is final whenever any
path $\rho^{\prime}$ in $\mathcal{A}_{k}^{\prime}$ with
$\pi_{\mathord{last}}(\rho^{\prime})=\rho$ is, this means
$L_{\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})}=L_{\mathcal{A}_{k}^{\prime}}$.
This proves the final result:

###### Theorem 3.1

$\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ is an IBA that accepts
the same language as $\mathcal{A}_{k}$.

###### Proof

We will prove equivalence between $\mathcal{A}_{k}^{\prime}$ and
$\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$. Combined with Lemma 5,
this gives us the required result. As before, we need to show that the edges
of $\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ over loops have weight
1, any word $w$ has at most $N$ final paths for some global bound $N$, and the
sum of the weights of final paths over $w$ is 1 if $w$ is accepted by
$\mathcal{A}_{k}^{\prime}$ and 0 otherwise.

Pick any loop in $\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ and any
$a$-edge from any $\vec{r}$ to any $\vec{r^{\prime}}$. Note that
$w(\vec{r},a,\vec{r^{\prime}})>0$ implies that
$\mathord{size}(\vec{r})\leq\mathord{size}(\vec{r^{\prime}})$ and hence for
any $\vec{r},\vec{r^{\prime}}$ on that loop,
$\mathord{size}(\vec{r})=\mathord{size}(\vec{r^{\prime}})$. Let $w_{1}\ldots
w_{m}$ be such that there exists a path from an initial state to $\vec{r}$,
and let $w_{m+1}\ldots w_{n}$ be a word that traverses the loop starting with
this edge from $\vec{r}$ to $\vec{r^{\prime}}$ (hence, $w_{m+1}=a$). Finally
let $w_{n+1}w_{n+2}\ldots$ be a word such that $w_{1}\ldots
w_{m}(w_{m+1}\ldots w_{n})^{C}w_{n+1}\ldots$ has a final path that traverses
the loop over $\vec{r}$ at least $C$ times, such a word exists since every
state can reach a loop over a final state. Note that weights in
$\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ are integers. Then the
absolute weight of this path is at least
$w(\vec{r},w_{m+1},\vec{r^{\prime}})^{C}$. Using Lemmas 8 and 6, then, we see
that there exist at least $w(\vec{r},w_{m+1},\vec{r^{\prime}})^{C}$ final
paths over $w_{1}\ldots w_{m}(w_{m+1}\ldots w_{n})^{C}w_{n+1}\ldots$. Since
this is the case for any $C$, and the number of final paths over any word in
$\mathcal{A}_{k}^{\prime}$ is bounded above, we must have that
$w(\vec{r},w_{m+1},\vec{r^{\prime}})=1$ and hence
$\Delta(a)_{\vec{r},\vec{r^{\prime}}}=1$.

Now let $w$ be any word. By Lemma 6 a path in $\mathcal{A}_{k}^{\prime}$ is
final if and only if the path in
$\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ it maps to under
$\pi_{\mathord{last}}$ is final, and by Lemma 8 any path with nonzero weight
(i.e. any path) has at least one path in $\mathcal{A}_{k}^{\prime}$ mapping to
it. Hence we see that $\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ has
at most as many final paths over $w$ as $\mathcal{A}_{k}^{\prime}$ does, and
since the number of final paths in $\mathcal{A}_{k}^{\prime}$ is globally
bounded, so is the number of final paths in
$\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$.

Let $w$ be any word and define the equivalence relation $=_{\pi}\subseteq
Q^{\prime\omega}\times Q^{\prime\omega}$ as $\rho=_{\pi}\rho^{\prime}$ iff
$\pi_{\mathord{last}}(\rho)=\pi_{\mathord{last}}(\rho^{\prime})$ (note that
$\pi_{\mathord{last}}(\rho)\in([k]^{Q\times\mathbb{B}})^{\omega}$). Note that
this equivalence relation partitions the final paths of
$\mathcal{A}_{k}^{\prime}$ over $w$, and for any $\rho,\rho^{\prime}$ with
$\rho=_{\pi}\rho^{\prime}$,
$\mathord{weight}(\rho)=\mathord{weight}(\rho^{\prime})=(-1)^{\lim_{i\to\infty}|\rho_{i}|}$.
Each equivalence class can be represented by a path in
$\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$. Let $\rho^{\prime}$ be
the representative of the equivalence class containing $\rho$, and let $R$ be
the size of this equivalence class. By Lemma 8,
$\mathord{weight}(\rho^{\prime})=\mathord{weight}(\rho)R$. Hence, the sum of
the weights of final paths in
$\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ is equal to the sum of
the weights of all the equivalence classes of $=_{\pi}$ where the
representative is a final path, which by Lemma 6 is precisely the sum of the
weights of final paths in $\mathcal{A}_{k}^{\prime}$.

Hence, the weight of a word $w$ in
$\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ is equal to the weight of
$w$ in $\mathcal{A}_{k}^{\prime}$. This means
$\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ is equivalent to
$\mathcal{A}_{k}^{\prime}$ which is in turn equivalent to $\mathcal{A}_{k}$,
concluding the proof. ∎

###### Theorem 3.2

Given a $k$-ambiguous automaton $\mathcal{A}_{k}$ with $n$ states, the
disambiguation $\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ has at
most $k^{2n}$ states. Moreover,
$\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ can be calculated using a
PSPACE transducer.

###### Proof

The number of states follows from the size of $[k]^{Q\times\mathcal{B}}$. Note
that $k$ is at most singly exponential in the size of the state set of the
automaton, which follows from for instance [31, Theorem 2.1], or the fact that
finite ambiguity implies the nonexistence of diamonds on a loop. This means
that $k^{2n}$ is also singly exponential in $n$. Hence, we can iterate over
every element in $Q^{\prime\prime}$, each of which is a vector in
$[k]^{Q\times\mathcal{B}}$ which can be represented in polynomial space. Given
$\vec{r},\vec{r^{\prime}}\in Q^{\prime\prime}$ and $a\in\Sigma$, to calculate
$\Delta^{\prime\prime}(a)_{\vec{r},\vec{r^{\prime}}}$ we need to calculate
$(-1)^{\mathord{size}(\vec{r^{\prime}})-\mathord{size}(\vec{r})}$ and
$w(\vec{r},a,\vec{r^{\prime}})$. Clearly the former can be calculated in
polynomial space. For the latter, notice that $w(\vec{r},a,\vec{r^{\prime}})$
can be doubly exponential, requiring an exponential representation. Hence, we
cannot simply list the edges between states in $\mathcal{A}_{k}^{\prime}$ to
calculate $w(\vec{r},a,\vec{r^{\prime}})$. However, we have the following
lemma:

###### Lemma 9

Let $w(\vec{r},a,\vec{r^{\prime}})$ as defined above, let
$b^{\prime\prime}=\bot$ if $\vec{r}_{q,\bot}=0$ for every $q\in Q$ and
$b^{\prime\prime}=\top$ otherwise. For each $(q,b)\in Q\times\mathcal{B}$ let
$C_{q,b}$ denote the set of those
$\vec{r^{\prime}}[q,b]\in[k]^{Q\times\mathcal{B}}$ such that

$\mathord{size}(\vec{r^{\prime}}[q,b])\geq\vec{r}_{q,b}\quad\land\quad\forall(q^{\prime},b^{\prime})\in
Q\times\mathcal{B}\ .\
\vec{r^{\prime}}[q,b]_{q^{\prime},b^{\prime}}\leq\vec{r}_{q,b}\quad\land\\\
\forall(q^{\prime},b^{\prime})\in Q\times\mathcal{B}\ .\ ((b^{\prime}\neq(q\in
F\lor b)\land b^{\prime\prime})\lor
q^{\prime}\not\in\delta(q,a))\rightarrow\vec{r^{\prime}}[q,b]_{q^{\prime},b^{\prime}}=0\,.$

Let
$\\#\mathord{succ}(q,n,\vec{r^{\prime}}[q,b])=\sum_{j=0}^{n}(-1)^{j}{n\choose
j}\left(\prod_{q^{\prime},b^{\prime}}{n-j\choose\vec{r^{\prime}}[q,b]_{q^{\prime},b^{\prime}}}\right)$.
Then

$w(\vec{r},a,\vec{r^{\prime}})=\sum_{f:Q\times\mathcal{B}\rightarrow
C_{q,b}\mid\sum_{q,b}f(q,b)=\vec{r^{\prime}}}\prod_{q,b}\\#\mathord{succ}(q,\vec{r}_{q,b},f(q,b)).$

###### Proof

We have that $w(\vec{r},a,\vec{r^{\prime}})=|C^{\prime}|$, where $C^{\prime}$
is defined as in Lemma 7. We define the following equivalence relation: two
elements $f,f^{\prime}\in C^{\prime}$ are equivalent if for every $(q,b)\in
Q\times\mathcal{B}$ we have that
$\sum_{i}[[f(q,b,i)]]=\sum_{i}[[f^{\prime}(q,b,i)]]$, where for any set $S$,
$[[S]]$ denotes the characteristic vector of $S$.

Let $\mathcal{G}:=\\{g:Q\times\mathcal{B}\rightarrow
C_{q,b}\;\mid\;\sum_{q,b}g(q,b)=\vec{r^{\prime}}\\}$. Clearly the equivalence
classes of $C^{\prime}$ can be characterised by elements of $\mathcal{G}$. We
can view any function $f\in C^{\prime}$ as a way of distributing non-empty
successor sets over the numbered elements in $\vec{r}$ in such a way that it
adds up to $\vec{r^{\prime}}$. Hence, for any $g\in\mathcal{G}$, the number of
elements in the equivalence class of $g$ is given by those functions that, for
every $(q,b)\in Q\times\mathcal{B}$, distribute the elements in $g(q,b)$ to
the $\vec{r}_{q,b}$ paths ending in $(q,b)$. These distributions are
independent, and hence the number of elements in the equivalence class of $g$
is the product over all $(q,b)$ of the number of ways to distribute the
elements in $g(q,b)$.

This number is captured by $\\#\mathord{succ}(q,\vec{r},g(q,b))$. We will
explain $\\#\mathord{succ}$ as a balls-and-bins problem. We need to assign a
nonempty successor set to each of the $\vec{r}_{q,b}$ paths ending in $(q,b)$
such that for each $(q^{\prime},b^{\prime})\in Q\times\mathcal{B}$ there are
$g(q,b)_{q^{\prime},b^{\prime}}$ sets containing $(q^{\prime},b^{\prime})$.
This is equivalent to dividing
$\sum_{q^{\prime},b^{\prime}}g(q,b)_{q^{\prime},b^{\prime}}$ coloured balls,
with colours in $Q\times\mathcal{B}$, over $\vec{r}_{q,b}$ bins in such a way
that no bin has two balls of the same colour and no bin is empty. We can
express the number of distributions where bins may be empty by distributing
the balls per colour independently, this is given by
$\prod_{q^{\prime},b^{\prime}}{n\choose g(q,b)_{q^{\prime},b^{\prime}}}$ where
$n$ is the number of bins (i.e. $\vec{r}_{q,b}$). Using the inclusion-
exclusion principle, then, we can add the restriction that no bins may be
empty by including/excluding sets of empty bins. This gives us the formula
$\\#\mathord{succ}(q,\vec{r},g(q,b))=\sum_{j=0}^{n}(-1)^{j}{n\choose
j}\left(\prod_{q^{\prime},b^{\prime}}{n-j\choose\vec{r^{\prime}}[q,b]_{q^{\prime},b^{\prime}}}\right)$.

Hence, the number of elements in the equivalence class of $g$ is given by
$\prod_{q,b}\\#\mathord{succ}(q,\vec{r}_{q,b},g(q,b))$ and therefore we have
that
$w(\vec{r},a,\vec{r^{\prime}})=|C^{\prime}|=\sum_{g\in\mathcal{G}}\prod_{q,b}\\#\mathord{succ}(q,\vec{r}_{q,b},g(q,b))$.
∎

Using this lemma,, we can enumerate every vector in $C_{q,b}$ for every
$(q,b)$-pair, which is a polynomial combination of polynomially sized objects.
We can then calculate $\\#\mathord{succ}$ with a PSPACE transducer to find
$w(\vec{r},a,\vec{r^{\prime}})$. Hence, we can construct
$\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ with a PSPACE transducer.
∎

By Lemma 4, we have an $O(2^{n})$ lower bound even if $k=n$. From Theorem 3.2
we already have a $2^{O(n\log n)}$ upper bound, leaving only a small gap.

When the ambiguity is comparatively low, we can do even better:

###### Theorem 3.3

Given a $k$-ambiguous automaton $\mathcal{A}_{k}$ with $n$ states where
$k=O(\log n)$, the disambiguation
$\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ has at most $(2n)^{O(\log
n)}$ states. Moreover, $\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$
can be calculated using a POLYLOGSPACE transducer.

###### Proof

While in general, elements in $[\log n]^{[n]\times\mathbb{B}}$ take $2n\log n$
space to represent, we know that for any $\vec{r}\in Q^{\prime\prime}$,
$\sum_{i}\vec{r}_{i}\leq\log n$ and hence we can instead represent elements in
$Q^{\prime\prime}$ as vectors in $([n]\times\mathbb{B})^{\log n}$, which take
$\log(2n^{\log n})=O((\log n)^{2})$ space. Moreover,
$w(\vec{r},a,\vec{r^{\prime}})$ is at most exponential in the ambiguity of
$\mathcal{A}_{k}$ and hence we can simply enumerate the successors of any
$P\in Q^{\prime}$ with $\pi_{\mathord{last}}(P)=\vec{r}$ in POLYLOGSPACE.
Thus, we can calculate $\operatorname{\mathnormal{k}-dis}(\mathcal{A}_{k})$ in
POLYLOGSPACE. ∎

##  4 Model Checking IBA

In this section we will consider the problem of model checking IBAs against
Markov chains. A _Markov chain_ (MC) is a pair $(S,P)$ where $S$ is the finite
state set, and $P\in[0,1]^{S\times S}$ is a stochastic matrix specifying
transition probabilities. Given an initial distribution $\iota$, an MC
$\mathcal{M}$ induces a probability measure $\Pr^{\mathcal{M}}_{\iota}$ over
infinite words. The model checking question asks, what is the probability of
the language accepted by an IBA?

We show that model checking IBAs against MCs can be done in NC using a
modified procedure for model checking UBAs from [3]. This is the main theorem:

###### Theorem 4.1

Let $\mathcal{M}$ be an MC and let $\mathcal{A}$ be an IBA. The probability
that a random word sampled from $\mathcal{M}$ is in $L_{\mathcal{A}}$ can be
computed in NC.

In order to prove this, we will use the following properties of nonnegative
matrices:

###### Theorem 4.2

Let $M\in\mathbb{R}^{S\times S}$ be a nonnegative matrix. Then the following
all hold:

  1. 1.

The spectral radius $\rho(M)$ is an eigenvalue of $A$ and there is a
nonnegative eigenvector $\vec{x}$ with $M\vec{x}=\rho(M)\vec{x}$. Such a
vector $\vec{x}$ is called _dominant_.

  2. 2.

If $0\leq M^{\prime}\leq M$ then $\rho(M^{\prime})\leq\rho(M)$.

  3. 3.

There is $C\subseteq S$ such that $M_{C,C}$ is strongly connected and
$\rho(M_{C,C})=\rho(M)$.

###### Theorem 4.3

Let $M\in\mathbb{R}^{S\times S}$ be a strongly connected nonnegative matrix.
Then the following all hold:

  1. 1.

There is an eigenvector $\vec{x}$ with $M\vec{x}=\rho(M)\vec{x}$ such that
$\vec{x}$ is strictly positive in all its components.

  2. 2.

The eigenspace associated with $\rho(M)$ is one-dimensional.

  3. 3.

If $0\leq M^{\prime}<M$ (i.e. $M^{\prime}_{i,j}<M_{i,j}$ for some $i,j\in S$)
then $\rho(M^{\prime})<\rho(M)$.

  4. 4.

If $\vec{x}\geq 0$ and $M\vec{x}\leq\rho(M)\vec{x}$ then
$M\vec{x}=\rho(M)\vec{x}$.

These results can all be found in [4, Chapter 2]. We will also need the
following well-known fact about Markov chains.

###### Lemma 10

Let $\mathcal{M}=(S,P)$ be a Markov chain, and $\mathcal{L}\subseteq
S^{\omega}$ an $\omega$-regular language. Suppose $s_{0}\in S$ such that
$\operatorname{\mathit{Pr}}_{s_{0}}>0$. Then there exists $s_{0}\ldots
s_{n}\in\mathit{Paths}_{s_{0}}(P)$ such that
$\operatorname{\mathit{Pr}}_{s_{n}}(\\{w\in s_{n}S^{\omega}:s_{0}\ldots
s_{n-1}w\in\mathcal{L}\\})=1$.

This can be found for instance in [3, Lemma 16].

We will now outline the model checking procedure. As in [3] the algorithm will
consist of solving a system of linear equations, split up in two parts. The
first part is the basic linear system, which we will describe below, while the
second part will add normalising equations in the form of cuts (or pseudo-
cuts, if [18] is followed). Since the weights of the edges within SCCs are all
on loops, and therefore all have weight 1, this part can be copied verbatim
from Baier et al[3]. The difference is in the basic system of equations.

Given an automaton $\mathcal{A}=(Q,\Sigma,M,\alpha,F)$ and Markov chain
$\mathcal{M}=(S,P)$, we will write $\mathcal{A}[q]$ (resp. $\mathcal{M}[s]$)
to denote the weighted automaton (resp. Markov chain) starting in $q\in Q$
(resp. $s\in S$). W.l.o.g. we will assume that every $q\in Q$ is reachable
from some $q^{\prime}$ with $\alpha(q^{\prime})\neq 0$ and every $q\in Q$ can
reach a loop over a final state. Note that while $\mathcal{A}$ is an IBA,
$\mathcal{A}[q]$ does not necessarily have to be. We will write
$\operatorname{\mathbb{E}}_{\mathcal{M}}L_{\mathcal{A}}$ for the expected
weight of a word in $\mathcal{A}$ for a random word generated by
$\mathcal{M}$. Since the weight of a word in an IBA is either 0 or 1, we see
that
$\operatorname{\mathbb{E}}_{\mathcal{M}}L_{\mathcal{A}}=\operatorname{\mathit{Pr}}_{\mathcal{M}}(L_{\mathcal{A}})$
if $\mathcal{A}$ is an IBA.

###### Lemma 11

Let $\mathcal{A}=(Q,\Sigma,M,\alpha,F)$ be an IBA w.r.t. Markov chain
$\mathcal{M}=(S,P)$ with initial distribution $\iota$. The following equations
hold:

$\displaystyle\operatorname{\mathit{Pr}}_{\mathcal{M}}(L_{\mathcal{A}})$
$\displaystyle=$ $\displaystyle\sum_{s\in S}\iota(s)\sum_{q\in
Q}\alpha(q)\operatorname{\mathbb{E}}_{\mathcal{M}[s]}L_{\mathcal{A}[q]}$ (1)
$\displaystyle\operatorname{\mathbb{E}}_{\mathcal{M}[s]}L_{\mathcal{A}[q]}$
$\displaystyle=$ $\displaystyle\sum_{s^{\prime}\in S}\sum_{q^{\prime}\in
Q}P_{s,s^{\prime}}M(s)_{q,q^{\prime}}\operatorname{\mathbb{E}}_{\mathcal{M}[s^{\prime}]}L_{\mathcal{A}[q^{\prime}]}$
(2)

###### Proof

The first equation holds because of the fact that $\mathcal{A}$ is an IBA.
Note that for any $q\in Q$, $|\mathit{FinalPaths}_{\mathcal{A}[q]}(w)|\leq N$
for all $w\in S^{\omega}$. For the second equation we have the following:

$\displaystyle\operatorname{\mathbb{E}}_{\mathcal{M}[s]}L_{\mathcal{A}[q]}$
$\displaystyle=$
$\displaystyle\int_{w\in\mathit{Paths}(\mathcal{M}[s])}L_{\mathcal{A}[q]}(w)d\operatorname{\mathit{Pr}}(w)$
$\displaystyle=$ $\displaystyle\sum_{s^{\prime}\in
S}\int_{w\in\mathit{Paths}(\mathcal{M}[s])\cap
s^{\prime}S^{\omega}}L_{\mathcal{A}[q]}(w)d\operatorname{\mathit{Pr}}(w)\quad\textrm{since
the cylinder sets $sS^{\omega}$ partition $S^{\omega}$}$ $\displaystyle=$
$\displaystyle\sum_{s^{\prime}\in
S}P_{s,s^{\prime}}\int_{w\in\mathit{Paths}(\mathcal{M}[s^{\prime}])}L_{\mathcal{A}[q]}(sw)d\operatorname{\mathit{Pr}}(w)\quad\textrm{by
definition of $\operatorname{\mathit{Pr}}(w)$}$ $\displaystyle=$
$\displaystyle\sum_{s^{\prime}\in
S}P_{s,s^{\prime}}\int_{w\in\mathit{Paths}(\mathcal{M}[s^{\prime}])}\sum_{p\in\mathit{FinalPaths}_{\mathcal{A}[q]}(sw)}\mathit{weight}(p)d\operatorname{\mathit{Pr}}(w)\quad\textrm{definition
of $L_{\mathcal{A}[q]}$}$ $\displaystyle=$ $\displaystyle\sum_{s^{\prime}\in
S}P_{s,s^{\prime}}\int_{w\in\mathit{Paths}(\mathcal{M}[s^{\prime}])}\sum_{q^{\prime}\in
Q}M(s)_{q,q^{\prime}}\sum_{p\in\mathit{FinalPaths}_{\mathcal{A}[q^{\prime}]}(w)}\mathit{weight}(p)d\operatorname{\mathit{Pr}}(w)$
definition of $\mathit{FinalPaths}$ $\displaystyle=$
$\displaystyle\sum_{s^{\prime}\in S}\sum_{q^{\prime}\in
Q}P_{s,s^{\prime}}M(s)_{q,q^{\prime}}\int_{w\in\mathit{Paths}(\mathcal{M}[s^{\prime}])}\sum_{p\in\mathit{FinalPaths}_{\mathcal{A}[q^{\prime}]}(w)}\mathit{weight}(p)d\operatorname{\mathit{Pr}}(w)$
$\displaystyle=$ $\displaystyle\sum_{s^{\prime}\in S}\sum_{q^{\prime}\in
Q}P_{s,s^{\prime}}M(s)_{q,q^{\prime}}\int_{w\in\mathit{Paths}(\mathcal{M}[s^{\prime}])}L_{\mathcal{A}[q^{\prime}]}(w)d\operatorname{\mathit{Pr}}(w)\quad\textrm{by
definition of $L$}$ $\displaystyle=$ $\displaystyle\sum_{s^{\prime}\in
S}\sum_{q^{\prime}\in
Q}P_{s,s^{\prime}}M(s)_{q,q^{\prime}}\operatorname{\mathbb{E}}_{\mathcal{M}[s^{\prime}]}L_{\mathcal{A}[q^{\prime}]}$

∎

Let $\mathcal{M}=(S,P)$ be a Markov chain with state set $S$, and let $\iota$
be an initial distribution on $S$. Let $B\in\mathbb{R}^{(Q\times
S)\times(Q\times S)}$ be the following matrix:

$B_{\langle q,s\rangle,\langle
q^{\prime},s^{\prime}\rangle}=P_{s,s^{\prime}}M(s)_{q,q^{\prime}}.$ (3)

Define $\vec{z}\in\mathbb{R}^{Q\times S}$ by
$\vec{z}_{q,s}=\operatorname{\mathbb{E}}_{\mathcal{M}[s]}L_{\mathcal{A}[q]}$,
i.e., the expected weight of a word for the Markov chain starting in $s$ and
the automaton starting in $q$. Similar to [3, Lemma 4] we have the following:

###### Lemma 12

Let $B$ and $\vec{z}$ as defined above. We have that $\vec{z}=B\vec{z}$.

######  Proof (of Lemma 12)

Using Lemma 11:

$\displaystyle\vec{z}_{q,s}\ $ $\displaystyle=\
\operatorname{\mathbb{E}}_{\mathcal{M}[s]}L_{\mathcal{A}[q]}$ $\displaystyle=\
\sum_{s^{\prime}\in S}\sum_{q^{\prime}\in
Q}P_{s,s^{\prime}}M(s)_{q,q^{\prime}}\operatorname{\mathbb{E}}_{\mathcal{M}[s^{\prime}]}L_{\mathcal{A}[q^{\prime}]}$
$\displaystyle=\ (B\vec{z})_{q,s}$ ∎

W.l.o.g. we can assume that for every $\langle qs\rangle$ in $B$ we can reach
an accepting loop. We need to show that SCCs in $B$ have a spectral radius of
at most 1. In fact, we can give a probabilistic interpretation to values in
$(B_{C,C})^{n}$, where $C\subseteq Q\times S$ is an SCC in $B$. This mirrors
Proposition 6 in [3].

###### Lemma 13

Let $C\subseteq Q\times S$ and $\langle qs\rangle,\langle rt\rangle\in C$. Let
$n\in\mathbb{N}$. Define $A:=B_{C,C}$. Then $(A^{n})_{\langle
qs\rangle,\langle
rt\rangle}=\operatorname{\mathbb{E}}_{\mathcal{M}[s]}\mathit{weight}^{C,n}_{\langle
qs\rangle,\langle rt\rangle}(w)$, where

$\mathit{weight}^{C,n}_{\langle qs\rangle,\langle rt\rangle}(w)=\sum_{\langle
q_{0}s_{0}\rangle\ldots\langle q_{n}s_{n}\rangle\in\mathit{Paths}_{\langle
qs\rangle,\langle rt\rangle}(A),w\in s_{0}\ldots s_{n}S^{\omega}}\prod_{0\leq
i<n}M(s_{i})_{q_{i},q_{i+1}}.$

(Intuitively, $\mathit{weight}^{C,n}_{\langle qs\rangle,\langle rt\rangle}(w)$
is the weight of the prefixes of length $n$ of paths over $w$ in $C$ starting
in $\langle qs\rangle$ that reach $\langle rt\rangle$ at time $n$.)

Define

$E^{C,n}_{\langle qs\rangle,\langle rt\rangle}:=\\{s_{0}s_{1}\ldots\in
sS^{\omega}\mid\exists q_{1}\ldots q_{n}.\langle
q_{0}s_{0}\rangle\ldots\langle q_{n}s_{n}\rangle\in\mathit{Paths}_{\langle
qs\rangle,\langle rt\rangle}(A)\\}.$

In particular, if $C$ is (a subset of) an SCC, then $(A^{n})_{\langle
qs\rangle,\langle
rt\rangle}=\operatorname{\mathit{Pr}}_{\mathcal{M}[s]}\left(E^{C,n}_{\langle
qs\rangle,\langle rt\rangle}\right)$ and hence $\rho(A)\leq 1$.

###### Proof

$\displaystyle\operatorname{\mathbb{E}}_{\mathcal{M}[s]}\mathit{weight}^{C,n}_{\langle
qs\rangle,\langle rt\rangle}(w)$ $\displaystyle=$
$\displaystyle\int_{w\in\mathit{Paths}(\mathcal{M}[s_{0}])}\mathit{weight}^{C,n}_{\langle
qs\rangle,\langle rt\rangle}(w)d\operatorname{\mathit{Pr}}(w)$
$\displaystyle=$ $\displaystyle\sum_{s_{0}\ldots s_{n}\in
S^{n}}\int_{w\in\mathit{Paths}(\mathcal{M}[s])\cap s_{0}\ldots
s_{n}S^{\omega}}\mathit{weight}^{C,n}_{\langle qs\rangle,\langle
rt\rangle}(w)d\operatorname{\mathit{Pr}}(w)$ $\displaystyle=$
$\displaystyle\sum_{s_{0}\ldots s_{n}\in
S^{n}}\int_{w\in\mathit{Paths}(\mathcal{M}[s_{n}])}\prod_{0\leq
i<n}P_{s_{i},s_{i+1}}\mathit{weight}^{C,n}_{\langle qs\rangle,\langle
rt\rangle}(s_{0}\ldots s_{n}w)d\operatorname{\mathit{Pr}}(w)$ $\displaystyle=$
$\displaystyle\sum_{s_{0}\ldots s_{n}\in
S^{n}}\int_{w\in\mathit{Paths}(\mathcal{M}[s_{n}])}\prod_{0\leq
i<n}P_{s_{i},s_{i+1}}$ $\displaystyle\sum_{\langle
q_{0}s_{0}\rangle\ldots\langle q_{n}s_{n}\rangle\in\mathit{Paths}_{\langle
qs\rangle,\langle rt\rangle}(A),w\in s_{0}\ldots s_{n}S^{\omega}}\prod_{0\leq
i<n}M(s_{i})_{q_{i},q_{i+1}}d\operatorname{\mathit{Pr}}(w)$ $\displaystyle=$
$\displaystyle\sum_{s_{0}\ldots s_{n}\in
S^{n}}\int_{w\in\mathit{Paths}(\mathcal{M}[s_{n}])}$
$\displaystyle\sum_{\langle q_{0}s_{0}\rangle\ldots\langle
q_{n}s_{n}\rangle\in\mathit{Paths}_{\langle qs\rangle,\langle
rt\rangle}(A)),w\in s_{0}\ldots s_{n}S^{\omega}}\prod_{0\leq
i<n}P_{s_{i},s_{i+1}}M(s_{i})_{q_{i},q_{i+1}}d\operatorname{\mathit{Pr}}(w)$
$\displaystyle=$ $\displaystyle\sum_{s_{0}\ldots s_{n}\in S^{n}}\sum_{\langle
q_{0}s_{0}\rangle\ldots\langle q_{n}s_{n}\rangle\in\mathit{Paths}_{\langle
qs\rangle,\langle rt\rangle}(A)}\prod_{0\leq
i<n}P_{s_{i},s_{i+1}}M(s_{i})_{q_{i},q_{i+1}}$ $\displaystyle=$
$\displaystyle\sum_{s_{0}\ldots s_{n}\in S^{n}}\sum_{\langle
q_{0}s_{0}\rangle\ldots\langle q_{n}s_{n}\rangle\in\mathit{Paths}_{\langle
qs\rangle,\langle rt\rangle}(A)}\prod_{0\leq i<n}A_{\langle
q_{i}s_{i}\rangle,\langle q_{i+1}s_{i+1}\rangle}$ $\displaystyle=$
$\displaystyle(A^{n})_{\langle qs\rangle,\langle rt\rangle}$

Note that since an accepting loop can be reached from every state in $B$, no
SCC in $B$ can have diamonds: otherwise, one could traverse a loop over that
diamond $\log N+1$ times to get a word that has more than $N$ final paths.
Since any path that stays in an SCC has weight 1, and there are no diamonds in
SCCs, we see that if $C$ is (a subset of) an SCC, then
$\operatorname{\mathbb{E}}_{\mathcal{M}[s]}\mathit{weight}^{C,n}_{\langle
qs\rangle,\langle
rt\rangle}(w)=\operatorname{\mathit{Pr}}_{\mathcal{M}[s]}\left(E^{C,n}_{\langle
qs\rangle,\langle rt\rangle}\right)$ and hence $(A^{n})_{\langle
qs\rangle,\langle
rt\rangle}=\operatorname{\mathit{Pr}}_{\mathcal{M}[s]}\left(E^{C,n}_{\langle
qs\rangle,\langle rt\rangle}\right)$. ∎

The definitions of recurrent SCCs and cuts are completely equivalent to those
in [3] and are copied here verbatim: a _recurrent SCC_ is an SCC with spectral
radius 1. We call a recurrent SCC $D$ _accepting_ if for some $\langle
qt\rangle\in D$ we have $q\in F$. Let $D\subseteq Q\times S$ be an SCC of $B$.
A set $\alpha\subseteq D$ is called a _fiber_ if it can be written as
$\alpha=A\times\\{s\\}$ for some $A\subseteq Q,s\in S$. Given such a fiber
$\alpha$ and $t\in S$, if $M_{s,t}>0$ we then define a fiber

$\alpha\triangleright t:=\\{\langle q^{\prime}t\rangle\in D\mid
q^{\prime}\in\delta(q,s)\\}$

If $M_{s,t}=0$ then $\alpha\triangleright t$ is left undefined. We extend this
definition inductively by writing $\alpha\triangleright\epsilon=\alpha$ and
$\alpha\triangleright wt=(\alpha\triangleright w)\triangleright t$ for $t\in
S,w\in S^{*}$. If $\alpha$ is a singleton $\\{d\\}$ we may write
$d\triangleright w$ for $\alpha\triangleright w$.

We call a fiber $\alpha\subseteq D$ a _cut_ of $D$ if (i)
$\alpha=d\triangleright v$ for some $d\in D$ and $v\in S^{*}$, and (ii)
$\alpha\triangleright w\neq\emptyset$ holds for all $w\in S^{*}$ such that
$\alpha\triangleright w$ is defined. Clearly if $\alpha$ is a cut then so is
$\alpha\triangleright w$ when the latter is defined. Given a cut
$\alpha\subseteq D$, we call its characteristic vector
$\vec{\mu}\in\\{0,1\\}^{D}$ a _cut vector_.

Let $D$ be a recurrent SCC. A vector $\vec{\mu}\in[0,1]^{D}$ is called a _$D$
-normaliser_ if $\vec{\mu}^{T}\vec{z}=1$.

We will need versions of [3, Lemma 8] and [3, Lemma 10] as well. Lemma 10.1
only relies on the probabilistic interpretation of submatrices in SCCs as
shown in Lemma 13 and the nonnegativity of those matrices, and hence we can
invoke its proof verbatim:

######  Lemma 14 (Lemma 10.1 in [3])

Let $D\subseteq Q\times S$ be an SCC. Then $D$ is recurrent if and only if it
has a cut.

###### Proof

Verbatim from the proof in [3]. ∎

For our proof of [3, Lemma 8.1] we will first show something stronger:

###### Lemma 15

Let $D$ be a recurrent SCC, and let $C\subseteq Q\times S\setminus D$ be the
set of states outside of $D$ reachable from $D$. Then $\rho(B_{C,C})<1$.

###### Proof

Towards a contradiction, assume $\rho(B_{C,C})=1$. Then by Theorem 4.2.3 there
exists a recurrent SCC $D^{\prime}$ such that $D^{\prime}$ is reachable from
$D$. We will create a word consisting of five parts such that $\mathcal{A}$
has more than $N$ final paths over that word. Since $N$ is the global bound on
the number of final paths in $\mathcal{A}$, this leads to a contradiction.

  1. 1.

Firstly, pick $d=\langle qs_{0}\rangle\in D$. Let $s_{1}\ldots s_{i}$ be such
that $d\triangleright s_{1}\ldots s_{i}$ is a cut, such a word exists by Lemma
14.

  2. 2.

Let $s_{i+1}\ldots s_{j}$ be such that there exists a path from $d$ to some
$d^{\prime}\in D^{\prime}$ over $s_{1}\ldots s_{j}$.

  3. 3.

Let $s_{j+1}\ldots s_{k}$ be such that $d^{\prime}\triangleright s_{j+1}\ldots
s_{k}$ is a cut. Again this exists by Lemma 14.

  4. 4.

Let $s_{k+1}\ldots s_{l}$ be such that $d\in d\triangleright s_{1}\ldots
s_{l}$. This exists because $d\triangleright s_{1}\ldots s_{i}$ is a cut and
for any cut $c$ and any $s\in S$ we have that $c\triangleright s$ is also a
cut.

Then consider the word $(s_{1}\ldots s_{l})^{|D^{\prime}|(N+1)}$. Because
$d\in d\triangleright s_{1}\ldots s_{l}$ and we reach a cut in $D^{\prime}$
from $d$ over $s_{1}\ldots s_{l}$, this means at least $|D^{\prime}|(N+1)$
cuts in $D^{\prime}$ are reached after reading $(s_{1}\ldots
s_{l})^{|D^{\prime}|(N+1)}$ from $D$. By the pigeonhole principle, there
exists a $d^{\prime}\in D^{\prime}$ such that there are at least $N+1$ paths
from $d$ to $d^{\prime}$ over $(s_{1}\ldots s_{l})^{|D^{\prime}|(N+1)}$.
Hence, if we pick $s_{l+1}\ldots$ such that there is a final path from
$d^{\prime}$ over $s_{l+1}\ldots$, we see that there are more than $N$ final
paths from $d$ over $(s_{1}\ldots s_{l})^{|D^{\prime}|(N+1)}s_{l+1}\ldots$,
contradicting the global bound on the number of final paths in $\mathcal{A}$.
Thus, $\rho(D^{\prime})<1$ and therefore $\rho(B_{C,C})<1$. ∎

Now we can show Lemma 8.1:

######  Lemma 16 (Lemma 8.1 in [3])

Let $D$ be a recurrent SCC, and let $\vec{x}$ be any vector satisfying
$\vec{x}=B\vec{x}$. Then $\vec{x}_{D}=B_{D,D}\vec{x}_{D}$.

###### Proof

Let $\bar{D}=Q\times S\setminus D$ and let $C\subseteq\bar{D}$ be the set of
states reachable from $D$. For all $n$ we have:

$\displaystyle\vec{x}_{D}$ $\displaystyle=$ $\displaystyle(B^{n}\vec{x})_{D}$
$\displaystyle=$ $\displaystyle
B^{n-1}B_{D,D}\vec{x}_{D}+B^{n-1}B_{D,\bar{D}}\vec{x}_{\bar{D}}$
$\displaystyle=$ $\displaystyle
B^{n-1}B_{D,D}\vec{x}_{D}+B_{C,C}^{n-1}B_{D,\bar{D}}\vec{x}_{\bar{D}}.$

Since $\rho(B_{C,C})<1$ by Lemma 15, this second term goes to 0 as $n$ goes to
infinity. Hence, $\vec{x}_{D}=B_{D,D}\vec{x}_{D}$. ∎

The proof of Lemma 8.2 in [3] relies on the following lemma:

###### Lemma 17

Let $D$ be a recurrent SCC in $B$, and let $\langle q,s\rangle\in D$. Then
almost surely all final paths of $\mathcal{A}[q]$ are contained in $D$, and
for any $\langle q^{\prime},s^{\prime}\rangle\not\in D$ reachable from
$\langle q,s\rangle$, $z_{\langle q^{\prime},s^{\prime}\rangle}=0$.

###### Proof

Suppose that with positive probability a word starting in $s$ is generated
such that $\mathcal{A}[q]$ has a final path outside $D$. We will construct a
word consisting of three repeating parts that admits more than $N$ final
paths:

  1. 1.

Let $s_{0}\ldots s_{l}\in S^{*}$ be such that $s_{0}=s$ and $\langle
q,s\rangle\triangleright s_{1}\ldots s_{l}$ is a cut containing $\langle
q,s\rangle$. Such a word exists by Lemma 14.

  2. 2.

The language of words that have a final path outside $D$ is regular. The
probability of generating a word with a final path outside $D$ is bounded from
above by the sum of probabilities of reaching some $\langle
q^{\prime},s^{\prime}\rangle$ outside $D$ times the probability of generating
a word starting in $s^{\prime}$ over which there exists a final path from
$q^{\prime}$, and the probability of generating a word with a final path
outside $D$ is nonzero. Therefore, there must exist $\langle
q^{\prime},s^{\prime}\rangle\not\in D$ reachable from $\langle q,s\rangle$
such that with nonzero probability, a word starting in $s^{\prime}$ is
generated over which $\mathcal{A}[q^{\prime}]$ has a final path. Let
$s_{l}\ldots s_{m^{\prime}}$ be such that $s_{m^{\prime}}=s^{\prime}$ and
$M(s_{l}\ldots s_{m^{\prime}})_{q,q^{\prime}}>0$. By Lemma 10 there exists a
word $s_{m^{\prime}}\ldots s_{m}$ such that
$\operatorname{\mathit{Pr}}_{s_{m}}(\\{w\in s_{m}S^{\omega}\mid\textrm{there
exists a final path from $q^{\prime}$ over $s_{m^{\prime}}\ldots
s_{m}w$}\\})=1$. Hence, $s_{l}\ldots s_{m}$ is such that
$\operatorname{\mathit{Pr}}_{s_{l}}(s_{l}\ldots s_{m}S^{\omega})>0$ and any
word prefixed by $s_{l}\ldots s_{m}$ almost surely has a final path outside
$D$.

  3. 3.

Let $\langle q^{\prime\prime},s^{\prime\prime}\rangle\in\langle
q,s\rangle\triangleright s_{0}\ldots s_{m}$ (which exists since $\langle
q,s\rangle\triangleright s_{0}\ldots s_{l}$ is a cut and by extension so is
$\langle q,s\rangle\triangleright s_{0}\ldots s_{m}$). By strongly
connectedness of $D$ there exists $s_{m}\ldots s_{n}\in S^{*}$ such that
$s_{m}=s^{\prime\prime}$ and $\langle q,s\rangle\in\langle
q^{\prime\prime},s^{\prime\prime}\rangle\triangleright s_{m+1}\ldots s_{n}$.

Now consider the word $(s_{0}\ldots s_{n})^{N+1}$. By construction, $\langle
q,s\rangle\in\langle q,s\rangle\triangleright s_{0}\ldots s_{n}$ and there
exists $\langle q^{\prime},s^{\prime}\rangle\not\in D$ such that $q$ reaches
$q^{\prime}$ over $s_{0}\ldots s_{m-1}$ and
$\operatorname{\mathit{Pr}}_{s_{m}}(\\{w\in s_{m}S^{\omega}\mid\textrm{there
exists a final path from $q^{\prime}$ over $s_{m^{\prime}}\ldots
s_{m}w$}\\})=1$. Hence, after every iteration of $s_{0}\ldots s_{n}$, the
automaton can nondeterministically choose to stay in $D$ or move to a set of
states out of $D$ after which it will almost surely have a final path. Thus,
for almost any word prefixed with $(s_{0}\ldots s_{n})^{N+1}$, there are at
least $N+1$ final paths, which contradicts the fact that $\mathcal{A}$ is an
IBA. This shows that almost surely any final path from $\langle q,s\rangle\in
D$ stays in $D$, and hence for any $\langle
q^{\prime},s^{\prime}\rangle\not\in D$ reachable from $\langle q,s\rangle$,
$z_{\langle q^{\prime},s^{\prime}\rangle}=0$. ∎

With this we can invoke the proof of Lemma 8.2 verbatim:

######  Lemma 18 (Lemma 8.2 in [3])

Let $D$ be a recurrent SCC. For all $d\in D$, we have $\vec{z}_{d}>0$ iff $D$
is accepting.

###### Proof

Verbatim from [3], relying only on Lemma 17 and the probabilistic
interpretation in Lemma 13. ∎

The proof of Lemma 10.2 in [3] only relies on Lemma 18 and hence can be
invoked verbatim. This shows that cut vectors are $D$-normalisers.

######  Lemma 19 (Lemma 10.2 in [3])

Let $D$ be an accepting recurrent SCC and let $\vec{\mu}$ be a cut vector in
$D$. Then $\vec{\mu}^{\top}\vec{z}_{D}=1$.

###### Proof

Verbatim. ∎

Finally we can prove our version of Lemma 12:

######  Lemma 20 (Lemma 12 in [3])

Let $\mathcal{D}_{+}$ be the set of accepting recurrent SCCs, and
$\mathcal{D}_{0}$ the set of non-accepting recurrent SCCs. For each
$D\in\mathcal{D}_{+}$, let $\vec{\mu}_{D}\in[0,1]^{D}$ be a $D$-normalizer
(which exists by Lemma 19). Then $\vec{z}$ is the unique solution of the
following linear system:

$\displaystyle\vec{\zeta}$ $\displaystyle=B\vec{\zeta}$ for all
$D\in\mathcal{D}_{+}$: $\displaystyle\vec{\mu}^{\top}_{D}\vec{\zeta}_{D}$
$\displaystyle=1$ for all $D\in\mathcal{D}_{0}$:
$\displaystyle\vec{\zeta}_{D}$ $\displaystyle=\vec{0}$

###### Proof

This proof is equivalent to the one in [3] and is included for completeness.
The vector $\vec{z}$ solves the system of equations by Lemma 12, Lemma 18, and
the definition of a $D$-normalizer. To show uniqueness, let $\vec{x}$ solve
the system of equations. We show that $\vec{x}=\vec{z}$.

  * •

Let $D\in\mathcal{D}_{0}$. Then $\vec{x}_{D}=\vec{0}=\vec{z}_{D}$.

  * •

Let $D\in\mathcal{D}_{+}$. By Lemma 16, we have
$\vec{x}_{D}=B_{D,D}\vec{x}_{D}$ and $\vec{z}_{D}=B_{D,D}\vec{z}_{D}$. By
Theorem 4.3, the eigenspace of $B_{D,D}$ is one-dimensional, implying that
$\vec{x}_{D}$ is a scalar multiple of $\vec{z}_{D}$. We have
$\vec{\mu}_{D}^{\top}\vec{x}_{D}=1=\vec{\mu}_{D}^{\top}\vec{z}_{D}$, hence
$\vec{x}_{D}=\vec{z}_{D}$.

  * •

Let $D:=\bigcup\mathcal{D}_{+}\cup\bigcup\mathcal{D}_{0}$ be the union of all
recurrent SCCs, and let $\bar{D}:=(Q\times S)\setminus D$. We have
$\vec{x}-\vec{z}=B(\vec{x}-\vec{z})$. It follows

$\displaystyle\vec{x}_{\bar{D}}-\vec{z}_{\bar{D}}$ $\displaystyle=$
$\displaystyle
B_{\bar{D},\bar{D}}(\vec{x}_{\bar{D}}-\vec{z}_{\bar{D}})+B_{\bar{D},D}(\vec{x}_{D}-\vec{z}_{D})$
$\displaystyle=$ $\displaystyle
B_{\bar{D},\bar{D}}(\vec{x}_{\bar{D}}-\vec{z}_{\bar{D}})+B_{\bar{D},D}(\vec{0})$
$\displaystyle=$ $\displaystyle
B_{\bar{D},\bar{D}}(\vec{x}_{\bar{D}}-\vec{z}_{\bar{D}})$

by the previous two items. By Lemma 15, $\rho(B_{\bar{D},\bar{D}})<1$. Thus,
$\vec{x}_{\bar{D}}=\vec{z}_{\bar{D}}$. ∎

This enables us to prove Theorem 4.1:

######  Proof (of Theorem 4.1)

It suffices to calculate $D$-normalisers and solve the system of equations
described in Lemma 20. Solving a system of equations can be done in NC, and we
can find a $D$-normaliser using [3, Lemma 22] in NC, proving the theorem. ∎

###### Corollary 3

Let $\mathcal{M}$ be an MC and let $\mathcal{A}_{k}$ be a $k$-ABA with $n$
states, where $k=O(\log n)$. The probability that a random word sampled from
$\mathcal{M}$ is in $L_{\mathcal{A}}$ can be computed in POLYLOGSPACE.

###### Proof

This combines Theorems 3.3 and 4.1. Since NC is contained in POLYLOGSPACE
[23], this proves the corollary. ∎

PSPACE-hardness of model checking $k$-ABAs against Markov chains can be shown
easily from the _finite intersection problem_ introduced by D. Kozen [19].
This problem asks, given a set of deterministic automata, whether the
intersection of the languages is empty. By considering the union of the
complements of the automata as a $k$-ABA we see that the probabilistic
universality problem for $k$-ABAs is PSPACE-hard. Membership in PSPACE is
shown by translating the $k$-ABA into an equivalent IBA and model checking
this IBA against the Markov chain.

###### Theorem 4.4

The model checking problem for $k$-ABAs is PSPACE-complete.

###### Corollary 4

Let $\mathcal{M}$ be an MC and let $\mathcal{A}$ be an NBA with $n$ states.
The probability that a word in $L_{\mathcal{A}}$ is accepted by $\mathcal{M}$
can be computed in PSPACE.

###### Proof

By Löding et al. [22], $\mathcal{A}$ can be converted in a $k$-ABA
$\mathcal{A}_{k}$ with at most $3^{n}$ states where $k=n$. Hence, using
Corollary 3, we can calculate $\Pr(L_{\mathcal{A}_{k}})=\Pr(L_{\mathcal{A}})$
in POLYLOG($2^{n}$) = POLY($n$) space. ∎

#### Acknowledgements

Mathieu Kubik, Tomasz Ponitka, and Joao Paulo Costalonga contributed ideas to
the proofs of Lemmas 3, 2, and 9, respectively.

## References

  * [1] Almagor, S., Boker, U., Kupferman, O.: What’s decidable about weighted automata? Information and Computation (2020)
  * [2] Angluin, D., Antonopoulos, T., Fisman, D.: Strongly Unambiguous Büchi Automata Are Polynomially Predictable With Membership Queries. In: 28th EACSL Annual Conference on Computer Science Logic (CSL 2020) (2020)
  * [3] Baier, C., Kiefer, S., Klein, J., Klüppelholz, S., Müller, D., Worrell, J.: Markov chains and unambiguous Büchi automata (extended version of a CAV’16 paper). arXiv:1605.00950 (2016), http://arxiv.org/abs/1605.00950
  * [4] Berman, A., Plemmons, R.J.: Nonnegative matrices in the mathematical sciences. Academic Press (1979)
  * [5] Berstel, J., Reutenauer, C.: Rational Series and Their Languages. Springer (1988)
  * [6] Carlyle, J.W., Paz, A.: Realizations by stochastic finite automata. Journal of Computer and System Sciences 5(1), 26–40 (1971)
  * [7] Colcombet, T.: Unambiguity in automata theory. In: 17th International Workshop on Descriptional Complexity of Formal Systems (DCFS) (2015)
  * [8] Droste, M., Kuich, W., Vogler, H.: Handbook of Weighted Automata. Springer Publishing Company, Incorporated, 1st edn. (2009)
  * [9] Droste, M., Meinecke, I.: Weighted automata and regular expressions over valuation monoids. International Journal of Foundations of Computer Science (2011)
  * [10] Fijalkow, N.: Undecidability results for probabilistic automata. ACM SIGLOG News 4(4), 10–17 (2017)
  * [11] Filiot, E., Gentilini, R., Raskin, J.F.: Finite-Valued Weighted Automata. In: 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014) (2014)
  * [12] Fliess, M.: Matrices de Hankel. Journal de Mathématiques Pures et Appliquées 53, 197–222 (1974)
  * [13] Golomb, S.W., Goldstein, R.M., Hales, A.W., Welch, L.R.: Shift register sequences. Holden-Day series in information systems, Holden-Day, San Francisco (1967)
  * [14] Holzer, M., Kutrib, M.: Nondeterministic descriptional complexity of regular languages. International Journal of Foundations of Computer Science (2003)
  * [15] Indzhev, E., Kiefer, S.: On complementing unambiguous automata and graphs with many cliques and cocliques. arXiv preprint arXiv:2105.07470 (2021)
  * [16] Jirásek, J., Jirásková, G., Sebej, J.: Operations on unambiguous finite automata. International Journal of Foundations of Computer Science 29(5), 861–876 (2018)
  * [17] Karmarkar, H., Joglekar, M., Chakraborty, S.: Improved upper and lower bounds for Büchi disambiguation. In: Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings (2013)
  * [18] Kiefer, S., Widdershoven, C.: Efficient analysis of unambiguous automata using matrix semigroup techniques. arXiv preprint arXiv:1906.10093 (2019)
  * [19] Kozen, D.: Lower bounds for natural proof systems. In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977). pp. 254–266. IEEE (1977)
  * [20] Leung, H.: Separating exponentially ambiguous finite automata from polynomially ambiguous finite automata. SIAM Journal of Computing 27(4), 1073–1082 (1998)
  * [21] Leung, H.: Descriptional complexity of NFA of different ambiguity. International Journal of Foundations of Computer Science 16(5), 975–984 (2005)
  * [22] Löding, C., Pirogov, A.: On finitely ambiguous Büchi automata. In: International Conference on Developments in Language Theory. pp. 503–515. Springer (2018)
  * [23] Papadimitriou, C.M.: Computational complexity. Addison-Wesley, Reading, Massachusetts (1994)
  * [24] Paz, A.: Introduction to probabilistic automata. Academic Press (2014)
  * [25] Rabin, M.O.: Probabilistic automata. Information and control 6(3), 230–245 (1963)
  * [26] Raskin, M.: A superpolynomial lower bound for the size of non-deterministic complement of an unambiguous automaton. In: 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018) (2018)
  * [27] Safra, S.: On the complexity of omega-automata. In: Proc. 29th IEEE Symp. Found. of Comp. Sci. pp. 319–327 (1988)
  * [28] Schmidt, E.: Succinctness of descriptions of context-free, regular and finite languages. Ph.D. thesis, Cornell University, Ithaca, NY (1978)
  * [29] Schützenberger, M.: On the definition of a family of automata. Information and Control 4(2), 245–270 (1961)
  * [30] Tzeng, W.G.: On path equivalence of nondeterministic finite automata. Information Processing Letters 58(1), 43–46 (1996)
  * [31] Weber, A., Seidl, H.: On the degree of ambiguity of finite automata. Theoretical Computer Science 88(2), 325–349 (1991)