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:

• ISoLA 2020 (postponed to October 21) presenting our paper “Statistical Model Checking: Black or White?” (publication [12]).

Publications

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

Other

[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 paper or QComp 2020 Competition).
• 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

• 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

• TACAS 2020 Artifact Evaluation Committee

• TACAS 2019 Artifact Evaluation Committee

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

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

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])
• BT Summer 20: Christoph Weinhuber, Learning Domain-Specific Predicates in Decision Trees for Explainable Controller Representation
• BT Summer 20: Arin Mirza, Bounded Value Iteration for Simple Stochastic Games with Infinite-Horizon Objectives