Abstract: Probabilistic pushdown automata (pPDA) are a standard model for discrete probabilistic programs with procedures and recursion. In pPDA, many quantitative properties are characterized as least fixpoints (LFP) of polynomial equation systems. This includes in particular termination probabilities and expected runtimes. In this talk, I consider the problem of synthesizing certificates —i.e. succinct and easily verifiable proofs— that these quantities lie within certain bounds. To this end, I first characterize the polynomial systems that admit easy-to-check certificates in form of inductive rational-valued upper bounds on their LFP. Second, I present a sound and complete Optimistic Value Iteration algorithm for computing such certificates. Third, I explain how certificates for polynomial systems can be transferred to certificates for various quantitative pPDA properties. Finally, I present some experiments demonstrating that the algorithm computes certificates for several intricate example programs as well as stochastic context-free grammars with >10^4 production rules.

Short Bio: Tobias is a PhD student in the Software Modeling and Verification Group at RWTH Aachen University, Germany. He started his PhD in 2020 under the supervision of Joost-Pieter Katoen. Tobias’ research focuses on the automatic formal verification of probabilistic programs. His speciality are programs featuring recursive function calls and the corresponding abstract models such as pushdown automata. Tobias participates in the EU-funded MISSION project, a shared research effort between several European and Argentinian partners focussing on the application of model-based software tools in the space domain.

--

Comunicaciones DCC