Efficient Controller Synthesis for Consumption Games with Multiple Resource Types. - Tomás Brázdil; Krishnendu Chatterjee; Antonín Kucera 001; Petr Novotný 001 (CAV, 2012)

Minimizing Expected Termination Time in One-Counter Markov Decision Processes. - Tomás Brázdil; Antonín Kucera 001; Petr Novotný 001; Dominik Wojtczak (ICALP (2), 2012)

Determinacy in Stochastic Games with Unbounded Payoff Functions. - Tomás Brázdil; Antonín Kucera 001; Petr Novotný 001 (MEMICS, 2012)

Solvency Markov Decision Processes with Interest. - Tomás Brázdil; Taolue Chen 001; Vojtech Forejt; Petr Novotný 001; Aistis Simaitis (FSTTCS, 2013)

Minimizing Running Costs in Consumption Systems. - Tomás Brázdil; David Klaska; Antonín Kucera 001; Petr Novotný 001 (CAV, 2014)

Zero-reachability in probabilistic multi-counter automata. - Tomás Brázdil; Stefan Kiefer; Antonín Kucera 001; Petr Novotný 001; Joost-Pieter Katoen (CSL-LICS, 2014)

Long-Run Average Behaviour of Probabilistic Vector Addition Systems. - Tomás Brázdil; Stefan Kiefer; Antonín Kucera 001; Petr Novotný 001 (LICS, 2015)

Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout Synthesis. - Tomás Brázdil; Lubos Korenciak; Jan Krcál; Petr Novotný 001; Vojtech Rehák (QEST, 2015)

Stochastic Shortest Path with Energy Constraints in POMDPs: (Extended Abstract). - Tomás Brázdil; Krishnendu Chatterjee; Martin Chmelik; Anchit Gupta; Petr Novotný 001 (AAMAS, 2016)

Optimizing the Expected Mean Payoff in Energy Markov Decision Processes. - Tomás Brázdil; Antonín Kucera 001; Petr Novotný 001 (ATVA, 2016)

Stability in Graphs and Games. - Tomás Brázdil; Vojtech Forejt; Antonín Kucera 001; Petr Novotný 001 (CONCUR, 2016)

Stochastic Shortest Path with Energy Constraints in POMDPs. - Tomás Brázdil; Krishnendu Chatterjee; Martin Chmelik; Anchit Gupta; Petr Novotný 001 (CoRR, 2016)

Optimizing Expectation with Guarantees in POMDPs (Technical Report). - Krishnendu Chatterjee; Petr Novotný 001; Guillermo A. Pérez 001; Jean-François Raskin; Dorde Zikelic (CoRR, 2016)

Optimizing Expectation with Guarantees in POMDPs. - Krishnendu Chatterjee; Petr Novotný 001; Guillermo A. Pérez 001; Jean-François Raskin; Dorde Zikelic (AAAI, 2017)

Stochastic invariants for probabilistic termination. - Krishnendu Chatterjee; Petr Novotný 001; Dorde Zikelic (POPL, 2017)

Efficient Algorithms for Checking Fast Termination in VASS. - Tomás Brázdil; Krishnendu Chatterjee; Antonín Kucera 001; Petr Novotný 001; Dominik Velan (CoRR, 2017)

Expectation Optimization with Probabilistic Guarantees in POMDPs with Discounted-Sum Objectives. - Krishnendu Chatterjee; Adrián Elgyütt; Petr Novotný 001; Owen Rouillé (IJCAI, 2018)

Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS. - Tomás Brázdil; Krishnendu Chatterjee; Antonín Kucera 001; Petr Novotný 001; Dominik Velan; Florian Zuleger (LICS, 2018)

On the Complexity of Iterative Tropical Computation with Applications to Markov Decision Processes. - Nikhil Balaji; Stefan Kiefer; Petr Novotný 001; Guillermo A. Pérez 001; Mahsa Shirmohammadi (CoRR, 2018)

Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. - Sheshansh Agrawal; Krishnendu Chatterjee; Petr Novotný 001 (Proc. ACM Program. Lang., 2018)

Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs. - Krishnendu Chatterjee; Hongfei Fu 001; Petr Novotný 001; Rouzbeh Hasheminezhad (ACM Trans. Program. Lang. Syst., 2018)

Deciding Fast Termination for Probabilistic VASS with Nondeterminism. - Tomás Brázdil; Krishnendu Chatterjee; Antonín Kucera 001; Petr Novotný 001; Dominik Velan (ATVA, 2019)

On the Complexity of Value Iteration. - Nikhil Balaji; Stefan Kiefer; Petr Novotný 001; Guillermo A. Pérez 001; Mahsa Shirmohammadi (ICALP, 2019)

Bidding Games on Markov Decision Processes. - Guy Avni; Thomas A. Henzinger; Rasmus Ibsen-Jensen; Petr Novotný 001 (RP, 2019)

Termination Analysis of Probabilistic Programs with Martingales. - Krishnendu Chatterjee; Hongfei Fu 001; Petr Novotný 001 (Foundations of Probabilistic Programming, 2020)

Reinforcement Learning of Risk-Constrained Policies in Markov Decision Processes. - Tomás Brázdil; Krishnendu Chatterjee; Petr Novotný 001; Jiri Vahala (AAAI, 2020)

Multiple-Environment Markov Decision Processes: Efficient Analysis and Applications. - Krishnendu Chatterjee; Martin Chmelík; Deep Karkhanis; Petr Novotný 001; Amélie Royer (ICAPS, 2020)

Qualitative Controller Synthesis for Consumption Markov Decision Processes. - Frantisek Blahoudek; Tomás Brázdil; Petr Novotný 001; Melkior Ornik; Pranay Thangeda; Ufuk Topcu (CAV (2), 2020)

Fuel in Markov Decision Processes (FiMDP): A Practical Approach to Consumption. - Frantisek Blahoudek; Murat Cubuktepe; Petr Novotný 001; Melkior Ornik; Pranay Thangeda; Ufuk Topcu (FM, 2021)

Proving non-termination by program reversal. - Krishnendu Chatterjee; Ehsan Kafshdar Goharshady; Petr Novotný 001; Dorde Zikelic (PLDI, 2021)

On-the-fly adaptation of patrolling strategies in changing environments. - Tomás Brázdil; David Klaska; Antonín Kucera 001; Vít Musil; Petr Novotný 001; Vojtech Rehák (UAI, 2022)

Shielding in Resource-Constrained Goal POMDPs. - Michal Ajdarów; Simon Brlej; Petr Novotný 001 (AAAI, 2023)

Synthesizing Resilient Strategies for Infinite-Horizon Objectives in Multi-Agent Systems. - David Klaska; Antonín Kucera 001; Martin Kurecka; Vít Musil; Petr Novotný 001; Vojtech Rehák (IJCAI, 2023)

Games on Graphs. - Nathanaël Fijalkow; Nathalie Bertrand 001; Patricia Bouyer-Decitre; Romain Brenguier; Arnaud Carayol; John Fearnley; Hugo Gimbert; Florian Horn 001; Rasmus Ibsen-Jensen; Nicolas Markey; Benjamin Monmege; Petr Novotný 001; et al. (CoRR, 2023)

On Lexicographic Proof Rules for Probabilistic Termination. - Krishnendu Chatterjee; Ehsan Kafshdar Goharshady; Petr Novotný 001; Jiri Zárevúcky; Dorde Zikelic (Formal Aspects Comput., 2023)

Efficient Strategy Synthesis for MDPs With Resource Constraints. - Frantisek Blahoudek; Petr Novotný 001; Melkior Ornik; Pranay Thangeda; Ufuk Topcu (IEEE Trans. Autom. Control., 2023)

Asymptotic Analysis of Probabilistic Programs: When Expectations Do Not Meet Our Expectations. - Michal Ajdarów; Antonín Kucera 001; Petr Novotný 001 (Principles of Verification (1), 2024)

Solving Long-run Average Reward Robust MDPs via Stochastic Games. - Krishnendu Chatterjee; Ehsan Kafshdar Goharshady; Mehrdad Karrabi; Petr Novotný 001; Dorde Zikelic (IJCAI, 2024)

Equivalence and Similarity Refutation for Probabilistic Programs. - Krishnendu Chatterjee; Ehsan Kafshdar Goharshady; Petr Novotný 001; Dorde Zikelic (Proc. ACM Program. Lang., 2024)

Threshold UCT: Cost-Constrained Monte Carlo Tree Search with Pareto Curves. - Martin Kurecka; Václav Nevyhostený; Petr Novotný 001; Vít Uncovský (AAAI, 2025)

Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs. - Michal Ajdarów; James C. A. Main; Petr Novotný 001; Mickael Randour (ICALP, 2025)

Bidding Games on Markov Decision Processes with Quantitative Reachability Objectives. - Guy Avni; Martin Kurecka; Kaushik Mallik; Petr Novotný 001; Suman Sadhukhan (AAMAS, 2025)

Refuting Equivalence in Probabilistic Programs with Conditioning. - Krishnendu Chatterjee; Ehsan Kafshdar Goharshady; Petr Novotný 001; Dorde Zikelic (TACAS (2), 2025)