Publications

Antonín Kučera

Technical Reports

  1. Minimizing Expected Termination Time in One-Counter Markov Decision Processes.
    by T. Brázdil, A. Kučera, P. Novotný, and D. Wojtczak. arXiv:1205.1473 [cs.FL]
  2. 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]
  3. 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]
  4. Efficient Analysis of Probabilistic Programs with an Unbounded Counter.
    by T. Brázdil, S. Kiefer, and A. Kučera. arXiv:1102.2529 [cs.FL]
  5. 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. Technical report FIMU-RS-2011-02, Faculty of Informatics MU, 32 pages, 2011.
    PDF. (Also available at arXiv:1104.3489 [cs.GT].)
  6. 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]
  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. Reachability Games on Extended Vector Addition Systems with States.
    by T. Brázdil, P. Jančar, and A. Kučera. Technical report FIMU-RS-2010-02, Faculty of Informatics MU, 38 pages, 2010.
    PDF. (Also available at arXiv:1002.2557 [cs.GT].)
  9. 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
  10. One-Counter Markov Decision Processes.
    by T. Brázdil, V. Brožek, K. Etessami, A. Kučera, and D. Wojtczak. arXiv:0904.2511 [cs.GT]
  11. 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. (The most recent and corrected version is available at 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. Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances.
    by J. Esparza, A. Kučera, and R. Mayr. Technical report FIMU-RS-2004-07, Faculty of Informatics MU, 26 pages, 2005.
    PostScript, PDF
  17. On the Decidability of Temporal Properties of Probabilistic Pushdown Automata.
    by T. Brázdil, A. Kučera, and O. Stražovský. Technical report FIMU-RS-2005-01, Faculty of Informatics MU, 33 pages, 2005.
    PostScript, PDF
  18. Characteristic Patterns for LTL.
    by A. Kučera and J. Strejček. Technical report FIMU-RS-2004-10, Faculty of Informatics MU, 22 pages, 2004.
    PostScript, PDF
  19. Deciding Probabilistic Bisimilarity over Infinite-State Probabilistic Systems.
    by T. Brázdil, A. Kučera, and O. Stražovský. Technical report FIMU-RS-2004-06, Faculty of Informatics MU, 26 pages, 2004.
    PostScript, PDF
  20. A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications.
    by A. Kučera and Ph. Schnoebelen. Technical report FIMU-RS-2004-05, Faculty of Informatics MU, 32 pages, 2004.
    PostScript, PDF
  21. An Effective Characterization of Properties Definable by LTL Formulae with a Bounded Nesting Depth of the Next-Time Operator.
    by A. Kučera and J. Strejček. Technical report FIMU-RS-2004-04, Faculty of Informatics MU, 11 pages, 2004.
    PostScript, PDF
  22. Model Checking Probabilistic Pushdown Automata.
    by J. Esparza, A. Kučera, and R. Mayr. Technical report FIMU-RS-2004-03, Faculty of Informatics MU, 34 pages, 2004.
    PostScript, PDF
  23. A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata.
    by A. Kučera and R. Mayr. Technical report FIMU-RS-2004-01, Faculty of Informatics MU, 38 pages, 2004.
    PostScript, PDF
  24. The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL.
    by A. Kučera and J. Strejček. Technical report FIMU-RS-2002-03, Faculty of Informatics MU, 24 pages, 2002.
    PostScript, PDF
  25. Why is Simulation Harder Than Bisimulation?
    by A. Kučera and R. Mayr. Technical report FIMU-RS-2002-02, Faculty of Informatics MU, 26 pages, 2002.
    PostScript, PDF
  26. On the Complexity of Semantic Equivalences for Pushdown Automata and BPA.
    by A. Kučera and R. Mayr. Technical report FIMU-RS-2002-01, Faculty of Informatics MU, 32 pages, 2002.
    PostScript, PDF
  27. Model-Checking LTL with Regular Valuations for Pushdown Systems.
    by J. Esparza, A. Kučera, and S. Schwoon. Informatics Research Report EDI-INF-RR-0044, Division of Informatics, University of Edinburgh (LFCS), 17 pages, 2001.
    PostScript, PDF
  28. On Simulation-Checking with Sequential Systems.
    by A. Kučera. Technical report FIMU-RS-2000-05, Faculty of Informatics MU, 34 pages, 2000.
    PostScript, PDF
  29. Efficient Verification Algorithms for One-Counter Processes.
    by A. Kučera. Technical report FIMU-RS-2000-03, Faculty of Informatics MU, 24 pages, 2000.
    PostScript, PDF
  30. A Logical Viewpoint on Process-Algebraic Quotients.
    by A. Kučera and J. Esparza. Technical report FIMU-RS-2000-01, Faculty of Informatics MU, 26 pages, 2000.
    PostScript, PDF
  31. Simulation and Bisimulation over One-Counter Processes.
    by P. Jančar, A. Kučera, and F. Moller. Uppsala Computing Science Research Report No. 165, Uppsala University, 13 pages, 1999.
    PostScript, PDF
  32. Simulation Preorder on Simple Process Algebras.
    by A. Kučera and R. Mayr. Technical report TUM-I9902, TU-Munchen, 23 pages, 1999.
    PostScript, PDF
  33. Weak Bisimilarity with Infinite-State Systems can be Decided in Polynomial Time.
    by A. Kučera and R. Mayr. Technical report TUM-I9830, TU-Munchen, 28 pages, 1998.
    PostScript, PDF
  34. Deciding Bisimulation-Like Equivalences with Finite-State Processes.
    by P. Jančar, A. Kučera, and R. Mayr. Technical report TUM-I9805, TU-Munchen, 24 pages, 1998.
    PostScript, PDF
  35. Bisimilarity of Processes with Finite-state Systems.
    by P. Jančar and A. Kučera. Technical report FIMU-RS-97-02, Faculty of Informatics MU, 19 pages, 1997.
    PostScript, PDF
  36. How to Parallelize Sequential Processes.
    by A. Kučera. Technical report FIMU-RS-96-05, Faculty of Informatics MU, 24 pages, 1996.
    PostScript, PDF
  37. Comparing Expressibility of Normed BPA and Normed BPP Processes.
    by I. Černá, M. Křetínský, and A. Kučera. Technical report FIMU-RS-96-02, Faculty of Informatics MU, 28 pages, 1996.
    PostScript, PDF
  38. Regularity is Decidable for Normed PA Processes in Polynomial Time.
    by A. Kučera. Technical report FIMU-RS-96-01, Faculty of Informatics MU, 17 pages, 1996.
    PostScript, PDF
  39. Deciding Regularity in Process Algebras.
    by A. Kučera. BRICS Report Series RS-95-52, Department of Computer Science, University of Aarhus, 42 pages, 1995.
    PostScript, PDF

Proceedings Papers

  1. Determinacy in Stochastic Games with Unbounded Payoff Functions.
    by T. Brázdil, A. Kučera, and P. Novotný. In Proceedings of 8th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2012), LNCS, Springer. To appear.
    PDF
  2. 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), pages 141-152, volume 7392 of LNCS, Springer, 2012.
    PDF
  3. 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), pages 23-38, volume 7358 of LNCS, Springer, 2012
    PDF
  4. 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.
    PDF
  5. 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.
    PDF
  6. 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.
    PDF
  7. 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.
    PDF
  8. 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.
    PDF
  9. 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.
    PDF
  10. 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.
    PDF
  11. 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.
    PDF
  12. 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.
    PDF
  13. 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.
    PDF
  14. 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 230-242, volume 5330 of LNCS. Springer, 2008.
    PostScript, PDF
  15. 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.
    PostScript, PDF
  16. The Satisfiability Problem for Probabilistic CTL.
    by T. Brázdil, V. Forejt, J. Křetí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.
    PostScript, PDF
  17. 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.
    PostScript, PDF
  18. 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.
    PostScript, PDF
  19. 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.
    PostScript, PDF
  20. 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.
    PostScript, PDF
  21. On the Controller Synthesis for Finite-State Markov Decision Processes.
    by A. Kučera and O. Stražovský. In Proceedings of 25th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS 2005), pages 541-552, volume 3821 of LNCS, Springer, 2005.
    PostScript, PDF
  22. 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.
    PostScript, PDF
  23. Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances.
    by J. Esparza, A. Kučera, and R. Mayr. In Proceedings of 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005), pages 117-126, IEEE Computer Society, 2005.
    PostScript, PDF
  24. On the Decidability of Temporal Properties of Probabilistic Pushdown Automata.
    by T. Brázdil, A. Kučera, and O. Stražovský. In Proceedings of 22nd International Symposium on Theoretical Aspects of Computer Science (STACS 2005), pages 145-157, volume 3404 of LNCS, Springer, 2005.
    PostScript, PDF
  25. Characteristic Patterns for LTL.
    by A. Kučera and J. Strejček. In Proceedings of 31st Conference on Current Trends in Theory and Practice of Informatics (SOFSEM'05), pages 239-249, volume 3381 of LNCS, Springer, 2005.
    PostScript, PDF
  26. A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications.
    by A. Kučera and Ph. Schnoebelen. In Proceedings of 15th International Conference on Concurrency Theory (CONCUR'04), pages 371-386, volume 3170 of LNCS, Springer, 2004.
    PostScript, PDF
  27. Deciding Probabilistic Bisimilarity over Infinite-State Probabilistic Systems.
    by T. Brázdil, A. Kučera, and O. Stražovský. In Proceedings of 15th International Conference on Concurrency Theory (CONCUR'04), pages 193-208, volume 3170 of LNCS, Springer, 2004.
    PostScript, PDF
  28. A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata.
    by A. Kučera and R. Mayr. In Proceedings of 3rd IFIP International Conference on Theoretical Computer Science (IFIP TCS2004), pages 395-408, Kluwer, 2004.
    PostScript, PDF
  29. Model-Checking Probabilistic Pushdown Automata.
    by J. Esparza, A. Kučera, and R. Mayr. In Proceedings of 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004), pages 12-21, IEEE Computer Society, 2004.
    PostScript, PDF
  30. Deciding Bisimilarity between BPA and BPP Processes.
    by P. Jančar, A. Kučera, and F. Moller. In Proceedings of 14th International Conference on Concurrency Theory (CONCUR'03), pages 159-173, volume 2761 of LNCS, Springer, 2003.
    PostScript, PDF
  31. On Homogeneous Segments.
    by R. Batůšek, I. Kopeček, and A. Kučera. In Proceedings of 5th International Conference on Text Speech and Dialogue (TSD 2003), pages 152-157, volume 2807 of LNCS, Springer, 2003.
    PostScript, PDF
  32. The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL.
    by A. Kučera and J. Strejček. In Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'02), pages 276-291, volume 2471 of LNCS, Springer, 2002.
    PostScript, PDF
  33. Why is Simulation Harder Than Bisimulation?
    by A. Kučera and R. Mayr. In Proceedings of 13th International Conference on Concurrency Theory (CONCUR'02), pages 594-609, volume 2421 of LNCS, Springer, 2002.
    PostScript, PDF
  34. On the Complexity of Semantic Equivalences for Pushdown Automata and BPA.
    by A. Kučera and R. Mayr. In Proceedings of 27th International Symposium on Mathematical Foundations of Computer Science (MFCS 2002), pages 433-445, volume 2420 of LNCS, Springer, 2002.
    PostScript, PDF
  35. Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds.
    by P. Jančar, A. Kučera, F. Moller, and Z. Sawa. In Proceedings of Foundations of Software Science and Computation Structures (FOSSACS 2002), pages 172-186, volume 2303 of LNCS, Springer, 2002.
    PostScript, PDF
  36. Model-Checking LTL with Regular Valuations for Pushdown Systems.
    by J. Esparza, A. Kučera, and S. Schwoon. In Proceedings of 4th International Symposium on Theoretical Aspects of Computer Software (TACS 2001), pages 316-339, volume 2215 of LNCS, Springer, 2001.
  37. On Simulation-Checking with Sequential Systems.
    by A. Kučera. In Proceedings of 6th Asian Computing Science Conference (ASIAN 2000), pages 133-148, volume 1961 of LNCS, Springer, 2000.
    PostScript, PDF
  38. Efficient Verification Algorithms for One-Counter Processes.
    by A. Kučera. In Proceedings of 27th International Colloquium on Automata, Languages, and Programming (ICALP 2000), pages 317-328, volume 1853 of LNCS, Springer, 2000.
    PostScript, PDF
  39. Simulation and Bisimulation over One-Counter Processes.
    by P. Jančar, A. Kučera, and F. Moller. In Proceedings of 17th International Symposium on Theoretical Aspects of Computer Science (STACS 2000), pages 334-345, volume 1770 of LNCS, Springer, 2000.
    PostScript, PDF
  40. A Logical Viewpoint on Process-Algebraic Quotients.
    by A. Kučera and J. Esparza. In Proceedings of 8th Annual Conference of the European Association for Computer Science Logic (CSL'99), pages 499-514, volume 1683 of LNCS, Springer, 1999.
    PostScript, PDF
  41. Weak Bisimilarity with Infinite-State Systems can be Decided in Polynomial Time.
    by A. Kučera and R. Mayr. In Proceedings of 10th International Conference on Concurrency Theory (CONCUR'99), pages 368-382, volume 1664 of LNCS, Springer, 1999.
    PostScript, PDF
  42. Simulation Preorder on Simple Process Algebras.
    by A. Kučera and R. Mayr. In Proceedings of 26th International Colloquium on Automata, Languages, and Programming (ICALP'99), pages 503-512, volume 1644 of LNCS, Springer, 1999.
    PostScript, PDF
  43. Deciding Bisimulation-Like Equivalences with Finite-State Processes.
    by P. Jančar, A. Kučera, and R. Mayr. In Proceedings of 25th International Colloquium on Automata, Languages, and Programming (ICALP'98), pages 200-211, volume 1443 of LNCS, Springer, 1998.
    PostScript, PDF
  44. On Finite Representations of Infinite-State Behaviours.
    by A. Kučera. In Proceedings of 24th Seminar on Current Trends in Theory and Practice of Informatics (SOFSEM'97), pages 481-488, volume 1338 of LNCS, Springer, 1997.
    PostScript, PDF
  45. Bisimilarity of Processes with Finite-State Systems.
    by P. Jančar and A. Kučera. In Proceedings of 2nd International Workshop on Verification of Infinite State Systems (INFINITY'97), pages 72-86, UPMAIL TR No. 148, University of Uppsala, 1997.
    PostScript, PDF
  46. How to Parallelize Sequential Processes.
    by A. Kučera. In Proceedings of 8th International Conference on Concurrency Theory (CONCUR'97), pages 302-316, volume 1243 of LNCS, Springer, 1997.
    PostScript, PDF
  47. Regularity is Decidable for Normed PA Processes in Polynomial Time.
    by A. Kučera. In Proceedings of 16th Conference on Foundations of Software Technology and Theoretical Computer Science (FST-TCS'96), pages 111-122, volume 1180 of LNCS, Springer, 1996.
    PostScript, PDF
  48. Regularity is Decidable for Normed BPA and Normed BPP Processes in Polynomial Time.
    by A. Kučera. In Proceedings of 23rd Seminar on Current Trends in Theory and Practice of Informatics (SOFSEM'96), pages 377-384, volume 1175 of LNCS, Springer, 1996.
    PostScript, PDF
  49. Bisimilarity is Decidable in the Union of Normed BPA and Normed BPP Processes.
    by I. Černá, M. Křetínský and A. Kučera. In Proceedings of 1st International Workshop on Verification of Infinite State Systems (INFINITY'96), pages 32-46, MIP-9614, University of Passau, 1996.
    PostScript, PDF

Journals

  1. Stochastic Game Logic.
    by C. Baier, T. Brázdil, M. Größer, and A. Kučera. Acta Informatica. 49:203-224. Springer, 2012. DOI 10.1007/s00236-012-0156-0.
    Preprint available as PDF.
  2. Analyzing Probabilistic Pushdown Automata.
    by T. Brázdil, J. Esparza, S. Kiefer, and A. Kučera. Formal Methods in System Design. Springer, 2012. DOI 10.1007/s10703-012-0166-0. A semi-formal survey of the existing results and proof techniques.
    Preprint available as PDF.
  3. 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, 2012. DOI 10.1016/j.ic.2012.01.008.
    Preprint available as PDF.
  4. 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.
    Preprint available as PDF.
  5. On the Complexity of Checking Semantic Equivalences between Pushdown Processes and Finite-state Processes.
    by A. Kučera and R. Mayr. Information and Computation. 208(7):772-796. Elsevier, 2010.
    Preprint available as PDF.
  6. Deciding Probabilistic Bisimilarity over Infinite-State Probabilistic Systems.
    by T. Brázdil, A. Kučera, and O. Stražovský. Acta Informatica. 45(2):131-154. Springer, 2008.
    Preprint available as PDF.
  7. On the Controller Synthesis for Finite-State Markov Decision Processes.
    by A. Kučera and O. Stražovský. Fundamenta Informaticae. 82(1-2):141-153. IOS Press, 2008.
    Preprint available as PDF.
  8. 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.
    Preprint available as PDF.
  9. Comparing Infinite-State Systems with Their Finite-State Specifications.
    by A. Kučera and Ph. Schnoebelen. Theoretical Computer Science. 358(2-3):315-333. Elsevier, 2006.
    Preprint available as PDF.
  10. Equivalence Checking on Infinite-State Systems: Techniques and Results.
    by A. Kučera and P. Jančar. Theory and Practice of Logic Programming. 6(3):227-264. Cambridge University Press, 2006.
    Preprint available as PDF.
  11. Model-Checking Probabilistic Pushdown Automata.
    by J. Esparza, A. Kučera, and R. Mayr. Logical Methods in Computer Science. 2(1:2):1-31, 2006.
  12. The Stuttering Principle Revisited.
    by A. Kučera and J. Strejček. Acta Informatica, 41(7-8):415-434. Springer, 2005.
    Preprint available as PDF.
  13. DP Lower Bounds for Equivalence-Checking and Model-Checking of One-Counter Automata.
    by P. Jančar, A. Kučera, F. Moller, and Z. Sawa. Information and Computation, 188(1):1-19. Academic Press, 2004.
    Preprint available as PDF.
  14. A Logical Viewpoint on Process-Algebraic Quotients.
    by A. Kučera, and J. Esparza. Journal of Logic and Computation, 13(6):863-880. Oxford University Press, 2003.
    Preprint available as PDF.
  15. Model-Checking LTL with Regular Valuations for Pushdown Systems.
    by J. Esparza, A. Kučera, and S. Schwoon. Information and Computation 186(2):355-376. Academic Press, 2003.
    Preprint available as PDF.
  16. The Complexity of Bisimilarity-Checking for One-Counter Processes.
    by A. Kučera. Theoretical Computer Science, 304(1-3):157-183. Elsevier, 2003.
    Preprint available as PDF.
  17. Simulation Preorder over Simple Process Algebras.
    by A. Kučera and R. Mayr. Information and Computation 173(2):184-198. Academic Press, 2002.
    Preprint available as PDF.
  18. Weak Bisimilarity between Finite-State Systems and BPA or normed BPP is Decidable in Polynomial Time.
    by A. Kučera and R. Mayr. Theoretical Computer Science 270(1-2):677-700. Elsevier, 2002.
    Preprint available as PDF.
  19. Deciding Bisimulation-Like Equivalences with Finite-State Processes.
    by P. Jančar, A. Kučera, and R. Mayr. Theoretical Computer Science, 258(1-2):409-433. Elsevier, 2001.
    Preprint available as PDF.
  20. Effective Decomposability of Sequential Behaviours.
    by A. Kučera. Theoretical Computer Science, 242(1-2):71-89. Elsevier, 2000.
    Preprint available as PDF.
  21. Regularity of Normed PA Processes.
    by A. Kučera. Information Processing Letters, 72(1-2):9-17. Elsevier, 1999.
  22. On Finite Representations of Infinite-State Behaviours.
    by A. Kučera. Information Processing Letters, 70(1):23-30. Elsevier, 1999.
  23. Comparing Expressibility of Normed BPA and Normed BPP Processes.
    by I. Černá, M. Křetínský, and A. Kučera. Acta Informatica, 36(3):233-256. Springer, 1999.
  24. Bisimilarity of Processes with Finite-State Systems.
    by P. Jančar and A. Kučera. In Volume 9 of ENTCS, Elsevier, 1997.
  25. Bisimilarity is Decidable in the Union of Normed BPA and Normed BPP Processes.
    by I. Černá, M. Křetínský, and A. Kučera. In Volume 5 of ENTCS, Elsevier, 1997.

Invited Papers

  1. Playing Games with Counter Automata.
    by A. Kučera. In Proceedings of 6th International Workshop on Reachability Problems (RP 2012), pages 29-41, volume 7550 of LNCS, Springer, 2012.
  2. Methods for Quantitative Analysis of Probabilistic Pushdown Automata.
    by A. Kučera. In Proceedings of 7th International Workshop on Verification of Infinite-State Systems (Infinity 2005), pages 3-15, volume 149(1) of ENTCS, Elsevier, 2006.
  3. Equivalence-Checking with Infinite-State Systems: Techniques and Results.
    by A. Kučera and P. Jančar. In Proceedings of 29th Seminar on Current Trends in Theory and Practice of Informatics (SOFSEM 2002), pages 41-73, volume 2540 of LNCS, Springer, 2002.

Book Chapters

  1. Turn-Based Stochastic Games.
    by A. Kučera. In Lectures in Game Theory for Computer Scientists (edited by Krzysztof R. Apt and Erich Grädel). Pages 146-184, Cambridge University Press, 2011. ISBN 9780521198660.
  2. Randomness: A Tool for Constructing and Analyzing Computer Programs.
    by A. Kučera. In Randomness through Computation (edited by Hector Zenil). World Scientific, 2011. ISBN 978-981-4327-74-9.
  3. Effective Analysis of Infinite State Stochastic Processes and Games.
    by A. Kučera. In Logics and Languages for Reliability and Security (edited by J. Esparza, B. Spanfelner, O. Grumberg). Pages 155-178, IOS Press, 2010. ISBN 978-1-60750-099-5.

Edited Volumes

  1. Theoretical Computer Science 417(3).
    Edited by P. Hliněný and A. Kučera. A special issue of TCS devoted to MFCS 2010. Elsevier, 2012. ISSN 0304-3975.
  2. Proceedings of 4th International Workshop on Reachability Problems (RP 2010).
    Edited by A. Kučera and I. Potapov. ISBN 3-642-15348-8. Volume 6227 of LNCS, Springer, 2010.
  3. Proceedings of 35th International Symposium on Mathematical Foundations of Computer Science (MFCS 2010).
    Edited by P. Hliněný and A. Kučera. ISBN 3-642-15154-X. Volume 6281 of LNCS, Springer, 2010.
  4. Proceedings of 35th Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2009).
    Edited by M. Nielsen, A. Kučera, P.B. Miltersen, C. Palamidessi, P. Tůma, and F. Valencia. ISBN 3-540-95890-8. Volume 5404 of LNCS, Springer, 2009.
  5. Proceedings of 35th Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2009), volume II.
    Edited by M. Bieliková, M. Nielsen, A. Kučera, P.B. Miltersen, C. Palamidessi, P. Tůma, and F. Valencia. ISBN 978-80-7378-059-3. MATFYZPRESS, 2009.
  6. Proceedings of 32nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2007).
    Edited by L. Kučera and A. Kučera. ISBN 3-540-74455-X. Volume 4708 of LNCS, Springer, 2007.
  7. Proceedings of 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006).
    Edited by L. Matyska, A. Kučera, T. Vojnar, Z. Kotásek, D. Antoš, and O. Krajíček. ISBN 80-214-3287-X. Faculty of Information Technology, Brno University of Technology, 2006.
  8. Proceedings of 1st Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2005).
    Edited by M. Češka, J. Gruska, and A. Kučera. Technical report FIMU-RS-2005-11, Faculty of Informatics, Masaryk University, Brno, 2005.
  9. Proceedings of 14th International Conference on Concurrency Theory (CONCUR 2002).
    Edited by L. Brim, P. Jančar, M. Křetínský, and A. Kučera. ISBN 3-540-44043-7. Volume 2421 of LNCS, Springer, 2002.
  10. Proceedings of 4th International Workshop on Verification of Infinite State Systems (INFINITY 2002).
    Edited by A. Kučera and R. Mayr. ENTCS 68(6), Elsevier, 2002. (Pre-Proceedings are available as a technical report FIMU-RS-2002-04.)