Welcome to the Homepage of Jan Křetínský

A more up-to-date homepage is here.

I am a full professor at the Faculty of Informatics, Masaryk University, Brno, Czech Republic. I am also affiliated as a professor for Formal Methods for Software Reliability at the Chair for Foundations of Software Reliability and Theoretical Computer Science, with Technical University of Munich, Germany.

We are hiring postdocs/PhD/undergrads
on EU projects on verification&AI, in particular the ERC grant InOVationCS starting in June 2025.

For the concrete research areas, please visit the updated webpage of our LiVe Lab and see the call.

Contact

firstname.lastname@tum.de
Room: MI 03.11.044
Faculty of Informatics, Technical University of Munich
Boltzmannstr. 3, 85748 Garching, Germany
Tel.: +49 89 289 17209
ORCID iD: 0000-0002-8122-2881
I may look like any of the guys on the right. So don't be surprised when contacting me in person:-)

Research

ha-index: 89

Areas

verification and synthesis
probabilistic model checking
applications of machine learning in verification
verification of learnt systems, e.g. neural networks
explainable AI, in particular explainable controllers of cyber-physical systems
temporal logics, in particular LTL and PCTL
automata theory
continuous-time stochastic processes and games
modal transition systems

Publications

See DBLP or Google Scholar.

Tools

Automata Tutor v3 is a teaching tool for courses on automata theory and introduction to computation
SeQuaiA performs semi-quantitative analysis of chemical reaction networks
dtControl 2.0 represents CPS controllers as decision trees, improving memory footprint and explainability while preserving guarantees
Rabinizer 4 translates LTL formulae to various (semi-)deterministic automata (previous versions 3.1 and 2) with Owl as a reusable library for developing such translations with additional infrastructure
MoChiBA is a PRISM-based probabilistic LTL model checker based on semi-deterministic (limit-deterministic) Büchi automata
MoTraS for modal transition systems and their extensions
PET (Partial Exploration Tool, aka PRISM TUM in QComp, under development) is a probabilistic model checker for stochastic games, MDP and related models with (unbounded) reachability and mean payoff objectives, featuring also a module for statistical model checking

Projects (running)

Verified AI is a collaboration with AUDI AG on subprojects of EU H2020 Hi-Drive project.
Group-By Objectives in Probabilistic Verification (GOPro) is a DFG project 427755713.
Continuous Verification of CYber-Physical Systems (ConVeY) is a DFG research training group GRK 2428.

Projects (previous)

Statistical Unbounded Verification (SUV) is a DFG project 383882557.
Verified Model Checkers (VMC) is a DFG project 317422601.
Platform-Aware Synthesis of Embedded Control Software (PARSEC) is a TUM IGSSE project 10.06.
In collaboration, my PhD student Julia Eisentraut has obtained the following projects:
- Proven Security for systems with human interaction (ProSec) is a project funded by the German Federal Ministry of Education and Research (Bundesministerium für Bildung und Forschung) and supported by Software Campus performed in collaboration of TUM and DATEV eG
- Formal Methods for Analysis of Attack-Defence Diagrams is a PhD project of Studienstiftung des deutschen Volkes

Community service

Events organization

Dagstuhl Seminar 24361 Artificial Intelligence and Formal Methods Join Forces for Reliable Autonomy, September 2024
Dagstuhl Seminar 24231 Stochastic Games, June 2024
LiVe 2024: 8th workshop on Learning in Verification, satellite event of ETAPS, April 2024
LiVe 2023: 7th workshop on Learning in Verification, satellite event of ETAPS, April 2023
ETAPS 2022 (general chair)
FOMEO 2022: 2nd Workshop on Formal Methods Education Online, proposed as a satellite event of FLoC, July 2022
LiVe 2022: 6th workshop on Learning in Verification, satellite event of ETAPS, April 2022
FOMEO 2021: Formal Methods Education Online, satellite event of ICALP, July 2021
LiVe 2021: 5th workshop on Learning in Verification, satellite event of ETAPS, March 2021
LiVe 2020: 4th workshop on Learning in Verification, satellite event of ETAPS, April 2020 postponed due to COVID-19 until next LiVe edition
LiVe 2019: 3rd workshop on Learning in Verification, satellite event of ETAPS, April 2019
Game Solving: Theory and Practice, satellite event of ICALP, July 2018
LiVe 2018: 2nd workshop on Learning in Verification, satellite event of ETAPS, April 2018
Dagstuhl Seminar 18121 Machine Learning and Model Checking Join Forces, March 2018
Workshop on Formal Methods for Attack Trees, Munich, November 2017
LiVe 2017: 1st Workshop on Learning in Verification, satellite event of ETAPS, April 2017

PC Member

2025: AAAI-DC, CONCUR, FMICS, ICALP, ICTAC, RV, VMCAI
2024: FMICS, ICTAC, ISoLA (track co-organizer), LATIN, LiVe (chair), MOVEP
2023: AISoLA (track co-organizer), CD-MAKE, DAV, FORMATS, ICALP, ICTAC, LiVe (chair), QEST, TiCSA
2022: LICS, LiVe (chair), QEST, TACAS, VMCAI
2021: CMSB, CONCUR, HSCC, LiVe (chair), QEST, TACAS
2020: CMSB, GandALF, ICTAC, LiVe (co-chair), NETYS, QEST, TACAS, TTCS, VMCAI
2019: ACSD, FORMATS, GandALF, ICTAC, LiVe (co-chair), MoRe, QAPL, SR, TACAS, VMCAI
2018: ACSD, CAV (AEC), FORMATS, ICTAC, LiVe (co-chair), QAPL, QEST, SR, TACAS
2017: ACSD, FORMATS, LiVe (co-chair), QAPL, QEST, SOFSEM, TACAS, TIME, TTCS
2016: ECAI, MEMICS
2015: QAPL

SC Member

ETAPS (since 2021)

My programme to support EATCS

I would like to support continuous summer-school activities to raise awareness of importance of TCS among the young researchers and as means of building bridges to other areas of CS, in particular AI.
Further, I would like to help preserving the balance within the brotherhood of TCS "Volume A" and "Volume B" through equal efforts in advertisement and prize-awarding activities.

Invited Talks

Invited talks at conferences, workshops, summer schools

Workshop on Verifiable and Robust AI (VRAI) 2023
Marktoberdorf Summer School 2023
AlgoMaNet Summer School 2023
Logic Mentoring Workshop (at CSL) 2023
Quantitative Aspects of Variant-rich Systems (QAVS) 2022
Quantitative Logics and Automata (seminar at TU Dresden)
Modern Trends in Informatics (seminar at Brno University of Technology)
Formal Methods and Models (seminar at LaBRI) 2021
11th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF) 2020
IRIF Modelling and Verification (seminar at Paris Diderot University) 2020
16th International Conference on Quantitative Evaluation of SysTems (QEST) 2019
Workshop on Security practices for Internet of Things (SPIoT) 2019
6th International Workshop on Synthesis of Complex Parameters (SynCoP) 2019
Highlights of Logic, Games and Automata (Highlights) 2018
2nd School on Foundations of Programming and Software Systems: Logic and Learning (FLOC + EATCS + SIGLOG summer school) 2018
Learning in Verification and Verification of Learning (seminar organized by the universities of Brussels and Mons) in 2018
Logic and Learning (workshop at Alan Turing Institute of data science) in 2018

Invitation-based seminars and workshops

Czech-French AI Workshop 2022
Rigorous Automated Planning (Lorentz Center Workshop) 2022
Bellairs workshop on Learning and Verification in 2019
Google Summer of Code (at Google in Munich) in 2017
Quantitative Systems: Theory and Applications (QuaSy) 2017
KiMfest 2017
Trends and Challenges in Quantitative Verification (Mysore workshop) 2016
International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (Isola): 2016, 2018, 2020 (moved to 2021), 2022, 2023 (co-organizing the track Verification meets Learning and Statistics)
Dagstuhl seminars:
Verification and Synthesis of Human-Robot Interaction 2019
Machine Learning and Model Checking Join Forces 2018 (co-organizer)
Formal Synthesis of Cyber-Physical Systems 2017
Game Theory in AI, Logic, and Algorithms 2017
Computer-Assisted Engineering for Robotics and Autonomous Systems 2017
Non-Zero-Sum-Games and Control 2015
Quantitative Models: Expressiveness, Analysis, and New Applications 2014
Quantitative Models: Expressiveness and Analysis 2010

Reviewing

Reviewer for journals (selection): Acta Informatica, Information Processing Letters, Journal of Automated Reasoning, Journal of Computer and System Sciences, Performance Evaluation, Robotics and Automation Letters, Software and Systems Modeling, Theoretical Computer Science, Transactions on Modeling and Computer Simulation, Transactions on Programming Languages and Systems, Transactions on Software Engineering
Reviewer for conferences (selection): CAV, CONCUR, CSL, FoSSaCS, FORMATS, FM, FSTTCS, ICALP, LATA, LICS, MFCS, POPL, QEST, STACS, STOC, TACAS
PhD theses:
Jakob Piribauer: On Non-Classical Stochastic Shortest Path Problems (Dresden University of Technology, Germany, 2021)
Yuliya Butkova: Towards Efficient Analysis of Markov Automata (University of Saarland, Germany, 2020)
Maxime Audinot: Assisted Design and Analysis of Attck Trees (University of Rennes 1, France, 2018)
Enno Ruijters: Zen and the Art of Railway Maintenance (University of Twente, The Netherlands, 2018)
Grant proposals:
Charles University Grant Agency (GAUK)
Czech Science Foundation (GACR, Mathematics&Informatics panel vice-chair)
European Research Council (ERC Advanced/Consolidator/Starting Grants)
French National Research Agency (ANR)
German Research Foundation (DFG)
Israel Science Foundation (ISF)
National Research, Development and Innovation Office, Hungary (NRDI)
Vienna Science and Technology Fund (WWTF)

Teaching

Lectures

IN2007 Complexity (Summer 2016, 2019)
IN0011 Einführung in die theoretische Informatik (Summer 2018), tool Automata Tutor v3
IN2340 Quantitative verification (Winter 2016/17, 2017/18, 2018/19, 2020/21, 2021/2022)
IN2157 Fundamental algorithms (Winter 2016/17, 2017/18, 2018/19, 2021/2022)
IN2148 Gems of computer science I (Perlen der Informatik 1) (Winter 2016/17, 2017/18, 2018/19, 2019/20, 2020/21, 2021/2022)
IN2050 Model Checking (Summer 2016, 2017, 2020, 2021, 2022)
IN2041 Automata and Formal Languages (Winter 2015/16, 2019/20)

Tutorials (past)

Technical University Munich

IN0018 Diskrete Wahrscheinlichkeitstheorie (Summer 2012)
IN2007 Complexity (TUM, Summer 2010, 2011)
IN2041 Automata and Formal Languages (Winter 2009/10, 2010/11, 2011/12, 2012/13)

Masaryk University

IA008 Computational Logic (Spring 2009)
IB102 Automata and Grammars (Autumn 2007)
MB003 Linear Algebra and Geometry I (Spring 2008)
MB005 Foundations of mathematics (Autumn 2007)
M1110 Linear Algebra and Geometry I (Autumn 2007)

Supervision

Post-docs

Sudeep Kanav (planned from 2023)
Debraj Chakraborty (planned from 2023)
Sadegh Mohagheghi (planned from 2023)
Alexandros Evangelidis (since 2020)
PhD Students
Maximilian Prokop (planned from 2023)
Sabine Rieder (with AUDI since 2021, also Master's thesis)
Marta Grobelna (since 2021, partially with Fraunhofer)
Muqsit Azeem (since 2020)
Florian Dorfhuber (since 2020)
Stefanie Mohr (Mühlberger) (since 2020, also Master's thesis)
Kush Grover (since 2019)
Maximilian Weininger: Solving Stochastic Games Reliably (since 2018, also Guided research and Master's thesis)
Julia Eisentraut (Krämer) (since 2017, now Member of Parliament of North Rhine-Westphalia)
Pranav Ashok: A Learning Twist on Controllers: Synthesis via Partial Exploration and Concise Representations (2016-2021, now at Fraunhofer IKS)
Tobias Meggendorfer: Verification of Discrete-Time Markov Decision Processes (2016-2021, also Master's thesis, now at IST Austria)
Salomon Sickert: A Unified Translation of Linear Temporal Logic to Omega-Automata (informally co-supervised, 2015-2019, also Bachelor's thesis, now at Hebrew University of Jerusalem)

Master's theses
Maximilian Prokop: Predicting Efficient Initial Strategies for Parity Games in LTL-Synthesis Using Machine Learning (2022; resulted in a joint paper at CAV'23)
Calvin Chau: Raising the Abstraction Level of Hardware Model Checking by Generating Verification Code from Activity Diagrams (2022, with Apple)
Alexander Slivinskiy: Facilitating Experimental Analysis of Algorithms for Stochastic Games: Random Model Generation and Mining the Results (2022; resulted in a joint paper at ATVA'22)
Sabine Rieder: Learning Support Vector Machines for Predicting Winning Strategies in LTL Synthesis (2021; resulted in a joint paper at CAV'23)
Sebastian Mair: Improving Deep Q-Learning Using Statistical Model Checking (2021)
Emmanouil Seferis: Safety Verification of Deep Neural Networks: Run-time Monitoring (2020, with AUDI and prof. Knoll; resulted in a joint paper at RV'21)
Stefanie Mühlberger (Mohr): Faster Verification of Neural Networks with Clustering-based Compression (2020; resulted in a joint paper at ATVA'20)
Alexander Manta: Machine Learning Guidance in Automata-Theoretic Approach for Reactive LTL Synthesis (2019; resulted in a joint paper at ATVA'19)
Christopher Polster: Refinement for Game-Based Abstractions of Continuous-Space Linear Stochastic Systems (2019)
Sebastian Fiss: Learning Methods for Parity Games and Their Application to LTL Synthesis (2018)
Matthias Franze: A direct translation from the FGX-Fragment of LTL to Deterministic Parity Automata (2018)
Maximilian Weininger: Heuristics For Solving Stochastic Games (2017; resulted in a joint paper at CAV'18)
Rupam Bhattacharya: Leveraging Deep Learning Solutions for Predictive Maintenance of Industrial Datasets (2017, with BMW)
Clara Waldmann: Translations of LTL to Parity Automata (2016; resulted in a joint paper at TACAS'17)
Bachelor's theses
Alexander Taepper: Containing the State Space Explosion in the Model Checking of Attack-Defense Trees (2022)
Florian Jüngermann: Learning Algebraic Predicates for Explainable Controllers (2021; resulted in a joint paper in STTT)
Alicia Dimroth: Neural Network Abstraction Using Principal Component Analysis (2021)
Manuel Bildhauer: Generation of Attack-Defense-Diagrams from Event Sequences of previous Attacks (2020)
Mathias Jackermeier: dtControl: Decision Tree Learning for Explainable Controller Representation (2020; resulted in a joint paper at HSCC'20)
Christoph Weinhuber: Learning Domain-Specific Predicates in Decision Trees for Explainable Controller Representation (2020; resulted in a joint paper at TACAS'21)
Alexander Slivinskiy: Solving Simple Stochastic Games with Quadratic Programming (2020; resulted in a joint paper at GandALF'20)
Lukas Michel: Mean-Payoff Optimization in Modal Markov Decision Processes (2020; resulted in a joint paper at UAI'20)
Fabian Michel: Parity Modal Markov Decision Processes (2019; resulted in a joint paper at UAI'20)
Calvin Chau: Computing a Distribution-based Probabilistic Bisimulation (2019; resulted in a joint journal submission)
Emanuel Ramneantu: Exercises on regular expressions in Automata Tutor (2019; resulted in a joint paper at CAV'20)
Alexej Rotar: The Satisfiability Problem for Fragments of PCTL (Bachelor thesis in 2018; resulted in a joint paper at CONCUR'18)
Guided research and others
Maria del Sol Barrientos Moreno: Are Attack-Defense Trees Useful for Communicating Risk to Non-experts? (2022)
Philipp Klocke: Neural Network Runtime Monitor (with AUDI; 2021)
Maximilian Prokop: Developement of more sophisticated evaluation methods for edge classification in parity games as well as new classification methods (2021)
Calvin Chau: Abstraction Refinement for Neural Networks (2021; resulted in a joint submission)
Christian Backs: Machine Learning for Prediction of Edge Performance in LTL Synthesis (2020)
Maximilian Weininger: Translating Linear Temporal Logic to Parity Automata (guided research in 2016; resulted in a joint paper at TACAS'17)
Christopher Ziegler (Google Summer of Code in 2016; resulted in a joint paper at CAV'18)
Past Bachelor theses (advisor 2010-2013)
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
Philipp Meyer: Algorithms for Refinement of Modal Process Rewrite Systems
Alexander Manta: Implementation of Algorithms for Modal Transition Systems with Durations

Education and previous positions

From 2015 to 2021 I was a tenure-track assistant professor at the Chair for Foundations of Software Reliability and Theoretical Computer Science, Technical University of Munich, Germany. From 2013 to 2015 I was an IST Fellow at IST Austria hosted by the group of Thomas Henzinger and the group of Krishnendu Chatterjee.
I received my PhD at the Technical University Munich, Germany, where my advisor was Javier Esparza. The thesis Verification of Discrete- and Continuous-Time Non-Deterministic Markovian Systems was defended summa cum laude (with distinction). I received another PhD at Masaryk University Brno, Czech Republic, with my advisor being Antonín Kučera and my thesis Modal Transition Systems: Extensions and Analysis (with distinction). There I also received my Master's and Bachelor's degrees in computer science, mathematics, philosophy and linguistics.

Personal

I am also interested in travelling, photography, skiing, windsurfing, volleyball, chocolate, languages etc.