Stochastic Games with Branching-Time Winning Objectives. - Tomás Brázdil; Václav Brozek; Vojtech Forejt; Antonín Kucera 001 (LICS, 2006)

Strategy Synthesis for Markov Decision Processes and Branching-Time Logics. - Tomás Brázdil; Vojtech Forejt (CONCUR, 2007)

Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives. - Tomás Brázdil; Vojtech Forejt; Antonín Kucera 001 (ICALP (2), 2008)

The Satisfiability Problem for Probabilistic CTL. - Tomás Brázdil; Vojtech Forejt; Jan Kretínský; Antonín Kucera 001 (LICS, 2008)

Reachability in recursive Markov decision processes. - Tomás Brázdil; Václav Brozek; Vojtech Forejt; Antonín Kucera 001 (Inf. Comput., 2008)

Reachability in Stochastic Timed Games. - Patricia Bouyer; Vojtech Forejt (ICALP (2), 2009)

Branching-Time Model-Checking of Probabilistic Pushdown Automata. - Tomás Brázdil; Václav Brozek; Vojtech Forejt (INFINITY, 2009)

Automated Verification Techniques for Probabilistic Systems. - Vojtech Forejt; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (SFM, 2011)

Quantitative Multi-objective Verification for Probabilistic Systems. - Vojtech Forejt; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001; Hongyang Qu 001 (TACAS, 2011)

Pareto Curves for Probabilistic Model Checking. - Vojtech Forejt; Marta Z. Kwiatkowska; David Parker 001 (ATVA, 2012)

Playing Stochastic Games Precisely. - Taolue Chen 001; Vojtech Forejt; Marta Z. Kwiatkowska; Aistis Simaitis; Ashutosh Trivedi 001; Michael Ummels (CONCUR, 2012)

Bisimilarity of Probabilistic Pushdown Automata. - Vojtech Forejt; Petr Jancar; Stefan Kiefer; James Worrell 001 (FSTTCS, 2012)

Incremental Runtime Verification of Probabilistic Systems. - Vojtech Forejt; Marta Z. Kwiatkowska; David Parker 001; Hongyang Qu 001; Mateusz Ujma (RV, 2012)

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

Safe schedulability of bounded-rate multi-mode systems. - Rajeev Alur; Vojtech Forejt; Salar Moarref; Ashutosh Trivedi 001 (HSCC, 2013)

Multi-objective Discounted Reward Verification in Graphs and MDPs. - Krishnendu Chatterjee; Vojtech Forejt; Dominik Wojtczak (LPAR, 2013)

On Stochastic Games with Multiple Objectives. - Taolue Chen 001; Vojtech Forejt; Marta Z. Kwiatkowska; Aistis Simaitis; Clemens Wiltsche (MFCS, 2013)

PRISM-games: A Model Checker for Stochastic Multi-Player Games. - Taolue Chen 001; Vojtech Forejt; Marta Z. Kwiatkowska; David Parker 001; Aistis Simaitis (TACAS, 2013)

Automatic verification of competitive stochastic systems. - Taolue Chen 001; Vojtech Forejt; Marta Z. Kwiatkowska; David Parker 001; Aistis Simaitis (Formal Methods Syst. Des., 2013)

Continuous-time stochastic games with time-bounded reachability. - Tomás Brázdil; Vojtech Forejt; Jan Krcál; Jan Kretínský; Antonín Kucera 001 (Inf. Comput., 2013)

Verification of Markov Decision Processes Using Learning Algorithms. - Tomás Brázdil; Krishnendu Chatterjee; Martin Chmelik; Vojtech Forejt; Jan Kretínský; Marta Z. Kwiatkowska; David Parker 001; Mateusz Ujma (ATVA, 2014)

Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. - Vojtech Forejt; Daniel Kroening; Ganesh Narayanaswamy; Subodh Sharma 001 (FM, 2014)

Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes - Tomás Brázdil; Václav Brozek; Krishnendu Chatterjee; Vojtech Forejt; Antonín Kucera 001 (Log. Methods Comput. Sci., 2014)

Language equivalence of probabilistic pushdown automata. - Vojtech Forejt; Petr Jancar; Stefan Kiefer; James Worrell 001 (Inf. Comput., 2014)

Branching-time model-checking of probabilistic pushdown automata. - Tomás Brázdil; Václav Brozek; Vojtech Forejt; Antonín Kucera 001 (J. Comput. Syst. Sci., 2014)

On Frequency LTL in Probabilistic Systems. - Vojtech Forejt; Jan Krcál (CONCUR, 2015)

Controller Synthesis for MDPs and Frequency LTL GU. - Vojtech Forejt; Jan Krcál; Jan Kretínský (LPAR, 2015)

MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives. - Tomás Brázdil; Krishnendu Chatterjee; Vojtech Forejt; Antonín Kucera 001 (TACAS, 2015)

Permissive Controller Synthesis for Probabilistic Systems. - Klaus Dräger; Vojtech Forejt; Marta Z. Kwiatkowska; David Parker 001; Mateusz Ujma (Log. Methods Comput. Sci., 2015)

Controller synthesis for MDPs and Frequency LTL$ setminus$GU. - Vojtech Forejt; Jan Krcál; Jan Kretínský (CoRR, 2015)

Decidability Results for Multi-objective Stochastic Games. - Romain Brenguier; Vojtech Forejt (ATVA, 2016)

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

Expected reachability-time games. - Vojtech Forejt; Marta Kwiatkowska; Gethin Norman; Ashutosh Trivedi 001 (Theor. Comput. Sci., 2016)

Trading performance for stability in Markov decision processes. - Tomás Brázdil; Krishnendu Chatterjee; Vojtech Forejt; Antonín Kucera 001 (J. Comput. Syst. Sci., 2017)

Schedulability of Bounded-Rate Multimode Systems. - Rajeev Alur; Vojtech Forejt; Salar Moarref; Ashutosh Trivedi 001 (ACM Trans. Embed. Comput. Syst., 2017)

Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. - Vojtech Forejt; Saurabh Joshi 001; Daniel Kroening; Ganesh Narayanaswamy; Subodh Sharma 001 (ACM Trans. Program. Lang. Syst., 2017)

Game Characterization of Probabilistic Bisimilarity, and Applications to Pushdown Automata. - Vojtech Forejt; Petr Jancar; Stefan Kiefer; James Worrell 001 (Log. Methods Comput. Sci., 2018)

Model Checking Probabilistic Systems. - Christel Baier; Luca de Alfaro; Vojtech Forejt; Marta Kwiatkowska (Handbook of Model Checking, 2018)

Learning Algorithms for Verification of Markov Decision Processes. - Tomás Brázdil; Krishnendu Chatterjee; Martin Chmelik; Vojtech Forejt; Jan Kretínský; Marta Kwiatkowska; Tobias Meggendorfer; David Parker 001; Mateusz Ujma (TheoretiCS, 2025)