The authors consider a probabilistic recursive program working on data of unbounded size, for example, with a geometric probability distribution for what the data looks like. This makes sense for common data structures like trees. Is the expected time that the program will terminate finite? Is it almost sure (probability 1) that all runs, finite and infinite, satisfy a property specified by a deterministic Rabin automaton on infinite words? When the program can be modeled as a probabilistic one-counter automaton, the authors show such questions can be answered in polynomial time.

An earlier work considered more general probabilistic pushdown systems, but used the decidability of the existential theory of the reals, which has greater complexity. The main idea is that although the system is modeled as an infinite Markov chain, the questions can be answered by analyzing another finite Markov chain with some “good” conditions. The paper is quite technical; the justification that these ideas are correct involves the construction of suitable martingales.