Computing least fixed points of probabilistic systems of polynomials

We study systems of equations of the form X₁ = f ₁(X₁,⋯, X_n),⋯, X_n = f_n(X₁,⋯, X_n) where each f_i is a polynomial with nonnegative coefficients that add up to 1. The least nonnegative solution, say μ, of such equation systems is central to problems from various areas, like physics, biology, computational linguistics and probabilistic program verification. We give a simple and strongly polynomial algorithm to decide whether μ = (1,⋯, 1) holds. Furthermore, we present an algorithm that computes reliable sequences of lower and upper bounds on μ, converging linearly to μ. Our algorithm has these features despite using inexact arithmetic for efficiency. We report on experiments that show the performance of our algorithms.