Recognizing ω-regular languages with probabilistic automata

Probabilistic finite automata as acceptors for languages over finite words have been studied by many researchers. In this paper, we show how probabilistic automata can serve as acceptors for ω-regular languages. Our main results are that our variant of probabilistic Buchi automata (PBA) is more expressive than non-deterministic ω-automata, but a certain subclass of PBA, called uniform PBA, has exactly the power of ω-regular languages. This also holds for probabilistic ω-automata with Streett or Rabin acceptance. We show that certain ω-regular languages have uniform PBA of linear size, while any nondeterministic Streett automaton is of exponential size, and vice versa. Finally, we discuss the emptiness problem for uniform PBA and the use of PBA for the verification of Markov chains against qualitative linear-time properties.