Decidable Problems for Probabilistic Automata on Infinite Words

TL;DR

This paper investigates the decidability of key qualitative problems for probabilistic automata on infinite words with parity acceptance, identifying decidable subclasses and establishing complexity bounds.

Contribution

It unifies existing results, introduces a robust subclass with decidable problems, and analyzes complexity for probabilistic automata on infinite words.

Findings

Decidable for a robust subclass of probabilistic automata

Positive and almost problems decidable for lasso-shaped words

Most problems are PSPACE-complete

Abstract

We consider probabilistic automata on infinite words with acceptance defined by parity conditions. We consider three qualitative decision problems: (i) the positive decision problem asks whether there is a word that is accepted with positive probability; (ii) the almost decision problem asks whether there is a word that is accepted with probability 1; and (iii) the limit decision problem asks whether for every epsilon > 0 there is a word that is accepted with probability at least 1 - epsilon. We unify and generalize several decidability results for probabilistic automata over infinite words, and identify a robust (closed under union and intersection) subclass of probabilistic automata for which all the qualitative decision problems are decidable for parity conditions. We also show that if the input words are restricted to lasso shape (regular) words, then the positive and almost problems are decidable for all probabilistic automata with parity conditions. For most decidable problems we show an optimal PSPACE-complete complexity bound.