Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

ESPARZA Javier KUČERA Antonín MAYR Richard

Year of publication 2005
Type Article in Proceedings
Conference Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005)
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords Probabilistic Pushdown Automata; Infinite Markov Chains; Quantitative Analysis
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.