Model checking LTL with regular valuations for pushdown systems J Esparza, A Kučera, S Schwoon Information and Computation 186 (2), 355-376, 2003 | 140 | 2003 |

Measure, Π_{1}^{0}-classes and complete extensions of PAA Kučera Recursion theory week, 245-259, 1985 | 107 | 1985 |

Reachability games on extended vector addition systems with states T Brázdil, P Jančar, A Kučera International Colloquium on Automata, Languages, and Programming, 478-489, 2010 | 101 | 2010 |

An alternative, priority-free, solution to Post's problem A Kučera International Symposium on Mathematical Foundations of Computer Science, 493-500, 1986 | 95 | 1986 |

Deciding bisimulation-like equivalences with finite-state processes P Jančar, A Kučera, R Mayr Theoretical Computer Science 258 (1-2), 409-433, 2001 | 87 | 2001 |

On the decidability of temporal properties of probabilistic pushdown automata T Brázdil, A Kučera, O Stražovský Annual Symposium on Theoretical Aspects of Computer Science, 145-157, 2005 | 83 | 2005 |

Lowness for the class of random sets A Kučera, SA Terwijn The Journal of Symbolic Logic 64 (4), 1396-1402, 1999 | 81 | 1999 |

Model-checking LTL with regular valuations for pushdown systems J Esparza, A Kučera, S Schwoon International Symposium on Theoretical Aspects of Computer Software, 316-339, 2001 | 74 | 2001 |

Equivalence-checking on infinite-state systems: Techniques and results A Kučera, P Jančar Theory and Practice of Logic Programming 6 (3), 227-264, 2006 | 70* | 2006 |

One-counter Markov decision processes T Brázdil, V Brožek, K Etessami, A Kučera, D Wojtczak Proceedings of the twenty-first annual ACM-SIAM symposium on Discrete …, 2010 | 68 | 2010 |

On the controller synthesis for finite-state Markov decision processes A Kučera, O Stražovský International Conference on Foundations of Software Technology and …, 2005 | 46 | 2005 |

Qualitative reachability in stochastic BPA games T Brázdil, V Brožek, A Kučera, J Obdržálek Information and Computation 209 (8), 1160-1183, 2011 | 44 | 2011 |

Demuth randomness and computational complexity A Kučera, A Nies Annals of Pure and Applied Logic 162 (7), 504-513, 2011 | 44 | 2011 |

DP lower bounds for equivalence-checking and model-checking of one-counter automata P Jančar, A Kučera, F Moller, Z Sawa Information and Computation 188 (1), 1-19, 2004 | 44 | 2004 |

Efficient controller synthesis for consumption games with multiple resource types T Brázdil, K Chatterjee, A Kučera, P Novotný International Conference on Computer Aided Verification, 23-38, 2012 | 41 | 2012 |

The stuttering principle revisited A Kučera, J Strejček Acta Informatica 41 (7-8), 415-434, 2005 | 40 | 2005 |

Simulation and bisimulation over one-counter processes P Jančar, A Kučera, F Moller Annual Symposium on Theoretical Aspects of Computer Science, 334-345, 2000 | 40 | 2000 |

On relative randomness A Kučera Annals of Pure and Applied Logic 63 (1), 61-67, 1993 | 39 | 1993 |

On the use of diagonally nonrecursive functions A Kučera Studies in Logic and the Foundations of Mathematics 129, 219-239, 1989 | 36 | 1989 |

Trading performance for stability in Markov decision processes T Brázdil, K Chatterjee, V Forejt, A Kučera Journal of Computer and System Sciences 84, 144-170, 2017 | 35 | 2017 |