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

Survey papers

1. Analyzing Probabilistic Pushdown Automata.
   by T. Brázdil, J. Esparza, S. Kiefer, and A. Kučera. A semi-formal survey of the existing results and proof techniques submitted to FMSD. Comments are welcome. Preprint available as PDF.

Conference proceedings

1. Minimizing Expected Termination Time in One-Counter Markov Decision Processes.
   by T. Brázdil, A. Kučera, P. Novotný, and D. Wojtczak. In Proceedings of 39th International Colloquium on Automata, Languages and Programming (ICALP 2012). To Appear.
   
   
2. Efficient Controller Synthesis for Consumption Games with Multiple Resource Types.
   by T. Brázdil, K. Chatterjee, A. Kučera, and P. Novotný. In Proceedings of 24th International Conference on Computer Aided Verification (CAV 2012). To Appear.
   
   
3. Stabilization of Branching Queueing Networks.
   by T. Brázdil and S. Kiefer. In Proceedings of 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012), Leibniz International Proceedings in Informatics (LIPIcs), 2012. To appear.
   
   
4. Fixed-delay Events in Generalized Semi-Markov Processes Revisited.
   by T. Brázdil, J. Krčál, J. Křetínský, and V. Řehák. In Proceedings of 22st International Conference on Concurrency Theory (CONCUR 2011), pages 140-155, volume 6901 of LNCS, Springer, 2011.
   
   
5. Runtime Analysis of Probabilistic Programs with Unbounded Recursion.
   by T. Brázdil, S. Kiefer, A. Kučera, and I. Hutařová Vařeková. In Proceedings of 38th International Colloquium on Automata, Languages and Programming (ICALP 2011), pages 319-331, volume 6756 of LNCS, Springer, 2011.
   
   
6. Approximating the termination value of One-counter MDPs and Stochastic Games.
   by T. Brázdil, V. Brožek, K. Etessami, and A. Kučera. In Proceedings of 38th International Colloquium on Automata, Languages and Programming (ICALP 2011), pages 332-343, volume 6756 of LNCS, Springer, 2011.
   
   
7. Efficient Analysis of Probabilistic Programs with an Unbounded Counter.
   by T. Brázdil, S. Kiefer, and A. Kučera. In Proceedings of 23rd International Conference on Computer Aided Verification (CAV 2011), pages 208-224, volume 6806 of LNCS. Springer, 2011.
   
   
8. Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.
   by T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt, and A. Kučera. In Proceedings of 26th Annual IEEE Symposium on Logic in Computer Science (LICS 2011). IEEE, 2011.
   
   
9. Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata.
   by T. Brázdil, J. Krčál, J. Křetínský, A. Kučera, and V. Řehák. In Proceedings of 14th International Conference on Hybrid Systems: Computation and Control (HSCC'11), pages 33-42. ACM, 2011.
   
   
10. One-Counter Stochastic Games.
    by T. Brázdil, V. Brožek, and Kousha Etessami. In Proceedings of 30th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), pages 108-119, Leibniz International Proceedings in Informatics (LIPIcs), 2010.
    
    
11. Stochastic Real-Time Games with Qualitative Timed Automata Objectives.
    by T. Brázdil, J. Krčál, J. Křetínský, A. Kučera, and V. Řehák. In Proceedings of 21st International Conference on Concurrency Theory (CONCUR 2010), pages 207-221, volume 6269 of LNCS. Springer, 2010.
    
    
12. Space-efficient scheduling of stochastically generated tasks.
    by T. Brázdil, J. Esparza, S. Kiefer, and M. Luttenberger. In Proceedings of 37th International Colloquium on Automata, Languages, and Programming (ICALP 2010), part II, volume 6199 of LNCS, ARCoSS, pages 539-550. Springer, 2010.
    
    
13. Reachability Games on Extended Vector Addition Systems with States.
    by T. Brázdil, P. Jančar, and A. Kučera. In Proceedings of 37th International Colloquium on Automata, Languages, and Programming (ICALP 2010), pages 478-489, volume 6199 of LNCS. Springer, 2010.
    
    
14. 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), pages 863-874, 2010.
    
    
15. 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). pages 49.60, 2009.
    
    
16. 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), pages 61-72, 2009.
    
    
17. 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.
    
    
18. 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.
    
    
19. 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.
    
    
20. 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.
    
    
21. 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.
    
    
22. 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.
    
    
23. 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.
    
    
24. 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.
    
    
25. 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.
    
    
26. 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.
    
    
27. 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.
    
    
28. 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. Approximating the termination value of One-counter MDPs and Stochastic Games.
   by T. Brázdil, V. Brožek, K. Etessami, and A. Kučera. Information and Computation. Elsevier. To appear.


2. Space-efficient scheduling of stochastically generated tasks.
   by T. Brázdil, J. Esparza, S. Kiefer, and M. Luttenberger. Information and Computation. 210(9):87-110. Elsevier. 2012.
   
   
3. Qualitative Reachability in Stochastic BPA Games.
   by T. Brázdil, V. Brožek, A. Kučera, and J. Obdržálek. Information and Computation. 209(8):1160-1183. Elsevier, 2011.
   
   
4. Deciding Probabilistic Bisimilarity over Infinite-State Probabilistic Systems.
   by T. Brazdil, A. Kucera, and O. Strazovsky. Acta Informatica. 45(2):131-154. Springer, 2008.
   
   
5. 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.
   
   
6. 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 (incomplete :-( )

1. Efficient Controller Synthesis for Consumption Games with Multiple Resource Types.
   by T. Brázdil, K. Chatterjee, A. Kučera, and P. Novotný. arXiv:1202.0796 [cs.GT]
   
   
2. Approximating the termination value of One-counter MDPs and Stochastic Games.
   by T. Brázdil, V. Brožek, K. Etessami, and A. Kučera. arXiv:1104.4978 [cs.GT]
   
   
3. Efficient Analysis of Probabilistic Programs with an Unbounded Counter.
   by T. Brázdil, S. Kiefer, and A. Kučera. arXiv:1102.2529 [cs.FL]
   
   
4. Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.
   by T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt, and A. Kučera. arXiv:1104.3489 [cs.GT].
   
   
5. Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata.
   by T. Brázdil, J. Krčál, J. Křetínský, A. Kučera, and V. Řehák. arXiv:1101.4204 [cs.SY]
   
   
6. Reachability Games on Extended Vector Addition Systems with States.
   by T. Brázdil, P. Jančar, and A. Kučera. arXiv:1002.2557 [cs.GT].
   
   
7. Runtime Analysis of Probabilistic Programs with Unbounded Recursion.
   by T. Brázdil, S. Kiefer, A. Kučera, and I. Hutařová Vařeková. arXiv:1007.1710 [cs.LO]
   
   
8. 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. Technical report FIMU-RS-2009-09, Faculty of Informatics MU, 46 pages, 2009.
   PostScript, PDF
   
   
9. 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]
   


10. Space-efficient scheduling of stochastically generated tasks.
    by T. Brázdil, J. Esparza, S. Kiefer, and M. Luttenberger. arXiv:1004.4286 [cs.PF]
    
    
11. Qualitative Reachability in Stochastic BPA Games.
    by T. Brázdil, V. Brožek, A. Kučera, and J. Obdržálek. arXiv:1003.0118 [cs.GT].
    
    
12. 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
    
    
13. 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
    
    
14. 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
    
    
15. 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
    
    
16. 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
    
    
17. 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
    
    
18. 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

• CONCUR 2012 - 23rd International Conference on Concurrency Theory (P.C. membership)
• QEST 2012 - 9th International Conference on Quantitative Evaluation of SysTems (P.C. membership)
• QAPL 2012 - Tenth Workshop on Quantitative Aspects of Programming Languages (P.C. membership)
• MFCS 2011 - 36TH INTERNATIONAL SYMPOSIUM ON MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE (P.C. membership)
• QAPL 2011 - Ninth Workshop on Quantitative Aspects of Programming Languages (P.C. membership)
• QAPL 2010 - Eighth Workshop on Quantitative Aspects of Programming Languages (P.C. membership)
• 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

• Petr Slovák
  
• Jan Kretínský
  
• Václav Brožek
  
• Vojtěch Forejt
  

Teaching (czech)

Personal