Vojtech Forejt

Publication Activity (10 Years)

Years Active: 2006-2024
Publications (10 Years): 12

Top Topics

Controller Synthesis

Markov Decision Process

Infinite Horizon

Top Venues

Log. Methods Comput. Sci.

J. Comput. Syst. Sci.

Publications

Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Kretínský, Marta Kwiatkowska, Tobias Meggendorfer, David Parker, Mateusz Ujma
Learning Algorithms for Verification of Markov Decision Processes. CoRR (2024)
Vojtech Forejt, Petr Jancar, Stefan Kiefer, James Worrell
Game Characterization of Probabilistic Bisimilarity, and Applications to Pushdown Automata. Log. Methods Comput. Sci. 14 (4) (2018)
Rajeev Alur, Vojtech Forejt, Salar Moarref, Ashutosh Trivedi
Schedulability of Bounded-Rate Multimode Systems. ACM Trans. Embed. Comput. Syst. 16 (3) (2017)
Tomás Brázdil, Krishnendu Chatterjee, Vojtech Forejt, Antonín Kucera
Trading performance for stability in Markov decision processes. J. Comput. Syst. Sci. 84 (2017)
Vojtech Forejt, Saurabh Joshi, Daniel Kroening, Ganesh Narayanaswamy, Subodh Sharma
Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. ACM Trans. Program. Lang. Syst. 39 (4) (2017)
Vojtech Forejt, Petr Jancar, Stefan Kiefer, James Worrell
Game Characterization of Probabilistic Bisimilarity, and Applications to Pushdown Automata. CoRR (2017)
Tomás Brázdil, Vojtech Forejt, Antonín Kucera, Petr Novotný
Stability in Graphs and Games. CONCUR (2016)
Tomás Brázdil, Vojtech Forejt, Antonín Kucera, Petr Novotný
Stability in Graphs and Games. CoRR (2016)
Romain Brenguier, Vojtech Forejt
Decidability Results for Multi-objective Stochastic Games. CoRR (2016)
Romain Brenguier, Vojtech Forejt
Decidability Results for Multi-objective Stochastic Games. ATVA (2016)
Vojtech Forejt, Marta Kwiatkowska, Gethin Norman, Ashutosh Trivedi
Expected reachability-time games. Theor. Comput. Sci. 631 (2016)
Vojtech Forejt, Marta Z. Kwiatkowska, Gethin Norman, Ashutosh Trivedi
Expected Reachability-Time Games. CoRR (2016)
Klaus Dräger, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Mateusz Ujma
Permissive Controller Synthesis for Probabilistic Systems. Log. Methods Comput. Sci. 11 (2) (2015)
Vojtech Forejt, Jan Krcál
On Frequency LTL in Probabilistic Systems. CONCUR (2015)
Vojtech Forejt, Jan Krcál, Jan Kretínský
Controller synthesis for MDPs and Frequency LTL$\setminus$GU. CoRR (2015)
Tomás Brázdil, Krishnendu Chatterjee, Vojtech Forejt, Antonín Kucera
MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives. TACAS (2015)
Tomás Brázdil, Krishnendu Chatterjee, Vojtech Forejt, Antonín Kucera
MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives. CoRR (2015)
Vojtech Forejt, Jan Krcál
On Frequency LTL in Probabilistic Systems. CoRR (2015)
Vojtech Forejt, Jan Krcál, Jan Kretínský
. LPAR (2015)
Klaus Dräger, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Mateusz Ujma
Permissive Controller Synthesis for Probabilistic Systems. TACAS (2014)
Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Kretínský, Marta Z. Kwiatkowska, David Parker, Mateusz Ujma
Verification of Markov Decision Processes Using Learning Algorithms. ATVA (2014)
Tomás Brázdil, Václav Brozek, Krishnendu Chatterjee, Vojtech Forejt, Antonín Kucera
Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes Log. Methods Comput. Sci. 10 (1) (2014)
Vojtech Forejt, Daniel Kroening, Ganesh Narayanaswamy, Subodh Sharma
Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. FM (2014)
Tomás Brázdil, Václav Brozek, Vojtech Forejt, Antonín Kucera
Branching-time model-checking of probabilistic pushdown automata. J. Comput. Syst. Sci. 80 (1) (2014)
Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Kretínský, Marta Z. Kwiatkowska, David Parker, Mateusz Ujma
Verification of Markov Decision Processes using Learning Algorithms. CoRR (2014)
Vojtech Forejt, Petr Jancar, Stefan Kiefer, James Worrell
Language equivalence of probabilistic pushdown automata. Inf. Comput. 237 (2014)
Tomás Brázdil, Taolue Chen, Vojtech Forejt, Petr Novotný, Aistis Simaitis
Solvency Markov Decision Processes with Interest. FSTTCS (2013)
Tomás Brázdil, Krishnendu Chatterjee, Vojtech Forejt, Antonín Kucera
Trading Performance for Stability in Markov Decision Processes. LICS (2013)
Krishnendu Chatterjee, Vojtech Forejt, Dominik Wojtczak
Multi-objective Discounted Reward Verification in Graphs and MDPs. LPAR (2013)
Rajeev Alur, Vojtech Forejt, Salar Moarref, Ashutosh Trivedi
Safe Schedulability of Bounded-Rate Multi-Mode Systems CoRR (2013)
Tomás Brázdil, Vojtech Forejt, Jan Krcál, Jan Kretínský, Antonín Kucera
Continuous-time stochastic games with time-bounded reachability. Inf. Comput. 224 (2013)
Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, Aistis Simaitis, Clemens Wiltsche
On Stochastic Games with Multiple Objectives. MFCS (2013)
Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Aistis Simaitis
PRISM-games: A Model Checker for Stochastic Multi-Player Games. TACAS (2013)
Tomás Brázdil, Krishnendu Chatterjee, Vojtech Forejt, Antonín Kucera
Trading Performance for Stability in Markov Decision Processes CoRR (2013)
Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Aistis Simaitis
Automatic verification of competitive stochastic systems. Formal Methods Syst. Des. 43 (1) (2013)
Rajeev Alur, Vojtech Forejt, Salar Moarref, Ashutosh Trivedi
Safe schedulability of bounded-rate multi-mode systems. HSCC (2013)
Tomás Brázdil, Taolue Chen, Vojtech Forejt, Petr Novotný, Aistis Simaitis
Solvency Markov Decision Processes with Interest. CoRR (2013)
Vojtech Forejt, Marta Z. Kwiatkowska, David Parker
Pareto Curves for Probabilistic Model Checking CoRR (2012)
Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, Aistis Simaitis, Ashutosh Trivedi, Michael Ummels
Playing Stochastic Games Precisely. CONCUR (2012)
Vojtech Forejt, Petr Jancar, Stefan Kiefer, James Worrell
Bisimilarity of Probabilistic Pushdown Automata CoRR (2012)
Vojtech Forejt, Petr Jancar, Stefan Kiefer, James Worrell
Bisimilarity of Probabilistic Pushdown Automata. FSTTCS (2012)
Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Aistis Simaitis
Automatic Verification of Competitive Stochastic Systems. TACAS (2012)
Vojtech Forejt, Marta Z. Kwiatkowska, David Parker
Pareto Curves for Probabilistic Model Checking. ATVA (2012)
Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Hongyang Qu, Mateusz Ujma
Incremental Runtime Verification of Probabilistic Systems. RV (2012)
Vojtech Forejt, Marta Z. Kwiatkowska, Gethin Norman, David Parker
Automated Verification Techniques for Probabilistic Systems. SFM (2011)
Tomás Brázdil, Václav Brozek, Krishnendu Chatterjee, Vojtech Forejt, Antonín Kucera
Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. LICS (2011)
Vojtech Forejt, Marta Z. Kwiatkowska, Gethin Norman, David Parker, Hongyang Qu
Quantitative Multi-objective Verification for Probabilistic Systems. TACAS (2011)
Vojtech Forejt, Marta Z. Kwiatkowska, Gethin Norman, Ashutosh Trivedi
Expected Reachability-Time Games. FORMATS (2010)
Tomás Brázdil, Václav Brozek, Vojtech Forejt
Branching-Time Model-Checking of Probabilistic Pushdown Automata. INFINITY (2009)
Tomás Brázdil, Vojtech Forejt, Jan Krcál, Jan Kretínský, Antonín Kucera
Continuous-Time Stochastic Games with Time-Bounded Reachability. FSTTCS (2009)
Patricia Bouyer, Vojtech Forejt
Reachability in Stochastic Timed Games. ICALP (2) (2009)
Tomás Brázdil, Václav Brozek, Vojtech Forejt, Antonín Kucera
Reachability in recursive Markov decision processes. Inf. Comput. 206 (5) (2008)
Tomás Brázdil, Vojtech Forejt, Antonín Kucera
Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives. ICALP (2) (2008)
Tomás Brázdil, Vojtech Forejt, Jan Kretínský, Antonín Kucera
The Satisfiability Problem for Probabilistic CTL. LICS (2008)
Tomás Brázdil, Vojtech Forejt
Strategy Synthesis for Markov Decision Processes and Branching-Time Logics. CONCUR (2007)
Tomás Brázdil, Václav Brozek, Vojtech Forejt, Antonín Kucera
Reachability in Recursive Markov Decision Processes. CONCUR (2006)
Tomás Brázdil, Václav Brozek, Vojtech Forejt, Antonín Kucera
Stochastic Games with Branching-Time Winning Objectives. LICS (2006)