Homepage of Tomáš Brázdil

RNDr. Tomáš Brázdil, Ph.D. Department of Computer Science Faculty of Informatics Masaryk University Brno, Czech Republic Email: xbrazdil (for the rest see bottom of this page)

Research

• Algorithmic analysis of stochastic systems
• Probabilistic temporal logics
• Stochastic processes and games

Ph.D. thesis

Awards & Fellowships

• E. W. Beth Dissertation Prize
• Alexander von Humboldt Fellowship
• Rector's Prize for the best Ph.D. students of Masaryk University

Publications

Conference proceedings

1. One-Counter Markov Decision Processes.
   by T. Brázdil, V. Brožek, K. Etessami, A. Kučera, and D. Wojtczak. In Proceedings of ACM-SIAM Symposium on Discrete Algorithms (SODA 2010). To appear.
   
   
2. On the Memory Consumption of Probabilistic Pushdown Automata.
   by T. Brázdil, J. Esparza, and S. Kiefer, In Proceedings of 29th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS 2009). To appear.
   
   
3. Continuous-Time Stochastic Games with Time-Bounded Reachability.
   by T. Brázdil, V. Forejt, J. Krčál, J. Křetínský, and A. Kučera. In Proceedings of 29th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS 2009). To appear.
   
   
4. Qualitative Reachability in Stochastic BPA Games.
   by T. Brázdil, V. Brožek, A. Kučera, and J. Obdržálek. In Proceedings of 26th International Symposium on Theoretical Aspects of Computer Science (STACS 2009), pages 207-218, 2009.
   
   
5. Discounted Properties of Probabilistic Pushdown Automata.
   by T. Brázdil, V. Brožek, J. Holeček, and A. Kučera. In Proceedings of 15th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2008), pages 148-159, volume 5126 of LNCS. Springer, 2008.
   
   
6. Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives.
   by T. Brázdil, V. Forejt, and A. Kučera. In Proceedings of 35th International Colloquium on Automata, Languages and Programming (ICALP 2008), pages 148-159, volume 5126 of LNCS. Springer, 2008.
   
   
7. The Satisfiability Problem for Probabilistic CTL.
   by T. Brázdil, V. Forejt, J. Kretínský and A. Kučera. In Proceedings of 23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008), pages 391-402, IEEE Computer Society, 2008.
   
   
8. Stochastic Game Logic.
   by C. Baier, T. Brázdil, M. Größer, and A. Kučera. In Proceedings of 4th International Conference on the Quantitative Evaluation of SysTems (QEST 2007), pages 227-236, IEEE Computer Society, 2007.
   
   
9. Strategy Synthesis for Markov Decision Processes and Branching-Time Logics.
   by T. Brázdil and V. Forejt. In Proceedings of 18th International Conference on Concurrency Theory (CONCUR 2007), 428-444, volume 4703 of LNCS, Springer, 2007.
   
   
10. Reachability in Recursive Markov Decision Processes.
    by T. Brázdil, V. Brožek, V. Forejt, and A. Kučera. In Proceedings of 17th International Conference on Concurrency Theory (CONCUR 2006), pages 358-374, volume 4137 of LNCS. Springer, 2006.
    
    
11. Stochastic Games with Branching-Time Winning Objectives.
    by T. Brázdil, V. Brožek, V. Forejt, and A. Kučera. In Proceedings of 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), pages 349-358, IEEE Computer Society, 2006.
    
    
12. Computing the Expected Accumulated Reward and Gain for a Subclass of Infinite Markov Chains.
    by T. Brázdil and A. Kučera. In Proceedings of 25th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS 2005), pages 372-383, volume 3821 of LNCS, Springer, 2005.
    
    
13. Analysis and Prediction of the Long-Run Behavior of Probabilistic Sequential Programs with Recursion.
    by T. Brázdil, J. Esparza, and A. Kučera. In Proceedings of 46th Annual Symposium on Foundations of Computer Science (FOCS 2005), pages 521-530, IEEE Computer Society, 2005.
    
    
14. On the Decidability of Temporal Properties of Probabilistic Pushdown Automata.
    by T. Brázdil, A. Kucera, and O. Strazovský. In Proceedings of 22nd International Symposium on Theoretical Aspects of Computer Science (STACS'05), pages 145-157, volume 3404 of LNCS, Springer-Verlag, 2005.
    
    
15. Deciding Probabilistic Bisimilarity over Infinite-State Probabilistic Systems.
    by T. Brazdil, A. Kucera, and O. Strazovsky. In Proceedings of 15th International Conference on Concurrency Theory (CONCUR'04), pages 193-208, volume 3170 of LNCS, Springer-Verlag, 2004.
    
    

Workshop proceedings

1. Branching-Time Model-Checking of Probabilistic Pushdown Automata.
   by T. Brázdil, V. Brožek, and V. Forejt In Proceedings of 9th International Workshop on Verification of Infinite-State Systems (INFINITY 2007), pages 24-33, University of Lisboa, 2007.
   
   
2. Local Distributed Model Checking of RegCTL.
   by T. Brazdil, I. Cerna In Proceedings of 1st International Workshop on Parallel and Distributed Model Checking (PDMC'02), volume 68 of Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers, 2002.
   
   

Journals

1. Deciding Probabilistic Bisimilarity over Infinite-State Probabilistic Systems.
   by T. Brazdil, A. Kucera, and O. Strazovsky. Acta Informatica. 45(2):131-154. Springer, 2008.
   
   
2. Reachability in Recursive Markov Decision Processes.
   by T. Brázdil, V. Brožek, V. Forejt, and A. Kučera. Information and Computation. 206(5):520-537. Elsevier, 2008.
   
   
3. Model checking of RegCTL.
   by T. Brazdil and I. Cerna, in Computing and Informatics, Slovensko. ISSN 1335-9150, 2006, vol. 25, no. 1, pages 81-97.



Technical Reports

1. One-Counter Markov Decision Processes.
   by T. Brázdil, V. Brožek, K. Etessami, A. Kučera, and D. Wojtczak. arXiv:0904.2511v4 [cs.GT]
   


2. Space-efficient scheduling of stochastically generated tasks.
   by T. Brázdil, J. Esparza, S. Kiefer, and M. Luttenberger. Technical report, Technische Universität München, Institut für Informatik, April 2009.
   PDF
   
   
3. Qualitative Reachability in Stochastic BPA Games.
   by T. Brázdil, V. Brožek, A. Kučera, and J. Obdržálek. Technical report FIMU-RS-2009-01, Faculty of Informatics MU, 37 pages, 2009.
   PostScript, PDF
   
   
4. Discounted Properties of Probabilistic Pushdown Automata.
   by T. Brázdil, V. Brožek, J. Holeček, and A. Kučera. Technical report FIMU-RS-2008-08, Faculty of Informatics MU, 32 pages, 2008.
   PostScript, PDF
   
   
5. Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives.
   by T. Brázdil, V. Forejt, and A. Kučera. Technical report FIMU-RS-2008-05, Faculty of Informatics MU, 48 pages, 2008.
   PostScript, PDF
   
   
6. The Satisfiability Problem for Probabilistic CTL.
   by T. Brázdil, V. Forejt, J. Křetínský, and A. Kučera. Technical report FIMU-RS-2008-03, Faculty of Informatics MU, 34 pages, 2008.
   PostScript, PDF
   
   
7. Stochastic Games with Branching-Time Winning Objectives.
   by T. Brázdil, V. Brožek, V. Forejt, and A. Kučera. Technical report FIMU-RS-2006-02, Faculty of Informatics MU, 37 pages, 2006.
   PostScript, PDF
   
   
8. On the Decidability of Temporal Properties of Probabilistic Pushdown Automata.
   by T. Brázdil, A. Kucera, and O. Strazovský. Technical report FIMU-RS-2005-01, Faculty of Informatics MU, 33 pages, 2005.
   PostScript, PDF
   
   
9. Deciding Probabilistic Bisimilarity over Infinite-State Probabilistic Systems.
   by T. Brazdil, A. Kucera, and O. Strazovsky. Technical report FIMU-RS-2004-06, Faculty of Informatics MU, 26 pages, 2004.
   PostScript, PDF
   
   
10. Model Checking in IPv6 Hardware Router Design.
    by J. Barnat, T. Brazdil, P. Krcal, V. Rehak, and D. Safranek. Technical Report 07, CESNET, July 2002.
    PostScript

Memberships

• QAPL 2009 - Seventh Workshop on Quantitative Aspects of Programming Languages (P.C. membership)
• QAPL 2008 - Sixth Workshop on Quantitative Aspects of Programming Languages (P.C. membership)

Past Master Students

• Bc. et Bc. et Bc. Jan Kretínský
  
• Mgr. Václav Brožek
  
• Mgr. Vojtěch Forejt
  

Teaching (czech)

Personal