59 citations · 458 across the 94 of their papers we have counts for
9 papers · 1 filter
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…
A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)
Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski +2
This paper presents a quantitative program verification infrastructure for discrete probabilistic programs. Our infrastructure can be viewed as the probabilistic analogue of Boogie…
Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen +2
We present an exact Bayesian inference method for inferring posterior distributions encoded by probabilistic programs featuring possibly unbounded loops. Our method is built on a d…
Search and Explore: Symbiotic Policy Synthesis in POMDPs
Roman Andriushchenko, Alexander Bork, Milan Češka +3
This paper marries two state-of-the-art controller synthesis methods for partially observable Markov decision processes (POMDPs), a prominent model in sequential decision making un…
Finding an -close Variation of Parameters in Bayesian Networks
Bahare Salmani, Joost-Pieter Katoen
This paper addresses the -close parameter tuning problem for Bayesian Networks (BNs): find a minimal -close amendment of probability entries in a given set of (rows in) condi…
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…
Lower Bounds for Possibly Divergent Probabilistic Programs
Shenghua Feng, Mingshuai Chen, Han Su +3
We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to almost-surely terminating programs -- as is the ca…
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…