Recurrence and Transience for Probabilistic Automata

Abstract

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 infinity. We  
introduce associated notions of recurrence and transience for 
non-homogeneous finite Markov chains and study the computational 
complexity of the associated problems. As Probabilistic B\"uchi Automata 
(PBA) have been an attempt to generalize B\"uchi automata to a 
probabilistic context, we define a class of Constrained Probabilistic 
Automata  with our new accepting condition on runs. The accepted language 
is defined by the requirement that the measure of the set of accepting 
runs is positive (probable semantics) or equals 1 (almost-sure 
semantics).  In contrast to the PBA case, we prove that 
the emptiness problem for the language of a constrained probabilistic 
B\"uchi automaton with the probable semantics is decidable.