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

• Rabinizer 4 (developed with Tobias Meggendorfer, Salomon Sickert, and Christopher Ziegler) and the previous versions Rabinizer 3 (developed with Zuzana Komarkova), Rabinizer 2 (developed with Ruslan Ledesma Garza) and Rabinizer (developed with Andreas Gaiser): tools for translation of LTL formulae to deterministic automata
• MoTraS (developed with Salomon Sickert), and the old version (developed with Martin Stoll): graphical tools implementing algorithms for modal transition systems and their extensions
• MoChiBA (developed with Salomon Sickert): a probabilistic LTL model checker based on semi-deterministic (limit-deterministic) automata

Community service

Events organization

• LiVe 2020: 4th workshop on Learning in Verification, satellite event of ETAPS, April 2020
• 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: TACAS
• 2020: 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
• 16th International Conference on Quantitative Evaluation of SysTems (QEST) 2019
• Bellairs workshop on Learning and Verification in 2019
• Highlights 2018
• 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (Isola) 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
• Quantitative Systems: Theory and Applications (QuaSy) 2017
• KiMfest 2017
• 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (Isola) 2016
• Weighted Automata: Theory and Applications (WATA) 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
• Reviewer for conferences (selection): CAV, CONCUR, CSL, FoSSaCS, FORMATS, FM, FSTTCS, ICALP, LATA, LICS, MFCS, POPL, QEST, STACS, STOC, TACAS
• Grant proposals: Charles University Grant Agency, European Research Council (ERC Advanced Grants)

Teaching

Lectures

• IN2007 Complexity (Summer 2016, Summer 2019)
• IN0011 Einführung in die theoretische Informatik (Summer 2018)
• IN2340 Quantitative verification (Winter 2016/17, 2017/18, 2018/19)
• 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)
• IN2050 Model Checking (Summer 2016, 2017)
• IN2041 Automata and Formal Languages (Winter 2015/16, 2019/20)

Tutorials

• 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

• Kush Grover (since 2019)
• Maximilian Weininger (since 2018, also Guided research and Master thesis)
• Julia Krämer (since 2017)
• Pranav Ashok (since 2016)
• Tobias Meggendorfer (since 2016, also Master thesis)
• Salomon Sickert (informally co-supervised, 2015-2019)

  Master theses

• Stefanie Mohr-Mühlberger
• 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)
• Clara Waldmann: Translations of LTL to Parity Automata (2016; resulted in a joint paper at TACAS'17)

  Others

• Calvin Chau: Computing a Distribution-based Probabilistic Bisimulation (2019)
• 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