Probabilistic Automata over Infinite Words: Expressiveness, Efficiency, and Decidability

TL;DR

This paper explores probabilistic automata over infinite words, analyzing their expressiveness, efficiency, and decision problems, with a focus on probable semantics and various acceptance conditions.

Contribution

It provides a comprehensive overview of the fundamental properties of probabilistic omega-automata, highlighting their expressiveness and decision complexities.

Findings

Probabilistic omega-automata have distinct expressiveness compared to nondeterministic automata.

Decision problems vary significantly depending on acceptance semantics and conditions.

Probable semantics offers a unique perspective on automata behavior over infinite words.

Abstract

Probabilistic omega-automata are variants of nondeterministic automata for infinite words where all choices are resolved by probabilistic distributions. Acceptance of an infinite input word can be defined in different ways: by requiring that (i) the probability for the accepting runs is positive (probable semantics), or (ii) almost all runs are accepting (almost-sure semantics), or (iii) the probability measure of the accepting runs is greater than a certain threshold (threshold semantics). The underlying notion of an accepting run can be defined as for standard omega-automata by means of a Buechi condition or other acceptance conditions, e.g., Rabin or Streett conditions. In this paper, we put the main focus on the probable semantics and provide a summary of the fundamental properties of probabilistic omega-automata concerning expressiveness, efficiency, and decision problems.