Resolving Nondeterminism by Chance

The notion of history-determinism was introduced independently, with slightly different definitions, by Henzinger and Piterman [24] for solving games without determinisation, by Colcombet [14] for cost-functions, and by Kupferman, Safra, and Vardi [28] for recognising derived tree languages of word automata. For $\omega$-regular automata, these variations all coincide [8]. For coBüchi-recognisable languages, history-deterministic automata can be exponentially more succinct than any equivalent deterministic ones [27]. Checking whether a given automaton is HD is decidable in polynomial time for Büchi and coBüchi automata [3, 27] and more generally also for parity automata of any fixed parity index [31]. History-determinism has been studied for richer automata models, such as pushdown automata [32, 20] timed automata [12, 11, 23] and quantitative automata [9, 10].

Recently, and independently from us, Henzinger, Prakash and Thejaswini [25] introduced classes of stochastically resolvable automata. The main difference of their work compared to ours is that they study the qualitative setting, where resolvers are required to succeed almost-surely, with probability one. In the terminology introduced above these are $1$-resolvable automata. They study such automata on infinite words and compare their expressiveness, relative succinctness, against history-deterministic and semantically deterministic automata. Over finite words, these notions coincide: an NFA is $1$-stochastically resolvable iff it is $1$-memoryless stochastically resolvable iff it is semantically deterministic iff it is history-deterministic. They also consider the complexity of determining whether an automaton is $1$-resolvable and establish that this is in polynomial time for safety automata, and $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$-complete for reachability and weak automata, and remains open for more general classes.

For a fixed probabilistic automaton, deciding whether a given $\lambda$ is a lower bound corresponds to the undecidable emptiness problem [37], while asking if such a $\lambda$ exists relates to the undecidable zero-isolation problem [19]. These problems become more tractable under restrictions such as bounded ambiguity [15, 16, 17, 18]. In the unary case, checking if $\lambda$ is a lower bound is equivalent to the long-standing open positivity problem for linear recurrence sequences [36] and is also hard for Markov chains [45]. In contrast, our setting allows the probabilistic automaton to vary, asking whether some choice of probabilities satisfies the desired properties.

The unary case can be seen as a synthesis problem on parametric Markov chains. Consider the distribution transformer perspective [2, 5], where a Markov chain induces a sequence of distributions over states. Then the $\lambda$-resolvability problem asks, for universal NFA, whether there exists a parameter assignment such that the sequence of distributions is “globally” in the semi-algebraic set $S=\{x\in {[0,1]}^Q|{\sum }_{q\in Q}{x}_q=1\text{ and }{\sum }_{q\in F}{x}_q\ge \lambda \}$ (distributions with probability mass at least $\lambda$ in accepting states). When the NFA is non-universal the “globally” condition must be adjusted to the eventually periodic pattern of the NFA. Existing work characterises, up to a set of measure zero, parameters that satisfy prefix-independent properties or “eventually” properties such as Finally Globally in $S$ [5]. For general parametric questions, there is always the special case where the parameters are redundant, which encodes the aforementioned positivity problem [45]. This special case does not necessarily arise in our setting, as the problem has all transitions parameterised independently (only the structure is fixed), which leaves hope for $\lambda$-resolvability.

We focus on automata over finite words and consider the decision problems whether a given automaton is resolvable. We distinguish the two variants of this problem, asking whether the automaton is positively resolvable, or whether it is $\lambda$-resolvable for a given value of $\lambda$. Our results are as follows, see also Table 1 for a summary.

• $\mathrm{■}$

  We introduce the quantitative notion of $\lambda$-memoryless stochastic resolvability, and show $\lambda$-resolvability induces a strict hierarchy of automata with varying parameter $\lambda \in (0,1)$.

• $\mathrm{■}$

  We show that checking $\lambda$-resolvability is undecidable already for NFA, on finite words, and therefore also for automata on infinite words regardless of the accepting condition.

• $\mathrm{■}$

  We complement this by showing that both positive resolvability and $\lambda$-resolvability remain decidable for finitely-ambiguous automata.

• $\mathrm{■}$

  We present complexity upper and lower bounds for several well-studied variations of finitely-ambiguous automata (summarised in Table 1). In particular, checking positive resolvability is $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$-complete for finitely-ambiguous automata, $\mathrm{𝖭𝖫}$-complete for unambiguous ($1$-ambiguous) automata, and in the polynomial hierarchy for (unrestricted) unary automata. Checking $\lambda$-resolvability is $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$-hard even for $k$-ambiguous automata (and $\mathrm{𝖼𝗈𝖭𝖯}$-hard over a unary alphabet).

A nondeterministic finite automaton (NFA) $𝒜$ consists of a finite alphabet $\mathrm{\Sigma }$, a finite set of states $Q$, an initial state $q_0$, a set of accepting states $F\subseteq Q$, and a set of transitions $\mathrm{\Delta }\subseteq Q\times \mathrm{\Sigma }\times Q$. We also use $p\stackrel{𝜎}{\to }q$ to signify that $(p,\sigma ,q)\in \mathrm{\Delta }$. $𝒜$ is unary if $|\mathrm{\Sigma }|=1$; a deterministic finite automaton (DFA) if, for every $(p,\sigma )\in Q\times \mathrm{\Sigma }$, there exists at most one state $q\in Q$ such that $p\stackrel{𝜎}{\to }q$; and complete if, for every $(p,\sigma )\in Q\times \mathrm{\Sigma }$, there exists some $q\in Q$ such that $p\stackrel{𝜎}{\to }q$.

Given a word $w={\sigma }_1\mathrm{\dots }{\sigma }_n\in {\mathrm{\Sigma }}^{\ast }$, a run $\pi$ of $𝒜$ on $w$ is a sequence of transitions ${\tau }_1\mathrm{\dots }{\tau }_n$, where each transition ${\tau }_i=(p_i,{\sigma }_i,q_i)\in \mathrm{\Delta }$ for $i\in [1,n]$, and $q_i=p_{i+1}$ for $i\in [1,n-1]$. The run $\pi$ is accepting if $p_1=q_0$ and $q_n\in F$. A word is accepted by $𝒜$ if there exists an accepting run on it. We denote by $ℒ(𝒜)$ the set of words accepted by $𝒜$. Additionally, we use ${\mathrm{ACC}}_{𝒜}(w)$ to denote the set of all accepting runs of $𝒜$ on $w$. We omit the subscript $𝒜$ when it is clear from the context. An NFA $𝒜$ is $k$-ambiguous if, for every word $w\in {\mathrm{\Sigma }}^{\ast }$, it holds that $|\mathrm{ACC}(w)|\le k$. It is unambiguous when $k=1$. Moreover, $𝒜$ is finitely-ambiguous if it is $k$-ambiguous for some $k\in {\mathbb{Z}}_{+}$. We use UFA and FNFA to refer to unambiguous and finitely-ambiguous NFA, respectively.

For $q\in Q$, let ${𝒜}_q$ denote the automaton $𝒜$ with $q$ as its initial state, and for $S\subseteq \mathrm{\Delta }$, let ${𝒜}_S$ denote the automaton obtained from $𝒜$ by restricting its transitions to $S$. For $\tau \in S$, we often say $\tau$ is nondeterministic in $S$ to mean $\tau$ is nondeterministic in ${𝒜}_S$. $\mathrm{\Delta }$ induces a transition function ${\delta }_{𝒜}:2^Q\times {\mathrm{\Sigma }}^{\ast }\mapsto 2^Q$, where ${\delta }_{𝒜}(Q^{\prime },w)$ is the set of all states where runs on word $w$ can end up in when starting from any state $q\in Q^{\prime }$. Formally, for all $Q^{\prime }\subseteq Q$, ${\delta }_{𝒜}(Q^{\prime },ϵ)=Q^{\prime }$, and for all $w\in {\mathrm{\Sigma }}^{\ast }$ and $\sigma \in \mathrm{\Sigma }$, ${\delta }_{𝒜}(Q^{\prime },w\cdot \sigma )=\{q\mid (p,\sigma ,q)\in \mathrm{\Delta }\text{ and }p\in {\delta }_{𝒜}(Q^{\prime },w)\}$. When $Q^{\prime }=\{p\}$, we often abuse notation and write ${\delta }_{𝒜}(p,w)$ instead of ${\delta }_{𝒜}(\{p\},w)$, and we omit the subscript $𝒜$ when it is clear from the context. An NFA is trim if every state $q\in Q$ is reachable from the initial state, and can reach an accepting state, i.e., $q\in \delta (q_0,w)$ and $\delta (q,w^{\prime })\cap F\ne \mathrm{\varnothing }$ for some words $w,w^{\prime }$.

A probabilistic finite automaton (PFA) $𝒫$ is an extension of nondeterministic finite automaton that assigns an acceptance probability to each word. Specifically, $𝒫$ is an NFA augmented with an assignment $\mathrm{\Theta }:\mathrm{\Delta }\to {[0,1]}_{ℝ}$, where for every $(p,\sigma )\in Q\times \mathrm{\Sigma }$, ${\sum }_{\tau =(p,\sigma ,q)\in \mathrm{\Delta }}\mathrm{\Theta }(\tau )=1$. Accordingly, $𝒫$ is a 6-tuple of the form $(\mathrm{\Sigma },Q,q_0,\mathrm{\Delta },F,\mathrm{\Theta })$. Given a transition $\tau =(p,\sigma ,q)$, the value $\mathrm{\Theta }(\tau )$ represents the probability of transitioning from state $p$ to state $q$ upon reading the symbol $\sigma$. With a slight abuse of language, we also call $(p,\sigma ,q,d)$ a transition of $𝒫$, where $d=\mathrm{\Theta }(p,\sigma ,q)$. We say that $𝒫$ is based on the NFA $𝒜=(\mathrm{\Sigma },Q,q_0,\mathrm{\Delta },F)$ and call this its underlying NFA.¹¹1The condition ${\sum }_{\tau =(p,\sigma ,q)\in \mathrm{\Delta }}\mathrm{\Theta }(\tau )=1$ may not hold for some pairs $(p,\sigma )$ if the underlying NFA is not complete. Any NFA can be made complete by introducing a non-accepting sink state. Thus, throughout this paper, we assume that the underlying NFA of every PFA is implicitly made complete.

We use $𝒫(w)$ to denote the probability that $𝒫$ accepts word $w$ where:

For every threshold $\lambda \in {[0,1]}_{ℝ}$, let $ℒ({𝒫}_{\ge \lambda })$ denote the set of all words accepted with probability at least $\lambda$, that is: $ℒ({𝒫}_{\ge \lambda }):=\{w\in {\mathrm{\Sigma }}^{\ast }\mid 𝒫(w)\ge \lambda \}.$

We also use ${𝒫}_{\ge \lambda }$ to refer to the PFA $𝒫$ with a given threshold $\lambda$. Similarly, we define ${𝒫}_{\le \lambda }$, ${𝒫}_{>\lambda }$, and . A PFA $𝒫$ is called simple if, for every transition $(p,a,q,d)$ of $𝒫$, the probability $d$ belongs to $\{0,\frac{1}{2},1\}$. Since transitions with $d=0$ do not affect the language accepted by a PFA, we assume $d\ne 0$ for all transitions in the remainder of this paper.

Given an NFA $𝒜$, a (memoryless) stochastic resolver $ℛ$ for $𝒜$ resolves nondeterminism during the run on a word on-the-fly, randomly, and positionally. Formally, $ℛ:\mathrm{\Delta }\mapsto [0,1]$, such that ${\sum }_{\tau =(p,\sigma ,q)\in \mathrm{\Delta }}ℛ(\tau )=1$ holds for every pair $(p,\sigma )\in Q\times \mathrm{\Sigma }$. A resolver $ℛ$ for $𝒜$ turns it into a PFA ${𝒫}_{ℛ}^{𝒜}$. We call $\{\tau \in \mathrm{\Delta }\mid ℛ(\tau )>0\}$ the support of $ℛ$.

Given a threshold $\lambda \in [0,1]$, we say that $𝒜$ is $\lambda$-memoryless stochastically resolvable (or simply $\lambda$-resolvable) if there exists a resolver $ℛ$ for $𝒜$ such that $ℒ(𝒫_{}^{\prime }{}_{\ge \lambda }{}^{})=ℒ(𝒜)$, where ${𝒫}^{\prime }={𝒫}_{ℛ}^{𝒜}$. An automaton $𝒜$ is positively memoryless stochastically resolvable (or simply positively resolvable) if it is $\lambda$-resolvable for some $\lambda \in (0,1]$.

Let $\lambda =\frac{m}{n}$ where $m,n\in {\mathbb{Z}}_{+}$ and . The NFA ${𝒜}_{\lambda }$ over unary alphabet $\{a\}$ is as follows. In the initial state $q_0$ upon reading the letter $a$, ${𝒜}_{\lambda }$ nondeterministically goes to one of $n$ branches, each with $\left(\genfrac{}{}{0pt}{}{n}{m}\right)$ states. Consider an arbitrary ordering of all $m$ sized subsets of $[n]$, $S_1,\mathrm{\dots },S_{\left(\genfrac{}{}{0pt}{}{n}{m}\right)}$. For any branch $j\in [n]$ and $i\in [\left(\genfrac{}{}{0pt}{}{n}{m}\right)]$, the $i$-th state on the $j$-th branch - $q_{S_i}^j$, is accepting iff $j\in S_i$. Refer to Figure 3 for an example with $\lambda =\frac{2}{3}$. The automaton ${𝒜}_{\lambda }$ is $m$-ambiguous, where each word in $\{a^i|i\in [\left(\genfrac{}{}{0pt}{}{n}{m}\right)]\}$ has exactly $m$ accepting runs. Moreover, ${𝒜}_{\lambda }$ is $\frac{m}{n}$-resolvable, since the uniform resolver that picks any transition at $q_0$ with probability $\frac{1}{n}$, accepts every word with probability exactly $\frac{m}{n}$. For any other resolver $ℛ$, consider the $m$ branches $i_1,\mathrm{\dots },i_m$, with the lowest assigned probabilities. Let $\mathrm{\ell }$ be the unique index such that $S_{\mathrm{\ell }}=\{i_1,\mathrm{\dots },i_m\}$. Then for the word $a^{\mathrm{\ell }}$, we have . Hence, ${𝒜}_{\lambda }$ is not $(\lambda +ϵ)$-resolvable for any $ϵ>0$. $◀$

Our approach relies on a reduction from the undecidable universality problem for simple²²2Note that [19] proves the (strict) emptiness problem for simple PFA is undecidable. Since a PFA is universal if and only if its complement is empty, the universality problem is also undecidable. PFAs [37, 19] to the $\lambda$-resolvability problem for an NFA. Consider a simple PFA $𝒫$ over the alphabet $\mathrm{\Sigma }$, whose underlying NFA is $𝒜$. For a simple PFA, the structure of its underlying NFA uniquely determines the probabilities on its transitions: for each state $q$ and letter $\sigma$, there are either one or two outgoing transitions from $q$ labelled with $\sigma$; if there is one transition it must have probability $1$ and if there are two, each must have probability $\frac{1}{2}$.

Intuitively, we want the resolver (if it exists) for the underlying automaton $𝒜$ of $𝒫$ to always induce a simple PFA. So, $𝒜$ is $\lambda$-resolvable if and only if ${𝒫}_{\ge \lambda }$ and $𝒜$ recognise the same language. In principle, a resolver for an NFA does not necessarily enforce that two outgoing transitions both have probability $\frac{1}{2}$ and may use any arbitrary split. To enforce an equal split, we construct an NFA ${𝒜}^{\prime }$ over an extended alphabet ${\mathrm{\Sigma }}^{\prime }$, such that ${𝒜}^{\prime }$ is a super-automaton of $𝒜$. By this, we mean that the alphabet, state set, set of accepting states, and transition set of $𝒜$ are all subsets of those of ${𝒜}^{\prime }$, and we refer to $𝒜$ as a sub-automaton of ${𝒜}^{\prime }$. The constructed NFA ${𝒜}^{\prime }$ is designed so that it admits only one possible $\frac{1}{4}$-resolver, and that the resolver matches the underlying probabilities of the simple PFA $𝒫$ on the part of the automaton of ${𝒜}^{\prime }$ corresponding to $𝒜$. These relations are described in Figure 3.

Our construction has the property that ${𝒜}^{\prime }$ is $\frac{1}{4}$-resolvable if and only if ${𝒫}_{\ge \frac{1}{2}}$ is universal. Essentially, the only possible resolver induces a probabilistic automaton ${𝒫}^{\prime }$ on ${𝒜}^{\prime }$ such that ${𝒫}^{\prime }(w^{\prime }\cdot w)=\frac{1}{2}\cdot 𝒫(w)$ for all words $w\in ℒ(A)$, where $w^{\prime }$ is a fixed word over ${\mathrm{\Sigma }}^{\prime }\setminus \mathrm{\Sigma }$. This ensures $𝒫(w)\ge \frac{1}{2}\iff {𝒫}^{\prime }(w^{\prime }\cdot w)\ge \frac{1}{4}$ for $w\in ℒ(A)$. The construction itself introduces new words, however these words are $\frac{1}{4}$-resolvable by construction.

Without loss of generality, we fix $\mathrm{\Sigma }=\{a,b\}$. ${𝒫}_{\ge \frac{1}{2}}$ is not universal if $𝒜$ is not, and since universality for NFA is decidable, we assume that $ℒ(𝒜)={\mathrm{\Sigma }}^{\ast }$. We construct a super-automaton ${𝒜}^{\prime }$ of $𝒜$ such that it satisfies the following three properties:

1. C.1

   For every state $p$ of ${𝒜}^{\prime }$ and every $\sigma \in {\mathrm{\Sigma }}^{\prime }$, ${𝒜}^{\prime }$ has at most two distinct transitions of the form $(p,\sigma ,q)$ for some state $q$.

2. C.2

   If ${𝒜}^{\prime }$ is $\frac{1}{4}$-resolvable, then its $\frac{1}{4}$-resolvable solution must be a simple PFA.

3. C.3

   The language $ℒ({𝒜}^{\prime })$ is the disjoint union of two languages, ${ℒ}_{\text{ext}}$ (essentially an extension of $ℒ(𝒜)$) and ${ℒ}_{\text{ind}}$ (essentially corresponding to the new part of ${𝒜}^{\prime }$), satisfying:

   1. (a)

      For every $w\in {ℒ}_{\text{ind}}$, ${𝒫}^{\prime }(w)\ge \frac{1}{4}$.

   2. (b)

      For every $w^{\prime \prime }\in {ℒ}_{\text{ext}}$, where ${ℒ}_{\text{ext}}=S\cdot {\mathrm{\Sigma }}^{\ast }$ for some singleton set $S=\{w^{\prime }\}$ over ${\mathrm{\Sigma }}^{\prime }\setminus \mathrm{\Sigma }$ and $w^{\prime \prime }=w^{\prime }\cdot w$ with $w\in {\mathrm{\Sigma }}^{\ast }$, we have ${𝒫}^{\prime }(w^{\prime \prime })=\frac{1}{2}\cdot 𝒫(w)$.

Properties C.1 and C.2 ensure that the simple PFA ${𝒫}^{\prime }$ based on ${𝒜}^{\prime }$ is the unique $\frac{1}{4}$-resolvable solution to ${𝒜}^{\prime }$ if it is $\frac{1}{4}$-resolvable. Notice that regardless of whether ${𝒜}^{\prime }$ has a $\frac{1}{4}$-resolvable solution, ${𝒫}^{\prime }$ is based on ${𝒜}^{\prime }$, and for each word $w\in ℒ({𝒜}^{\prime })$, ${𝒫}^{\prime }$ returns its acceptance probability, which may be less than $\frac{1}{4}$. Property C.3 states that ${𝒫}^{\prime }$ is a $\frac{1}{4}$-resolvable solution to ${𝒜}^{\prime }$ if and only if ${𝒫}_{\ge \frac{1}{2}}$ is universal. Accordingly, we have:

By Lemma 3, we can prove the undecidability of $\lambda$-resolvability by constructing, for any simple PFA $𝒫$ with underlying NFA $𝒜$, an NFA ${𝒜}^{\prime }$ satisfying C.1–C.3. In the remainder of this section, we show how to do this and give intuitions for why these properties hold for the constructed automata. Property C.1 will hold trivially by construction, so we will focus on C.2 and C.3.

The automaton ${𝒜}^{\prime }$ will consist of two sub-automata ${𝒜}_{\text{ind}}$ and ${𝒜}_{\text{ext}}$. The first one, ${𝒜}_{\text{ind}}$ recognises the language ${ℒ}_{\text{ind}}$, which does not depend on the structure of the original NFA $𝒜$, but rather on the numbers of $𝒜$’s states and transitions. In contrast, ${𝒜}_{\text{ext}}$ is an extension (super-automaton) of $𝒜$ corresponding to the language ${ℒ}_{\text{ext}}$.

Consider the NFA $𝒜$ given in Figure 5, where $ℒ(A)=\{aab\}$. This NFA is $\frac{1}{2}$-resolvable. Moreover, every PFA based on $𝒜$ is a $\frac{1}{2}$-resolvable solution, which is neither unique nor necessarily simple. However, if we add two transitions to $𝒜$ and derive the NFA $ℬ$ as shown in Figure 5, where for every word $w\in \{aa\mathrm{♯},aa\mathrm{♭}\}⊊ℒ(B)$, the accepting run on $w$ is unique, then the $\frac{1}{2}$-resolvable solution PFA to $ℬ$ becomes both unique and simple. Note that we not only introduce new transitions but also add a newly accepting state $q_f^{\prime }$ to ensure that no additional words over $\{a,b,\mathrm{♯},\mathrm{♭}\}$ are introduced in a more general case. This example illustrates how property C.2 can be enforced.

More specifically, referring to Figure 7, if $𝒜$ has nondeterministic transitions to states $q$ and $r$ from $p$ on reading $a$, we introduce two new transitions, $(q,\mathrm{♯},q_f^{\prime })$ and $(r,\mathrm{♭},q_f^{\prime })$, in ${𝒜}^{\prime }$, where $\mathrm{♯}$ and $\mathrm{♭}$ are newly introduced symbols corresponding to the original transitions $(p,a,q)$ and $(p,a,r)$, respectively. If we can ensure that there exists a unique word $w_p$ corresponding to state $p$, such that there is a run from the initial state $q_0^{\prime }$ of ${𝒜}^{\prime }$ to $p$ with probability exactly $\frac{1}{2}$, and that the accepting runs on the words $w_p\cdot a\cdot \mathrm{♯}$ and $w_p\cdot a\cdot \mathrm{♭}$ are unique, then we can guarantee that if the PFA ${𝒫}^{\prime }$ is a $\frac{1}{4}$-resolvable solution to ${𝒜}^{\prime }$, then the transition probabilities for both $(p,a,q)$ and $(p,a,r)$ in ${𝒫}^{\prime }$ must be $\frac{1}{2}$. The details of the run on the word $w_p$ are shown in Figure 8. For words of the form ${\$}_0{\$}_i{\$}_j$ where $i=1,2$ and $j=3,\mathrm{\dots },6$, the NFA in this figure has a unique accepting run. Analogous to the NFA $ℬ$, the symbols ${\$}_0,\mathrm{\dots },{\$}_6$, $p$, and $q_0$ are newly introduced and are not in $\mathrm{\Sigma }$. Every PFA based on this automaton is a $\frac{1}{4}$-resolvable solution if the transitions labelled with ${\$}_0$, ${\$}_1$, and ${\$}_2$ have probability exactly $\frac{1}{2}$. For each state $p$, we define $w_p={\$}_{0}p$, treating $p$ as a symbol. Consequently, the run of ${𝒫}^{\prime }$ from $q_0^{\prime }$ to $p$ on $w_p$ has probability exactly $\frac{1}{2}$. We apply this technique to every nondeterministic transition in $𝒜$. Note that the automaton shown in Figure 8 is a part of ${𝒜}^{\prime }$, is disjoint from $𝒜$, and connects to $𝒜$ through transitions of the form $(y,p,p)$ for $p\in Q$. Hence, if ${𝒜}^{\prime }$ has a $\frac{1}{4}$-resolvable solution ${𝒫}^{\prime }$, then for all transitions inherited from $𝒜$, their probability values in ${𝒫}^{\prime }$ must be $\frac{1}{2}$. Accordingly, this construction ensures that property C.2 holds.

Apart from the states of $𝒜$ that have outgoing nondeterministic transitions, we also introduce a transition $(y,q_0,q_0)$ to ${𝒜}^{\prime }$, regardless of whether $q_0$ itself has nondeterministic transitions. See Figure 7 and Figure 8. Consequently, the probability of the run of ${𝒫}^{\prime }$ from $q_0^{\prime }$ to $q_0$ on the word $w_{q_0}={\$}_0{q}_0$ is exactly $\frac{1}{2}$. Moreover, for every word $w\in {\mathrm{\Sigma }}^{\ast }$, we have $w_{q_0}\cdot w\in ℒ({𝒜}^{\prime })$ if and only if $w\in ℒ(A)$. Hence, property C.3b follows.

It is important to explain why we consider the $\frac{1}{4}$-resolvable problem of ${𝒜}^{\prime }$ instead of the $\frac{1}{2}$-resolvable one, as in the previous example with the NFA $ℬ$. Refer to Figure 7 for a modified example. Our intention is to force the $\frac{1}{2}$ probability split using words of the form $w_p\cdot w\cdot {\sigma }^{\prime }$, where $|w|=1$ and ${\sigma }^{\prime }\in \{\mathrm{♯},\mathrm{♭}\}$, however the construction introduces other words that need to be managed. For example, the words $w_p\cdot a\cdot {(ab)}^i\cdot \mathrm{♯}$ and $w_p\cdot a\cdot {(ab)}^i\cdot \mathrm{♭}$ belong to $ℒ({𝒜}^{\prime })$ for all $i\in {\mathbb{Z}}_{+}$. However, for the simple PFA ${𝒫}^{\prime }$ based on ${𝒜}^{\prime }$, we have and ${𝒫}^{\prime }(w_p\cdot a\cdot {(ab)}^i\cdot \mathrm{♭})\ge \frac{1}{2}$ for all $i\in {\mathbb{Z}}_{+}$. Even if we set the probability of the run of ${𝒫}^{\prime }$ from the state $q_0^{\prime }$ to $p$ on $w_p$ to be $1$, we still have ${𝒫}^{\prime }(w_p\cdot a\cdot {(ab)}^i\cdot \mathrm{♯})\to 0$ as $i\to \mathrm{\infty }$. That is, when we introduce the transitions $(q,\mathrm{♯},q_f^{\prime })$ and $(r,\mathrm{♭},q_f^{\prime })$, we may also introduce additional words into $ℒ({𝒜}^{\prime })$. However, based on our tentative construction of ${𝒜}^{\prime }$, it is possible that $ℒ(𝒫_{}^{\prime }{}_{\ge \frac{1}{2}}{}^{})⊊ℒ({𝒜}^{\prime })$, regardless of whether $𝒫$ is universal or not. The words in $ℒ({𝒜}^{\prime })\setminus ℒ(𝒫_{}^{\prime }{}_{\ge \frac{1}{2}}{}^{})$ are of the form ${\$}_0\cdot p\cdot w\cdot {\sigma }^{\prime }$, where $p\in Q$, $w\in {\mathrm{\Sigma }}^{\ast }$ with $|w|\ne 1$, and ${\sigma }^{\prime }$ is a symbol introduced for a nondeterministic transition, such as $\mathrm{♯}$ or $\mathrm{♭}$, etc.

To address this issue, we ensure the probability is at least $\frac{1}{4}$ probability when $|w|\ne 1$, we construct a DFA ${𝒜}_{\text{extra}}$ recognising the language $\{{\$}_0\}\cdot Q\cdot ({\mathrm{\Sigma }}^{\ast }\setminus \mathrm{\Sigma })\cdot \{\mathrm{♯},\mathrm{♭},\mathrm{\dots }\}$ and add it to ${𝒜}^{\prime }$. The automaton ${𝒜}_{\text{extra}}$ includes a unique transition from the initial state $q_0^{\prime }$ to a state $x$ upon reading symbol ${\$}_0$. This transition $(q_0^{\prime },{\$}_0,x)$ is the same as the one shown in Figure 8, with the rest of ${𝒜}_{\text{extra}}$ continuing from $x$. For every simple PFA based on the automaton given in Figure 8, the probability value of the transition $(q_0^{\prime },{\$}_0,x)$ is $\frac{1}{2}$. Thus, for every additional word $w\notin {ℒ}_{\text{ext}}$, we have ${𝒫}^{\prime }(w)\ge \frac{1}{4}$, ensuring that property C.3a holds. Hence, the constructed ${𝒜}^{\prime }$ satisfies properties C.1–C.3.

From Lemma 3, it follows that the $\lambda$-resolvability problem for NFA is undecidable. $◀$

Let $𝒜=(\{a\},Q,q_0,\mathrm{\Delta },F)$ be a unary NFA over the alphabet $\{a\}$, with $|Q|=d$, initial state $q_0$ encoded in a row vector $I\in {\{0,1\}}^d$ and final states encoded in a column vector $F\in {\{0,1\}}^d$. We ask if there is a $P\in {[0,1]}^{d\times d}$ with support at most $\mathrm{\Delta }$ and $\lambda$ such that $I{P}^{n}F\ge \lambda$ whenever $a^n\in ℒ(𝒜)$.

If $P$ exists, it has some support $S\subseteq \mathrm{\Delta }$ and we guess this support of $P$ non-deterministically. The choice of support induces a new NFA ${𝒜}_S\subseteq 𝒜$, in which every edge will be attributed a non-zero probability and $ℒ({𝒜}_S)=\{a^n\mid I{P}^{n}F>0\}$. We verify, in $\mathrm{𝖼𝗈𝖭𝖯}$ [43], that $ℒ({𝒜}_S)=ℒ(𝒜)$. If not, this is not a good support.

Henceforth, we assume $ℒ({𝒜}_S)=ℒ(𝒜)$ and consider the condition to check whether the support $S$ is good. For any $P$ with support $S$ we have $I{P}^{n}F>0$ for $a^n\in ℒ({𝒜}_S)$. It remains to decide whether this probability can be bounded away from zero, that is for some $\lambda >0$, $I{P}^{n}F>\lambda$ whenever $a^n\in ℒ({𝒜}_S)$. The condition we describe is independent of the exact choice of $P$ and is based only on the structure of ${𝒜}_S$. Using $T$ from Lemma 5 we decompose $ℒ({𝒜}_S)$ into $T$ phases and define for all $k\in \{0,\mathrm{\dots },T-1\}$ the set ${ℒ}_k=\{a^{k+Tn}\mid n\in \mathbb{N}\}\cap ℒ(𝒜)$. Each ${ℒ}_k$ is either finite, in which case it turns out there is nothing to do, or eventually periodic with period $T$, in which case we use Lemma 5’s characterisation of non-zero limit:

${ℒ}_k$ is finite.

There is nothing to decide: any $P$ with support $S$ induces a lower bound $\min \{I{P}^k{(P^T)}^{n}F\mid n\in \mathbb{N},a^{k+Tn}\in {ℒ}_k\}>0$ on the weight of the words in ${ℒ}_k$, as the minimum over a finite set of non-zero values.

${ℒ}_k$ is eventually periodic.

We check there exists a path from $q_0$ to some final state $q_f\in F$ of length $k+T\mathrm{\ell }$ for some $\mathrm{\ell }\le d$, and that $q_f$ is in some bottom SCC in ${𝒜}_{𝒮}$. Then for any $P$ with support $S$, Lemma 5 entails a limit distribution ${\pi }^{(k)}\in {[0,1]}^d$ such that ${lim}_{n\to \mathrm{\infty }}I{P}^k{(P^T)}^n={\pi }^{(k)}$, in which ${\pi }^{(k)}(q_f)$ is non-zero. Thus ${lim}_{n\to \mathrm{\infty }}I{P}^k{(P^T)}^{n}F={\pi }^{(k)}F={ϵ}_k>0$. In particular, there exists $n_k$ such that, for all $n^{\prime }>n_k$, we have $I{P}^k{(P^T)}^{n^{\prime }}F>{ϵ}_k/2$. Hence, there is a lower bound on the weights of words in ${ℒ}_k$: $\min \{I{P}^k{(P^T)}^{n}F\mid n:a^{k+Tn}\in {ℒ}_k,n\le n_k\}\cup \{{ϵ}_k/2\}>0$, which is a minimum over a finite set of non-zero values.
If there is no such path, then for any $P$ with support $S$, the limit distribution is zero in all final states: the probability tends to zero no matter the exact choice of probabilities.

For a given $k$, it can be decided in polynomial time whether ${ℒ}_k$ is finite and whether there is a path of the given type. On a boolean matrix $A_S$ representing the reachability graph of ${𝒜}_S$, the vector $I{(A_S)}^k$ and boolean matrix ${(A_S)}^T$ can be computed by iterated squaring in which the reachability questions can be checked.

Thus to summarise, our procedure guesses a support $S\subseteq \mathrm{\Delta }$ and the period $T$ in $\mathrm{𝖭𝖯}$, and verifies in $\mathrm{𝖼𝗈𝖭𝖯}$ both that $ℒ({𝒜}_{𝒮})=ℒ(𝒜)$ and guess the to verify the required reachability queries for $k$. $◀$ In Theorem 11 we show that the problem is $\mathrm{𝖼𝗈𝖭𝖯}$-hard already in the finite-ambiguous case, we present this result alongside the non-unary case in Section 6 due to commonalities.