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.

Upcoming presentations

You can meet me at the following upcoming conferences:


Probabilistic model checking and controller synthesis for stochastic games

[12] Ashok, 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

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


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


Past Presentations

Community Service