Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Resolving Nondeterminism with Randomness

Thomas A. Henzinger, Aditya Prakash, K. S. Thejaswini

TL;DR

This work broadens the landscape between deterministic and nondeterministic $\f$-regular automata by introducing stochastic resolvability and memoryful strategies, yielding new classes (MA, MR, SR) that interpolate between HD/SD and full nondeterminism. It analyzes two interaction models—adversarial and stochastic resolvability—and establishes a nuanced hierarchy of expressivity, succinctness, and computational complexity across safety, reachability, weak, coB"uchi, and Büchi conditions. Key results include polynomial-time SR→MA conversion for coB"uchi, NP-completeness for MA recognition, and strict parity index hierarchies for SR automata, along with complexity separations among MA, MR, SR, and HD across various acceptance conditions. The findings illuminate trade-offs between succinctness and decidability, with practical implications for reactive synthesis and model checking, and raise open questions about resolver-independence of probabilities and the full decidability landscape for SR/MR in parity settings.

Abstract

In automata theory, while determinisation provides a standard route to solving many common problems in automata theory, some weak forms of nondeterminism can be dealt with in some problems without costly determinisation. For example, the handling of specifications given by nondeterministic automata over infinite words for the problems of reactive synthesis or runtime verification requires resolving nondeterministic choices without knowing the future of the input word. We define and study classes of $ω$-regular automata for which the nondeterminism can be resolved by a policy that uses a combination of memory and randomness on any input word, based solely on the prefix read so far. We examine two settings for providing the input word to an automaton. In the first setting, called adversarial resolvability, the input word is constructed letter-by-letter by an adversary, dependent on the resolver's previous decisions. In the second setting, called stochastic resolvability, the adversary pre-commits to an infinite word and reveals it letter-by-letter. In each setting, we require the existence of an almost-sure resolver, i.e., a policy that ensures that as long as the adversary provides a word in the language of the underlying nondeterministic automaton, the run constructed by the policy is accepting with probability 1. The class of automata that are adversarially resolvable is the well-studied class of history-deterministic automata. The case of stochastically resolvable automata, on the other hand, defines a novel class. Restricting the class of resolvers in both settings to stochastic policies without memory introduces two additional new classes of automata. We show that the new automaton classes offer interesting trade-offs between succinctness, expressivity, and computational complexity, providing a fine gradation between deterministic automata and nondeterministic automata.

Resolving Nondeterminism with Randomness

TL;DR

This work broadens the landscape between deterministic and nondeterministic -regular automata by introducing stochastic resolvability and memoryful strategies, yielding new classes (MA, MR, SR) that interpolate between HD/SD and full nondeterminism. It analyzes two interaction models—adversarial and stochastic resolvability—and establishes a nuanced hierarchy of expressivity, succinctness, and computational complexity across safety, reachability, weak, coB"uchi, and Büchi conditions. Key results include polynomial-time SR→MA conversion for coB"uchi, NP-completeness for MA recognition, and strict parity index hierarchies for SR automata, along with complexity separations among MA, MR, SR, and HD across various acceptance conditions. The findings illuminate trade-offs between succinctness and decidability, with practical implications for reactive synthesis and model checking, and raise open questions about resolver-independence of probabilities and the full decidability landscape for SR/MR in parity settings.

Abstract

In automata theory, while determinisation provides a standard route to solving many common problems in automata theory, some weak forms of nondeterminism can be dealt with in some problems without costly determinisation. For example, the handling of specifications given by nondeterministic automata over infinite words for the problems of reactive synthesis or runtime verification requires resolving nondeterministic choices without knowing the future of the input word. We define and study classes of -regular automata for which the nondeterminism can be resolved by a policy that uses a combination of memory and randomness on any input word, based solely on the prefix read so far. We examine two settings for providing the input word to an automaton. In the first setting, called adversarial resolvability, the input word is constructed letter-by-letter by an adversary, dependent on the resolver's previous decisions. In the second setting, called stochastic resolvability, the adversary pre-commits to an infinite word and reveals it letter-by-letter. In each setting, we require the existence of an almost-sure resolver, i.e., a policy that ensures that as long as the adversary provides a word in the language of the underlying nondeterministic automaton, the run constructed by the policy is accepting with probability 1. The class of automata that are adversarially resolvable is the well-studied class of history-deterministic automata. The case of stochastically resolvable automata, on the other hand, defines a novel class. Restricting the class of resolvers in both settings to stochastic policies without memory introduces two additional new classes of automata. We show that the new automaton classes offer interesting trade-offs between succinctness, expressivity, and computational complexity, providing a fine gradation between deterministic automata and nondeterministic automata.

Paper Structure

This paper contains 26 sections, 61 theorems, 27 equations, 14 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Automata and resolution of nondeterminism
  3. Automata
  4. Resolution of nondeterminism
  5. Comparisons between the different notions
  6. Safety automata
  7. Reachability and weak automata
  8. CoBüchi automata
  9. Büchi automata
  10. Expressivity
  11. Complexity of recognition
  12. Memoryless adversarially resolvable automata
  13. Memoryless-stochastically resolvable automata and stochastically resolvable automata
  14. Discussion
  15. Useful definitions and lemmas
  16. ...and 11 more sections

Key Result

Lemma 2

For every parity automaton $\mathcal{A}$, a resolver $\mathcal{M}$ is an almost-sure resolver for $\mathcal{A}$ if and only if $\mathcal{M}$ is a finite-memory strategy that is almost-surely winning for Eve against all strategies of Adam in the SR game on $\mathcal{A}$.

Figures (14)

  • Figure 1: Examples of resolving nondeterminism with randomness
  • Figure 2: The landscape of automata that admit different resolvers
  • Figure 3: A coBüchi automaton that is SD but not SR. Rejecting transitions are represented by dashed arrows.
  • Figure 4: A HD coBüchi automaton that is not MR. Rejecting transitions are represented by dashed arrows.
  • Figure 5: A semantically deterministic Büchi automaton that is not stochastically resolvable. The accepting transitions are double-arrowed, and the initial state is $q_0$.
  • ...and 9 more figures

Theorems & Definitions (102)

  • Definition 1: History-determinism game
  • Example 2
  • Lemma 2
  • Lemma 4
  • proof
  • Theorem 5
  • Theorem 6
  • Theorem 7
  • Lemma 7: Folklore
  • Lemma 8
  • ...and 92 more