Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Resolving Nondeterminism by Chance

Soumyajit Paul, David Purser, Sven Schewe, Qiyi Tang, Patrick Totzke, Di-De Yen

TL;DR

This paper introduces and analyzes stochastic on-the-fly resolution of nondeterminism for automata, defining $\lambda$-memoryless stochastic resolvability as the existence of a memoryless resolver that makes the acceptance probability $\mathcal{P}(w)$ meet $\mathcal{L}(\mathcal{P}_{\geq\lambda}) = \mathcal{L}(\mathcal{A})$ on finite words. It establishes a spectrum of resolvability from $0$ to $1$, showing $0$-resolvable corresponds to unrestricted nondeterminism and $1$-resolvable aligns with history-determinism; however, deciding $\lambda$-resolvability is undecidable for general NFAs, while decidable for finitely-ambiguous automata with varying complexity across classes. The authors also provide constructive results, including a unary automaton family $\mathcal{A}_{\lambda}$ that demonstrates strict separations in the spectrum, and a reduction-based undecidability proof via simple PFAs. In the unary case, they give a detailed decision framework showing $\text{PR}$ and $\lambda$-resolvability can be analyzed via Markov-chain representations and sub-automata checks, achieving decidability and precise complexity characterizations for several restricted cases, thereby advancing understanding of when nondeterminism can be effectively resolved with probabilistic guarantees.

Abstract

History-deterministic automata are those in which nondeterministic choices can be correctly resolved stepwise: there is a strategy to select a continuation of a run given the next input letter so that if the overall input word admits some accepting run, then the constructed run is also accepting. Motivated by checking qualitative properties in probabilistic verification, we consider the setting where the resolver strategy can randomize and only needs to succeed with lower-bounded probability. We study the expressiveness of such stochastically-resolvable automata as well as consider the decision questions of whether a given automaton has this property. In particular, we show that it is undecidable to check if a given NFA is $λ$-stochastically resolvable. This problem is decidable for finitely-ambiguous automata. We also present complexity upper and lower bounds for several well-studied classes of automata for which this problem remains decidable.

Resolving Nondeterminism by Chance

TL;DR

This paper introduces and analyzes stochastic on-the-fly resolution of nondeterminism for automata, defining -memoryless stochastic resolvability as the existence of a memoryless resolver that makes the acceptance probability meet on finite words. It establishes a spectrum of resolvability from to , showing -resolvable corresponds to unrestricted nondeterminism and -resolvable aligns with history-determinism; however, deciding -resolvability is undecidable for general NFAs, while decidable for finitely-ambiguous automata with varying complexity across classes. The authors also provide constructive results, including a unary automaton family that demonstrates strict separations in the spectrum, and a reduction-based undecidability proof via simple PFAs. In the unary case, they give a detailed decision framework showing and -resolvability can be analyzed via Markov-chain representations and sub-automata checks, achieving decidability and precise complexity characterizations for several restricted cases, thereby advancing understanding of when nondeterminism can be effectively resolved with probabilistic guarantees.

Abstract

History-deterministic automata are those in which nondeterministic choices can be correctly resolved stepwise: there is a strategy to select a continuation of a run given the next input letter so that if the overall input word admits some accepting run, then the constructed run is also accepting. Motivated by checking qualitative properties in probabilistic verification, we consider the setting where the resolver strategy can randomize and only needs to succeed with lower-bounded probability. We study the expressiveness of such stochastically-resolvable automata as well as consider the decision questions of whether a given automaton has this property. In particular, we show that it is undecidable to check if a given NFA is -stochastically resolvable. This problem is decidable for finitely-ambiguous automata. We also present complexity upper and lower bounds for several well-studied classes of automata for which this problem remains decidable.

Paper Structure

This paper contains 7 sections, 4 theorems, 1 equation, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Nondeterministic Finite Automata
  4. Probabilistic Finite Automata
  5. Stochastic Resolvers
  6. Lambda-Resolvability
  7. Deciding Resolvability for Unary Finite Automata

Key Result

Theorem 1

For every $\lambda \in (0,1)_{\mathbb{Q}\xspace}$ there exists a unary NFA $\mathcal{A}_{\lambda}$ such that $\mathcal{A}_{\lambda}$ is $\lambda$-resolvable but not $(\lambda + \epsilon)$-resolvable for any $\epsilon>0$.

Figures (3)

  • Figure 1: Two unambiguous NFA (all missing transitions implicitly go to a non-accepting sink). The one on the left is $\lambda$-resolvable for all $\lambda\le 1/2$. The one on the right is not positively resolvable, because no matter the choice of transition probability, the probability of $b^n$ tends to zero as $n$ grows.
  • Figure 2: The automaton $\mathcal{A}_{\lambda}$ for $\lambda = \frac{2}{3}$, in the proof of \ref{['thm:lambda-spectrum']}.
  • Figure 3: The construction for \ref{['thm:undecidable']}.

Theorems & Definitions (4)

  • Theorem 1
  • Theorem 2
  • Theorem 3
  • Lemma 3