Vojtech Forejt

59 papers A* 4A 5B 13Journal 27Unranked 9

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