The report FIMU-RS-2005-07
Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances
A full version of the paper presented at LICS 2005. July 2005, 26 pages.
Available as Postscript,
Probabilistic pushdown automata (pPDA) have been identified as a natural model
for probabilistic programs with recursive procedure calls. Previous
works considered the decidability and complexity of the model-checking
problem for pPDA and various probabilistic temporal logics.
In this paper we concentrate on computing the expected values and variances
of various random variables defined over runs of a given probabilistic
pushdown automaton. In particular, we show how to compute the expected
accumulated reward and the expected gain for certain classes of reward
functions. Using these results, we show how to analyze various quantitative
properties of pPDA that are not expressible in conventional
probabilistic temporal logics.