Model Checking Temporal Properties of Recursive Probabilistic Programs

TL;DR

This work establishes the decidability of model checking probabilistic pushdown automata (pPDA) against ω-visibly pushdown languages (ω-VPL) and CaRet-based specifications, addressing recursive probabilistic programs. The authors combine automata-theoretic techniques by determinizing CaRet into a stair-parity DVPA, forming a product with a pVPA, and reducing acceptance to a stair-parity condition on a finite step chain; crucially, probabilities are handled via the existential theory of the reals (ETR) to stay within PSPACE. The main results include PSPACE decidability for qualitative and quantitative model checking against stair-parity DVPA, with extended implications to Büchi VPA and CaRet, yielding 2EXPSPACE/2EXPTIME bounds for CaRet and EXPTIME-complete qualitative results for Büchi VPA. These findings enable automated verification of recursive probabilistic programs against expressive, structure-aware temporal properties, broadening the scope beyond ω-regular specifications. The work also outlines future directions for tightening complexity bounds and extending to related logics such as visibly LTL and OPTL, as well as approximate verification techniques.

Abstract

Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices and recursive procedures. Temporal properties are useful for specifying the chronological order of events during program execution. Existing approaches for model checking pPDA against temporal properties have focused mostly on $ω$-regular and LTL properties. In this paper, we give decidability and complexity results for the model checking problem of pPDA against $ω$-visibly pushdown languages that can be described by specification logics such as CaRet. These logical formulae allow specifying properties that explicitly take the structured computations arising from procedural programs into account. For example, CaRet is able to match procedure calls with their corresponding future returns, and thus allows to express fundamental program properties such as total and partial correctness.

Figures (9)

• Figure 1: Recursive probabilistic program modeling the outbreak of an infectious disease. $\texttt{uniform}(a,b)$ stands for the discrete uniform distribution on $[a,b]$.
• Figure 2: Example infection rates by age groups.
• Figure 3: Chain of reductions used in this paper. ETR stands for existential theory of the reals, i.e., the existentially quantified fragment of the FO-theory over $(\mathbb{R}, +, \cdot, \leq)$.
• Figure 4: Left: An example VPA (in fact, a DVPA) with $\Gamma = \{Z, \bot\}$ over input alphabet $\Sigma = \{c\} \uplus \{\tau\} \uplus \{r\}$. Transitions labeled $c,Z$ are call transitions that push $Z$ on the stack. The transitions labeled $\tau$ are internal transitions; they ignore the stack completely. Transitions labeled $Z,r$ and $\bot, r$ are return transitions that are only enabled if $Z$ ($\bot$, respectively) is on top of the stack. When executing $Z,r$, the symbol $Z$ is popped from the stack. However, the special bottom-of-stack symbol $\bot$ can never be popped (e.g., position 1 in the run). Right: The unique run of the DVPA on input word $\tau \, r \, c \, \tau \, \tau \, c \, r \, c^2 \, r^2 \, c^3 \, r^3 \ldots$. Steps are underlined.
• Figure 5: CaRet's various next modalities applied to the initial fragment of an example word. Call, internal, and return positions are depicted as boxes, circles, and rhombs, respectively. Note that $\bigcirc^a$ of position 3 is undefined because $\bigcirc^g$ is a return. Whether or not $\bigcirc^a$ of position 0 is defined depends on how the words continues after position 5; more specifically, it is defined iff there occurs a return position on the same height as position 5. In this case, $\bigcirc^a$ of position 0 will point to the first such occurrence.

Theorems & Definitions (38)

• Definition 2.1: VPA vpl
• Definition 2.2: $\omega$-VPL vpl
• Definition 2.3: Step
• Example 2.4
• Remark 2.5
• Definition 2.6: Stair-parity vpGames
• Example 2.7
• Theorem 2.8: vpGames
• Definition 2.9: Syntax of CaRet caret
• Definition 2.10: Semantics of CaRet