On the Decidability of Temporal Properties of Probabilistic Pushdown Automata. - Tomás Brázdil; Antonín Kucera 001; Oldrich Strazovský (STACS, 2005)

Deciding probabilistic bisimilarity over infinite-state probabilistic systems. - Tomás Brázdil; Antonín Kucera 001; Oldrich Strazovský (Acta Informatica, 2008)

On the Controller Synthesis for Finite-State Markov Decision Processes. - Antonín Kucera 001; Oldrich Strazovský (Fundam. Informaticae, 2008)