Methods for Quantitative Analysis of Probabilistic Pushdown Automata

We present several constructions and techniques which have recently been used to tackle the prob- lems of qualitative/quantitative analysis of probabilistic pushdown automata.