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

Since October 2015 I am a tenure-track assistant professor at the Chair for Foundations of Software Reliability and Theoretical Computer Science, Technical University of Munich, Germany.

Contact

firstname.lastname@in.tum.de
Room: MI 03.11.044
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
For h-index, see Google Scholar

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

See DBLP, or my CV or Google Scholar. Some full versions are accessible as technical reports not listed by DBLP. The bibtex entries can be found here.

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 2019: 3rd workshop on Learning in Verification, proposed as a 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

2020: TACAS
2019: ACSD, FORMATS, ICTAC, LiVe (co-chair), QAPL, 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

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
Quantitative Systems: Theory and Applications (QuaSy) 2017
KiMfest 2017
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
7x Dagstuhl seminar: 2018, 2017 (3x), 2015, 2014, 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

Teaching

Lectures

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)
IN2050 Model Checking (Summer 2016, 2017)
IN2007 Complexity (Summer 2016)
IN2041 Automata and Formal Languages (Winter 2015/2016)

Tutorials

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)

Students

PhD Students

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, since 2015)
Master theses
Alexander Manta (2018)
Christopher Polster (2018)
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
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 Students (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
Michael Opitz: Algorithms for the Verification of Open Interactive Markov Chains

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

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