Publications

Antonín Kučera

Technical Reports

  1. Efficient Algorithms for Checking Fast Termination in VASS.
    by T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, and D. Velan. arXiv:1708.09253 [cs.LO]
  2. Synthesis of Optimal Resilient Control Strategies.
    by C. Baier, C. Dubslaff, Ľ. Korenčiak, A. Kučera, and V. Řehák. arXiv:1707.03223 [cs.SY]
  3. Mean-Payoff Optimization in Continuous-Time Markov Chains with Parametric Alarms.
    by C. Baier, C. Dubslaff, Ľ. Korenčiak, A. Kučera, and V. Řehák. arXiv:1706.06486 [cs.PF]
  4. Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration.
    by Ľ. Korenčiak, A. Kučera, and V. Řehák. arXiv:1607.00372 [cs.PF]
  5. Stability in Graphs and Games.
    by T. Brázdil, V. Forejt, A. Kučera, and P. Novotný. arXiv:1604.006386 [cs.LO]
  6. Strategy Synthesis in Adversarial Patrolling Games.
    by T. Brázdil, P. Hliněný, A. Kučera, V. Řehák, and M. Abaffy. arXiv:1507.03407 [cs.GT]
  7. Strategy Synthesis for General Deductive Games Based on SAT Solving.
    by M. Klimoš and A. Kučera. arXiv:1407.3926 [cs.AI]
  8. Minimizing Running Costs in Consumption Systems.
    by T. Brázdil, D. Klaška, A. Kučera, and P. Novotný. arXiv:1402.4995 [cs.SY]
  9. 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]
  10. 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]
  11. 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]
  12. Efficient Analysis of Probabilistic Programs with an Unbounded Counter.
    by T. Brázdil, S. Kiefer, and A. Kučera. arXiv:1102.2529 [cs.FL]
  13. 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].)
  14. 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]
  15. 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]
  16. 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].)
  17. 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
  18. 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]
  19. 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].)
  20. 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
  21. 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
  22. 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
  23. 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
  24. 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
  25. 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
  26. 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
  27. 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
  28. 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
  29. 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
  30. 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
  31. 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
  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. Technical report FIMU-RS-2002-03, Faculty of Informatics MU, 24 pages, 2002.
    PostScript, PDF
  33. 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
  34. 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
  35. 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
  36. 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
  37. 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
  38. 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
  39. 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
  40. Simulation Preorder on Simple Process Algebras.
    by A. Kučera and R. Mayr. Technical report TUM-I9902, TU-Munchen, 23 pages, 1999.
    PostScript, PDF
  41. 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
  42. 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
  43. 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
  44. How to Parallelize Sequential Processes.
    by A. Kučera. Technical report FIMU-RS-96-05, Faculty of Informatics MU, 24 pages, 1996.
    PostScript, PDF
  45. 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
  46. 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
  47. 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. Synthesis of Optimal Resilient Control Strategies.
    by C. Baier, C. Dubslaff, L. Korenčiak, A. Kučera, and V. Řehák. In Proceedings of 15th International Symposium on Automated Technology for Verification and Analysis (ATVA 2017). Springer, 2017. To appear.
  2. Mean-payoff optimization in continuous-time Markov chains with parametric alarms.
    by C. Baier, C. Dubslaff, L. Korenčiak, A. Kučera, and V. Řehák. In Proceedings of 14th International Conference on Quantitative Evaluation of SysTems (QEST 2017). Springer, 2017. To appear.
  3. Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration.
    by L. Korenčiak, A. Kučera, and V. Řehák. In Proceedings of IEEE International Symposium on Modelling, Analysis and Simulation of Computer and Telecommunications Systems (MASCOTS 2016), pages 367-372. IEEE, 2016.
  4. Optimizing the Expected Mean Payoff in Energy Markov Decision Processes.
    by T. Brázdil, A. Kučera, and P. Novotný. In Proceedings of 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016), pages 32-49, volume 9938 of LNCS, Springer, 2016.
  5. Stability in Graphs and Games.
    by T. Brázdil, V. Forejt, A. Kučera, and P. Novotný. In Proceedings of 27th International Conference on Concurrency Theory (CONCUR 2016), pages 10:1-10:14, LIPIcs 59, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
    PDF
  6. Regular Strategies and Strategy Improvement: Efficient Tools for Solving Large Patrolling Problems.
    by A. Kučera and T. Lamser. In Proceedings of 15th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2016), pages 1171-1179, 2016.
    PDF
  7. Cobra: A Tool for Solving General Deductive Games.
    by M. Klimoš and A. Kučera. In Proceedings of 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2015), pages 31-47, volume 9450 of LNCS, Springer 2015.
    PDF
  8. Long-Run Average Behaviour of Probabilistic Vector Addition Systems.
    by T. Brázdil, S. Kiefer, A. Kučera, and P. Novotný. In Proceedings of 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015), pages 44-55, IEEE, 2015.
    PDF
  9. MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives.
    by T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera. In Proceedings of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015), pages 181-187, volume 9035 of LNCS, Springer, 2015.
    PDF
  10. Minimizing Running Costs in Consumption Systems.
    by T. Brázdil, D. Klaška, A. Kučera, and P. Novotný. In Proceedings of 26th International Conference on Computer Aided Verification (CAV 2014), pages 457-472, volume 8559 of LNCS. Springer, 2014
    PDF
  11. Zero-Reachability in Probabilistic Multi-Counter Automata.
    by T. Brázdil, S. Kiefer, A. Kučera, P. Novotný, and J.-P. Katoen. In Proceedings of 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2014). ACM, 2014.
    PDF
  12. Solving Adversarial Patrolling Games with Bounded Error (Extended Abstract).
    by M. Abaffy, B. Bošanský, T. Brázdil, J. Krčál, A. Kučera, and V. Řehák. In Proceedings of 13th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2014), 2014.
  13. Trading Performance for Stability in Markov Decision Processes.
    by T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera. In Proceedings of 28th Annual IEEE Symposium on Logic in Computer Science (LICS 2013), pages 331-340. IEEE, 2013.
    PDF
  14. 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), pages 94-105, volume 7721 of LNCS, Springer, 2013
    PDF
  15. 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
  16. 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
  17. 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
  18. 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
  19. 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
  20. 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), pages 33-42. IEEE, 2011.
    PDF
  21. 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
  22. 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
  23. 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
  24. 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
  25. 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
  26. 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
  27. 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
  28. 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
  29. 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
  30. 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
  31. 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
  32. 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
  33. 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
  34. 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
  35. 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
  36. 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
  37. 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
  38. 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
  39. 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
  40. 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
  41. 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
  42. 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
  43. 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
  44. 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
  45. 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
  46. 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
  47. 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
  48. 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
  49. 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.
  50. 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
  51. 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
  52. 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
  53. 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
  54. 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
  55. 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
  56. 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
  57. 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
  58. 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
  59. 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
  60. 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
  61. 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
  62. 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. A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata.
    by A. Kučera and R. Mayr. Journal of Computer and System Sciences. Elsevier, 2017. To appear.
  2. Trading performance for stability in Markov decision processes.
    by T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera. Journal of Computer and System Sciences. 84(2017):144-170. Elsevier, 2017. DOI 10.1016/j.jcss.2016.09.009.
  3. Runtime Analysis of Probabilistic Programs with Unbounded Recursion.
    by T. Brázdil, S. Kiefer, A. Kučera, I. Hutařová Vařeková. Journal of Computer and System Sciences. 81(1):288-310. Elsevier, 2015. DOI 10.1016/j.jcss.2014.06.005.
  4. Efficient Analysis of Probabilistic Programs with an Unbounded Counter.
    by T. Brázdil, S. Kiefer, and A. Kučera. Journal of the ACM. 61(6), Article 41, 35 pages, 2014. DOI 10.1145/2629599.
  5. Branching-time model-checking of probabilistic pushdown automata.
    by T. Brázdil, V. Brožek, V. Forejt, and A. Kučera. Journal of Computer and System Sciences. 80(1):139-156. Elsevier, 2014. DOI 10.1016/j.jcss.2013.07.001.
  6. Markov Decision Processes with Multiple Long-run Average Objectives.
    by T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt, and A. Kučera. Logical Methods in Computer Science. 10(1):1-29, 2014.
  7. 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. Information and Computation. 224:46-70. Elsevier, 2013. DOI 10.1016/j.ic.2013.01.001.
  8. 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. 222:121-138. Elsevier, 2013. DOI 10.1016/j.ic.2012.01.008.
    Preprint available as PDF.
  9. Analyzing Probabilistic Pushdown Automata.
    by T. Brázdil, J. Esparza, S. Kiefer, and A. Kučera. Formal Methods in System Design. 43(2):124-163. Springer, 2013. DOI 10.1007/s10703-012-0166-0. A semi-formal survey of the existing results and proof techniques.
    Preprint available as PDF.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. 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.
  18. 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.
  19. 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.
  20. 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.
  21. 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.
  22. 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.
  23. 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.
  24. 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.
  25. 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.
  26. 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.
  27. Effective Decomposability of Sequential Behaviours.
    by A. Kučera. Theoretical Computer Science, 242(1-2):71-89. Elsevier, 2000.
    Preprint available as PDF.
  28. Regularity of Normed PA Processes.
    by A. Kučera. Information Processing Letters, 72(1-2):9-17. Elsevier, 1999.
  29. On Finite Representations of Infinite-State Behaviours.
    by A. Kučera. Information Processing Letters, 70(1):23-30. Elsevier, 1999.
  30. 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.
  31. Bisimilarity of Processes with Finite-State Systems.
    by P. Jančar and A. Kučera. In Volume 9 of ENTCS, Elsevier, 1997.
  32. 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. On the Existence and Computability of Long-Run Average Properties in Probabilistic VASS.
    by A. Kučera. In Proceedings of 20th International Symposium on Fundamentals of Computation Theory (FCT 2015), pages 1-13, volume 9210 of LNCS, Springer, 2015.
    Preprint available as PDF.
  2. 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.
    Preprint available as PDF.
  3. 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.
  4. 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. Fundamenta Informaticae 123(1).
    Edited by A. Ciabattoni, R. Freivalds, A. Kučera, I. Potapov, and S. Szeider. A special issue devoted to MFCS&CSL 2010 Satellite Workshops. IOS Press, 2013. ISSN 0169-2968.
  2. Proceedings of 8th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2012).
    Edited by A. Kučera, T.A. Henzinger, J. Nešetřil, T. Vojnar, and D. Antoš. ISBN 978-3-642-36044-2. Volume 7721 of LNCS, Springer, 2013.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.)