Due to their \emph{quantitative} nature, probabilistic programs pose non-trivial challenges for designing compositional and efficient program analyses. Many analyses for probabilistic programs rely on \emph{iterative} approximation. This article presents an interprocedural dataflow-analysis framework, called \emph{NPA-PMA}, for designing and implementing (partially) \emph{non-iterative} program analyses of probabilistic programs with unstructured control-flow, nondeterminism, and general recursion. NPA-PMA is based on Newtonian Program Analysis (NPA), a generalization of Newton’s method to solve equation systems over semirings. The key challenge for developing NPA-PMA is to handle multiple kinds of \emph{confluences} in both the algebraic structures that specify analyses and the equation systems that encode control flow: semirings support a single confluence operation, whereas NPA-PMA involves three confluence operations (conditional, probabilistic, and nondeterministic).

Our work introduces \emph{$\omega$-continuous pre-Markov algebras} ($\omega$PMAs) to factor out common parts of different analyses; adopts \emph{regular infinite-tree expressions} to encode probabilistic programs with unstructured control-flow; and presents a \emph{linearization} method that makes Newton’s method applicable to the setting of regular-infinite-tree equations over $\omega$PMAs. NPA-PMA allows analyses to supply a non-iterative strategy to solve linearized equations. Our experimental evaluation demonstrates that (i) NPA-PMA holds considerable promise for outperforming Kleene iteration, and (ii) provides great generality for designing program analyses.