Tobias Winkler

Email
tobias.winkler at cs.rwth-aachen.de
Address
Room 4231
Ahornstraße 55
D-52074 Aachen

I am a doctoral researcher and PhD candidate in the Software Modeling and Verification Group headed by Professor Joost-Pieter Katoen. Moreover, I am associated with the research training group UnRAVel.

Research

My research focuses on automatic formal verification of discrete probabilistic systems, both from a theoretical and practical point of view. More specifically, my research interests include:

  • Probabilistic Model Checking: Probabilistic Pushdown Automata, Markov Decision Processes, Stochastic Games, Multi-Objectives, Temporal Logics, Certificates
  • Quantitative Program Analysis: Probabilistic Programs, Weighted Programs, Semi-automatic Loop Verification, Strategy Synthesis, Termination Analysis
  • Tool Support for the topics listed above.

I am currently supervising our UnRAVeL research student assistant Samuel Rode. In the past, I have supervised our research student assistants Johannes Lehmann, Christina Gehnen, Adrian Gallus, Tom Biskup, and our DAAD RISE intern Arman Ozcan.

Thesis projects

If you are interested in writing a Bachelor/Master’s thesis in any of the areas mentioned above, don’t hesitate to contact me. You can also contact thesis at i2.informatik.rwth-aachen.de for a general request. I am currently supervising or have supervised the following thesis projects:

Ongoing thesis projects

  • An Automata-based Semantics for the Probabilistic ReDiP Language (working title) – Master’s thesis.

Past thesis projects

Teaching

Current semester

Past semesters

Awards

Peer Review

Journals

Conferences & Workshops

  • IJCAR 2024 (external reviewer)
  • CAV 2024 (PC member Artifact Evaluation / external reviewer)
  • AAMAS 2024 (external reviewer)
  • SODA 2024 (external reviewer)
  • MFCS 2023 (external reviewer)
  • ATVA 2023 (external reviewer)
  • SYNT 2023 @CAV 2023 (PC member)
  • POPL 2023 (external reviewer)
  • ICTAC 2022 (external reviewer)
  • CONCUR 2022 (external reviewer)
  • ICALP 2022 (external reviewer)
  • LICS 2022 (external reviewer)
  • CAV 2022 (PC member Artifact Evaluation / external reviewer)
  • POPL 2022 (external reviewer)
  • CONCUR 2021 (external reviewer)
  • CAV 2021 (PC member Artifact Evaluation / external reviewer)
  • FoSSaCS 2021 (external reviewer)

Selected Talks

Publications

You can also find me on dblp and Google Scholar.

2024
DOI fulltext PDF [bibtex]
@article{PSSRNPP2024,
title = {Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs},
author = {Kevin Batz and Tom Jannik Biskup and Joost-Pieter Katoen and Tobias Winkler},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {8},
pages = {pages 93},
type = {Journal Article},
year = {2024},
doi = {10.1145/3632935},
url = { https://publications.rwth-aachen.de/record/979194},
}×
[issue]
Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen, Tobias Winkler. Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs, Proceedings of the ACM on programming languages 8, pages 93, ACM, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{C2024,
title = {Complexity and decidability of multi-objective stochastic games},
author = {Tobias Winkler},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen},
type = {Master Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-02592},
url = { https://publications.rwth-aachen.de/record/980848},
}×
[issue]
Tobias Winkler. Complexity and decidability of multi-objective stochastic games, Master Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@conference{ACEVTSDMC2024,
title = {Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains},
author = {Hannah Mertens and Joost-Pieter Katoen and Tim Quatmann and Tobias Winkler},
publisher = {Springer},
booktitle = {LNCS},
volume = {14571},
pages = {237-257},
type = {Conference Paper},
year = {2024},
doi = {10.1007/978-3-031-57249-4_12},
url = { https://publications.rwth-aachen.de/record/990356},
}×
[issue]
Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, Tobias Winkler. Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains, 30. International Conference TACAS (TACAS 2024), Volume 14571 of LNCS, 237-257, Springer, 2024.
2023
DOI arXiv:2302.00513 fulltext PDF [bibtex]
@unpublished{EPIUGF2023,
title = {Exact Probabilistic Inference Using Generating Functions},
author = {Lutz Klinkenberg and Tobias Winkler and Mingshuai Chen and Joost-Pieter Katoen},
pages = {3 Seiten},
type = {Preprint},
year = {2023},
doi = {10.48550/arXiv.2302.00513},
url = { https://arxiv.org/abs/2302.00513},
}×
[issue]
Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen. Exact Probabilistic Inference Using Generating Functions, 3 Seiten, 2023. https://arxiv.org/abs/2302.00513
DOI fulltext PDF [bibtex]
@article{S2023,
title = {Stochastic games with lexicographic objectives},
author = {Krishnendu Chatterjee and Joost-Pieter Katoen and Stefanie Mohr and Maximilian Weininger and Tobias Winkler},
publisher = {Springer},
journal = {Formal methods in system design},
pages = {41 Seiten},
type = {Journal Article},
year = {2023},
doi = {10.1007/s10703-023-00411-4},
url = { https://publications.rwth-aachen.de/record/954240},
}×
[issue]
Krishnendu Chatterjee, Joost-Pieter Katoen, Stefanie Mohr, Maximilian Weininger, Tobias Winkler. Stochastic games with lexicographic objectives, Formal methods in system design, 41 Seiten, Springer, 2023.
DOI fulltext PDF [bibtex]
@conference{CPPAOVI2023,
title = {Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration},
author = {Tobias Winkler and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {13994},
pages = {391-409},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-30820-8_24},
url = { https://publications.rwth-aachen.de/record/972636},
}×
[issue]
Tobias Winkler, Joost-Pieter Katoen. Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration, 29. International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Volume 13994 of LNCS, 391-409, Springer, 2023.
DOI [bibtex]
@conference{OCERTPPA2023,
title = {On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata},
author = {Tobias Winkler and Joost-Pieter Katoen},
publisher = {IEEE},
pages = {13 Seiten},
type = {Conference Paper},
year = {2023},
doi = {10.1109/LICS56636.2023.10175714},
url = { https://publications.rwth-aachen.de/record/972664},
}×
[issue]
Tobias Winkler, Joost-Pieter Katoen. On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata, 38. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2023), 13 Seiten, IEEE, 2023.
DOI fulltext PDF [bibtex]
@article{MCTPRPP2023,
title = {Model Checking Temporal Properties of Recursive Probabilistic Programs},
author = {Tobias Winkler and Christina Gehnen and Joost-Pieter Katoen},
publisher = {Department of Theoretical Computer Science, Technical University of Braunschweig},
journal = {Logical methods in computer science},
volume = {19(4)},
pages = {pages 24},
type = {Journal Article},
year = {2023},
doi = {10.46298/lmcs-19(4:24)2023},
url = { https://publications.rwth-aachen.de/record/976967},
}×
[issue]
Tobias Winkler, Christina Gehnen, Joost-Pieter Katoen. Model Checking Temporal Properties of Recursive Probabilistic Programs, Logical methods in computer science 19 (4), pages 24, Department of Theoretical Computer Science, Technical University of Braunschweig, 2023.
2022
DOI [bibtex]
@conference{OCRPMCSE2022,
title = {Out of Control: Reducing Probabilistic Models by Control-State Elimination},
author = {Tobias Winkler and Johannes Lehmann and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {13182, Theoretical Computer Science and General Issues},
pages = {450-472},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-030-94583-1_22},
url = { https://publications.rwth-aachen.de/record/838775},
}×
[issue]
Tobias Winkler, Johannes Lehmann, Joost-Pieter Katoen. Out of Control: Reducing Probabilistic Models by Control-State Elimination, 23. International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2022), Volume 13182, Theoretical Computer Science and General Issues of LNCS, 450-472, Springer, 2022.
DOI fulltext PDF [bibtex]
@conference{MCTPRPP2022,
title = {Model Checking Temporal Properties of Recursive Probabilistic Programs},
author = {Tobias Winkler and Christina Gehnen and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {13242},
pages = {449-469},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-030-99253-8_23},
url = { https://publications.rwth-aachen.de/record/843600},
}×
[issue]
Tobias Winkler, Christina Gehnen, Joost-Pieter Katoen. Model Checking Temporal Properties of Recursive Probabilistic Programs, Foundations of Software Science and Computation Structures : 25. International Conference (FOSSACS 2022), Volume 13242 of LNCS, 449-469, Springer, 2022.
DOI fulltext PDF [bibtex]
@article{W2022,
title = {Weighted programming: a programming paradigm for specifying mathematical models},
author = {Kevin Batz and Adrian Gallus and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Tobias Winkler},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
pages = {pages 66},
type = {Journal Article},
year = {2022},
doi = {10.1145/3527310},
url = { https://publications.rwth-aachen.de/record/845157},
}×
[issue]
Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Tobias Winkler. Weighted programming: a programming paradigm for specifying mathematical models, Proceedings of the ACM on programming languages, pages 66, ACM, 2022.
DOI fulltext PDF [bibtex]
@conference{DPYRDVPPGF2022,
title = {Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions},
author = {Mingshuai Chen and Joost-Pieter Katoen and Lutz Klinkenberg and Tobias Winkler},
publisher = {Springer},
booktitle = {LNCS},
volume = {13371},
pages = {79-101},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-031-13185-1_5},
url = { https://publications.rwth-aachen.de/record/848175},
}×
[issue]
Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler. Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions, 34. International Conference on Computer Aided Verification (CAV 2022), Volume 13371 of LNCS, 79-101, Springer, 2022.
2021
DOI [bibtex]
@conference{GFPP2021,
title = {Generating Functions for Probabilistic Programs},
author = {Lutz Klinkenberg and Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Joshua Moerman and Tobias Winkler},
publisher = {Springer},
booktitle = {Theoretical Computer Science and General Issues},
volume = {12561},
pages = {231-248},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-68446-4_12},
url = { https://publications.rwth-aachen.de/record/807881},
}×
[issue]
Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler. Generating Functions for Probabilistic Programs, 30. International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2020), Volume 12561 of Theoretical Computer Science and General Issues, 231-248, Springer, 2021.
DOI [bibtex]
@article{TM2021,
title = {The complexity of reachability in parametric Markov decision processes},
author = {Sebastian Junges and Joost-Pieter Katoen and Guillermo A. Pérez and Tobias Winkler},
publisher = {Elsevier},
journal = {Journal of computer and system sciences},
volume = {119},
pages = {pages 183-210},
type = {Journal Article},
year = {2021},
doi = {10.1016/j.jcss.2021.02.006},
url = { https://publications.rwth-aachen.de/record/816179},
}×
[issue]
Sebastian Junges, Joost-Pieter Katoen, Guillermo A. Pérez, Tobias Winkler. The complexity of reachability in parametric Markov decision processes, Journal of computer and system sciences 119, pages 183-210, Elsevier, 2021.
DOI arXiv:2109.08317 fulltext PDF [bibtex]
@conference{SGDMO2021,
title = {Stochastic Games with Disjunctions of Multiple Objectives},
author = {Tobias Winkler and Maximilian Weininger},
publisher = {NICTA},
booktitle = {EPTCS},
volume = {346},
pages = {85-100},
type = {Conference Paper},
year = {2021},
doi = {10.4204/EPTCS.346.6},
url = { https://arxiv.org/abs/2109.08317},
}×
[issue]
Tobias Winkler, Maximilian Weininger. Stochastic Games with Disjunctions of Multiple Objectives, 12. International Symposium on Games, Automata, Logics and Formal Verification (GandALF), Volume 346 of EPTCS, 85-100, NICTA, 2021.
2020
DOI fulltext PDF [bibtex]
@conference{SGLRSO2020,
title = {Stochastic Games with Lexicographic Reachability-Safety Objectives},
author = {Krishnendu Chatterjee and Joost-Pieter Katoen and Maximilian Weininger and Tobias Winkler},
publisher = {Springer},
booktitle = {LNCS},
volume = {12225},
pages = {398-420},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-53291-8_21},
url = { https://publications.rwth-aachen.de/record/795010},
}×
[issue]
Krishnendu Chatterjee, Joost-Pieter Katoen, Maximilian Weininger, Tobias Winkler. Stochastic Games with Lexicographic Reachability-Safety Objectives, 32. International Conference on Computer Aided Verification (CAV 2020), Volume 12225 of LNCS, 398-420, Springer, 2020.
DOI [bibtex]
@conference{AVGRSG2020,
title = {Approximating Values of Generalized-Reachability Stochastic Games},
author = {Pranav Ashok and Krishnendu Chatterjee and Jan Křetínský and Maximilian Weininger and Tobias Winkler},
publisher = {Association for Computing Machinery},
booktitle = {ACM conferences},
pages = {102-115},
type = {Conference Paper},
year = {2020},
doi = {10.1145/3373718.3394761},
url = { https://publications.rwth-aachen.de/record/795011},
}×
[issue]
Pranav Ashok, Krishnendu Chatterjee, Jan Křetínský, Maximilian Weininger, Tobias Winkler. Approximating Values of Generalized-Reachability Stochastic Games, 35. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '20), ACM conferences, 102-115, Association for Computing Machinery, 2020.
arXiv:2007.06327 [bibtex]
@unpublished{GFPP2020,
title = {Generating Functions for Probabilistic Programs},
author = {Lutz Klinkenberg and Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Joshua Moerman and Tobias Winkler},
type = {Preprint},
year = {2020},
url = { https://arxiv.org/abs/2007.06327},
}×
[issue]
Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler. Generating Functions for Probabilistic Programs, 2020. https://arxiv.org/abs/2007.06327
2019
DOI fulltext PDF [bibtex]
@conference{OCRPMDP2019,
title = {On the Complexity of Reachability in Parametric Markov Decision Processes},
author = {Tobias Winkler and Sebastian Junges and Guillermo A. Pérez and Joost-Pieter Katoen},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, August},
booktitle = {Leibniz international proceedings in informatics : LIPIcs},
volume = {140},
type = {Conference Paper},
year = {2019},
doi = {10.4230/LIPICS.CONCUR.2019.14},
url = { https://publications.rwth-aachen.de/record/780394},
}×
[issue]
Tobias Winkler, Sebastian Junges, Guillermo A. Pérez, Joost-Pieter Katoen. On the Complexity of Reachability in Parametric Markov Decision Processes, 30. International Conference on Concurrency Theory (CONCUR), Volume 140 of Leibniz international proceedings in informatics : LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, August, 2019.