Curriculum Vitae

Curriculum Vitae

Person-Related Identification Information

• Jan Křetínský
  born 26/12/1984 in Brno

Department

• Faculty of Informatics, Masaryk University
  Botanická 68a, Brno 602 00

Education and Academic Qualifications

• 2011: RNDr. degree, Informatics - Parallel and Distributed Systems, Probabilistic Timed Systems with Non-Determinism, Faculty of Informatics, Masaryk University
• 2010: Master's degree, Mathematics - Algebra and Discrete Mathematics, Modal Transition Systems, Faculty of Science, Masaryk University
• 2009: Master's degree, Informatics - Parallel and Distributed Systems, Fundamental Properties of Probabilistic Branching-Time Logics, Faculty of Informatics, Masaryk University
• 2007: Bachelor's degree, Mathematics - Mathematics, Monadic Second Order Logic on Infinite Words and Trees, Faculty of Science, Masaryk University
• 2007: Bachelor's degree, Humanities - Philosophy, General Linguistics, Mathematical Framework for Natural Language Formal Description, Faculty of Arts, Masaryk University
• 2007: Bachelor's degree, Informatics - Informatics, Use-mention Distinction in Transparent Intensional Logic, Faculty of Informatics, Masaryk University

Teaching Activities

• Diskrete Wahrscheinlichkeitstheorie TUM (Summer 2012)
• Complexity TUM (Summer 2010, 2011)
• Automata and Formal Languages TUM (Winter 2009/10, 2010/11, 2011/12, 2012/13)
• Complexity TUM (Summer 2010)
• IA008 Computational Logic FI (Spring 2009)
• IB102 Automata and Grammars FI (Autumn 2007)
• MB003 Linear Algebra and Geometry I FI (Spring 2008)
• MB005 Foundations of mathematics FI (Autumn 2007)
• M1110 Linear Algebra and Geometry I PřF (Autumn 2007)
• Students:
• Carlos Camino: Probabilistic Cellular Automata
• Moritz Fuchs: An Advanced Solver for Presburger Arithmetic
• Martin Stoll: MoTraS: A Tool for Modal Transition Systems
• Salomon Sickert: Refinement Algorithms for Parametric Modal Transition Systems
• Imre Vadász: Discretization of Time-Bounded Reachability in Generalized Semi-Markov Games
• Dennis Kraft: Almost Sure Winning Strategies in Stochastic Real Time Games with Timed Automata Objectives
• Markus Dausch: Tool for Continuous Time Stochastic Games (GUI and Simulations)
• Tuan Duc Nguyen: An Extension of a Tool for Modal Transition Systems
• Philip Meyer: Algorithms for Refinement of Modal Process Rewrite Systems
• Alexander Manta
• Michael Opitz

Scientific and Research Activities

• continuous-time stochastic processes and games; CoTtaGe (under development) - algorithms for continuous-time stochastic games and their extensions
• temporal logics, in particular LTL and PCTL; Rabinizer 2 (developed with Ruslan Ledesma Garza), and Rabinizer (developed with Andreas Gaiser) - translation of LTL formulae to deterministic Rabin automata
• modal transition systems; MoTraS (developed with Salomon Sickert), and the old version (developed with Martin Stoll) - algorithms for modal transition systems and their extensions

Academic Stays

• computer science department and CISS, Aalborg University, Denmark (one semester in 2009 and one month in 2011)
• INRIA Rennes, France (3 weeks in 2012)
• IST Austria, Klosterneuburg, Austria (2 weeks in 2012, 2 weeks in 2013)
• Chair for Foundations of Software Reliability and Theoretical Computer Science, Technische Universität München, Garching, Germany (frequent visits in 2009-2013)

Awards Related to Science and Research

• 2009: Rector's Prize
• 2007: Dean's Prize

Major Publications

• KŘETÍNSKÝ, Jan, Tobias MEGGENDORFER, Maximilian PROKOP and Sabine RIEDER. Guessing Winning Policies in LTL Synthesis by Semantic Learning. In Constantin Enea and Akash Lal. Computer Aided Verification - 35th International Conference, CAV 2023, Proceedings, Part I. Cham: Springer, 2023, p. 390-414. ISBN 978-3-031-37705-1. Available from: https://dx.doi.org/10.1007/978-3-031-37706-8_20. info
• SVOREŇOVÁ, Mária, Jan KŘETÍNSKÝ, Martin CHMELÍK, Krishnendu CHATTERJEE, Ivana ČERNÁ and Calin BELTA. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. Elsevier, 2017, vol. 23, February 2017, p. 230-253. ISSN 1751-570X. Available from: https://dx.doi.org/10.1016/j.nahs.2016.04.006. info
• DACA, Przemyslaw, Thomas A. HENZINGER, Jan KŘETÍNSKÝ and Tatjana PETROV. Faster Statistical Model Checking for Unbounded Temporal Properties. In Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016. Berlin Heidelberg: Springer, 2016, p. 112-129. ISBN 978-3-662-49673-2. Available from: https://dx.doi.org/10.1007/978-3-662-49674-9_7. info
• DACA, Przemyslaw, Thomas A. HENZINGER, Jan KŘETÍNSKÝ and Tatjana PETROV. Linear Distances between Markov Chains. Online. In 27th International Conference on Concurrency Theory, CONCUR 2016. Schloss Dagstuhl: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016, p. 1-15. ISBN 978-3-95977-017-0. Available from: https://dx.doi.org/10.4230/LIPIcs.CONCUR.2016.20. info
• SICKERT, Salomon, Javier ESPARZA, Stefan JAAX and Jan KŘETÍNSKÝ. Limit-Deterministic Büchi Automata for Linear Temporal Logic. In Computer Aided Verification - 28th International Conference, CAV 2016. Switzerland: Springer, 2016, p. 312-332. ISBN 978-3-319-41539-0. Available from: https://dx.doi.org/10.1007/978-3-319-41540-6_17. info
• SICKERT, Salomon and Jan KŘETÍNSKÝ. MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata. In Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016. Switzerland: Springer, 2016, p. 130-137. ISBN 978-3-319-46519-7. Available from: https://dx.doi.org/10.1007/978-3-319-46520-3_9. info
• KŘETÍNSKÝ, Jan. Survey of Statistical Verification of Linear Unbounded Properties: Model Checking and Distances. In Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016. Switzerland: Springer, 2016, p. 27-45. ISBN 978-3-319-47165-5. Available from: https://dx.doi.org/10.1007/978-3-319-47166-2_3. info
• ESPARZA, Javier, Jan KŘETÍNSKÝ and Salomon SICKERT. From LTL to deterministic automata (A safraless compositional approach). Formal Methods in System Design. Springer Netherlands, 2016, vol. 49, No 3, p. 219-271. ISSN 0925-9856. Available from: https://dx.doi.org/10.1007/s10703-016-0259-2. info
• FAHRENBERG, Uli, Jan KŘETÍNSKÝ, Axel LEGAY and Louis-Marie TRAONOUEZ. Compositionality for Quantitative Specifications. In The 11th International Symposium on Formal Aspects of Component Software - FACS 2014. Heidelberg Dordrecht London New York: Springer, 2015, p. 306-324. ISBN 978-3-319-15316-2. Available from: https://dx.doi.org/10.1007/978-3-319-15317-9_19. info
• SVOREŇOVÁ, Mária, Jan KŘETÍNSKÝ, Martin CHMELÍK, Krishnendu CHATTERJEE, Ivana ČERNÁ and Calin BELTA. Temporal Logic Control for Stochastic Linear Systems using Abstraction Refinement of Probabilistic Games. Online. In Proceedings of ACM international conference on Hybrid Systems: Computation and Control. Seattle, Washington, USA: Association for Computing Machinery (ACM), 2015, p. 259-268. ISBN 978-1-4503-3433-4. Available from: https://dx.doi.org/10.1145/2728606.2728608. info
• BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN, Mikael H. MOLLER, Salomon SICKERT and Jiří SRBA. Refinement checking on parametric modal transition systems. Acta Informatica. Springer, 2015, vol. 52, 2-3, p. 269-297. ISSN 0001-5903. Available from: https://dx.doi.org/10.1007/s00236-015-0215-4. info
• CHATTERJEE, Krishnendu, Zuzana KOMÁRKOVÁ and Jan KŘETÍNSKÝ. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. In Thirtieth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Los Alamitos, California: IEEE, 2015, p. 244-256. ISBN 978-1-4799-8875-4. Available from: https://dx.doi.org/10.1109/LICS.2015.32. info
• BRÁZDIL, Tomáš, Krishnendu CHATTERJEE, Martin CHMELÍK, Andreas FELLNER and Jan KŘETÍNSKÝ. Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. In Daniel Kroening, Corina Pasareanu. Computer Aided Verification: 27th International Conference, CAV 2015. Cham: Springer, 2015, p. 158-177. ISBN 978-3-319-21689-8. Available from: https://dx.doi.org/10.1007/978-3-319-21690-4_10. info
• BABIAK, Tomáš, František BLAHOUDEK, Alexandre DURET-LUTZ, Joachim KLEIN, Jan KŘETÍNSKÝ, David MÜLLER, David PARKER and Jan STREJČEK. The Hanoi Omega-Automata Format. In Daniel Kroening, Corina Pasareanu. Computer Aided Verification: 27th International Conference, CAV 2015. Cham: Springer, 2015, p. 479-486. ISBN 978-3-319-21689-8. Available from: https://dx.doi.org/10.1007/978-3-319-21690-4_31. info
• FOREJT, Vojtěch, Jan KRČÁL and Jan KŘETÍNSKÝ. Controller Synthesis for MDPs and Frequency LTL\GU. In LPAR 2015. Suva, Fiji: Springer, 2015, p. 162-177. ISBN 978-3-662-48898-0. Available from: https://dx.doi.org/10.1007/978-3-662-48899-7_12. info
• KŘETÍNSKÝ, Jan, Kim Guldstrand LARSEN, Simon LAURSEN and Jiří SRBA. Polynomial Time Decidability of Weighted Synchronization under Partial Observability. Online. In 26th International Conference on Concurrency Theory (CONCUR 2015). Dagstuhl, Germany: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015, p. 142-154. ISBN 978-3-939897-91-0. Available from: https://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.142. info
• ESPARZA, Javier and Jan KŘETÍNSKÝ. From LTL to Deterministic Automata: A Safraless Compositional Approach. In Computer Aided Verification - 26th International Conference, CAV 2014. Heidelberg Dordrecht London New York: Springer, 2014, p. 192-208. ISBN 978-3-319-08866-2. Available from: https://dx.doi.org/10.1007/978-3-319-08867-9_13. info
• HERMANNS, Holger, Jan KRČÁL and Jan KŘETÍNSKÝ. Probabilistic Bisimulation: Naturally on Distributions. In CONCUR 2014 - Concurrency Theory - 25th International Conference. Heidelberg Dordrecht London New York: Springer, 2014, p. 249-265. ISBN 978-3-662-44583-9. Available from: https://dx.doi.org/10.1007/978-3-662-44584-6_18. info
• BRÁZDIL, Tomáš, Krishnendu CHATTERJEE, Martin CHMELÍK, Vojtěch FOREJT, Jan KŘETÍNSKÝ, Marta KWIATKOWSKA, David PARKER and Mateusz UJMA. Verification of Markov Decision Processes using Learning Algorithms. In Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014. Heidelberg Dordrecht London New York: Springer, 2014, p. 98-114. ISBN 978-3-319-11935-9. Available from: https://dx.doi.org/10.1007/978-3-319-11936-6_8. info
• KOMÁRKOVÁ, Zuzana and Jan KŘETÍNSKÝ. Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata. In Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014. Heidelberg Dordrecht London New York: Springer, 2014, p. 235-241. ISBN 978-3-319-11935-9. Available from: https://dx.doi.org/10.1007/978-3-319-11936-6_17. info
• BRÁZDIL, Tomáš, Vojtěch FOREJT, Jan KRČÁL, Jan KŘETÍNSKÝ and Antonín KUČERA. Continuous-Time Stochastic Games with Time-Bounded Reachability. Information and Computation. Elsevier, 2013, vol. 224, No 1, p. 46-70. ISSN 0890-5401. Available from: https://dx.doi.org/10.1016/j.ic.2013.01.001. info
• CHATTERJEE, Krishnendu, Andreas GAISER and Jan KŘETÍNSKÝ. Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. In Computer Aided Verification - 25th International Conference, CAV 2013. Heidelberg Dordrecht London New York: Springer, 2013, p. 559-575. ISBN 978-3-642-39798-1. Available from: https://dx.doi.org/10.1007/978-3-642-39799-8_37. info
• BRÁZDIL, Tomáš, Ľuboš KORENČIAK, Jan KRČÁL, Jan KŘETÍNSKÝ and Vojtěch ŘEHÁK. On time-average limits in deterministic and stochastic Petri nets. In ACM/SPEC International Conference on Performance Engineering, ICPE'13. New York: ACM, 2013, p. 421-422. ISBN 978-1-4503-1636-1. Available from: https://dx.doi.org/10.1145/2479871.2479936. info
• KŘETÍNSKÝ, Jan and Salomon SICKERT. On Refinements of Boolean and Parametric Modal Transition Systems. In Z. Liu, J. Woodcock, and H. Zhu. Theoretical Aspects of Computing - ICTAC 2013 - 10th International Colloquium. Heidelberg Dordrecht London New York: Springer, 2013, p. 213-230. ISBN 978-3-642-39717-2. Available from: https://dx.doi.org/10.1007/978-3-642-39718-9_13. info
• BENEŠ, Nikola, Benoit DELAHAYE, Uli FAHRENBERG, Jan KŘETÍNSKÝ and Axel LEGAY. Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory. In CONCUR 2013 - Concurrency Theory - 24th International Conference. Heidelberg Dordrecht London New York: Springer, 2013, p. 76-90. ISBN 978-3-642-40183-1. Available from: https://dx.doi.org/10.1007/978-3-642-40184-8_7. info
• HERMANNS, Holger, Jan KRČÁL and Jan KŘETÍNSKÝ. Compositional Verification and Optimization of Interactive Markov Chains. In CONCUR 2013 - Concurrency Theory - 24th International Conference. Heidelberg Dordrecht London New York: Springer, 2013, p. 364-379. ISBN 978-3-642-40183-1. Available from: https://dx.doi.org/10.1007/978-3-642-40184-8_26. info
• KŘETÍNSKÝ, Jan and Salomon SICKERT. MoTraS: A Tool for Modal Transition Systems and Their Extensions. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013. Heidelberg Dordrecht London New York: Springer, 2013, p. 487-491. ISBN 978-3-319-02443-1. Available from: https://dx.doi.org/10.1007/978-3-319-02444-8_41. info
• KŘETÍNSKÝ, Jan and Ruslan LEDESMA GARZA. Rabinizer 2: Small Deterministic Automata for LTL\GU. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013. Heidelberg Dordrecht London New York: Springer, 2013, p. 446-450. ISBN 978-3-319-02443-1. Available from: https://dx.doi.org/10.1007/978-3-319-02444-8_32. info
• BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN, Mikael H. MOLLER and Jiří SRBA. Dual-Priced Modal Transition Systems with Time Durations. In LPAR-18 - Logic for Programming, Artificial Intelligence, and Reasoning: 18th International Conference. Heidelberg Dordrecht London New York: Springer, 2012, p. 122-137. ISBN 978-3-642-28716-9. Available from: https://dx.doi.org/10.1007/978-3-642-28717-6_12. info
• KŘETÍNSKÝ, Jan and Javier ESPARZA. Deterministic Automata for the (F,G)-fragment of LTL. In Computer Aided Verification - 24th International Conference. Heidelberg Dordrecht London New York: Springer, 2012, p. 7-22. ISBN 978-3-642-31423-0. Available from: https://dx.doi.org/10.1007/978-3-642-31424-7_7. info
• BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN and Jiří SRBA. EXPTIME-Completeness of Thorough Refinement on Modal Transition Systems. Information and Computation. Elsevier, 2012, vol. 218, September, p. 54-68. ISSN 0890-5401. Available from: https://dx.doi.org/10.1016/j.ic.2012.08.001. info
• BENEŠ, Nikola and Jan KŘETÍNSKÝ. Modal Process Rewrite Systems. In Theoretical Aspects of Computing - ICTAC 2012. Berlin Heidelberg: Springer, 2012, p. 120-135. ISBN 978-3-642-32942-5. Available from: https://dx.doi.org/10.1007/978-3-642-32943-2_9. info
• GAISER, Andreas, Jan KŘETÍNSKÝ and Javier ESPARZA. Rabinizer: Small Deterministic Automata for LTL(F,G). In Automated Technology for Verification and Analysis - 10th International Symposium ATVA 2012. Berlin Heidelberg: Springer, 2012, p. 72-76. ISBN 978-3-642-33385-9. Available from: https://dx.doi.org/10.1007/978-3-642-33386-6_7. info
• BRÁZDIL, Tomáš, Holger HERMANNS, Jan KRČÁL, Jan KŘETÍNSKÝ and Vojtěch ŘEHÁK. Verification of Open Interactive Markov Chains. In Deepak D'Souza and Telikepalli Kavitha and Jaikumar Radhakrishnan. IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2012, p. 474-485. ISBN 978-3-939897-47-7. Available from: https://dx.doi.org/10.4230/LIPIcs.FSTTCS.2012.474. URL info
• BRÁZDIL, Tomáš, Jan KRČÁL, Jan KŘETÍNSKÝ, Antonín KUČERA and Vojtěch ŘEHÁK. Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata. In Emilio Frazzoli, Radu Grosu. HSCC 11: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control. New York: ACM, 2011, p. 33-42. ISBN 978-1-4503-0629-4. info
• BRÁZDIL, Tomáš, Jan KRČÁL, Jan KŘETÍNSKÝ and Vojtěch ŘEHÁK. Fixed-delay Events in Generalized Semi-Markov Processes Revisited. In CONCUR 2011 - Concurrency Theory: 22nd International Conference. Berlin Heidelberg New York: Springer, 2011, p. 140-155. ISBN 978-3-642-23216-9. info
• BENEŠ, Nikola, Ivana ČERNÁ and Jan KŘETÍNSKÝ. Modal Transition Systems: Composition and LTL Model Checking. In ATVA 2011 - Automated Technology for Verification and Analysis: 9th International Symposium. Heidelberg Dordrecht London New York: Springer, 2011, p. 228-242. ISBN 978-3-642-24371-4. info
• BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN, Mikael H. MOLLER and Jiří SRBA. Parametric Modal Transition Systems. In ATVA 2011 - Automated Technology for Verification and Analysis: 9th International Symposium. Heidelberg Dordrecht London New York: Springer, 2011, p. 275-289. ISBN 978-3-642-24371-4. info
• BRÁZDIL, Tomáš, Jan KRČÁL, Jan KŘETÍNSKÝ, Antonín KUČERA and Vojtěch ŘEHÁK. Stochastic Real-Time Games with Qualitative Timed Automata Objectives. In CONCUR 2010 - Concurrency Theory. Berlin Heidelberg New York: Springer, 2010, p. 207-221. ISBN 978-3-642-15374-7. Available from: https://dx.doi.org/10.1007/978-3-642-15375-4_15. info
• BENEŠ, Nikola and Jan KŘETÍNSKÝ. Process Algebra for Modal Transition Systemses. In MEMICS 2010. Brno: NOVPRESS s.r.o., 2010, p. 20-27. ISBN 978-80-87342-10-7. info
• BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN and Jiří SRBA. On Determinism in Modal Transition Systems. Theoretical Computer Science. Elsevier, 2009, 410/2009, No 41, p. 4026-4043. ISSN 0304-3975. info
• BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN and Jiří SRBA. Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete. In Theoretical Aspects of Computing - ICTAC 2009, 6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings. Heidelberg: Springer-Verlag, 2009, p. 112-126. ISBN 978-3-642-03465-7. Available from: https://dx.doi.org/10.1007/978-3-642-03466-4_7. info
• BRÁZDIL, Tomáš, Vojtěch FOREJT, Jan KRČÁL, Jan KŘETÍNSKÝ and Antonín KUČERA. Continuous-Time Stochastic Games with Time-Bounded Reachability. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2009). Dagstuhl, Germany: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2009, p. 61-72. ISBN 978-3-939897-13-2. info
• BRÁZDIL, Tomáš, Vojtěch FOREJT, Jan KŘETÍNSKÝ and Antonín KUČERA. The Satisfiability Problem for Probabilistic CTL. In 23rd IEEE Symposium on Logic in Computer Science (LICS 2008), 24-27 June 2008, Pittsburgh, USA, Proceedings. Los Alamitos, California: IEEE Computer Society, 2008, p. 391-402, 10 pp. ISBN 978-0-7695-3183-0. info

2013/06/20