TY - GEN
T1 - Quantitative analysis of probabilistic pushdown automata
T2 - 20th Annual IEEE Symposium on Logic in Computer Science, LICS 2005
AU - Esparza, Javier
AU - Kučera, Antonín
AU - Mayr, Richard
PY - 2005
Y1 - 2005
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=26844538915&partnerID=8YFLogxK
U2 - 10.1109/LICS.2005.39
DO - 10.1109/LICS.2005.39
M3 - Conference contribution
AN - SCOPUS:26844538915
SN - 0769522661
T3 - Proceedings - Symposium on Logic in Computer Science
SP - 117
EP - 126
BT - Proceedings - 20th Annual IEEE symposium on Logic in Computer Science, LICS 2005
Y2 - 26 June 2005 through 29 June 2005
ER -