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...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.