E-Mail: firstname.lastname@tum.de
ORCID:
0000-0002-8122-2881Address:
Botanická 554/68a 602 00 Brno
Jan Křetínský
Office: C514
E-Mail: firstname.lastname@tum.de
ORCID: 0000-0002-8122-2881
Address:
E-Mail: firstname.lastname@tum.de
ORCID:
0000-0002-8122-2881Address:
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.
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
Full List of Publications
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 and the old version (developed with Martin Stoll): graphical tools implementing algorithms –> 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)
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
- Debraj Chakraborty (since 2023)
- Sudeep Kanav (2023 - 2025)
- Sadegh Mohagheghi (2023 - 2024)
- Alexandros Evangelidis (2020 - 2022)
PhD Students
- Maximilian Prokop (since 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) <!– - Cristian Neufuss: Translating Natural Language for a Regex Compiler Language using Neural Networks (2019)
- Safa Mert Akmese: Generating Richer Predicates for Decision Trees (2019)
- Sebastian Mair: Support of Pushdown-Automata in Automata Tutor (2019)
- Christian Backs: Automatic generation of exercises on Turing machines (2018) –>
- 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.
Research Areas
Value Iteration for Stochastic Games
We develop value iteration algorithms for stochastic games.
Runtime Monitoring of Neural Network
We develop runtime monitors for neural networks to improve their reliability.
Abstraction of Neural Network
We abstract neural networks to improve verification speed.
Machine Learning for LTL Synthesis
We apply machine learning to the LTL synthesis problem.
Translating LTL to Automata
We design algorithms for translating LTL to different types of automata.
Explaining Controllers via Decision Trees
We develop methods for explaining controllers with decision trees.
Explaining Controllers via Automata
We develop methods for explaining controllers via automata.
Concurrent Stochastic Games
We develop techniques for the verification of concurrent stochastic games which extend turn-based stochastic games by allowing players to select actions simultaneously in each state, reflecting more realistic scenarios of interactive agents acting concurrently.
Tools
SemML
In this project we develop learning-based exploration heuristics for LTL Synthesis that exploit the semantic labelling of the underlying Automaton/Game.
MONITIZER
We create a tool (Monitizer) that optimizes monitors on a NN for a specific task.
dtControl
Represent controllers as decision trees. Improve memory footprint, boost explainability while preserving guarantees.
Automata Tutor is an online teaching tool that aids instructors and students in large courses on automata and formal languages with many different exercise types.