Publications

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 = {Theoretical Computer Science and General Issues},
volume = {13182},
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, 23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI22), Volume 13182 of Theoretical Computer Science and General Issues, 450-472, Springer, 2022.
2021
DOI [bibtex]
@article{PDCD2021,
title = {Probabilistic Data with Continuous Distributions},
author = {Martin Grohe and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Peter Lindner},
publisher = {ACM},
journal = {ACM SIGMOD record},
volume = {50(1)},
pages = {pages 69-76},
type = {Journal Article},
year = {2021},
doi = {10.1145/3471485.3471502},
url = { https://publications.rwth-aachen.de/record/820984},
}×
[issue] 		Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Peter Lindner. Probabilistic Data with Continuous Distributions, ACM SIGMOD record 50 (1), pages 69-76, ACM, 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 fulltext PDF [bibtex]
@article{D2021,
title = {Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings},
author = {Erika Ábrahám and James H. Davenport and Matthew England and Gereon Kremer},
publisher = {Elsevier Science},
journal = {Journal of Logical and Algebraic Methods in Programming},
volume = {119},
pages = {pages 100633},
type = {Journal Article},
year = {2021},
doi = {10.1016/j.jlamp.2020.100633},
url = { https://publications.rwth-aachen.de/record/816049},
}×
[issue] 		Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer. Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings, Journal of Logical and Algebraic Methods in Programming 119, pages 100633, Elsevier Science, 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 fulltext PDF [bibtex]
@article{R2021,
title = {Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {5},
pages = {pages 39},
type = {Journal Article},
year = {2021},
doi = {10.1145/3434320},
url = { https://publications.rwth-aachen.de/record/816245},
}×
[issue] 		Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning, Proceedings of the ACM on programming languages 5, pages 39, ACM, 2021.
DOI [bibtex]
@article{M2021,
title = {Markov automata with multiple objectives},
author = {Tim Quatmann and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
journal = {Formal methods in system design},
type = {Journal Article},
year = {2021},
doi = {10.1007/s10703-021-00364-6},
url = { https://publications.rwth-aachen.de/record/816671},
}×
[issue] 		Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen. Markov automata with multiple objectives, Formal methods in system design, Springer, 2021.
DOI arXiv:2104.02438 fulltext PDF [bibtex]
@unpublished{OFDVSWRA2021,
title = {Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata},
author = {Mikołaj Bojańczyk and Bartek Klin and Joshua Moerman},
pages = {16 Seiten},
type = {Preprint},
year = {2021},
doi = {10.18154/RWTH-2021-03671},
url = { https://arxiv.org/abs/2104.02438},
}×
[issue] 		Mikołaj Bojańczyk, Bartek Klin, Joshua Moerman. Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata, 16 Seiten, 2021. https://arxiv.org/abs/2104.02438
DOI fulltext PDF [bibtex]
@conference{MOLATR2021,
title = {Multi-objective Optimization of Long-run Average and Total Rewards},
author = {Tim Quatmann and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12651},
pages = {230-249},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-72016-2_13},
url = { https://publications.rwth-aachen.de/record/817768},
}×
[issue] 		Tim Quatmann, Joost-Pieter Katoen. Multi-objective Optimization of Long-run Average and Total Rewards, 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021), Volume 12651 of LNCS, 230-249, Springer, 2021.
DOI fulltext PDF [bibtex]
@conference{FPOMC2021,
title = {Finding Provably Optimal Markov Chains},
author = {Jip Josephine Spel and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12651},
pages = {173-190},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-72016-2_10},
url = { https://publications.rwth-aachen.de/record/818128},
}×
[issue] 		Jip Josephine Spel, Sebastian Junges, Joost-Pieter Katoen. Finding Provably Optimal Markov Chains, 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021), Volume 12651 of LNCS, 173-190, Springer, 2021.
DOI fulltext PDF [bibtex]
@article{A2021,
title = {A pre-expectation calculus for probabilistic sensitivity},
author = {Alejandro Aguirre and Gilles Barthe and Justin Hsu and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Association for Computing Machinery},
journal = {Proceedings of the ACM on programming languages},
volume = {5(POPL)},
pages = {pages 52},
type = {Journal Article},
year = {2021},
doi = {10.1145/3434333},
url = { https://publications.rwth-aachen.de/record/819375},
}×
[issue] 		Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. A pre-expectation calculus for probabilistic sensitivity, Proceedings of the ACM on programming languages 5 (POPL), pages 52, Association for Computing Machinery, 2021.
DOI [bibtex]
@article{C2021,
title = {Counterexample-guided inductive synthesis for probabilistic systems},
author = {Milan Češka and Hans Christian Hensel and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
journal = {Formal aspects of computing},
volume = {33(4/5)},
pages = {pages 637-667},
type = {Journal Article},
year = {2021},
doi = {10.1007/s00165-021-00547-2},
url = { https://publications.rwth-aachen.de/record/820111},
}×
[issue] 		Milan Češka, Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen. Counterexample-guided inductive synthesis for probabilistic systems, Formal aspects of computing 33 (4/5), pages 637-667, Springer, 2021.
DOI [bibtex]
@conference{ACCBCHRG2021,
title = {Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars},
author = {Ira Justus Fesefeldt and Christoph Matheja and Thomas Noll and Johannes Schulte},
publisher = {Springer},
booktitle = {LNCS},
volume = {12741},
pages = {283-293},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-78946-6_15},
url = { https://publications.rwth-aachen.de/record/820755},
}×
[issue] 		Ira Justus Fesefeldt, Christoph Matheja, Thomas Noll, Johannes Schulte. Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars, 14th International Conference on Graph Transformation (ICGT21), Volume 12741 of LNCS, 283-293, Springer, 2021.
DOI fulltext PDF [bibtex]
@book{F2021,
title = {Foundations of probabilistic programming},
author = {},
editor = {Gilles Barthe and Joost-Pieter Katoen and Alexandra Silva},
publisher = {Cambridge University Press},
pages = {xiv, 568 Seiten : Illustrationen},
type = {Book},
year = {2021},
doi = {10.1017/9781108770750},
url = { https://publications.rwth-aachen.de/record/814578},
}×
[issue] 		Gilles Barthe (ed), Joost-Pieter Katoen (ed), Alexandra Silva (ed). Foundations of probabilistic programming, xiv, 568 Seiten : Illustrationen, Cambridge University Press, 2021.
DOI fulltext PDF [bibtex]
@article{TS2021,
title = {The probabilistic model checker STORM},
author = {Hans Christian Hensel and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann and Matthias Volk},
publisher = {Springer},
journal = {International journal on software tools for technology transfer},
pages = {22 Seiten},
type = {Journal Article},
year = {2021},
doi = {10.1007/s10009-021-00633-z},
url = { https://publications.rwth-aachen.de/record/822059},
}×
[issue] 		Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk. The probabilistic model checker STORM, International journal on software tools for technology transfer, 22 Seiten, Springer, 2021.
DOI [bibtex]
@conference{OCPPQVQCR2021,
title = {On Correctness, Precision, and Performance in Quantitative Verification: QComp 2020 Competition Report},
author = {Carlos E. Budde and Arnd Hartmanns and Michaela Klauck and Jan Křetínský and David Parker and Tim Quatmann and Andrea Turrini and Zhen Zhang},
publisher = {Springer},
booktitle = {LNCS},
volume = {12479},
pages = {216-241},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-83723-5_15},
url = { https://publications.rwth-aachen.de/record/834796},
}×
[issue] 		Carlos E. Budde, Arnd Hartmanns, Michaela Klauck, Jan Křetínský, David Parker, Tim Quatmann, Andrea Turrini, Zhen Zhang. On Correctness, Precision, and Performance in Quantitative Verification: QComp 2020 Competition Report, 9th International Symposium on Leveraging Applications of Formal Methods (ISoLA 2020), Volume 12479 of LNCS, 216-241, Springer, 2021.
DOI [bibtex]
@conference{ADPP2021,
title = {A Debugger for Probabilistic Programs},
author = {Alexander Hoppen and Thomas Noll},
booktitle = {LNCS},
volume = {13085},
pages = {282-289},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-92124-8_16},
url = { https://publications.rwth-aachen.de/record/836481},
}×
[issue] 		Alexander Hoppen, Thomas Noll. A Debugger for Probabilistic Programs, International Conference on Software Engineering and Formal Methods (SEFM 2021), Volume 13085 of LNCS, 282-289, 2021.
DOI fulltext PDF [bibtex]
@conference{SIBCDCP2021,
title = {Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming},
author = {Qiuye Wang and Mingshuai Chen and Bai Xue and Naijun Zhan and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12759, Theoretical Computer Science and General Issues},
pages = {443-466},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-81685-8_21},
url = { https://publications.rwth-aachen.de/record/822586},
}×
[issue] 		Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen. Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming, 33rd International Conference on Computer-Aided Verification (CAV 2021), Volume 12759, Theoretical Computer Science and General Issues of LNCS, 443-466, Springer, 2021.
DOI [bibtex]
@conference{AMANDFT2021,
title = {A Modular Approach to Non-deterministic Dynamic Fault Trees},
author = {Sascha Müller and Adeline Jordon and Andreas Gerndt and Thomas Noll},
publisher = {Springer},
booktitle = {Programming and Software Engineering},
volume = {12852},
pages = {243-257},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-83903-1_16},
url = { https://publications.rwth-aachen.de/record/835216},
}×
[issue] 		Sascha Müller, Adeline Jordon, Andreas Gerndt, Thomas Noll. A Modular Approach to Non-deterministic Dynamic Fault Trees, 40th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2021), Volume 12852 of Programming and Software Engineering, 243-257, Springer, 2021.
DOI fulltext PDF [bibtex]
@article{S2021,
title = {Synthesizing optimal bias in randomized self-stabilization},
author = {Matthias Volk and Borzoo Bonakdarpour and Joost-Pieter Katoen and Saba Aflaki},
publisher = {Springer},
journal = {Distributed computing},
pages = {21 Seiten},
type = {Journal Article},
year = {2021},
doi = {10.1007/s00446-021-00408-4},
url = { https://publications.rwth-aachen.de/record/835189},
}×
[issue] 		Matthias Volk, Borzoo Bonakdarpour, Joost-Pieter Katoen, Saba Aflaki. Synthesizing optimal bias in randomized self-stabilization, Distributed computing, 21 Seiten, Springer, 2021.
DOI [bibtex]
@conference{ASMPMCUG2021,
title = {Accelerating SpMV Multiplication in Probabilistic Model Checkers Using GPUs},
author = {Muhammad Hannan Khan and Osman Hassan and Shahid Khan},
publisher = {Springer},
booktitle = {LNCS},
volume = {12819},
pages = {86-104},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-85315-0_6},
url = { https://publications.rwth-aachen.de/record/835153},
}×
[issue] 		Muhammad Hannan Khan, Osman Hassan, Shahid Khan. Accelerating SpMV Multiplication in Probabilistic Model Checkers Using GPUs, 18th International Colloquium on Theoretical Aspects of Computing (ICTAC 2021), Volume 12819 of LNCS, 86-104, Springer, 2021.
DOI [bibtex]
@conference{MCMFLF2021,
title = {Model Checking the Multi-Formalism Language FIGARO},
author = {Shahid Khan and Matthias Volk and Joost-Pieter Katoen and Alexis Braibant and Marc Bouissou},
publisher = {IEEE},
pages = {463-470},
type = {Conference Paper},
year = {2021},
doi = {10.1109/DSN48987.2021.00056},
url = { https://publications.rwth-aachen.de/record/835145},
}×
[issue] 		Shahid Khan, Matthias Volk, Joost-Pieter Katoen, Alexis Braibant, Marc Bouissou. Model Checking the Multi-Formalism Language FIGARO, 2021 51st Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), 463-470, IEEE, 2021.
DOI fulltext PDF [bibtex]
@conference{PATISPP2021,
title = {PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs},
author = {Roman Andriushchenko and Milan Češka and Sebastian Junges and Joost-Pieter Katoen and Šimon Stupinský},
publisher = {Springer},
booktitle = {LNCS},
volume = {12759, Theoretical Computer Science and General Issues},
pages = {856-869},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-81685-8_40},
url = { https://publications.rwth-aachen.de/record/834351},
}×
[issue] 		Roman Andriushchenko, Milan Češka, Sebastian Junges, Joost-Pieter Katoen, Šimon Stupinský. PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs, 33rd International Conference on Computer-Aided Verification (CAV 2021), Volume 12759, Theoretical Computer Science and General Issues of LNCS, 856-869, Springer, 2021.
DOI [bibtex]
@conference{TOPTA2021,
title = {Tweaking the Odds in Probabilistic Timed Automata},
author = {Arnd Hartmanns and Joost-Pieter Katoen and Bram Kohlen and Jip Josephine Spel},
publisher = {Springer},
booktitle = {LNCS},
volume = {12846},
pages = {39-58},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-85172-9_3},
url = { https://publications.rwth-aachen.de/record/828609},
}×
[issue] 		Arnd Hartmanns, Joost-Pieter Katoen, Bram Kohlen, Jip Josephine Spel. Tweaking the Odds in Probabilistic Timed Automata, 18th International Conference on Quantitative Evaluation of Systems (QEST 2021), Volume 12846 of LNCS, 39-58, Springer, 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, 12th International Symposium on Games, Automata, Logics and Formal Verification (GandALF), Volume 346 of EPTCS, 85-100, NICTA, 2021.
DOI fulltext PDF [bibtex]
@conference{LIAPP2021,
title = {Latticed $k$-Induction with an Application to Probabilistic Programs},
author = {Kevin Batz and Mingshuai Chen and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schröer},
publisher = {Springer},
booktitle = {LNCS},
volume = {12760},
pages = {524-549},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-81688-9_25},
url = { https://publications.rwth-aachen.de/record/822587},
}×
[issue] 		Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer. Latticed $k$-Induction with an Application to Probabilistic Programs, 33rd International Conference on Computer-Aided Verification (CAV 2021), Volume 12760 of LNCS, 524-549, Springer, 2021.
Show all