Important notice

This webpage has last been updated in August 2022. I have since become an IST-BRIDGE fellow. See here for my current webpage.

About Me

Hello! Since December 2017, I’m a Doctoral candidate advised by Prof. Jan Křetínský in the Chair for Foundations of Software Reliability and Theoretical Computer Science at the Technical University of Munich.

My current work revolves around formal methods and verification. The main branch of my work is concerned with the model of stochastic games, which are probabilistic systems exhibiting controlled as well as adversarial non-determinism. Given an objective (e.g. “Reach the target state”), solving a stochastic game amounts to computing the optimal strategies of both players as well as the corresponding probability to satisfy the objective at each state if both play optimally. Thus, this problem can be considered probabilistic model checking as well as controller synthesis.

Another branch of my work considers compact and explainable representation of controllers (this includes both controllers generated by solving stochastic games as well as controllers generated by any other tool). For this, my co-authors and I have developed the tool dtControl, which can transfer controllers from various formats into smaller and more explainable decision trees.

Read more about my research activities on dblp or google scholar, or check out any of my publications listed below.

Publications

Probabilistic model checking and controller synthesis for stochastic games

[19] Křetínský, J., Ramneantu, E., Slivinskiy, A., & Weininger, M. (2022). Comparison of algorithms for simple stochastic games. Information and Computation. (Invited special issue for [11]) (paper)

[18] Eisentraut, J., Kelmendi, E., Křetínský, J., & Weininger, M. (2022). Value iteration for simple stochastic games: Stopping criterion and learning algorithm. Information and Computation. (Journal version of [3]) (paper)

[16] Weininger, M., Grover, K., Misra, S., & Kretinsky, J. (2021). Guaranteed Trade-Offs in Dynamic Information Flow Tracking Games. CDC 2021. (paper)

[15] Winkler, T., & Weininger, M. (2021). Stochastic Games with Disjunctions of Multiple Objectives. GandALF 2021. (pre-print)

[12] Ashok, P., Daca, P., Kretinsky, J., & Weininger, M. (2020). Statistical Model Checking: Black or White?. Isola 2020 - 30 years of Statistical Model Checking! (SMC). (paper)

[11] Kretinsky, J., Ramneantu, E., Slivinskiy, A., & Weininger, M. (2020). Comparison of Algorithms for Simple Stochastic Games. GandALF 2020. (paper).

[10] Chatterjee, K., Katoen, J., Weininger, M., & Winkler, T. (2020). Stochastic Games with Lexicographic Reachability-Safety Objectives. CAV 2020. (pre-print).

[8] Ashok, P., Chatterjee, K., Kretinsky, J., Weininger, M., & Winkler, T. (2020). Approximating Values of Generalized-Reachability Stochastic Games. LICS 2020. (paper)

[6] Weininger, M., Meggendorfer, T., & Kretinsky, J. (2019). Satisfiability Bounds for omega-Regular Properties in Bounded-Parameter Markov Decision Processes. CDC 2019. (paper)

[4] Ashok, P., Kretinsky, J., & Weininger, M. (2019). PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games. CAV 2019. (paper).

[3] Kelmendi, E., Krämer, J., Kretinsky, J., & Weininger, M. (2018). Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm. CAV 2018. (pre-print).

Small and explainable representation of controllers

[13] Ashok, P., Jackermeier, M., Kretinsky, J., Weinhuber, C., Weininger, M., & Yadav, M. (2021). dtcontrol 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts. TACAS 2021. (paper)

[7] Ashok, P., Jackermeier, M., Jagtap, P., Kretinsky, J., Weininger, M., & Zamani, M. (2020). dtControl: decision tree learning algorithms for controller representation. HSCC 2020. (paper).

[5] Ashok, P., Kretinsky, J., Larsen, K.G., Le Coënt, A., Taankvist, J.H., & Weininger, M. (2019). SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes. QEST 2019. (pre-print).

Other

[17] Kretinsky, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2021). Index appearance record with preorders. Acta Informatica. (paper)

[14] Esparza, J., Kiefer, S., Kretinsky, J., & Weininger, M. (2021). Enforcing omega-Regular Properties in Markov Chains by Restarting. CONCUR 2021. (pre-print)

[9] D’Antoni, L., Helfrich, M., Kretinsky, J., Ramneantu, E., & Weininger, M. (2020). Automata Tutor v3. CAV 2020. (pre-print).

[2] Křetínský, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2017). Index appearance record for transforming Rabin automata into parity automata. TACAS 2017. (pre-print).

[1] Zolg, D. P., Wilhelm, M., Schnatbaum, K., Zerweck, J., Knaute, T., Delanghe, B., …, Weininger, M. & Yu, P. (2017). Building ProteomeTools based on a complete synthetic human proteome. Nature methods 14.3 (2017): 259. (paper).

Tools

• 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 (cf. QComp 2019 or QComp 2020).
• dtControl represents CPS controllers as decision trees, improving memory footprint and explainability while preserving guarantees (cf. publication [7] or this demo paper, as well their respective presentations listed below).
• Automata Tutor v3 is a teaching tool for courses on automata theory and introduction to theoretical computer science (cf. publication [9] and the respective presentation).

Past Presentations

• Solving All Kinds of Simple Stochastic Games @ ROCKS’22, May 22.
• PAC Guarantees for unknown probabilities through sampling (Combining [4] and [6]) @ LiVe’22, April 22.
• Guaranteed Trade-Offs in Dynamic Information Flow Tracking Games @ CDC 21, December 21.
• Thesis title TBD (overview of my research) @ Retreat to move forward, October 21.
• Short talk: Comparison of Algorithms for Simple Stochastic Games @ Highlights 2021, September 21.
• Automata Tutor v3: Lessons learned and open questions @ FOMEO’21, July 21.
• dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts (Slides) @ TACAS 21, April 21.
• Decidability of Generalized Reachability Stochastic Games @ Spotlight on Games Workshop, November 20.
• Comparison of Algorithms for Simple Stochastic Games (Video that won a best video award) @ GandALF20, September 20.
• Approximating Values of Generalized-Reachability Stochastic Games (based on publication [8]) @ HIGHLIGHTS 2020, September 20.
• Tool demo “Compact and explainable strategy representations using dtControl” (Video) (based on publication [7] and our ongoing work) @ QEST 2020, September 20.
• Automata Tutor v3 (Video at 1:04:50) @ CAV20, July 20.
• Approximating Values of Generalized-Reachability Stochastic Games (Video) @ LICS20, July 20.
• dtControl: decision tree learning algorithms for controller representation (Video) @ HSCC20, April 20.
• Demo: dtControl: decision tree learning algorithms for controller representation (Video) @ HSCC20, April 20.
• Satisfiability Bounds for omega-Regular Properties in Bounded-Parameter Markov Decision Processes (slides) @ CDC19, December 2019
• BRTDP for Stochastic Games (slides, abstract) @ LiVe19, April 2019
• Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (poster) @ Workshop - Theory and Algorithms in Graph and Stochastic Games, March 2019
• Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (slides) @ CAV 18, June 2018
• Heuristics for Solving Stochastic Games: Stopping Criterion and Learning Algorithm @ TUM-I7 Workshop in Altmühltal, March 2018

Community Service

• Website chair and local staff at ETAPS 2022.

• Co-organizer of the workshop FOMEO in 2021 and 2022.

• TACAS Artifact Evaluation Committee 2019 and 2020

• Subreviewer for QEST 18/20/21, ICTAC 18/19/20, VMCAI 19/21/22, FORMATS 19, TACAS 19/20/22, CONCUR 20/21/22, ATVA 20, GandALF 20, HSCC 20, MFCS 21, LICS 22

Teaching

Courses

• Introduction to theoretical computer science (TA in Summer 18, technical support with the tool Automata Tutor in Summer 19 and 20).
• Discrete structures (Tutor Winter 19/20).
• Seminar “Security and Verification” (Organizer Summer 20).
• Practical Course “Algorithms for Programming Contests” (Tutor Winter 20/21)
• Practical Course “Recent Advances in Model Checking” (Organizer Summer 22).
• Nachqualifikation Inf-GY THEO (Lecturer Summer 21 and 22).

Theses

• BT Summer 18: Christian Backs, Automatic generation of exercises on Turing machines (see publication [9])
• BT Summer 18: Sebastian Mair, Support of pushdown automata in Automata Tutor (see publication [9])
• BT Winter 18/19: Emanuel Ramneantu, Exercises on regular expressions in Automata Tutor (see publication [9])
• BT Summer 19: Safa Mert Akmese, Generating Richer Predicates for Decision Trees
• MT Summer 19: Tobias Winkler, Complexity of Multi Objective Stochastic Games (see publication [10])
• BT Winter 19/20: Mathias Jackermeier, dtControl: Decision Tree Learning for Explainable Controller Representation (see publication [7])
• BT Winter 19/20: Alexander Slivinskiy, Solving Simple Stochastic Games with Quadratic Programming (see publication [11] and [19])
• BT Summer 20: Christoph Weinhuber, Learning Domain-Specific Predicates in Decision Trees for Explainable Controller Representation (see publication [13])
• BT Summer 20: Arin Mirza, Bounded Value Iteration for Simple Stochastic Games with Infinite-Horizon Objectives
• BT Summer 21: Florian Jüngermann, Learning Algebraic Predicates for Explainable Controllers
• MT Winter 21/22: Alexander Slivinskiy, Facilitating Experimental Analysis of Algorithms for Stochastic Games: Random Model Generation and Mining the Results