BRÁZDIL, Tomáš, Václav BROŽEK, Jan HOLEČEK and Antonín KUČERA. Discounted Properties of Probabilistic Pushdown Automata. In Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008. Berlin Heidelberg New York: Springer, 2008, p. 230-242. ISBN 978-3-540-89438-4.
BRÁZDIL, Tomáš, Václav BROŽEK and Vojtěch FOREJT. Branching-Time Model-Checking of Probabilistic Pushdown Automata. In Proc. of 9th Internat. Workshop on Verification of Infinite-State Systems. Lisboa: Univerisity of Lisboa, 2007, p. 24-33.
ESPARZA, Javier, Antonín KUČERA and Richard MAYR. Model Checking Probabilistic Pushdown Automata. Logical Methods in Computer Science. 2006, vol. 2, 1-2, p. 1-31. ISSN 1860-5974.