10 citations · 36 across the 18 of their papers we have counts for
22 papers
Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops (Extended Version)
Darion Haase, Kevin Batz, Adrian Gallus +4
A fundamental computational task in probabilistic programming is to infer a program's output (posterior) distribution from a given initial (prior) distribution. This problem is cha…
Weighted Automata for Exact Inference in Discrete Probabilistic Programs
Dominik Geißler, Tobias Winkler
In probabilistic programming, the inference problem asks to determine a program's posterior distribution conditioned on its "observe" instructions. Inference is challenging, especi…
Verifying Sampling Algorithms via Distributional Invariants
Daniel Zilken, Kevin Batz, Joost-Pieter Katoen +1
This paper presents a Hoare-like veri cation framework for discrete probabilistic programs that we apply to two non-trivial sampling algorithms: Lumbroso's Fast Dice Roller and Saa…
Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Kevin Batz, Joost-Pieter Katoen, Francesca Randone +1
We lay out novel foundations for the computer-aided verification of guaranteed bounds on expected outcomes of imperative probabilistic programs featuring (i) general loops, (ii) co…
J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report)
Kevin Batz, Benjamin Lucien Kaminski, Christoph Matheja +1
Markov decision processes (MDPs) with rewards are a widespread and well-studied model for systems that make both probabilistic and nondeterministic choices. A fundamental result ab…
Markov Decision Processes with Sure Parity and Multiple Reachability Objectives
Raphaël Berthon, Joost-Pieter Katoen, Tobias Winkler
This paper considers the problem of finding strategies that satisfy a mixture of sure and threshold objectives in Markov decision processes. We focus on a single -regular object…
Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains
Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann +1
We study the accurate and efficient computation of the expected number of times each state is visited in discrete- and continuous-time Markov chains. To obtain sound accuracy guara…
Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen +1
We consider imperative programs that involve both randomization and pure nondeterminism. The central question is how to find a strategy resolving the pure nondeterminism such that…
On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata
Tobias Winkler, Joost-Pieter Katoen
Probabilistic pushdown automata (pPDA) are a natural operational model for a variety of recursive discrete stochastic processes. In this paper, we study certificates - succinct and…
Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration
Tobias Winkler, Joost-Pieter Katoen
Probabilistic pushdown automata (pPDA) are a standard model for discrete probabilistic programs with procedures and recursion. In pPDA, many quantitative properties are characteriz…
Exact Probabilistic Inference Using Generating Functions
Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen +1
Probabilistic programs are typically normal-looking programs describing posterior probability distributions. They intrinsically code up randomized algorithms and have long been at…
Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions
Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg +1
We study discrete probabilistic programs with potentially unbounded looping behaviors over an infinite state space. We present, to the best of our knowledge, the first decidability…
Weighted Programming
Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski +2
We study weighted programming, a programming paradigm for specifying mathematical models. More specifically, the weighted programs we investigate are like usual imperative programs…
Model Checking Temporal Properties of Recursive Probabilistic Programs
Tobias Winkler, Christina Gehnen, Joost-Pieter Katoen
Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices and recursive procedures. Temporal properties ar…
Stochastic Games with Disjunctions of Multiple Objectives
Tobias Winkler, Maximilian Weininger
Stochastic games combine controllable and adversarial non-determinism with stochastic behavior and are a common tool in control, verification and synthesis of reactive systems faci…
Stochastic Games with Disjunctions of Multiple Objectives (Technical Report)
Tobias Winkler, Maximilian Weininger
Stochastic games combine controllable and adversarial non-determinism with stochastic behavior and are a common tool in control, verification and synthesis of reactive systems faci…
Out of Control: Reducing Probabilistic Models by Control-State Elimination
Tobias Winkler, Johannes Lehmann, Joost-Pieter Katoen
State-of-the-art probabilistic model checkers perform verification on explicit-state Markov models defined in a high-level programming formalism like the PRISM modeling language. T…
The Complexity of Reachability in Parametric Markov Decision Processes
Sebastian Junges, Joost-Pieter Katoen, Guillermo A. Pérez +1
This article presents the complexity of reachability decision problems for parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where tran…
Generating Functions for Probabilistic Programs
Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski +3
This paper investigates the usage of generating functions (GFs) encoding measures over the program variables for reasoning about discrete probabilistic programs. To that end, we de…
Stochastic Games with Lexicographic Reachability-Safety Objectives
Krishnendu Chatterjee, Joost-Pieter Katoen, Maximilian Weininger +1
We study turn-based stochastic zero-sum games with lexicographic preferences over reachability and safety objectives. Stochastic games are standard models in control, verification,…
On the Complexity of Reachability in Parametric Markov Decision Processes
Tobias Winkler, Sebastian Junges, Guillermo A. Pérez +1
This paper studies parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where transitions probabilities are described by polynomials over…
Alternating Weak Automata from Universal Trees
Laure Daviaud, Marcin Jurdziński, Karoliina Lehtinen
An improved translation from alternating parity automata on infinite words to alternating weak automata is given. The blow-up of the number of states is related to the size of the…