Recurrence and Transience for Probabilistic Automata

Mathieu Tracol, Christel Baier & Marcus GröSser
In a context of $\omega$-regular specifications for infinite execution sequences, the classical B\"uchi condition, or repeated liveness condition, asks that an accepting state is visited infinitely often. In this paper, we show that in a probabilistic context it is relevant to strengthen this infinitely often condition. An execution path is now accepting if the \emph{proportion} of time spent on an accepting state does not go to zero as the length of the path goes to...