59 citations · 172 across the 59 of their papers we have counts for
4 papers · 1 filter
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…
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…
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…