Publications

Antonín Kučera

Proceedings Papers

  1. Multiple Mean-Payoff Optimization under Local Stability Constraints.
    by D. Klaška, A. Kučera, V. Kůr, V. Musil, and V. Řehák. In Proceedings of 39th Annual AAAI Conference on Artificial Intelligence (AAAI 2025), AAAI Press, 2025. To Appear.
  2. The Finite Satisfiability Problem for PCTL is Undecidable.
    by M. Chodil and A. Kučera In Proceedings of 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024), Article No.22, pages 1-14, 2024.
  3. Optimizing Local Satisfaction of Long-Run Average Objectives in Markov Decision Processes.
    by D. Klaška, A. Kučera, V. Kůr, V. Musil, and V. Řehák. In Proceedings of 38th Annual AAAI Conference on Artificial Intelligence (AAAI 2024), pages 20143-20150, AAAI Press, 2024.
  4. Asymptotic Complexity Estimates for Probabilistic Programs and their VASS Abstractions.
    by M. Ajdarów and A. Kučera. In Proceedings of 34th International Conference on Concurrency Theory (CONCUR 2023), pages 12:1-12:16, LIPIcs 279, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
  5. Synthesizing Resilient Strategies for Infinite-Horizon Objectives in Multi-Agent Systems.
    by D. Klaška, A. Kučera, M. Kurečka, V. Musil, P. Novotný, and V. Řehák. In Proceedings of 32nd International Joint Conference on Artificial Intelligence (IJCAI 2023), pages 171-179, 2023.
  6. Mean Payoff Optimization for Systems of Periodic Service and Maintenance.
    by D. Klaška, A. Kučera, V. Musil, and V. Řehák. In Proceedings of 32nd International Joint Conference on Artificial Intelligence (IJCAI 2023), pages 5386-5393, 2023.
  7. On-the-fly Adaptation of Patrolling Strategies in Changing Environments.
    by T. Brázdil, D. Klaška, A. Kučera, V. Musil, P. Novotný, and V. Řehák. In Proceedings of 38th Conference on Uncertainty in Artificial Intelligence (UAI 2022). PMLR 180:244-254, 2022.
  8. General Optimization Framework for Recurrent Reachability Objectives.
    by D. Klaška, A. Kučera, V. Musil, and V. Řehák. In Proceedings of 31st International Joint Conference on Artificial Intelligence (IJCAI-ECAI 2022), pages 4642-4648, International Joint Conferences on Artificial Intelligence, 2022.
  9. Minimizing Expected Intrusion Detection Time in Adversarial Patrolling (Extended abstract).
    by D. Klaška, A. Kučera, V. Musil, and V. Řehák. In Proceedings of 21st International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2022), pages 1660-1662, IFAAMAS, 2022.
  10. The Satisfiability Problem for a Quantitave Fragment of PCTL.
    by M. Chodil and A. Kučera. In Proceedings of 23rd International Symposium on Fundamentals of Computation Theory (FCT 2021), pages 149-161, volume 12867 of LNCS, Springer, 2021.
  11. Deciding Polynomial Termination Complexity for VASS Programs.
    by M. Ajdarów and A. Kučera. In Proceedings of 32nd International Conference on Concurrency Theory (CONCUR 2021), pages 30:1-30:15, LIPIcs 203, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
  12. Regstar: Efficient Strategy Synthesis for Adversarial Patrolling Games.
    by D. Klaška, A. Kučera, V. Musil, and V. Řehák. In Proceedings of 37th Conference on Uncertainty in Artificial Intelligence (UAI 2021), PMLR 161:471-481, 2021.
  13. Efficient Analysis of VASS Termination Complexity.
    by A. Kučera, J. Leroux, and D. Velan. In Proceedings of 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020), pages 676-688, ACM, 2020.
    PDF. Conference talk
  14. Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling.
    by M. Blondin, J. Esparza, M. Helfrich, A. Kučera, and P.J. Meyer. In Proceedings of 32nd International Conference on Computer Aided Verification (CAV 2020), pages 372-397, volume 12225 of LNCS, Springer, 2020.
  15. Adversarial Patrolling with Drones.
    by D. Klaška, A. Kučera, and V. Řehák. In Proceedings of 19th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2020), pages 629-637.
  16. Deciding Fast Termination for Probabilistic VASS with Nondeterminism.
    by T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, and D. Velan. In Proceedings of International Symposium on Automated Technology for Verification and Analysis (ATVA 2019), pages 462-478, volume 11781 of LNCS, Springer, 2019.
  17. Automatic Analysis of Expected Termination Time for Population Protocols.
    by M. Blondin, J. Esparza, and A. Kučera. In Proceedings of 29th International Conference on Concurrency Theory (CONCUR 2018), pages 33:1--33:16, LIPIcs 118, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
  18. Solving Patrolling Problems in the Internet Environment.
    by T. Brázdil, A. Kučera, and V. Řehák. In Proceedings of 27th International Joint Conference on Artificial Intelligence and 23rd European Conference on Artificial Intelligence (IJCAI-ECAI 2018), pages 121-127, 2018.
  19. Black Ninjas in the Dark: Formal Analysis of Population Protocols.
    by M. Blondin, J. Esparza, S. Jaax, and A. Kučera. In Proceedings of 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), pages 1-10, ACM, 2018.
  20. Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS.
    by T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, D. Velan, and F. Zuleger. In Proceedings of 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), pages 185-194, ACM, 2018.
  21. Automatic Synthesis of Efficient Regular Strategies in Adversarial Patrolling Games.
    by D. Klaška, A. Kučera, T. Lamser, and V. Řehák. In Proceedings of 17th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2018), pages 659-666.
  22. 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), pages 417-434, volume 10482 of LNCS, Springer, 2017.
  23. 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), pages 190-206, volume 10503 of LNCS, Springer, 2017.
  24. 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.
  25. 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.
  26. 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 für Informatik, 2016.
    PDF
  27. 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
  28. 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
  29. 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
  30. 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
  31. 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
  32. 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
  33. 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.
  34. 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
  35. 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
  36. 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
  37. 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
  38. 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
  39. 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
  40. 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
  41. 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
  42. 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
  43. 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
  44. 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
  45. 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
  46. 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
  47. 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
  48. 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
  49. 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
  50. 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
  51. 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
  52. 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
  53. 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
  54. 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
  55. 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
  56. 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
  57. 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
  58. 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
  59. 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
  60. 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
  61. 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
  62. 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
  63. 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
  64. 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
  65. 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
  66. 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
  67. 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
  68. 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
  69. 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
  70. 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.
  71. 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
  72. 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
  73. 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
  74. 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
  75. 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
  76. 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
  77. 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
  78. 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
  79. 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
  80. 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
  81. 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
  82. 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
  83. 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. The Satisfiability Problem for a Quantitative Fragment of PCTL.
    by M. Chodil and A. Kučera. Journal of Computer and System Sciences. Volume 139:103478, Elsevier, 2024. DOI 10.1016/j.jcss.2023.103478.
    Preprint available as PDF.
  2. Algorithmic Analysis of Termination and Counter Complexity in Vector Addition Systems with States: A Survey of Recent Results.
    by A. Kučera. ACM SIGLOG News. 8(4):4-21, 2021. DOI 10.1145/3527372.3527374.
    Preprint available as PDF.
  3. 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. ACM Transactions on Modeling and Computer Simulation (TOMACS). 29(4), Article 28, 2019. DOI 10.1145/3310225.
  4. 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. 91C (2018):82-103. Elsevier, 2018. DOI 10.1016/j.jcss.2017.09.004.
    Preprint available as PDF.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  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. Information and Computation. 222:121-138. Elsevier, 2013. DOI 10.1016/j.ic.2012.01.008.
    Preprint available as PDF.
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. 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.
  18. 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.
  19. 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.
  20. 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.
  21. 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.
  22. 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.
  23. 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.
  24. 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.
  25. 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.
  26. 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.
  27. 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.
  28. 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.
  29. 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.
  30. Effective Decomposability of Sequential Behaviours.
    by A. Kučera. Theoretical Computer Science, 242(1-2):71-89. Elsevier, 2000.
    Preprint available as PDF.
  31. Regularity of Normed PA Processes.
    by A. Kučera. Information Processing Letters, 72(1-2):9-17. Elsevier, 1999.
  32. On Finite Representations of Infinite-State Behaviours.
    by A. Kučera. Information Processing Letters, 70(1):23-30. Elsevier, 1999.
  33. 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.
  34. Bisimilarity of Processes with Finite-State Systems.
    by P. Jančar and A. Kučera. In Volume 9 of ENTCS, Elsevier, 1997.
  35. 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. The Satisfiability and Validity Problems for Probabilistic CTL.
    by A. Kučera. In Proceedings of 18th International Conference on Reachability Problems (RP 2024), pages 8-18, volume 15050 of LNCS, Springer, 2024.
  2. 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.
  3. 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.
  4. 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.
  5. 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. Satisfiability of Quantitative Probabilistic CTL: Rise to the Challenge.
    by M. Chodil, A. Kučera, and J. Křetínský. In Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday (edited by Jean-Francois Raskin, Krishnendu Chatterjee, Laurent Doyen, and Rupak Majumdar). Pages 364-387, Springer, 2022. ISBN 978-3-031-22336-5.
    DOI 10.1007/978-3-031-22337-2_18
  2. 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.
  3. 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.
  4. 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. Proceedings of 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024).
    Edited by R. Královič and A. Kučera. ISBN 978-3-95977-335-5. LIPIcs, Volume 306, 2024.
    DOI: 10.4230/LIPIcs.MFCS.2024
  2. Taming the Infinities of Concurrency. Essays Dedicated to Javier Esparza on the Occasion of His 60th Birthday.
    Edited by S. Kiefer, J. Křetínský, and A. Kučera. ISBN 978-3-031-56221-1. Volume 14660 of LNCS, Springer, 2024.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.)

Technical Reports

  1. Multiple Mean-Payoff Optimization under Local Stability Constraints.
    by D. Klaška, A. Kučera, V. Kůr, V. Musil, and V. Řehák. arXiv:2412.13369 [cs.AI]
  2. The General and Finite Satisfiability Problems for PCTL are Undecidable.
    by M. Chodil and A. Kučera. arXiv:2404.10648 [cs.LO]
  3. Optimizing Local Satisfaction of Long-Run Average Objectives in Markov Decision Processes.
    by D. Klaška, A. Kučera, V. Kůr, V. Musil, and V. Řehák. arXiv:2312.12325 [cs.MA]
  4. Asymptotic Complexity Estimates for Probabilistic Programs and their VASS Abstractions.
    by M. Ajdarów and A. Kučera. arXiv:2307.04707 [cs.FL]
  5. Synthesizing Resilient Strategies for Infinite-Horizon Objectives in Multi-Agent Systems.
    by D. Klaška, A. Kučera, M. Kurečka, V. Musil, P. Novotný, and V. Řehák. arXiv:2305.10070 [cs.MA]
  6. Mean Payoff Optimization for Systems of Periodic Service and Maintenance.
    by D. Klaška, A. Kučera, V. Musil, and V. Řehák. arXiv:2305.08555 [cs.GT]
  7. On-the-fly Adaptation of Patrolling Strategies in Changing Environments.
    by T. Brázdil, D. Klaška, A. Kučera, V. Musil, P. Novotný, and V. Řehák. arXiv:2206.08096 [cs.MA]
  8. General Optimization Framework for Recurrent Reachability Objectives.
    by D. Klaška, A. Kučera, V. Musil, and V. Řehák. arXiv:2205.14057 [cs.RO]
  9. Minimizing Expected Intrusion Detection Time in Adversarial Patrolling.
    by D. Klaška, A. Kučera, V. Musil, and V. Řehák. arXiv:2202.01095 [cs.MA]
  10. Regstar: Efficient Strategy Synthesis for Adversarial Patrolling Games.
    by D. Klaška, A. Kučera, V. Musil, and V. Řehák. arXiv:2108.08950 [cs.GT]
  11. The Satisfiability Problem for a Quantitave Fragment of PCTL.
    by M. Chodil and A. Kučera. arXiv:2107.03794 [cs.LO]
  12. Deciding Polynomial Termination Complexity for VASS Programs.
    by M. Ajdarów and A. Kučera. arXiv:2102.06889 [cs.LO]
  13. Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling.
    by M. Blondin, J. Esparza, M. Helfrich, A. Kučera, and P.J. Meyer. arXiv:2005.03555 [cs.LO]
  14. Automatic Analysis of Expected Termination Time for Population Protocols.
    by M. Blondin, J. Esparza, and A. Kučera. arXiv:1807.00331 [cs.LO]
  15. Synthesizing Efficient Solutions for Patrolling Problems in the Internet Environment.
    by T. Brázdil, A. Kučera, and V. Řehák. arXiv:1805.02861 [cs.AI]
  16. Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS.
    by T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, D. Velan, and F. Zuleger. arXiv:1804.10985 [cs.LO]
  17. 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]
  18. 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]
  19. 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]
  20. 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]
  21. Stability in Graphs and Games.
    by T. Brázdil, V. Forejt, A. Kučera, and P. Novotný. arXiv:1604.006386 [cs.LO]
  22. 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]
  23. Strategy Synthesis for General Deductive Games Based on SAT Solving.
    by M. Klimoš and A. Kučera. arXiv:1407.3926 [cs.AI]
  24. Minimizing Running Costs in Consumption Systems.
    by T. Brázdil, D. Klaška, A. Kučera, and P. Novotný. arXiv:1402.4995 [cs.SY]
  25. 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]
  26. 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]
  27. 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]
  28. Efficient Analysis of Probabilistic Programs with an Unbounded Counter.
    by T. Brázdil, S. Kiefer, and A. Kučera. arXiv:1102.2529 [cs.FL]
  29. 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].)
  30. 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]
  31. 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]
  32. 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].)
  33. 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
  34. 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]
  35. 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].)
  36. 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
  37. 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
  38. 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
  39. 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
  40. 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
  41. 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
  42. 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
  43. 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
  44. 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
  45. 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
  46. 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
  47. 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
  48. 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
  49. 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
  50. 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
  51. 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
  52. 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
  53. 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
  54. 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
  55. 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
  56. Simulation Preorder on Simple Process Algebras.
    by A. Kučera and R. Mayr. Technical report TUM-I9902, TU-Munchen, 23 pages, 1999.
    PostScript, PDF
  57. 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
  58. 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
  59. 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
  60. How to Parallelize Sequential Processes.
    by A. Kučera. Technical report FIMU-RS-96-05, Faculty of Informatics MU, 24 pages, 1996.
    PostScript, PDF
  61. 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
  62. 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
  63. 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