Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration

TL;DR

This paper introduces a method to certify bounds on probabilistic pushdown automata properties by characterizing polynomial systems and providing an algorithm for computing certificates, validated through experiments on complex programs.

Contribution

It presents a novel characterization of polynomial systems for certifiable bounds and an optimistic value iteration algorithm for certificate computation in pPDA.

Findings

Algorithm computes succinct certificates for complex programs.

Certificates transfer from polynomial systems to pPDA properties.

Effective on stochastic context-free grammars with over 10,000 rules.

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 of polynomial equation systems. In this paper, we study the problem of certifying that these quantities lie within certain bounds. To this end, we first characterize the polynomial systems that admit easy-to-check certificates for validating bounds on their least fixpoint. Second, we present a sound and complete Optimistic Value Iteration algorithm for computing such certificates. Third, we show how certificates for polynomial systems can be transferred to certificates for various quantitative pPDA properties. Experiments demonstrate that our algorithm computes succinct certificates for several intricate example programs as well as stochastic context-free grammars with $> 10^4$ production rules.