Biography

I am an assistant lecturer at the Lancaster University Leipzig (LUL).

I was an (interim) associate professor at the Technical University Munich (TUM) at the Campus Heilbronn during the summer semester 2023. Before that, I was Post-Doc at the Institute of Science and Technology Austria (ISTA) / Chatterjee group (2022-2023). I defended my PhD (with distinction) at the Technical University Munich (TUM) under Jan Křetínský (2017-2022). I obtained Masters’ degrees in Math and Computer Science at TUM (both with distinction).

Research

My main research interest is the formal verification of (finite state) probabilistic systems. Currently, I particularly seek to establish a broader recognition for notions of risk in such systems and usage of risk-aware verification.

Aside from that, I contribute to LTL-to-automaton translation, machine learning in verification, complexity theory, and game theory (bidding games & multi agent systems).

Selected Honors, Grants, Awards

Dagstuhl invitation counter: 4

Selected Publications

Authors sorted alphabetically. Click for a complete list.

Learning Algorithms for Verification of Markov Decision Processes
Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Křetínský, Marta Kwiatkowska, Tobias Meggendorfer, David Parker, and Mateusz Ujma
TheoretiCS 2025
DOI Preprint BibTeX
Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives
Jan Křetínský, Tobias Meggendorfer, and Maximilian Weininger
LICS 2023
DOI Preprint Poster Slides Video Website BibTeX
Faster Algorithm for Turn-based Stochastic Games with Bounded Treewidth
Krishnendu Chatterjee, Tobias Meggendorfer, Raimundo Saona, and Jakub Svoboda
SODA 2023
DOI BibTeX
Risk-Aware Stochastic Shortest Path
Tobias Meggendorfer
AAAI 2022
DOI Preprint Artefact Poster BibTeX
Owl: A Library for ω-Words, Automata, and LTL
Jan Křetínský, Tobias Meggendorfer, and Salomon Sickert
ATVA 2018
DOI GitHub Website BibTeX

Selected Service

Reviews:

  • PC (co-)chair: QEST+FORMATS AE 2024
  • PC member: AAAI (2023, 2024, 2025, 2026), ATVA (2024, 2026), ATVAART (2019), CAV AEC (2022, 2023, 2024), HSCC (2025), HSCC RE (2021, 2022, 2023, 2024, 2025), QEST+FORMATS (2026), RADICAL (2025), TACAS AE (2018, 2019, 2020), PLDI AEC (2023), RADICAL (2025), RP (2024)
  • (Sub)reviewer (selection): CDC, FoSSaCS, ICALP, LICS, MFCS, VMCAI
  • Journals (selection): JACM, TCS, STTT, FMSD, IEEE TSE
  • Grant agencies: Czech Science Foundation (CZF) (2 reviews)
  • Reviewer for AMS MathSciNet (9 reviews)
  • In total: ~90 reviews so far

Other:

Teaching

  • Developing DOMtutor: A generic library to utilize DOMjudge for teaching (presented at FOMEO’22).
  • Designed complete lecture on practical implementation of classical algorithms and data structures using DOMtutor
  • Lectured 6 distinct lectures, 8 times TA, >400h contact time as lecturer
  • Supervised 3 MSc, 4 BSc Theses, resulting in two papers

Tools & Libraries

Implementations I am involved in. An asterisk indicates main/sole developer role.

  • owl: A library for ω-words, automata, and LTL; state-of-the-art tool for LTL to automaton translations and reactive synthesis (paired with Strix and SemML below). Homepage and publication.
  • Rabinizer 4.0 (*): A tool-set to produce small automata from LTL formulae. Part of Owl. Homepage and publication.
  • SemML: Semantic Machine Learning for LTL reactive synthesis. Use ML guidance to improve synthesis. Based on Owl. Winner of SYNTCOMP 2024 LTL Realizability Track.
  • PET (*): A tool-set to efficiently analyse probabilistic systems using guided sampling. GitLab and publication (previous).
  • probabilistic-models (*): A generic, high-performance library to work with finite state probabilistic systems (e.g. Markov decision processes). GitLab.
  • JBDD (*): A pure-Java, high-performance implementation of (reduced, ordered) binary decision diagrams (ROBDD). GitHub.
  • naturals-util (*): A Java library of several utilities for efficiently working with natural numbers (e.g. wrappers for RoaringBitmap). GitHub.
  • DOMtutor (*): A library automating interaction with DOMjudge. Homepage and GitHub.

Practical Experience

  • Significant contributions to open-source projects, including RoaringBitmap, fastutil, and benchexec
  • (Co-)Developer of several major scientific tools and libraries (see above)
  • ~3yr FTE at an SMB as CTO, full stack developer for Java (Vaadin, Spring, Hibernate), and embedded systems developer (Raspberry Pi, busybox / buildroot, RAUC, Arduino), project lead for 1-3 developers

Other Interests

  • System administration
  • (Low-level) hardware engineering (embedded systems, PCB design, soldering, 3D printing)
  • Board Games (Go, Scythe, Root, Nemesis, …)
  • Digital Games (Baba Is You, Hollow Knight, Pyre, Factorio, Subnautica, …)
  • Martial Arts (Black Belt)
  • Home theatre / acoustics
  • Logic Puzzles (email me if you want to verify your solution idea)