Reference:

Javier Esparza, Antonín Kučera, and Richard Mayr. Model checking probabilistic pushdown automata. Logical Methods in Computer Science, 2006.

Suggested BibTeX entry:

@article{EKM05-LMCS,
    author = {Javier Esparza and Anton\'{\i}n Ku\v{c}era and Richard Mayr},
    journal = {Logical Methods in Computer Science},
    title = {Model Checking Probabilistic Pushdown Automata},
    year = {2006}
}