Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration

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.

This work is supported by the DFG research training group 2236 UnRAVeL and the ERC advanced research grant 787914 FRAPPANT.

1 Introduction

Complex software is likely to contain bugs. This applies in particular to model checking tools. This is a serious problem, as the possibility of such bugs compromises the trust one can put in the verification results, rendering the process of formal modeling and analysis less useful. Ideally, the implementation of a model checker should be formally verified itself [15]. However, due to the great complexity of these tools, this is often out of reach in practice. Certifying algorithms [31] mitigate this problem by providing an easy-to-check certificate along with their regular output. This means that there exists a verifier that, given the input problem, the output, and the certificate, constructs a formal proof that the output is indeed correct. The idea is that the verifier is much simpler than the algorithm, and thus likely to be bug-free or even amenable to formal verification.

Fig. 1.

Left: A stochastic context-free grammar (SCFG; e.g. [16]) and the associated positive polynomial system (PPS) which encodes the termination probabilities of each non-terminal, assuming production rules are taken uniformly at random. Right: The curves defined by the two equations. The least fixpoint (lfp) is $\approx (0.66,0.70)$. The thin colored area to the top right of the lfp is the set of inductive, self-certifying upper bounds on the lfp.

This paper extends the recent line of research on probabilistic certification [19, 23, 24, 41] to probabilistic pushdown automata [13, 30] (pPDA). pPDA and related models have applications in, amongst others, pattern recognition [39], computational biology [28], and speech recognition [25]. They are moreover a natural operational model for programs with procedures, recursion, and (discrete) probabilistic constructs such as the ability to flip coins. With the advent of probabilistic programming [32] as a paradigm for model-based machine learning [6], such programs have received lots of attention recently. Moreover, several efficient algorithms such as Hoare’s quicksort with randomized pivot selection (e.g. [26]) are readily encoded as probabilistic recursive programs.

A pPDA can be seen as a purely probabilistic variant of a standard pushdown automaton: Instead of reading an input word, it takes its transitions randomly based on fixed probability distributions over successor states. Quantities of interest in pPDA include reachability probabilities [13], expected runtimes [8], variances [14], satisfaction probabilities of temporal logic formulas [42, 47], and others (see [7] for an overview). pPDA are equivalent to Recursive Markov Chains [17]. In the past two decades there have been significant research efforts on efficient approximative algorithms for pPDA, especially a decomposed variant of Newton iteration [10,11,12, 16, 17, 27, 40] which provides guaranteed lower, and occasionally upper [10, 12] bounds on key quantities. However, even though implementations might be complex [46], these algorithms are not certifying.

Our technique for certificate generation is a non-trivial extension of Optimistic Value Iteration [22] (OVI) to pPDA. In a nutshell, the idea of OVI is to compute some lower bound $\boldsymbol{l}$ on the solution—which can be done using an approximative iterative algorithm—and then optimistically guess an upper bound $\boldsymbol{u} = \boldsymbol{l} + \boldsymbol{\varepsilon }$ and verify that the guess was correct. Prior to our paper, OVI had only been considered in Markov Decision Processes (MDP) [22] and Stochastic Games (SG) [1], where it is used to compute bounds on, e.g., maximal reachability probabilities. The upper bounds computed by OVI have a special property: They are self-certifying (also called inductive in our paper): Given the system and the bounds, one can check very easily that the bounds are indeed correct.

However, pPDA are much more complicated than MDP or SG for the following reasons: (i) pPDA may induce infinite-state Markov processes due to their unbounded stack; (ii) the analysis of pPDA requires solving non-linear equations; (iii) the complexity of basic decision problems is generally higher than in MDP/SG. For example, reachability in MDP is characterized as the least fixpoint (lfp) of a piece-wise linear function that can be computed in PTIME via, e.g., LP solving. On the other hand, reachability in pPDA requires computing a fixed point of a positive polynomial function, leading to a PSPACE complexity bound [13]. See Figure 1 for an example.

Contributions. Despite the difficulties mentioned above, we show in this paper that the general idea of OVI can be extended to pPDA, yielding a practically feasible algorithm with good theoretical properties. More concretely:

Contribution 1

We present an OVI-style algorithm for computing inductive upper bounds of any desired precision $\varepsilon > 0$ on the lfp of a positive polynomial system. Compared to the existing OVI [22], the key novelty of our algorithm is to compute a certain direction $\boldsymbol{v}$ in which to guess, i.e., the guess is $\boldsymbol{u} = \boldsymbol{l} + \varepsilon \boldsymbol{v}$ rather than $\boldsymbol{u} = \boldsymbol{l} + \boldsymbol{\varepsilon }$. The direction $\boldsymbol{v}$ is an estimate of a certain eigenvector. This ensures that we eventually hit an inductive bound, even if the latter lie in a very “thin strip” as in Figure 1, and yields a provably complete algorithm that is guaranteed to find an inductive bound in finite time (under mild assumptions).

Contribution 2

We implement our algorithm in the software tool pray and compare the new technique to an out-of-the-box approach based on SMT solving, as well as to standard OVI with a simpler guessing heuristic.

Related Work. Certification of pPDA has not yet been addressed explicitly, but some existing technical results go in a similar direction. For instance, [17, Prop. 8.7] yields certificates for non-termination in SCFG, but they require an SCC decomposition for verification. Farkas certificates for MDP [19] are more closely related to our idea of certificates. They require checking a set of linear constraints. A symbolic approach to verify probabilistic recursive programs on the syntax level including inductive proof rules for upper bounds was studied in [35]. A higher-order generalization of pPDA was introduced in [29], and an algorithm for finding upper bounds inspired by the Finite Element method was proposed. Applications of PPS beyond the analysis of pPDA include the recent factor graph grammars [9] as well as obtaining approximate counting formulas for many classes of trees in the framework of analytic combinatorics [18]. Regarding software tools, PReMo [46] implements iterative algorithms for lower bounds in Recursive Markov Chains, but it supports neither certificates nor upper bounds.

Paper Outline. We review the relevant background information on PPS in Section 2. Section 3 presents our theoretical results on inductive upper bounds in PPS as well as the new Optimistic Value Iteration algorithm. In Section 4 we explain how inductive bounds in PPS are used to certify quantitative properties of pPPA. The experimental evaluation is in Section 5. We conclude in Section 6. A full version of this paper is available online [44].

2 Preliminaries

Notation for Vectors. All vectors in this paper are column vectors and are written in boldface, e.g., $\boldsymbol{u} = (u_1, \ldots , u_n)^T$. For vectors $\boldsymbol{u} , \boldsymbol{u}'$, we write $\boldsymbol{u} \le \boldsymbol{u}'$ if $\boldsymbol{u}$ is component-wise less than or equal to $\boldsymbol{u}'$. Moreover, we write $\boldsymbol{u} < \boldsymbol{u}'$ if $\boldsymbol{u} \le \boldsymbol{u}'$ and $\boldsymbol{u} \ne \boldsymbol{u}'$, and $\boldsymbol{u} \prec \boldsymbol{u}'$ if $\boldsymbol{u}$ is component-wise strictly smaller than $\boldsymbol{u}'$. The zero vector is denoted $\boldsymbol{0}$. The max norm of a vector $\boldsymbol{u}$ is $||\boldsymbol{u}||_{\infty } = \max _{1\le i \le n} |u_i|$. We say that $\boldsymbol{u}$ is normalized if $||\boldsymbol{u}||_{\infty } = 1$.

Positive Polynomial Systems (PPS). Let $n \ge 1$ and $\boldsymbol{x} = (x_1 ,\ldots ,x_n)^T$ be a vector of variables. An n-dimensional PPS is an equation system of the form

$$ x_1 ~=~ f_1(x_1,\ldots ,x_n) \quad \ldots \quad x_n ~=~ f_n(x_1,\ldots ,x_n) $$

where for all $1 \le i \le n$, the function $f_i$ is a polynomial with non-negative real coefficients. An example PPS is the system $x = \frac{1}{2}(1 + xy^2), y = \frac{1}{3}(1 + x + y^2)$ from Figure 1. We also use vector notation for PPS: $\boldsymbol{x} = \boldsymbol{f}(\boldsymbol{x}) = (f_1(\boldsymbol{x}), \ldots , f_n(\boldsymbol{x}))^T$.

We write $\overline{\mathbb {R}}_{\ge 0}= \mathbb {R}_{\ge 0}\cup \{\infty \}$ for the extended non-negative reals. By convention, for all $a \in \overline{\mathbb {R}}_{\ge 0}$, $a \le \infty$, $a + \infty = \infty + a = \infty$, and $a \cdot \infty = \infty \cdot a$ equals 0 if $a = 0$ and $\infty$ otherwise. For $n \ge 1$, the partial order $(\overline{\mathbb {R}}_{\ge 0}^n, \le )$ is a complete lattice, i.e., all subsets of $\overline{\mathbb {R}}_{\ge 0}^n$ have an infimum and a supremum. In particular, there exists a least element $\boldsymbol{0}$ and a greatest element $\boldsymbol{\infty }= (\infty , \ldots , \infty )^T$. Every PPS induces a monotone function $\boldsymbol{f} :\overline{\mathbb {R}}_{\ge 0}^n \rightarrow \overline{\mathbb {R}}_{\ge 0}^n$, i.e., $\boldsymbol{u} \le \boldsymbol{v} \implies \boldsymbol{f}(\boldsymbol{u}) \le \boldsymbol{f}(\boldsymbol{v})$. By the Knaster-Tarski fixpoint theorem, the set of fixpoints of $\boldsymbol{f}$ is also a complete lattice, and thus there exists a least fixpoint (lfp) denoted by $\mu \boldsymbol{f}$.

In general, the lfp $\mu \boldsymbol{f}$ is a vector which may contain $\infty$ as an entry. For instance, this happens in the PPS $x = x+1$. A PPS $\boldsymbol{f}$ is called feasible if $\mu \boldsymbol{f} \prec \boldsymbol{\infty }$ (or equivalently, $\mu \boldsymbol{f} \in \mathbb {R}_{\ge 0}^n$). The Knaster-Tarski theorem also implies:

Lemma 1

(Inductive upper bounds). For all $\boldsymbol{u} \in \overline{\mathbb {R}}_{\ge 0}^n$ it holds that

$$\begin{aligned} \boldsymbol{f}(\boldsymbol{u}) \le \boldsymbol{u} \quad \text {implies}\quad \mu \boldsymbol{f} \le \boldsymbol{u} ~. \end{aligned}$$

Such a vector $\boldsymbol{u}$ with $\boldsymbol{u} \prec \boldsymbol{\infty }$ is called inductive upper bound.

If $\boldsymbol{f}$ is feasible, then $\mu \boldsymbol{f}$ is obviously an inductive upper bound. The problem is that $\mu \boldsymbol{f}$ may be irrational even if $\boldsymbol{f}$ has rational coefficients only (see Example 1 below) and can thus not easily be represented exactly. In Section 3 we show under which conditions there exist rational inductive upper bounds $\boldsymbol{u} \in \mathbb {Q}_{\ge 0}^n$.

A PPS is called clean if $\mu \boldsymbol{f} \succ \boldsymbol{0}$. Every PPS can be cleaned in linear time by identifying and removing the variables that are assigned 0 in the lfp [12, 17].

Given a PPS $\boldsymbol{f}$ and a point $\boldsymbol{u} \in \mathbb {R}_{\ge 0}^n$, we define the Jacobi matrix of $\boldsymbol{f}$ at $\boldsymbol{u}$ as the $n {\times } n$-matrix $\boldsymbol{f}'(\boldsymbol{u})$ with coefficients $\boldsymbol{f}'(\boldsymbol{u})_{1 \le i,j \le n} = \frac{\partial }{\partial x_j} f_i(\boldsymbol{u})$.

Example 1

Consider the example PPS $\boldsymbol{f}_{ex}$ with variables $\boldsymbol{x} = (x, y)^T$:

$$\begin{aligned} x ~=~ f_1(x,y) ~=~ y + 0.1{} & {} y ~=~ f_2(x,y) ~=~ 0.2x^2 + 0.8 xy + 0.1 ~. \end{aligned}$$

The line and the hyperbola defined by these equations are depicted in Figure 2 on Page 7. The fixpoints of $\boldsymbol{f}_{ex}$ are the intersections of these geometric objects; in this case there are two. In particular, $\boldsymbol{f}_{ex}$ is feasible and its lfp is

$$ \mu \boldsymbol{f}_{ex}~=~ \big (\, (27 {-} \sqrt{229}) / 50 \,,\, (22 {-} \sqrt{229}) / 50 \,\big )^T ~\approx ~ (0.237 \,,\, 0.137)^T ~. $$

Therefore, $\boldsymbol{f}_{ex}$ is clean as $\mu \boldsymbol{f}_{ex}\succ \boldsymbol{0}$. The Jacobi matrix of $\boldsymbol{f}_{ex}$ is

$$ \boldsymbol{f}_{ex}'(x,y) ~=~ \begin{pmatrix} \frac{\partial }{\partial x}f_1 \,&{}\, \frac{\partial }{\partial y}f_1 \\ \frac{\partial }{\partial x}f_2 \,&{}\, \frac{\partial }{\partial y}f_2 \end{pmatrix} ~=~ \begin{pmatrix} 0 \,&{}\, 1 \\ 0.4x + 0.8y \,&{}\, 0.8x \end{pmatrix} ~. $$

Note that the lfp $\mu \boldsymbol{f}_{ex}$ contains irrational numbers. In the above example, these irrational numbers could still be represented using square roots because the fixpoints of $\boldsymbol{f}_{ex}$ are the zeros of a quadratic polynomial. However, there are PPS whose lfp cannot be expressed using radicals, i.e., square roots and cubic roots, etc. [16]. This means that in general, there is no easy way to compute the lfp exactly. It is thus desirable to provide bounds, which we do in this paper.    $\triangle$

Matrices and Eigenvectors. Let M be a real $n{\times } n$-matrix. We say that M is non-negative (in symbols: $M \ge 0$) if it has no negative entries. M is called irreducible if for all $1 \le i,j \le n$ there exists $0 \le k < n$ such that $(M^k)_{i,j} \ne 0$. It is known that M is irreducible iff the directed graph $G_M = (\{1,\ldots ,n\}, E)$ with $(i,j) \in E$ iff $M_{i,j} \ne 0$ is strongly connected. A maximal irreducible submatrix of M is a square submatrix induced by a strongly connected component of $G_M$. The period of a strongly connected M is the length of the shortest cycle in $G_M$. It is instructive to note that PPS $\boldsymbol{x} = \boldsymbol{f} (\boldsymbol{x})$ are generalizations of linear equation systems of the form $\boldsymbol{x} = M \boldsymbol{x} + \boldsymbol{c}$, with $M \ge 0$ and $\boldsymbol{c} \ge \boldsymbol{0}$. Moreover, note that for any PPS $\boldsymbol{f}$ it holds that $\boldsymbol{f}'(\boldsymbol{u}) \ge 0$ for all $\boldsymbol{u} \succ \boldsymbol{0}$.

An eigenvector of an $n {\times } n$-matrix M with eigenvalue $\lambda \in \mathbb {C}$ is a (complex) vector $\boldsymbol{v} \ne \boldsymbol{0}$ satisfying $M \boldsymbol{v} = \lambda \boldsymbol{v}$. There are at most n different eigenvalues. The spectral radius $\rho (M) \in \mathbb {R}_{\ge 0}$ is the largest absolute value of the eigenvalues of M. The following is a fundamental theorem about non-negative matrices:

Theorem 1

(Perron-Frobenius; e.g. [37]). Let $M \ge 0$ be irreducible.

• (1) M has a strictly positive eigenvector $\boldsymbol{v} \succ \boldsymbol{0}$ with eigenvalue $\rho (M)$, the spectral radius of M, and all other eigenvectors $\boldsymbol{v'} \succ \boldsymbol{0}$ are scalar multiples of $\boldsymbol{v}$.

• (2) The eigenvalues of M with absolute value $\rho (M)$ are exactly the h numbers $\rho (M), \xi \rho (M), \ldots , \xi ^{h-1} \rho (M)$, where $\xi$ is a primitive hth root of unity.

The unique eigenvector $\boldsymbol{v} \succ \boldsymbol{0}$ with $||\boldsymbol{v}||_{\infty } = 1$ of an irreducible non-negative matrix M is called the Perron-Frobenius eigenvector of M.

Strongly Connected Components. To each PPS $\boldsymbol{f}$ we associate a finite directed graph $G_{\boldsymbol{f}} = (\{x_1,\ldots ,x_n\}, E)$, which, intuitively speaking, captures the dependency structure among the variables. Formally, $(x_i, x_j) \in E$ if the polynomial $f_i$ depends on $x_j$, i.e., $x_j$ appears in at least one term of $f_i$ with a non-zero coefficient. This is equivalent to saying that the partial derivative $\frac{\partial }{\partial x_j} f_i$ is not the zero polynomial. We say that $\boldsymbol{f}$ is strongly connected if $G_{\boldsymbol{f}}$ is strongly connected, i.e., for each pair $(x_i, x_j)$ of variables, there exists a path from $x_i$ to $x_j$ in $G_{\boldsymbol{f}}$. For instance, $\boldsymbol{f}_{ex}$ from Example 1 is strongly connected because the dependency graph has the edges $E = \{(x,y), (y,x), (y,y)\}$. Strong connectivity of PPS is a generalization of irreducibility of matrices; indeed, a matrix M is irreducible iff the PPS $\boldsymbol{x} = M \boldsymbol{x}$ is strongly connected. We often use the fact that $\boldsymbol{f}'(\boldsymbol{u})$ for $\boldsymbol{u} \succ \boldsymbol{0}$ is irreducible iff $\boldsymbol{f}$ is strongly connected.

PPS are usually analyzed in a decomposed fashion by considering the sub-systems induced by the strongly connected components (SCCs) of $G_{\boldsymbol{f}}$ in bottom-up order [16]. Here we also follow this approach and therefore focus on strongly connected PPS. The following was proved in [17, Lem. 6.5] and later generalized in [12, Thm. 4.1] (also see remark below [12, Prop. 5.4] and [17, Lem. 8.2]):

Theorem 2

([12, 17]). If $\boldsymbol{f}$ is feasible, strongly connected and clean, then for all $\boldsymbol{u} < \mu \boldsymbol{f}$, we have $\rho (\boldsymbol{f}'(\boldsymbol{u})) < 1$. As a consequence, $\rho (\boldsymbol{f}'(\mu \boldsymbol{f})) \le 1$.

Theorem 2 partitions all PPS $\boldsymbol{f}$ which satisfy its precondition into two classes: Either (1) $\rho (\boldsymbol{f}'(\mu \boldsymbol{f})) < 1$, or (2) $\rho (\boldsymbol{f}'(\mu \boldsymbol{f})) = 1$. In the next section we show that $\boldsymbol{f}$ admits non-trivial inductive upper bounds iff it is in class (1).

Example 2

Reconsider the PPS $\boldsymbol{f}_{ex}$ from Example 1. It can be shown that $\boldsymbol{v} = (1, \lambda _1)^T$ where $\lambda _1 \approx 0.557$ is an eigenvector of $\boldsymbol{f}_{ex}'(\mu \boldsymbol{f}_{ex})$ with eigenvalue $\lambda _1$. Thus by the Perron-Frobenius Theorem, $\rho (\boldsymbol{f}_{ex}'(\mu \boldsymbol{f}_{ex})) = \lambda _1 < 1$. As promised, there exist inductive upper bounds as can be seen in Figure 2.    $\triangle$

3 Finding Inductive Upper Bounds in PPS

In this section, we are concerned with the following problem: Given a feasible, clean, and strongly connected PPS $\boldsymbol{f}$, find a vector $\boldsymbol{0} \prec \boldsymbol{u} \prec \boldsymbol{\infty }$ such that $\boldsymbol{f}(\boldsymbol{u}) \le \boldsymbol{u}$, i.e., an inductive upper bound on the lfp of $\boldsymbol{f}$ (see Lemma 1).

3.1 Existence of Inductive Upper Bounds

Fig. 2.

The PPS $\boldsymbol{f}_{ex}$ corresponds to the solid red line and the solid blue curve. Its inductive upper bounds form the shaded area above the lfp $\mu \boldsymbol{f}_{ex}$. Lemma 2(4) ensures that one can fit the gray “cone” pointing in direction of the Perron-Frobenius eigenvector $\boldsymbol{v}$ inside the inductive region. The PPS $\boldsymbol{\tilde{f}}_{ ex }$ which comprises the dashed curve and the solid line does not have any non-trivial inductive upper bounds. Note that the tangent lines at $\mu \boldsymbol{\tilde{f}}_{ ex }$ are parallel to each other.

An important first observation is that inductive upper bounds other than the exact lfp do not necessarily exist. As a simple counter-example consider the 1-dimensional PPS $x = \frac{1}{2}x^2 + \frac{1}{2}$. If u is an inductive upper bound, then

$$ \frac{1}{2}u^2 + \frac{1}{2} \le u ~\implies ~ u^2 - 2u + 1 \le 0 ~\implies ~ (u-1)^2 \le 0 ~\implies ~ u=1 ~, $$

and thus the only inductive upper bound is the exact lfp $u=1$. Another example is the PPS $\boldsymbol{\tilde{f}}_{ ex }$ from Figure 2. What these examples have in common is the following property: Their derivative evaluated at the lfp is not invertible. Indeed, we have $\frac{\partial }{\partial x} (\frac{1}{2}x^2 + \frac{1}{2} - x) = x - 1$, and inserting the lfp $x=1$ yields zero. The higher dimensional generalization of this property to arbitrary PPS $\boldsymbol{f}$ is that the Jacobi matrix of the function $\boldsymbol{f} - \boldsymbol{x}$ evaluated at $\mu \boldsymbol{f}$ is singular; note that this is precisely the matrix $\boldsymbol{f}'(\mu \boldsymbol{f}) - I$. Geometrically, this means that the tangent lines at $\mu \boldsymbol{f}$ are parallel, as can be seen in Figure 2 for the example PPS $\boldsymbol{\tilde{f}}_{ ex }$. It should be intuitively clear from the figure that inductive upper bounds only exist if the tangent lines are not parallel. The next lemma makes this more precise:

Lemma 2

(Existence of inductive upper bounds). Let $\boldsymbol{f}$ be a feasible, clean, and strongly connected PPS. Then the following are equivalent:

• (1) The matrix $I- \boldsymbol{f}' (\mu \boldsymbol{f})$ is non-singular.

• (2) The spectral radius of $\boldsymbol{f}' (\mu \boldsymbol{f})$ satisfies $\rho (\boldsymbol{f}' (\mu \boldsymbol{f})) < 1$.

• (3) There exists $\boldsymbol{0} \prec \boldsymbol{u} \prec \boldsymbol{\infty }$ s.t. $\boldsymbol{f} (\boldsymbol{u}) < \boldsymbol{u}$ (i.e. $\boldsymbol{u}$ is inductive but not a fixpoint).

• (4) The matrix $\boldsymbol{f}' (\mu \boldsymbol{f})$ has a unique (normalized) eigenvector $\boldsymbol{v} \succ \boldsymbol{0}$ and there exist numbers $\delta _{max} > 0$ and $\varepsilon > 0$ s.t.

  $$ \boldsymbol{f}(\, \mu \boldsymbol{f} + \delta \cdot \boldsymbol{\tilde{v}} \,) \quad \prec \quad \mu \boldsymbol{f} + \delta \cdot \boldsymbol{\tilde{v}} $$

  holds for all $0< \delta \le \delta _{max}$ and vectors $\boldsymbol{\tilde{v}} \ge \boldsymbol{v}$ with $||\boldsymbol{v} - \boldsymbol{\tilde{v}} ||_{\infty } \le \varepsilon$.

The proof of Lemma 2 (see [44]) relies on a linear approximation of $\boldsymbol{f}$ via Taylor’s familiar theorem as well as Theorems 1 and 2. Condition (4) of Lemma 2 means that there exists a “truncated cone”

$$ Cone(\mu \boldsymbol{f}, \boldsymbol{v}, \varepsilon , \delta _{max}) ~=~ \{\, \mu \boldsymbol{f} + \delta \boldsymbol{\tilde{v}} \mid 0 \le \delta \le \delta _{max}, \boldsymbol{\tilde{v}} \ge \boldsymbol{v}, ||\boldsymbol{\tilde{v}} - \boldsymbol{v}||_{\infty } \le \varepsilon \,\} $$

which is entirely contained in the inductive region. The “tip” of the cone is located at the lfp $\mu \boldsymbol{f}$ and, the cone points in the direction of the Perron-Frobenius eigenvector $\boldsymbol{v}$, as illustrated in Figure 2 (assuming $\delta _{max} = 1$ for simplicity). The length $\delta _{max} > 0$ and the radius $\varepsilon > 0$ of the cone depend on $\rho (\boldsymbol{f}' (\mu \boldsymbol{f}))$, but for us it suffices that they are non-zero. Note that this cone has non-empty interior and thus contains rational-valued vectors. The idea of our Optimistic Value Iteration is to construct a sequence of guesses that eventually hits this cone.

3.2 The Optimistic Value Iteration Algorithm

The basic idea of Optimistic Value Iteration (OVI) can be applied to monotone functions of the form $\boldsymbol{\phi }:\mathbb {R}_{\ge 0}^n \rightarrow \mathbb {R}_{\ge 0}^n$ (in [22], $\boldsymbol{\phi }$ is the Bellman operator of an MDP). Kleene’s fixpoint theorem suggests a simple method for approximating the lfp $\mu \boldsymbol{\phi }$ from below: Simply iterate $\boldsymbol{\phi }$ starting at $\boldsymbol{0}$, i.e., compute the sequence $\boldsymbol{l}_0 = \boldsymbol{0}$, $\boldsymbol{l}_1 = \boldsymbol{\phi }(\boldsymbol{l}_0)$, $\boldsymbol{l}_2 = \boldsymbol{\phi }(\boldsymbol{l}_1)$, etc.¹ In the context of MDP, this iterative scheme is known as Value Iteration (VI). VI is easy to implement, but it is difficult to decide when to stop the iteration. In particular, standard stopping criteria such as small absolute difference of consecutive approximations are formally unsound [20]. OVI and other algorithms [3, 36] cope with this problem by computing not only a lower but also an upper bound on $\mu \boldsymbol{\phi }$. In the case of OVI, an upper bound with absolute error $\le \varepsilon$ is obtained as follows (we omit some details):

• (1) Compute $\boldsymbol{l}_k \le \mu \boldsymbol{\phi }$ such that $||\boldsymbol{l}_k - \boldsymbol{l}_{k-1}||_{\infty } \le \tau$, for some (small) $\tau > 0$.

• (2) Guess a candidate upper bound $\boldsymbol{u} = \boldsymbol{l}_k + \boldsymbol{\varepsilon }$.

  • (a) If $\boldsymbol{\phi }(\boldsymbol{u}) \le \boldsymbol{u}$ holds, i.e., $\boldsymbol{u}$ is inductive, then return $\boldsymbol{u}$.

  • (b) If not, refine $\boldsymbol{u}$ (see [22] for details). If the refined $\boldsymbol{u}$ is still not inductive, then go back to step (1) and try again with $0< \tau ' < \tau$.

We present our variant of OVI for PPS as Algorithm 1. The main differences to the above scheme are that (i) we do not insist on Kleene iteration for obtaining the lower bounds $\boldsymbol{l}$, and (ii) we approximate the eigenvector $\boldsymbol{v}$ from condition (4) of Lemma 2 and compute the “more informed” guesses $\boldsymbol{u} = \boldsymbol{l} + \varepsilon \boldsymbol{v}$, for various $\varepsilon$. Refining the guesses as original OVI does is not necessary (but see our remarks in Section 3.3 regarding floating point computations).

The functions $\texttt {improveLowerBound}$ and $\texttt {approxEigenvec}$ used in Algorithm 1 must satisfy the following contracts in order for the algorithm to be correct:

• The sequence $\boldsymbol{l}_0 = \boldsymbol{0}$, $\boldsymbol{l}_{i+1} = \texttt {improveLowerBound}(\boldsymbol{f}, \boldsymbol{l}_i)$ for $i \ge 0$, is a monotonically increasing sequence of rational vectors converging to $\mu \boldsymbol{f}$.

• $\texttt {approxEigenvec}$ must satisfy the following: Let $M \ge 0$ be an irreducible matrix with (normalized) Perron-Frobenius eigenvector $\boldsymbol{v} \succ \boldsymbol{0}$. Then for all $\varepsilon > 0$, we require that there exists $\tau > 0$ such that $||\texttt {approxEigenvec}(M, \tau ) - \boldsymbol{v}||_{\infty } \le \varepsilon$. In words, $\texttt {approxEigenvec}$ approximates $\boldsymbol{v}$ up to arbitrarily small absolute error if the tolerance $\tau$ is chosen sufficiently small. Moreover, $\texttt {approxEigenvec}(M, \tau )$ returns a rational vector.

In practice, both the Kleene and the Newton [12, 16, 17] update operator can be used to implement $\texttt {improveLowerBound}$. We outline a possible implementation of $\texttt {approxEigenvec}$ further below in Section 3.3.

Example 3

Consider the following PPS $\boldsymbol{f}$: $x = \frac{1}{4} x^2 + \frac{1}{8}$, $y = \frac{1}{4}xy + \frac{1}{4}y + \frac{1}{4}$. The table illustrates the execution of Algorithm 1 on $\boldsymbol{f}$ with $\varepsilon = 0.1$ and $c = 0.5$:

$\#$	$N$	$\tau$	$\boldsymbol{l}$	$\boldsymbol{l'}$	$||\boldsymbol{l}- \boldsymbol{l}'||_{\infty }$	$\boldsymbol{v}$	$\boldsymbol{u}$	$\boldsymbol{f}(\boldsymbol{u}) \le \boldsymbol{u}$
1	0	0.1	(0, 0)	(0.4, 0.3)	0.4
2	0	0.1	(0.4, 0.3)	(0.5, 0.4)	0.1	(1.0, 0.8)	(0.5, 0.38)	✗
3	1	0.05	(0.5, 0.4)	(0.55, 0.41)	0.05	(1.0, 0.9)	(0.6, 0.49)	✓

The algorithm has to improve the lower bound 3 times (corresponding to the 3 lines of the table). After the second improvement, the difference between the current lower bound $\boldsymbol{l}_2$ and the new bound $\boldsymbol{l'}_2$ does not exceed the current tolerance $\tau _2 = 0.1$ and the algorithm enters the optimistic guessing stage. The first guess $\boldsymbol{u} _2$ is not successful. The tolerance is then decreased to $\tau _3 = c \cdot \tau _2 = 0.05$ and the lower bound is improved to $\boldsymbol{l'}_3$. The next guess $\boldsymbol{u}_3$ is inductive.    $\triangle$

Theorem 3

Algorithm 1 is correct: when invoked with a strongly connected clean PPS $\boldsymbol{f}$ and $\varepsilon \in \mathbb {Q}_{> 0}$, then (if it terminates) it outputs a pair $(\boldsymbol{l},\boldsymbol{u})$ of rational vectors s.t. $\boldsymbol{l}\le \mu \boldsymbol{f}$, $\boldsymbol{f}(\boldsymbol{u}) \le \boldsymbol{u}$, and $||\boldsymbol{l} - \boldsymbol{u}||_{\infty } \le \varepsilon$. Moreover, if $\boldsymbol{f}$ is feasible and $I-\boldsymbol{f}'(\mu \boldsymbol{f})$ is non-singular, then the algorithm terminates.

The proof of Theorem 3 (see [44]) crucially relies on condition (4) of Lemma 2 that assures the existence of a “truncated cone” of inductive bounds centered around the Perron-Frobenius eigenvector of $\boldsymbol{f}'(\mu \boldsymbol{f})$ (see Figure 2 for an illustration). Intuitively, since the lower bounds $\boldsymbol{l}$ computed by the algorithm approach the lfp $\mu \boldsymbol{f}$, the eigenvectors of $\boldsymbol{f}'(\boldsymbol{l})$ approach those of $\boldsymbol{f}'(\mu \boldsymbol{f})$. As a consequence, it is guaranteed that the algorithm eventually finds an eigenvector that intersects the cone. The inner loop starting on line 7 is needed because the “length” of the cone is a priori unknown; the purpose of the loop is to scale the eigenvector down so that it is ultimately small enough to fit inside the cone.

3.3 Considerations for Implementing OVI

As said earlier, there are at least two options for $\texttt {improveLowerBound}$: Kleene or Newton iteration. We now show that $\texttt {approxEigenvec}$ can be effectively implemented as well. Further below we comment on floating point arithmetic.

Approximating the Eigenvector. A possible implementation of $\texttt {approxEigenvec}$ relies on the power iteration method (e.g. [38, Thm. 4.1]). Given a square matrix M and an initial vector $\boldsymbol{v}_0$ with $M\boldsymbol{v}_0 \ne \boldsymbol{0}$, power iteration computes the sequence $(\boldsymbol{v}_ i)_{i \ge 0}$ such that for $i > 0$, $\boldsymbol{v}_{i} = M \boldsymbol{v}_{i-1} / ||M \boldsymbol{v}_{i-1}||_{\infty }$.

Lemma 3

Let $M \ge 0$ be irreducible. Then power iteration applied to $M + I$ and any $\boldsymbol{v} _0 > \boldsymbol{0}$ converges to the Perron-Frobenius eigenvector $\boldsymbol{v} \succ \boldsymbol{0}$ of M.

The convergence rate of power iteration is determined by the ratio $|\lambda _2| / |\lambda _1|$ where $\lambda _1$ and $\lambda _2$ are eigenvalues of largest and second largest absolute value, respectively. Each time $\texttt {approxEigenvec}$ is called in Algorithm 1, the result of the previous call to $\texttt {approxEigenvec}$ may be used as initial approximation $\boldsymbol{v}_0$.

Exact vs Floating Point Arithmetic. So far we have assumed exact arithmetic for the computations in Algorithm 1, but an actual implementation should use floating point arithmetic for efficiency. However, this leads to unsound results. More specifically, the condition $\boldsymbol{f}(\boldsymbol{u}) \le \boldsymbol{u}$ may hold in floating point arithmetic even though it is actually violated. As a remedy, we propose to nevertheless run the algorithm with floats, but then verify its output $\boldsymbol{u}$ with exact arbitrary-precision rational arithmetic. That is, we compute a rational number approximation $\boldsymbol{u}_{\mathbb {Q}}$ of $\boldsymbol{u}$ and check $\boldsymbol{f}(\boldsymbol{u}_{\mathbb {Q}}) \le \boldsymbol{u}_{\mathbb {Q}}$ with exact arithmetic. If the check fails, we resort to the following refinement scheme which is an instance of the general k-induction principle for complete lattices from [5]: We iteratively check the conditions

$$ \boldsymbol{f}(\boldsymbol{u}_{\mathbb {Q}} \sqcap \boldsymbol{f}(\boldsymbol{u}_{\mathbb {Q}})) \le \boldsymbol{u}_{\mathbb {Q}} \,,\quad \boldsymbol{f} (\boldsymbol{u}_{\mathbb {Q}} \sqcap \boldsymbol{f}(\boldsymbol{u}_{\mathbb {Q}} \sqcap \boldsymbol{f}(\boldsymbol{u}_{\mathbb {Q}}))) \le \boldsymbol{u}_{\mathbb {Q}} \,,\quad \text {and so on,} $$

where $\sqcap$ denotes pointwise minimum. If one of the checks is satisfied, then $\mu \boldsymbol{f} \le \boldsymbol{u}_{\mathbb {Q}}$ [5]. This scheme often works well in practice (see Section 5). The original OVI from [22] uses a similar technique to refine its guesses.

4 Certificates for Probabilistic Pushdown Automata

This section shows how the results from Section 3 can be applied to pPDA. We introduce some additional notation. For finite sets A, $\mathcal {D}(A)$ denotes the set of probability distributions on A. In this section we often denote tuples without parentheses and commata, e.g., we may write ab rather than (a, b).

Definition 1

(pPDA [13]). A probabilistic pushdown automaton (pPDA) is a triple $\varDelta = (Q,\Gamma ,P)$ where $Q\ne \emptyset$ is a finite set of states, $\Gamma \ne \emptyset$ is a finite stack alphabet, and $P:Q\times \Gamma \rightarrow \mathcal {D}(Q\times \Gamma ^{\le 2})$ is a probabilistic transition function.

In the following, we often write $qZ \xrightarrow {p} r\alpha$ instead of $P(qZ)(r\alpha ) = p$ [13]. Intuitively, $qZ \xrightarrow {p} r\alpha$ means that if the pPDA is in state q and Z is on top of the stack, then with probability p, the pPDA moves to state r, pops Z and pushes $\alpha$ on the stack. More formally, the semantics of a pPDA $\varDelta = (Q,\Gamma ,P)$ is a countably infinite Markov chain with state space $Q\times \Gamma ^*$ and transition probability matrix M such that for all $q,r \in Q$, $Z \in \Gamma$, $\alpha \in \Gamma ^{\le 2}$, $\gamma \in \Gamma ^*$, we have

$$\begin{aligned} M(qZ\gamma , r\alpha \gamma ) ~=~ P(qZ)(r\alpha ) ~, \qquad M(q \varepsilon , q \varepsilon ) ~=~ 1 ~, \end{aligned}$$

and all other transition probabilities are zero. This Markov chain, where the initial state is fixed to qZ, is denoted $\mathcal {M}_{\varDelta }^{qZ}$ (see Figure 3 for an example). As usual, one can formally define a probability measure $\mathbb {P}_\varDelta ^{qZ}$ on the infinite runs of $\mathcal {M}_{\varDelta }^{qZ}$ via the standard cylinder construction (e.g., [2, Sec. 10]).

Consider a triple $qZr \in Q {\times } \Gamma {\times } Q$. We define the return probability² $[qZr]$ as the probability of reaching $r\varepsilon$ in the Markov chain $\mathcal {M}_{\varDelta }^{qZ}$, i.e., $[qZr] = \mathbb {P}_\varDelta ^{qZ} (\lozenge \{r\varepsilon \})$, where $\lozenge \{r\varepsilon \}$ is the set of infinite runs of $\mathcal {M}_{\varDelta }^{qZ}$ that eventually hit state $r\varepsilon$.

Fig. 3.

Top left: The pPDA $\varDelta _{ex}= (\{q, r\}, \{Z\}, P)$ where $P$ comprises the transitions $qZ \xrightarrow {1/4} qZZ,\, qZ \xrightarrow {1/2} q\varepsilon ,\, qZ \xrightarrow {1/4} r\varepsilon ,\, rZ \xrightarrow {1} r\varepsilon$. Top right: A fragment of the infinite underlying Markov chain $\mathcal {M}_{\varDelta }^{qZ}$, assuming initial configuration qZ. Bottom: The associated equation system from Theorem 4.

Theorem 4

(The PPS of return probabilities [13]³). Let $\varDelta = (Q,\Gamma ,P)$ be a pPDA and $(\langle qZr\rangle )_{qZr \,\in \, Q\times \Gamma \times Q}$ be variables. For each $\langle qZr\rangle$, define

$$ \langle qZr\rangle \quad =\quad \sum _{qZ \xrightarrow {p} sYX} p \cdot \sum _{t \in Q} \langle sYt\rangle \cdot \langle tXr\rangle ~+~ \sum _{qZ \xrightarrow {p} sY} p \cdot \langle sYr\rangle ~+~ \sum _{qZ \xrightarrow {p} r\varepsilon } p $$

and call the resulting PPS $\boldsymbol{f}_{\varDelta }$. Then $\mu \boldsymbol{f}_{\varDelta } = ([qZr])_{qZr \,\in \, Q\times \Gamma \times Q}$.

Example 4

Figure 3 shows a pPDA $\varDelta _{ex}$ and the associated PPS $\boldsymbol{f}_{\varDelta _{ex}}$. The least non-negative solution is $\langle qZq\rangle = 2 - \sqrt{2} \approx 0.586$ and $\langle qZr\rangle = \sqrt{2} - 1 \approx 0.414$ (and, of course, $\langle rZq\rangle = 0$, $\langle rZr\rangle = 1$). Thus by Theorem 4, the return probabilities are $[qZq] = 2 - \sqrt{2}$ and $[qZr] = \sqrt{2} - 1$.    $\triangle$

The PPS $\boldsymbol{f}_{\varDelta }$ is always feasible (because $\mu \boldsymbol{f}_{\varDelta } \le \boldsymbol{1}$). $\boldsymbol{f}_{\varDelta }$ is neither necessarily strongly connected nor clean. Let $\boldsymbol{\hat{f}}_{\varDelta }$ denote the cleaned up version of $\boldsymbol{f}_{\varDelta }$.

Proposition 1

(Basic Certificates for pPDA). A basic certificate for $\varDelta = (Q,\Gamma ,P)$ is a rational inductive upper bound $\boldsymbol{u} \in \mathbb {Q}_{\ge 0}^{Q\times \Gamma \times Q}$ on the lfp of the return probabilities system $\boldsymbol{f}_{\varDelta }$ (see Thm. 4). They have the following properties:

• (Existence) $\forall \varepsilon > 0$ there exists a basic certificate $\boldsymbol{u}$ with $||\mu \boldsymbol{f}_{\varDelta } - \boldsymbol{u}||_{\infty } \le \varepsilon$ if all maximal irreducible submatrices M of $\boldsymbol{\hat{f}}_{\varDelta }'(\mu \boldsymbol{\hat{f}}_{\varDelta })$ satisfy $\rho (M) < 1$.

• (Complexity) Let $\beta$ be the maximum number of bits used to encode any of the numerators and denominators of the fractions occurring in $\boldsymbol{u} \in \mathbb {Q}_{\ge 0}^{Q\times \Gamma \times Q}$. Then checking $\boldsymbol{f}_{\varDelta }(\boldsymbol{u}) \le \boldsymbol{u}$, i.e., whether $\boldsymbol{u}$ is basic certificate for $\varDelta$, can be done in time polynomial in $\beta$ and the size of $\varDelta$.

Existence of basic certificates follows from Lemma 2 applied to each SCC of the cleaned-up version of $\boldsymbol{f}_{\varDelta }$ individually. However, note that in order to merely check the certificate, i.e., verify the inequality $\boldsymbol{f}(\boldsymbol{u}) \le \boldsymbol{u}$, neither do SCCs need to be computed nor does the system has to be cleaned up.

Example 5

Reconsider the example pPDA and its associated (non-strongly connected) system of return probabilities from Figure 3. We verify that $\boldsymbol{u}_{qZq} = 3/5$ and $\boldsymbol{u}_{qZr} = 1/2$ (as well as $\boldsymbol{u}_{rZq} = 0, \boldsymbol{u}_{rZr} = 1$) is a basic certificate:

$$\begin{aligned} \frac{1}{4} \left( \frac{3}{5} \cdot \frac{3}{5} + \frac{1}{2} \cdot 0 \right) + \frac{1}{2} = \frac{59}{100} ~\overset{\checkmark }{\le }~ \frac{3}{5} \quad ,\quad \frac{1}{4} \left( \frac{3}{5} \cdot \frac{1}{2} + \frac{1}{2} \cdot 1 \right) + \frac{1}{4} = \frac{45}{100} ~\overset{\checkmark }{\le }~ \frac{1}{2} ~. \end{aligned}$$

Note that $[qZq] \approx 0.586 \le 3/5 = 0.6$ and $[qZr] \approx 0.414 \le 1/2 = 0.5$.    $\triangle$

In the following we outline how a variety of key quantities associated with a pPDA can be verified using basic certificates.

Upper Bounds on Temporal Properties. We may use basic certificates to verify that a bad state $r_{bad}$ is reached with low probability, e.g., at most $p = 0.01$. To this end, we remove the outgoing transitions of $r_{bad}$ and add the transitions $r_{bad}Z \xrightarrow {1} r_{bad}\varepsilon$ for all $Z \in \Gamma$. Clearly, $r_{bad}$ is reached with probability at most p from initial configuration qZ iff $[qZr_{bad}] \le p$. The results of [13] imply that this idea can be generalized to until-properties of the form $\mathcal {C}_1 \,\mathcal {U}\, \mathcal {C}_2$, where $\mathcal {C}_1$ and $\mathcal {C}_2$ are regular sets of configurations.

Certificates for the Output Distribution. Once a pPDA reaches the empty stack, we say that it has terminated. When modeling procedural programs, this corresponds to returning from a program’s main procedure. Assuming initial configuration qZ, the probability sub-distribution over the possible return values is then given by the return probabilities $\{[qZr] \mid r \in Q\}$. Missing probability mass models the probability of non-termination. Therefore, a basic certificate may be used to prove a point-wise upper bound on the output distribution as well as non almost-sure termination (AST). If a pPDA $\varDelta$ is known to be AST, then we can also certify a lower bound on the output distribution: Suppose that $\boldsymbol{u}$ is a basic certificate for $\varDelta$ and assume that $\varDelta$ is AST from initial configuration qZ. Define $\varepsilon = \sum _{r \in Q} \boldsymbol{u}_{qZr} - 1$. Then for all $r \in Q$, we have $\boldsymbol{u}_{qZr} - \varepsilon ~\le ~ [qZr] ~\le ~ \boldsymbol{u}_{qZr}$.

Example 6

The pPDA $\varDelta _{ex}$ from Figure 3 is AST from initial configuration qZ, as the transition $qZ \xrightarrow {1/4} r\varepsilon$ is eventually taken with probability 1, and the stack is emptied certainly once r is reached. Using the basic certificate from Example 5 we can thus (correctly) certify that $0.5 \le [qZq] \le 0.6$ and $0.4 \le [qZr] \le 0.5$.

Certificates for Expected Rewards. pPDA may also be equipped with a reward function $Q\rightarrow \mathbb {R}_{\ge 0}$. It was shown in [14] that the expected reward accumulated during the run of a pPDA is the solution of a linear equation system whose coefficients depends on the numbers $[qZr]$. Given a basic certificate $\boldsymbol{u}$, we obtain an equation system whose solution is an over-approximation of the true expected reward (see [44]). We may extend the basic certificate $\boldsymbol{u}$ by the solution of this linear system to make verification straightforward. Note that a program’s expected runtime [8, 35] is a special case of total expected reward.

5 Implementation and Experiments

Our Tool: pray . We implemented our algorithm in the prototypical Java-tool pray (Probabilistic Recursion AnalYzer) [43]. It supports two input formats: (i) Recursive probabilistic programs in a Java-like syntax (e.g. Figure 4); these programs are automatically translated to pPDA. (ii) Explicit PPS in the same syntax used by the tool PReMo [46]. The output of pray is a rational inductive upper bound on the lfp of the return probability PPS of the input program’s pPDA model (a basic certificate), or on the lfp of the explicitly given PPS. The absolute precision $\varepsilon$ is configurable. The implementation works as follows:

• (1) It parses the input and, if the latter is a program, constructs a pPDA model and the associated PPS of return probabilities.

• (2) It computes an SCC decomposition of the PPS under consideration using standard algorithms implemented in the jGraphT library [33].

• (3) It applies Algorithm 1 to the individual SCC in reverse topological order using floating point arithmetic. Algorithm 1 is instantiated with Kleene iteration⁴, the power iteration for approximating eigenvectors as outlined in Section 3.3, and constants $c=0.1$, $d=0.5$. We allow $\le 10$ guesses per SCC.

• (4) If stage (3) is successful, the tool verifies the resulting floating point certificate using exact rational number arithmetic as described in Section 3.3.

Baselines. To the best of our knowledge, no alternative techniques for finding inductive upper bounds in PPS have been described explicitly in the literature. However, there is an (almost) out-of-the-box approach using an SMT solver: Given a PPS $\boldsymbol{x} = \boldsymbol{f}(\boldsymbol{x})$, compute some lower bound $\boldsymbol{l}\le \mu \boldsymbol{f}$ using an iterative technique. Then query the SMT solver for a model (variable assignment) of the quantifier-free first-order logic formula $\varphi _{\boldsymbol{f}}(\boldsymbol{x}) = \bigwedge _{i=1}^n f_i(\boldsymbol{x}) \le x_i \wedge \boldsymbol{l}_i \le x_i \le \boldsymbol{l}_i + \varepsilon$ in the (decidable) theory of polynomial real arithmetic with inequality (aka QF_NRA in the SMT community). If such a model $\boldsymbol{u}$ exists, then clearly $\mu \boldsymbol{f} \le \boldsymbol{u}$ and $||\boldsymbol{l} - \boldsymbol{u}||_{\infty } \le \varepsilon$. If no model exists, then improve $\boldsymbol{l}$ and try again. We have implemented this approach using the state-of-the-art SMT solvers cvc5 [4] and z3 [34], the winners of the 2022 SMT-COMP in the category QF_NRA⁵.

As yet another baseline, we have also implemented a variant of OVI for PPS which is closer to the original MDP algorithm from [22]. In this variant, called “standard OVI” from now on, we compute the candidate $\boldsymbol{u}$ based on the relative update rule $\boldsymbol{u} = (1 + \varepsilon )\boldsymbol{l}$, where $\boldsymbol{l}$ is the current lower bound [22].

Research Questions. We aim to shed some light on the following questions: (A) How well does our algorithm scale? (B) Is the algorithm suitable for PPS with different characteristics, e.g., dense or sparse? (C) Is the requirement $\rho (\boldsymbol{f}(\mu \boldsymbol{f})') < 1$ restrictive in practice? (D) How does our OVI compare to the baselines?

Fig. 4.

Program evaluating a random and-or tree [8]. The prob-blocks execute the contained statements with the respective probabilities (syntax inspired by Java’s switch). Our tool automatically translates this program to a pPDA and computes a basic certificate (Proposition 1) witnessing that calling and() returns true and false with probability $\le 382/657 \approx 0.58$ and $391/933 \approx 0.42$, resp.

Benchmarks. To answer the above questions we run our implementation on two sets of benchmarks (Table 1 and Table 2, respectively). The first set consists of various example programs from the literature as well as a few new programs, which are automatically translated to pPDA. This translation is standard and usually takes not more than a few seconds. The programs golden, and-or (see Figure 4), virus, gen-fun are adapted from [8, 35, 42] and [32, Program 5.6], respectively. The source code of all considered programs is in [44]. We have selected only programs with possibly unbounded recursion depth which induce infinite Markov chains. The second benchmark set comprises explicit PPS from [46]. The instances brown, lemonde, negra, swbd, tiger, tuebadz, and wsj all encode SCFG from the area of language processing (see [46] for details). random is the return probability system of a randomly generated pPDA.

Table 1. Experiments with PPS obtained from recursive probabilistic programs. Columns vars and terms display the number of variables and terms in the PPS. Columns sccs and scc$_{max}$ indicate the number of non-trivial SCC and the size of the largest SCC. G is total number of guesses made by OVI (at least one guess per SCC). $t_{tot}$ is the total runtime excluding the time for model construction. $t_{\mathbb {Q}}$ is the percentage of $t_{tot}$ spent on exact rational arithmetic. D is the average number of decimal digits of the rational numbers in the certificate. The timeout (TO) was set to 10 minutes. Time is in ms. The absolute precision is $\varepsilon = 10^{-3}$.

Table 2. Experiments with explicitly given PPS (setup as in Table 1).

Summary of Results. We ran the experiments on a standard notebook. The approach based on cvc5 turns out to be not competitive (see [44]). We thus focus on z3 in the following. Both pray and the z3 approach handle most of the programs from Table 1 within a 10 minute time limit. The considered programs induce sparse PPS with 38 - 26,367 variables, and most of them have just a single SCC. Notably, the examples with greatest maximum SCC size are only solved by z3. pray and z3 need at most 95 and 31 seconds, respectively, for the instances where they succeed. In many cases (e.g., rw-5.01, golden, virus, brown, swbd), the resulting certificates formally disprove AST. For the explicit PPS in Table 2, pray solves all instances whereas z3 only solves 3/8 within the time limit, and only finds the trivial solution $\boldsymbol{1}$. Most of these benchmarks contain dense high-degree polynomials, and our tool spends most time on performing exact arithmetic. Standard OVI (rightmost columns in Tables 1 and 2) solves strictly less instances than our eigenvector-based OVI. On some instances, Standard OVI is slightly faster (if it succeeds). However, on some larger benchmarks (brown, swbd) our variant runs $\approx 3\times$ faster.

Evaluation of Research Questions. (A) Scalability: Our algorithm succeeds on instances with maximum SCC size of up to 8,000 and number of terms over 50,000. pray solves all instances with a maximum SCC size of $\le$ 1,000 in less than 2 minutes per instance. For the examples where our algorithm does not succeed (e.g., escape100) it is mostly because it fails converting a floating point to a rational certificate. (B) PPS with different flavors: The problems in Table 1 (low degree and sparse, i.e., few terms per polynomials) and Table 2 (higher degree and dense) are quite different. A comparison to the SMT approach suggests that our technique might be especially well suited for dense problems with higher degrees. (C) Non-singularity: The only instance where our algorithm fails because of the non-singularity condition is the symmetric random walk rw-0.500. We therefore conjecture that this condition is often satisfied in practice. (D) Comparison with baselines: There is no clear winner. Some instances can only be solved by one tool or the other (e.g., escape100 and brown). However, pray often delivers more succinct certificates, i.e., the rational numbers have less digits. Moreover, z3 behaves much less predictably than pray.

6 Conclusion and Future Work

We have proposed using inductive bounds as certificates for various properties in probabilistic recursive models, and presented the first dedicated algorithm for computing such bounds. Our algorithm already scales to non-trivial problems. A remaining bottleneck is the need for exact rational arithmetic. This might be improved using appropriate rounding modes as in [21]. Additional future work includes certificates for lower bounds and termination.