Tobias Winkler

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

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

Research

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

  • Probabilistic Model Checking, in particular stochastic games and probabilistic push-down systems
  • Parametric Probabilistic Models, that is, models that are not fully specified but depend on some parameters
  • Probabilistic Programs, in particular invariant-based and other rule-based approaches

I supervise our student assistants Johannes Lehmann, Christina Gehnen and Adrian Gallus (together with Kevin Batz and Benjamin Kaminski).

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 check our list of open topics. I am currently supervising or have supervised the following thesis projects:

Ongoing thesis projects

  • Compositional Control-Flow Reduction for Probabilistic Model Checking – Leon Barth, Bachelor’s thesis.
  • Implementation of an LTL Model Checker for Probabilistic Push-Down Automata – Laura Bamberger, Bachelor’s thesis.

Past thesis projects

  • Automata-based Model Checking of Recursive Systems – Christina Gehnen, Bachelor’s thesis. 2020.
    Christina has received an award from the Fachgruppe Informatik for her thesis.

Teaching

Current semester

Past semesters

Awards

  • Our paper Generating Functions for Probabilistic Programs (joint work with Kevin Batz, Lutz Klinkenberg, Benjamin Lucien Kaminski, Joost-Pieter Katoen and Joshua Moerman) has received the best paper award at LOPSTR 2020.
  • I was awarded the Springorum Medal in 2020 for receiving a master’s degree with distinction.

Peer Review

Journals

Conferences

Publications

You can also find me on dblp.

2021
fulltext PDF [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},
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, 30th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR2020), 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.
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, 32nd 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, 35th 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
Show all