CURRICULUM VITAE
Prof. Dr.rer.nat. RNDr. Mgr. Bc. Jan Křetínský, Ph.D.
Born: 1984 Nationality: Czech
ORCID iD 0000-0002-8122-2881
FORD classification: 1.2, R4
H-index: 28 at Google Scholar, 19 at Scopus, 13 at WoS
Citations:
● 2,202 at Google Scholar (with self-citations),
● 1,180/713 at Scopus (with/without self-citations),
● 628/473 at Web of Science (with/without self-citations).
Affiliation and Address: Department of Infromatics
School of Computation, Information and Technology, Technical University of Munich
Boltzmannstr. 3, D-85748 Garching bei München, Germany
Tel.: +49 89 289 17209, e-mail: jan.kretinsky@tum.de, web: https://www7.in.tum.de/~kretinsk/
Current Position: tenured W3-level professor for Formal Methods for Software Reliability
Upcoming Position: full professor at Faculty of Informatics, Masaryk University (MU) starting in 2023
Education and Academic Qualifications:
• 2007: Bachelor in Computer Science, MU (with distinction, Dean’s prize); Bachelor in Mathematics, MU
(with distinction), Bachelor in Philosophy and Linguistics
• 2009: Master in Computer Science, MU (with distinction, Rector’s prize)
• 2010: Master in Mathematics, MU (with distinction)
• 2013: Dr.rer.nat (Ph.D.) in Computer Science, Technical University of Munich, Germany (TUM) (with
distinction) with the thesis “Verification of Discrete- and Continuous-Time Non-Deterministic Markovian
Systems”
• 2014: Ph.D. in Computer Science, MU (with distinction) with the thesis “Modal Transition Systems:
Extensions and Analysis”
• 2019: habilitation at MU with the habilitation thesis entitled “Modern Probabilistic Verification”.
• 2021: tenure, W3-Professorship at TUM
• 2022: full professorship in the area of computer science at MU
Brief Employment History Description:
● 2009–13: researcher at TUM
● 2013–15: IST Fellow (independent postdoc researcher) at IST Austria (hosted by Thomas A. Henzinger
and Krishnendu Chatterjee)
● 2015–21: Tenure-Track Assistant Professor at TUM
● Since 2021: Permanent W3-Professor at TUM:
○ lecturer in courses of “Automata and Formal Languages”, “Complexity”, “Fundamental
algorithms”, “Gems of computer science”, “Introduction to theoretical computer science”,
“Model Checking”, and “Quantitative verification”
○ supervisor of 10 Ph.D. students (3 of whom have already defended their Ph.D.)
Research interests:
• verification and synthesis, temporal logics, automata theory
• probabilistic model checking, continuous-time stochastic processes and games, modal transition
systems
• applications of machine learning in verification, verification of learnt systems (e.g. neural networks)
• explainable AI, in particular explainable controllers of cyber-physical systems
Selected research results:
● Multiple novel techniques of model checking probabilistic systems, with applications of the techniques
in diverse areas incl. biochemistry, security, AI, robotics
● Novel methods of translating linear temporal logic to automata, with applications in synthesis,
reinforcement learning, robotics
● Pioneering works utilizing machine learning in verification; novel verification and monitoring of learnt
systems, incl. applications in automotive industry (AUDI AG)
● Pioneering works on explainable controllers of software and cyber-physical systems
● All mentioned techniques complemented with software tools
Five selected publications since 2016:
1. Javier Esparza, Jan Křetínský, and Salomon Sickert. A unified translation of linear temporal logic to ωautomata.
J. ACM, 67(6):33:1–33:61, 2020.
○ AIS Q1 journal, Scopus citations with/without self-citations: 5/3, Scopus Citation Percentile
(SCP): 48, Scopus Field-Weighted Citation Impact (FWCI): 0.49; conference version (LICS 2018 –
CORE A*) 15/6 , SCP 94%, FWCI 3.38
○ Role of Jan Křetínský: Designed a completely new approach to the translations (starting in
2012) and since then extended and improved it with the co-authors.
2. Salomon Sickert, Javier Esparza, Stefan Jaax, Jan Křetínský: Limit-Deterministic Büchi Automata for
Linear Temporal Logic. CAV (2) 2016: 312-332
○ CORE A* conference, Scopus citations with/without self-citations: 47/34, SCP 96%, FWCI
4.31.
○ Role of Jan Křetínský: Suggested the main approach, designed its use in probabilistic model
checking and proved its correctness
3. Jan Křetínský, Tobias Meggendorfer, Salomon Sickert, Christopher Ziegler: Rabinizer 4: From LTL to Your
Favourite Deterministic Automaton. CAV (1) 2018: 567-577
○ CORE A* conference, Scopus citations with/without self-citations: 22/16, SCP 97%, FWCI
4.94.
○ Role of Jan Křetínský: Suggested the main approach, most of the paper writing
4. Kush Grover, Fernando S. Barbosa, Jana Tumova, Jan Křetínský: Semantic Abstraction-Guided Motion
Planning for scLTL Missions in Unknown Environments. Robotics: Science and Systems (RSS) 2021
○ CORE A* conference, Scopus citations with/without self-citations: 1/1, SCP: 74%, FWCI:
1.06.
○ Role of Jan Křetínský: Suggested the main idea and designed the algorithm
5. Jan Křetínský: LTL-Constrained Steady-State Policy Synthesis. IJCAI 2021: 4104-4111
○ CORE A* conference, Scopus citations with/without self-citations: 0/0.
○ Role of Jan Křetínský: Complete paper
Five selected publications before 2016
1. Jan Křetínský, Javier Esparza: Deterministic Automata for the (F, G)-Fragment of LTL. CAV 2012: 7-22
○ CORE A* conference, Scopus citations with/without self-citations: 33/17, SCP 96%, FWCI
4.75.
○ Role of Jan Křetínský: Suggested, worked out and wrote the whole paper, except for
introduction.
2. Krishnendu Chatterjee, Andreas Gaiser, Jan Křetínský: Automata with Generalized Rabin Pairs for
Probabilistic Model Checking and LTL Synthesis. CAV 2013: 559-575
○ CORE A* conference, Scopus citations with/without self-citations: 35/19, SCP 97%, FWCI
5.79.
○ Role of Jan Křetínský: Worked out the theoretical part of the paper, wrote the paper.
3. Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Křetínský, Marta Z.
Kwiatkowska, David Parker, Mateusz Ujma: Verification of Markov Decision Processes Using Learning
Algorithms. ATVA 2014: 98-114
○ CORE A conference, Scopus citations with/without self-citations: 105/78, SCP 98%, FWCI
6.92.
○ Role of Jan Křetínský: Suggested the topic, designed and proved the key transformation
yielding the convergence and the error bounds and adapted the machine-learning technique to
the setting of reachability.
4. Holger Hermanns, Jan Krcál, Jan Křetínský: Probabilistic Bisimulation: Naturally on Distributions.
CONCUR 2014: 249-265
○ CORE A conference, Scopus citations with/without self-citations: 31/26, SCP 96%, FWCI
4.21.
○ Role of Jan Křetínský: Suggested the new perspective and designed the main new definition as
well as the co-algebraic description.
5. Krishnendu Chatterjee, Zuzana Komárková, Jan Křetínský: Unifying Two Views on Multiple Mean-Payoff
Objectives in Markov Decision Processes. LICS 2015: 244-256
○ CORE A* conference, Scopus citations with/without self-citations: 21/9, SCP 97%, FWCI
5.80.
○ Role of Jan Křetínský: Worked out most of the theory and proofs, wrote the paper.
Received international (not Czech) projects since 2016
● 2021—2024 Verified AI – ADAS/AD Systems (AUDI AG, PI with 1 PhD + 58k EUR)
● 2020—2023 Group-by Objectives in Probabilistic Verification (German Research Foundation (DFG), PI
with 620k EUR ~ 1 PhD + 1 postdoc)
● 2019—2023 Continuous Verification of Cyber-Physical Systems (DFG, co-PI with 2 PhD share in 5.5 M
EUR)
● 2018—2022 Statistical Unbounded Verification (DFG, PI with 313k EUR ~ 1 PhD)
● 2017—2022 Verified Model Checkers (DFG, co-PI with 264k EUR share ~ 1 PhD)
Received national (Czech) projects since 2016:
● 2023—2028 MUNI Award in Science and Humanities (MU, PI with 25 M CZK)
Other project highlights:
● Industrial collaboration: AUDI AG, Datev eG
● Grant application for ERC Starting Grant has been awarded Score 'A': Fully meets the ERC excellence
criterion and is recommended for funding if sufficient funds are available.
Research and Academic Stays:
• Beside stays at TUM, IST and MU, several stays at Aalborg University (6 months in total) and INRIA
Rennes (1 month in total)
Scientific awards and Recognition and Academic membership since 2016
● Invited talks at conferences (QEST; Highlights of Logic, Games and Automata), summer schools
(FLOC/EATCS/SIGLOG School on Foundations of Programming and Software Systems: Logic and Learning;
Ferienakademie; Marktoberdorf – invited for 2023), workshops and seminars (in total over 30)
● General chair of ETAPS 2022, member of the ETAPS SC 2021–23, (co-)chair of LiVe (Workshop on
Learning in Verification) 2017-2023
● PC Member (selection of conferences): ACSD (2017, 2018, 2019), CAV (AEC 2018), CMSB (2020, 2021),
CONCUR (2021), ECAI (2016), FORMATS (2017, 2018, 2019), GandALF (2019, 2020), HSCC (2021), ICALP
(2023), ICTAC (2018, 2019, 2020), LICS (2022), NETYS (2020), QEST (2017, 2018, 2020, 2021, 2022), SR
(2018, 2019), TACAS (2017, 2018, 2019, 2020, 2021, 2022), TIME (2017), TTCS (2017, 2020), VMCAI
(2019, 2020, 2022)
● Reviewer for research grant proposals (selection): European Research Council (ERC Advanced Grants,
ERC Consolidator Grants), French National Research Agency (ANR), German Research Foundation
(DFG), Israel Science Foundation (ISF)