Vojtěch Forejt's Publications
If you have any questions related to any of my publications, please do not hesitate and send me an e-mail (see my homepage for contact details).
Sort by: date, type, title
41 publications:
-
[BdAFK16]
C. Baier, L. de Alfaro, V. Forejt, and M. Kwiatkowska.
Probabilistic Model Checking.
In Handbook of Model Checking, Springer. To appear.
2016.
[pdf]
[bib]
-
[FKNP11]
V. Forejt, M. Kwiatkowska, G. Norman and D. Parker.
Automated Verification Techniques for Probabilistic Systems.
In M. Bernardo and V. Issarny (editors), Formal Methods for Eternal Networked Software Systems (SFM'11), volume 6659 of LNCS, pages 53-113, Springer.
June 2011.
[pdf]
[bib]
-
[FKNT16]
V. Forejt, M. Kwiatkowska, G. Norman, A. Trivedi.
Expected Reachability-Time Games.
Theoretical Computer Science, Elsevier. To appear.
2016.
[pdf]
[bib]
-
[DFK+15]
K. Draeger, V. Forejt, M. Kwiatkowska, D. Parker, M. Ujma.
Permissive Controller Synthesis for Probabilistic Systems.
Logical Methods in Computer Science, 11(2:16)2015, pages 1-34.
June 2015.
[pdf]
[bib]
-
[BBFK14]
T. Brázdil, V. Brožek, V. Forejt and A. Kučera.
Branching-time model-checking of probabilistic pushdown automata.
Journal of Computer and System Sciences, 80(1), pages 139-156, Elsevier.
2014.
[pdf]
[bib]
-
[BBC+14]
T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt and A. Kučera.
Markov Decision Processes with Multiple Long-run Average Objectives.
LMCS, 10(1).
2014.
[pdf]
[bib]
http://www.lmcs-online.org/ojs/viewarticle.php?id=1109&layout=abstract
-
[FJKW14]
V. Forejt, P. Jančar, S. Kiefer and J. Worrell.
Language equivalence of probabilistic pushdown automata.
Information and Computation, 237, pages 1-11, Elsevier.
October 2014.
[pdf]
[bib]
-
[BFK+13]
T. Brázdil, V. Forejt, J. Krčál, J. Křetínský and A. Kučera.
Continuous-Time Stochastic Games with Time-Bounded Reachability.
Information & Computation, 224, pages 46-70, Elsevier.
2013.
[pdf]
[bib]
-
[CFK+13b]
T. Chen, V. Forejt, M. Kwiatkowska, D. Parker and A. Simaitis.
Automatic Verification of Competitive Stochastic Systems.
Formal Methods in System Design, pages 43(1), pages 61-92, Springer.
February 2013.
[pdf]
[bib]
-
[BBF09]
T. Brázdil, V. Brožek and V. Forejt.
Branching-Time Model-Checking of Probabilistic Pushdown Automata.
Electronic Notes in Theoretical Computer Science, 239, pages 73-83, Elsevier Science Publishers.
2009.
[pdf]
[bib]
-
[BBFK08]
T. Brázdil, V. Brožek, V. Forejt and A. Kučera.
Reachability in recursive Markov decision processes.
Information and Computation, 206(5), pages 520-537.
2008.
[pdf]
[bib]
-
[BFK+16]
T. Brázdil, V. Forejt, A. Kučera, and P. Novotný.
Stability in Graphs and Games.
In CONCUR.
2016.
[pdf]
-
[BF16]
R. Brenguier and V. Forejt.
Decidability Results for Multi-objective Stochastic Games.
In ATVA.
2016.
[pdf]
-
[BCFK15]
T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera.
MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives.
In Christel Baier and Cesare Tinelli (editors), Proceedings of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015), volume 9035 of LNCS, pages 181-187, Springer.
2015.
[pdf]
[bib]
-
[FKK15]
Vojtěch Forejt, Jan Krčál and Jan Křetínský.
Controller synthesis for MDPs and Frequency LTL-GU.
In M. Davis, A. Fehnker and A. McIver and A. Voronkov (editors), LPAR, volume 9450 of LNCS, pages 162--177, Springer. To appear.
2015.
[pdf]
[bib]
-
[FK15]
V. Forejt and J. Krčál.
On Frequency LTL in Probabilistic Systems.
In Luca Aceto and David de Frutos-Escrig (editors), CONCUR, volume 42 of LIPIcs, pages 184-197, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
2015.
[pdf]
[bib]
-
[DFK+14]
K. Draeger, V. Forejt, M. Kwiatkowska, D. Parker and M. Ujma.
Permissive Controller Synthesis for Probabilistic Systems.
In Proc. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), volume 8413 of LNCS, pages 531-546, Springer.
2014.
[pdf]
[bib]
-
[FKNS14]
V. Forejt, D. Kroening, G. Narayanaswamy and S. Sharma.
Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs.
In Jones, Cliff and Pihlajasaari, Pekka and Sun, Jun (editors), FM 2014, volume 8442 of Lecture Notes in Computer Science, pages 263-278, Springer.
2014.
[pdf]
[bib]
-
[BCC+14]
T. Brázdil, K. Chatterjee, M. Chmelík, V. Forejt, J. Křetínský, M. Kwiatkowska, D. Parker and M. Ujma.
Verification of Markov Decision Processes using Learning Algorithms.
In Proc. 12th International Symposium on Automated Technology for Verification and Analysis (ATVA'14), volume 8837 of LNCS, pages 98-114, Springer.
2014.
[pdf]
[bib]
-
[BCF+13]
T. Brázdil, T. Chen, V. Forejt, P. Novotný, and A. Simaitis.
Solvency Markov Decision Processes with Interest.
In Anil Seth and Nisheeth K. Vishnoi (editors), IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013), volume 24 of Leibniz International Proceedings in Informatics (LIPIcs), pages 487-499, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
2013.
[pdf]
[bib]
-
[CFK+13]
T. Chen, V. Forejt, M. Kwiatkowska, D. Parker and A. Simaitis.
PRISM-games: A Model Checker for Stochastic Multi-Player Games.
In Proc. 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13), volume 7795 of LNCS, pages 185-191, Springer.
2013.
[pdf]
[bib]
-
[CFK+13c]
T. Chen, V. Forejt, M. Kwiatkowska, A. Simaitis and C. Wiltsche.
On Stochastic Games with Multiple Objectives.
In Krishnendu Chatterjee and Jiri Sgall (editors), Proc. 38th International Symposium on Mathematical Foundations of Computer Science (MFCS'13), volume 8087 of Lecture Notes in Computer Science, pages 266-277, Springer.
2013.
[pdf]
[bib]
-
[BCFK13]
T. Brázdil, K. Chatterjee, V. Forejt and A. Kučera.
Trading Performance for Stability in Markov Decision Processes.
In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, pages 331-340, IEEE Computer Society.
2013.
[pdf]
[bib]
-
[CFW13]
K. Chatterjee, V. Forejt, and D. Wojtczak.
Multi-objective discounted reward verification in graphs and MDPs.
In Ken McMillan, Aart Middeldorp and Andrei Voronkov (editors), LPAR-19, volume 8312 of Lecture Notes in Computer Science, pages 228-242, Springer.
2013.
[pdf]
[bib]
-
[AFMT13]
R. Alur, V. Forejt, S. Moarref and A. Trivedi.
Safe schedulability of bounded-rate multi-mode systems.
In Calin Belta and Franjo Ivancic (editors), Proceedings of the 16th international conference on Hybrid systems: computation and control, HSCC 2013, pages 243-252, ACM.
2013.
[pdf]
[bib]
-
[FJKW12]
V. Forejt, P. Jančar, S.Kiefer and J. Worrell.
Bisimilarity of Probabilistic Pushdown Automata.
In Deepak D'Souza, Telikepalli Kavitha and Jaikumar Radhakrishnan (editors), IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, volume 18 of LIPIcs, pages 448-460, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
2012.
[pdf]
[bib]
-
[CFK+12b]
T. Chen, V. Forejt, M. Kwiatkowska, A. Simaitis, A. Trivedi and M. Ummels.
Playing Stochastic Games Precisely.
In Proc. 23rd International Conference on Concurrency Theory (CONCUR'12), volume 7454 of LNCS, pages 348-363, Springer.
2012.
[pdf]
[bib]
-
[FKP12]
V. Forejt, M. Kwiatkowska and D. Parker.
Pareto Curves for Probabilistic Model Checking.
In Proc. 10th International Symposium on Automated Technology for Verification and Analysis (ATVA'12), volume 7561 of LNCS, pages 317-332, Springer.
2012.
[pdf]
[bib]
-
[FKP+12]
V. Forejt, M. Kwiatkowska, D. Parker, H. Qu and M. Ujma.
Incremental Runtime Verification of Probabilistic Systems.
In S. Qadeer and S. Tasiran (editors), Proc. 3rd International Conference on Runtime Verification (RV'12), volume 7687 of LNCS, pages 314-319, Springer.
September 2012.
[pdf]
[bib]
-
[CFK+12]
T. Chen, V. Forejt, M. Kwiatkowska, D. Parker and A. Simaitis.
Automatic Verification of Competitive Stochastic Systems.
In Proc. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12), volume 7214 of LNCS, pages 315-330, Springer.
March 2012.
[pdf]
[bib]
-
[BBC+11]
T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt and A. Kučera.
Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.
In Proc. 26th Annual IEEE Symposium on Logic in Computer Science (LICS'11), pages 33-42, IEEE Computer Society.
June 2011.
[pdf]
[bib]
-
[FKN+11]
V. Forejt, M. Kwiatkowska, G. Norman, D. Parker and H. Qu.
Quantitative Multi-Objective Verification for Probabilistic Systems.
In Proc. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), volume 6605 of LNCS, pages 112-127, Springer.
March 2011.
[pdf]
[bib]
-
[FKNT10a]
V. Forejt, M. Kwiatkowska, G. Norman and A. Trivedi.
Expected Reachability-Time Games.
In K. Chatterjee and T. Henzinger (editors), Proeedings of 8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'10), volume 6246 of LNCS, pages 122--136, Springer.
September 2010.
[pdf]
[bib]
-
[BFK+09]
T. Brázdil, V. Forejt, J. Krčál, J. Křetínský and A. Kučera.
Continuous-Time Stochastic Games with Time-Bounded Reachability.
In Proc. 29th Int. Conf. Foundations of Software Technology and Theoretical Computer Science (FSTTCS'09), volume 4 of LIPIcs, pages 61-72, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
2009.
[pdf]
[bib]
-
[BF09a]
P. Bouyer and V. Forejt.
Reachability in Stochastic Timed Games.
In S. Albers, A. Marchetti-Spaccamela, Y. Matias, S. E. Nikoletseas and W. Thomas (editors), Automata, Languages and Programming, 36th International Colloquium, ICALP 2009, Rhodes, greece, July 5-12, 2009, Proceedings, Part II, volume 5556 of Lecture Notes in Computer Science, pages 103-114, Springer.
2009.
[pdf]
[bib]
-
[BFK08]
T. Brázdil, V. Forejt and A. Kučera.
Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives.
In L. Aceto, I. Damgaard, L. Goldberg, M. Halldórsson, A. Ingólfsdóttir and I. Walukiewicz (editors), Proc. 35th Int. Colloq. Automata, Languages and Programming, Part II (ICALP'08), volume 5126 of LNCS, pages 148-159, Springer.
2008.
[pdf]
[bib]
-
[BFKK08]
T. Brázdil, V. Forejt, J. Křetínský and A. Kučera.
The Satisfiability Problem for Probabilistic CTL.
In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, pages 391-402, IEEE Computer Society.
2008.
[pdf]
[bib]
-
[BF07]
T. Brázdil and V. Forejt.
Strategy Synthesis for Markov Decision Processes and Branching-Time Logics.
In L. Caires and V. T. Vasconcelos (editors), CONCUR 2007 - Concurrency Theory, 18th International Conference,, volume 4703 of Lecture Notes in Computer Science, pages 428-444, Springer.
2007.
[pdf]
[bib]
-
[BBFK06a]
T. Brázdil, V. Brožek, V. Forejt and A. Kučera.
Reachability in Recursive Markov Decision Processes.
In C. Baier and H. Hermanns (editors), CONCUR, volume 4137 of Lecture Notes in Computer Science, pages 358-374, Springer.
2006.
[pdf]
[bib]
-
[BBFK06]
T. Brázdil, V. Brožek, V. Forejt and A. Kučera.
Stochastic Games with Branching-Time Winning Objectives.
In 21th IEEE Symp. Logic in Computer Science (LICS 2006), pages 349-358, IEEE CS Press.
2006.
[pdf]
[bib]
-
[LWFB05]
M. Leucker, M. Weber, V. Forejt and J. Barnat.
DivSPIN - A SPIN compatible distributed model checker.
In M. Leucker and J. van de Pol (editors), Proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation, pages 95-100.
2005.
[pdf]
[bib]
Sort by: date, type, title
