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

Contact

Research

Areas

• verification and synthesis
• probabilistic model checking
• applications of machine learning in verification
• temporal logics, in particular LTL and PCTL
• automata theory
• continuous-time stochastic processes and games
• modal transition systems

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 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)

• 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.
• 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

• ETAPS 2022 (general chair)
• 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

• 2021: HSCC, LiVe (co-chair), 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

Invited Talks

• Marktoberdorf Summer School in 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

• 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (Isola) 2020
• Bellairs workshop on Learning and Verification in 2019
• 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (Isola) 2018
• Google Summer of Code (at Google in Munich) in 2017
• Quantitative Systems: Theory and Applications (QuaSy) 2017
• KiMfest 2017
• 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (Isola) 2016
• Trends and Challenges in Quantitative Verification (Mysore workshop) 2016
• 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, 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 (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
  European Research Council (ERC Advanced Grants)
  French National Research Agency (ANR)
  German Research Foundation (DFG)

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)
• IN2157 Fundamental algorithms (Winter 2016/17, 2017/18, 2018/19)
• IN2148 Gems of computer science I (Perlen der Informatik 1) (Winter 2016/17, 2017/18, 2018/19, 2019/20, 2020/21)
• IN2050 Model Checking (Summer 2016, 2017, 2020)
• IN2041 Automata and Formal Languages (Winter 2015/16, 2019/20)

Tutorials (past)

• 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)

• 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)

Students

PhD Students

• Muqsit Azeem (planned start in 2020)
• Florian Dorfhuber (since 2020)
• Stefanie Mohr (Mühlberger) (since 2020, also Master's thesis)
• Kush Grover (since 2019)
• Maximilian Weininger (since 2018, also Guided research and Master's thesis)
• Julia Eisentraut (Krämer) (since 2017)
• Pranav Ashok (since 2016)
• Tobias Meggendorfer (since 2016, also Master's thesis)
• Salomon Sickert (informally co-supervised, 2015-2019, also Bachelor's thesis)

  Master's theses

• Emmanouil Seferis: Safety Verification of Deep Neural Networks: Run-time Monitoring (2020, with AUDI and prof. Knoll; resulted in a joint submission)
• 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 and others

• Lukas Michel: Mean-Payoff Optimization in Modal Markov Decision Processes (2020; resulted in a joint paper at UAI'20)
• Mathias Jackermeier: dtControl: Decision Tree Learning for Explainable Controller Representation (2020; resulted in a joint paper at HSCC'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 jounral submission)
• Alexej Rotar: The Satisfiability Problem for Fragments of PCTL (Bachelor thesis in 2018; resulted in a joint paper at CONCUR'18)
• 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 (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 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.
• My CV can be found here.

Personal